Verification of Bit-Flip Attacks against Quantized Neural Networks

TL;DR

This paper introduces BFAVerifier, a formal verification framework that rigorously assesses the vulnerability of quantized neural networks to bit-flip attacks, combining abstraction and MILP methods for soundness and completeness.

Contribution

The work presents the first verification framework specifically designed to identify and verify the absence of bit-flip attack vulnerabilities in quantized neural networks.

Findings

BFAVerifier effectively detects vulnerabilities across various architectures.

The framework is sound, complete, and efficient in practice.

Quantized neural networks show varying robustness depending on quantization levels.

Abstract

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.