# Verification of Bit-Flip Attacks against Quantized Neural Networks

arXiv: https://arxiv.org/abs/2502.16286 · HTML: https://mlsanity.com/paper/2502.16286/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 46 of its 88 references that are in the map.
- First posted on arXiv 22 Feb 2025.

## Builds on (most cited first, 30 of 46)

- [Deep Compression: Compressing Deep Neural Networks with Pruning, Trained Quantization and Huffman Coding](https://mlsanity.com/paper/1510.00149/) (2015)
- [Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference](https://mlsanity.com/paper/1712.05877/) (2017)
- [A Survey of Quantization Methods for Efficient Neural Network Inference](https://mlsanity.com/paper/2103.13630/) (2021)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Differentiable Soft Quantization: Bridging Full-Precision and Low-Bit Neural Networks](https://mlsanity.com/paper/1908.05033/) (2019)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Incremental Network Quantization: Towards Lossless CNNs with Low-Precision Weights](https://mlsanity.com/paper/1702.03044/) (2017)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Bit-Flip Attack: Crushing Neural Network with Progressive Bit Search](https://mlsanity.com/paper/1903.12269/) (2019)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems](https://mlsanity.com/paper/1911.01840/) (2019)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Terminal Brain Damage: Exposing the Graceless Degradation in Deep Neural Networks Under Hardware Fault Attacks](https://mlsanity.com/paper/1906.01017/) (2019)
- [DeepHammer: Depleting the Intelligence of Deep Neural Networks through Targeted Chain of Bit Flips](https://mlsanity.com/paper/2003.13746/) (2020)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [Probabilistic Safety for Bayesian Neural Networks](https://mlsanity.com/paper/2004.10281/) (2020)
- [DeepSteal: Advanced Model Extractions Leveraging Efficient Weight Stealing in Memories](https://mlsanity.com/paper/2111.04625/) (2021)
- [Abstraction based Output Range Analysis for Neural Networks](https://mlsanity.com/paper/2007.09527/) (2020)
- [Post-training Quantization for Neural Networks with Provable Guarantees](https://mlsanity.com/paper/2201.11113/) (2022)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)
- [Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification](https://mlsanity.com/paper/1902.09866/) (2019)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [RowHammer: A Retrospective](https://mlsanity.com/paper/1904.09724/) (2019)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Advanced Evasion Attacks and Mitigations on Practical ML-Based Phishing Website Classifiers](https://mlsanity.com/paper/2004.06954/) (2020)

## Built on by (most cited first, 2 of 2)

- [From Arithmetic to Logic: The Resilience of Logic and Lookup-Based Neural Networks Under Parameter Bit-Flips](https://mlsanity.com/paper/2603.22770/) (2026)
- [Toward a Generalized Defense Across Sparse, Continuous, and Structured Parameter Attacks](https://mlsanity.com/paper/2606.04317/) (2026)

## Abstract (arXiv)

In the rapidly evolving landscape of neural network security, the resilience of neural networks against bit-flip attacks (i.e., an attacker maliciously flips an extremely small amount of bits within its parameter storage memory system to induce harmful behavior), has emerged as a relevant area of research. Existing studies suggest that quantization may serve as a viable defense against such attacks. Recognizing the documented susceptibility of real-valued neural networks to such attacks and the comparative robustness of quantized neural networks (QNNs), in this work, we introduce BFAVerifier, the first verification framework designed to formally verify the absence of bit-flip attacks or to identify all vulnerable parameters in a sound and rigorous manner. BFAVerifier comprises two integral components: an abstraction-based method and an MILP-based method. Specifically, we first conduct a reachability analysis with respect to symbolic parameters that represent the potential bit-flip attacks, based on a novel abstract domain with a sound guarantee. If the reachability analysis fails to prove the resilience of such attacks, then we encode this verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Therefore, BFAVerifier is sound, complete, and reasonably efficient. We conduct extensive experiments, which demonstrate its effectiveness and efficiency across various network architectures, quantization bit-widths, and adversary capabilities.