Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification of Bit-Flip Attacks against Quantized Neural Networks

Yedi Zhang, Lei Huang, Pengfei Gao, Fu Song, Jun Sun, Jin Song Dong

TL;DR

BFAVerifier tackles the problem of verifying the absence of bit-flip attacks on quantized neural networks by proving $\mathcal{N} \models^\rho_{\mathfrak{m},\mathfrak{n}} \langle \phi,\psi \rangle$ for all admissible attack vectors $\rho$. It introduces SymPoly, an abstract domain for networks with symbolic parameters, combined with a MILP-based solver to achieve sound and complete verification across architectures, quantization schemes, and attacker capabilities. The framework demonstrates substantial efficiency gains over naive approaches (up to 30x) on benchmarks such as MNIST and ACAS Xu, while providing formal guarantees and identifying vulnerable parameters to prioritize protection. Overall, BFAVerifier offers a practical path toward robust, BF A-aware deployment of quantized neural networks in security-sensitive applications.

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.

Verification of Bit-Flip Attacks against Quantized Neural Networks

TL;DR

BFAVerifier tackles the problem of verifying the absence of bit-flip attacks on quantized neural networks by proving for all admissible attack vectors . It introduces SymPoly, an abstract domain for networks with symbolic parameters, combined with a MILP-based solver to achieve sound and complete verification across architectures, quantization schemes, and attacker capabilities. The framework demonstrates substantial efficiency gains over naive approaches (up to 30x) on benchmarks such as MNIST and ACAS Xu, while providing formal guarantees and identifying vulnerable parameters to prioritize protection. Overall, BFAVerifier offers a practical path toward robust, BF A-aware deployment of quantized neural networks in security-sensitive applications.

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.

Paper Structure

This paper contains 39 sections, 6 theorems, 8 equations, 11 figures, 13 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminary
  3. Neural Network and Quantization
  4. Bit-Flip Attacks
  5. Bit-Flip Attack Verification Problem
  6. Problem Definition
  7. A Naive Method by DeepPoly
  8. Methodology of BFAVerifier
  9. Overview of BFAVerifier
  10. SymPoly: An Abstract Domain for Networks with Symbolic Parameters
  11. Abstract domain.
  12. Affine abstract transformer for symbolic weights.
  13. Affine abstract transformer for symbolic biases.
  14. Details of Function BFA_RA
  15. Details of Function BFA_MILP
  16. ...and 24 more sections

Key Result

theorem 1

Verifying whether ${\mathcal{N}} \models^\rho_{\mathfrak{m},\mathfrak{n}} \langle \phi,\psi\rangle$ holds is NP-complete. ∎

Figures (11)

  • Figure 1: An illustration example of bit-flip attacks on an 8-bit quantized neural network. The attacker flips a single bit in the final/output layer, altering the value of parameter $\widehat{{\mathbf{W}}}^i_{j,k}$ from 85 to -43 (represented in two's complement) and misleading the network behavior.
  • Figure 2: A 3-layer DNN with ReLU activations and its quantized version.
  • Figure 3: Convex approximations of $\overrightarrow{{\mathbf{W}}}^{i+1}_{j,k}{\mathbf{x}}^i_{k,2}=\overrightarrow{{\mathbf{W}}}^{i+1}_{j,k}\cdot \text{ReLU}({\mathbf{x}}^i_{k,1})$ via different abstract transformations: (a) depicts the approximation derived by abstracting $\overrightarrow{{\mathbf{W}}}^{i+1}_{j,k}\cdot {\mathbf{a}}^i_{k,2}$, where ${\mathbf{a}}^i_{k,2}$ is an over-approximation of $\text{ReLU}({\mathbf{x}}^i_{k,1})$ obtained from DeepPoly, and the yellow and green lines gives the boundaries of $w_u\cdot {\mathbf{a}}^i_{k,2}$ and $w_u\cdot {\mathbf{a}}^i_{k,2}$. (b) directly give the approximation by linear boundaries with the minimal area in the input-output plane of the function $\overrightarrow{{\mathbf{W}}}^{i+1}_{j,k}\cdot \text{ReLU}({\mathbf{x}}^i_{k,1})$.
  • Figure 4: The construction of additional node $\tilde{{\mathbf{x}}}^{i}_{k,2}$ given a symbolic parameter $\overrightarrow{{\mathbf{W}}}^{i+1}_{j,k}$.
  • Figure 5: An illustration of the abstract transformer for the symbolic-weighted ReLU function $\overrightarrow{{\mathbf{W}}}^{i+1}_{j,k}\cdot \text{ReLU}({\mathbf{x}}^i_{k,1})$, where the first column defines the range (interval) of values $[w_l, w_u]$ for $\overrightarrow{{\mathbf{W}}}^{i+1}_{j,k}$. The second column gives the abstraction when $l^i_{k,1}>0$ for the abstract element ${\mathbf{a}}^i_{k,1}$ of ${\mathbf{x}}^i_{k,1}$, and the third (resp. fourth) column shows the abstraction of when $(l^i_{k,1} <0<u^i_{k,1}) \wedge (l^i_{k,1}+u^i_{k,1}\le 0)$ (resp. $(l^i_{k,1} < 0 < u^i_{k,1}) \wedge (l^i_{k,1}+u^i_{k,1}>0)$).
  • ...and 6 more figures

Theorems & Definitions (9)

  • definition 1: Attack Vector
  • definition 2: BFA-tolerance
  • theorem 1
  • definition 3: BFA-tolerant Robustness
  • theorem 2
  • theorem 3
  • theorem 4
  • theorem 5
  • theorem 6