Verification of Bit-Flip Attacks against Quantized Neural Networks
summary
BFAVerifier formally checks quantized neural networks for bit‑flip attacks by combining a sound abstraction‑based reachability engine with an MILP fallback encoded for off‑the‑shelf solvers. It claims soundness and completeness, builds an abstract domain that bounds flipped parameter ranges, and uses that to filter ~99% of parameters before MILP. On benchmarks and across activation functions and bit‑widths it either proves absence of attacks or returns concrete vulnerable parameter indices, showing practical verification rather than heuristic detection. abstraction + MILP
AI-written summary · about
chapters (13)
- 0:00Bit-flip attacks on quantized NNs
- 1:04Quantized neural networks
- 2:51Bit-flip attacks evolution
- 4:17Parameter-level bit-flip attacks
- 5:19MN attack model
- 6:02Verification problem formalized
- 7:06Framework overview and challenges
- 8:34Reachability analysis
- 10:40Weighted ReLU transformers
- 11:24MILP verification encoding
- 12:30Benchmarking results
- 14:58Contributions summary
- 15:23Q&A
related talks
11mExploiting Verified Neural Networks via Floating Point Numerical Error
59mVerification and Machine Learning
42mTowards Verification of General Neural Networks: A Dual Approach
08mVerifying Low-dimensional Input Neural Networks via Input Quantization
17mInput-Relational Verification of Deep Neural Networks
15mAutomated Verification of Network Function Binaries
20mIncremental Verification of Neural Networks
16mVerification of Neural Networks' Global Robustness