Verification of Bit-Flip Attacks against Quantized Neural Networks

Explore a 17-minute conference presentation that introduces BFAVerifier, the first formal verification framework designed to assess the security of quantized neural networks against bit-flip attacks. Learn how researchers from leading institutions have developed a comprehensive approach combining abstraction-based methods and Mixed-Integer Linear Programming (MILP) techniques to rigorously verify whether quantized neural networks can withstand malicious bit-flip attacks or identify all vulnerable parameters. Discover the novel abstract domain with sound guarantees used for reachability analysis with respect to symbolic parameters representing potential attacks, and understand how the framework encodes verification problems into equivalent MILP problems solvable by standard solvers when initial analysis proves insufficient. Examine extensive experimental results demonstrating the framework's effectiveness across various activation functions, quantization bit-widths, and adversary capabilities, while gaining insights into why quantized neural networks may offer superior robustness compared to real-valued networks against these sophisticated memory-based attacks. Access the complete research findings through the accompanying article and supplementary materials, including the open-source BFAVerifier implementation, presented at the OOPSLA 2025 conference by an international research team specializing in neural network security and formal verification methods.