PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Security Analysis of Neural Networks using Symbolic Intervals

Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, Suman Jana

arXiv:1804.10829v3cs.AIcs.LO

TL;DR

Formal security checking for DNNs is important, but existing testing lacks guarantees and solver-based verification incurs high overhead. ReluVal uses interval arithmetic with symbolic intervals and refinement to compute rigorous output bounds without SMT solvers, achieving a 200× average speedup over Reluplex. The results support symbolic interval analysis as a promising direction for rigorously analyzing DNN security properties.

  • Problem

    Existing DNN security testing seeks adversarial examples without formally guaranteeing their non-existence, while SMT-based verification is limited by high solver overhead.

  • Method

    ReluVal formally checks security properties of ReLU-based DNNs using interval arithmetic, symbolic intervals, and iterative refinement instead of SMT solvers.

  • Results

    200× faster on average than Reluplex, a state-of-the-art solver-based DNN verifier.

  • Takeaways & Limitations

    Symbolic interval analysis is a promising direction for rigorously analyzing different security properties of DNNs.

  • Takeaways & Limitations

    Training directly on intervals rather than individual samples is identified as future work.

Abstract

from arXiv · show

Due to the increasing deployment of Deep Neural Networks (DNNs) in real-world security-critical domains including autonomous vehicles and collision avoidance systems, formally checking security properties of DNNs, especially under different attacker capabilities, is becoming crucial. Most existing security testing techniques for DNNs try to find adversarial examples without providing any formal security guarantees about the non-existence of such adversarial examples. Recently, several projects have used different types of Satisfiability Modulo Theory (SMT) solvers to formally check security properties of DNNs. However, all of these approaches are limited by the high overhead caused by the solver. In this paper, we present a new direction for formally checking security properties of DNNs without using SMT solvers. Instead, we leverage interval arithmetic to compute rigorous bounds on the DNN outputs. Our approach, unlike existing solver-based approaches, is easily parallelizable. We further present symbolic interval analysis along with several other optimizations to minimize overestimations of output bounds. We design, implement, and evaluate our approach as part of ReluVal, a system for formally checking security properties of Relu-based DNNs. Our extensive empirical results show that ReluVal outperforms Reluplex, a state-of-the-art solver-based system, by 200 times on average. On a single 8-core machine without GPUs, within 4 hours, ReluVal is able to verify a security property that Reluplex deemed inconclusive due to timeout after running for more than 5 days. Our experiments demonstrate that symbolic interval analysis is a promising new direction towards rigorously analyzing different security properties of DNNs.

1 Introduction

DNNs in security-critical systems require formal guarantees that security properties hold across attacker-controlled input ranges, but solver-based analyses are costly. ReluVal replaces SMT solving with optimized interval analysis and substantially improves verification speed.

  • Motivation: Security-critical DNNs can exhibit exploitable corner-case errors from small, human-imperceptible adversarial perturbations.In systems such as ACAS Xu, an incorrectly handled corner case can cause significant damage.
  • Problem: Existing testing methods seek adversarial examples but do not formally guarantee their absence within specified input ranges.The target property is that no malicious input in a given range violates a security condition such as no collision.
  • Problem: Prior formal analyses rely on SMT solvers, whose efficiency severely limits security verification for highly nonlinear, non-convex DNN functions.ReLU activations make accurate output-range estimation difficult.
  • Approach: ReluVal computes rigorous DNN output bounds with interval arithmetic instead of SMT solvers, supporting formal secure or insecure outcomes for input ranges.It propagates input ranges layer by layer and can also classify secure and insecure subintervals.
  • Optimizations: Symbolic intervals preserve dependencies during propagation, while iterative refinement bisects inconclusive input ranges and is amenable to massive parallelization.ReluVal also uses gradient-based input selection to prioritize variables that influence outputs most.
  • Contributions: ReluVal is presented as the first interval-arithmetic system providing formal guarantees for DNN security.The paper identifies symbolic intervals and iterative refinement as key improvements over naive interval arithmetic.
  • Evaluation: 200× faster on average than Reluplex, ReluVal formally guaranteed all 15 evaluated properties and verified one property within 4 hours after Reluplex timed out beyond 5 days.The evaluation covered ACAS Xu and an MNIST network.

2 Background

The paper models ReLU-based DNNs as layered functions and specifies security through input-output behavior under bounded adversarial inputs. Interval arithmetic provides a natural way to propagate input ranges and check output safety properties.

  • Deep Learning Preliminaries: A feedforward DNN maps inputs to outputs through a sequence of parameterized layer transformations.Each layer applies a linear transformation followed by a nonlinear activation, with ReLU as the paper’s focus.
  • Target Systems: The target systems use DNNs for decisions in adversarial settings, including airborne collision avoidance systems such as ACAS Xu.ACAS Xu predicts actions from aircraft and intruder locations and speeds.
  • Threat Model: Figure 1 illustrates an adversarial input causing an aircraft DNN to recommend a right turn instead of a left turn, resulting in a collision.The figure contrasts the expected action in the upper view with the unsafe outcome in the lower view.
  • Security Properties: Input-output security properties require correct actions for adversarial inputs within specified ranges, avoiding complete specifications of opaque internal neuron states.Examples include steering left when an attacker vehicle approaches from the right.
  • Threat Model: The threat model permits different input features to vary within different intervals rather than requiring one overall L-norm bound.It also supports arbitrary output intervals when outputs are not explicit labels.
  • Interval Analysis: Interval arithmetic propagates ranges through the additions, multiplications, and simple nonlinear operations used by DNNs to check whether output intervals violate safety bounds.Its interval extension is intended to contain the function’s possible outputs over the input interval.

3 Overview

This section introduces interval-based verification and shows how dependency-aware symbolic intervals and iterative refinement tighten conservative output bounds.

  • ReluVal propagates input ranges through the network to determine whether a security property is secure, insecure, or unresolved by over-approximation.It can additionally classify subintervals as securely verified or containing concrete adversarial examples.
  • Naive interval arithmetic can produce extremely loose, unusable output bounds because it ignores dependencies among shared input variables.For the example, the dependency problem prevents the naive upper bound from being attained.
  • Figure 3 contrasts loose naive bounds, dependency-preserving symbolic analysis, and bisection-based reduction of over-approximation error.
  • Symbolic interval propagation: Symbolic interval propagation preserves input dependencies by representing intermediate neuron bounds symbolically, producing the concrete output interval [6,16] instead of the naive [0,22].The tighter interval verifies the example property that the steering angle is less than 20.
  • Iterative interval refinement: When symbolic bounds cannot pass safely through ReLU, ReluVal concretizes them and uses iterative refinement to reduce the resulting overestimation.Refinement repeatedly bisects the input range and propagates bounds on smaller subranges.

4 Proof of Correctness

The correctness analysis establishes that interval extensions safely over-approximate neural-network outputs and that iterative subdivision reduces this error toward arbitrary accuracy.

  • The correctness guarantee applies to most finite DNNs, while convergence of iterative refinement requires Lipschitz continuity.Finite compositions of Lipschitz-continuous functions retain Lipschitz continuity.
  • 4.1 Correctness of Overestimation: Naive interval extensions always contain the true output range because neural-network interval representations are inclusion isotonic.The argument uses the inclusion isotonicity of linear functions and common activation functions, including ReLU.
  • 4.2 Convergence in Finite Number of Splits: Splitting each input interval into N equal-width pieces and taking the union of their output ranges refines the interval estimate.The construction partitions every input dimension into N subintervals before recomputing the extension.
  • 4.2 Convergence in Finite Number of Splits: N-split refinement achieves at least N times smaller overestimation error than the unsplit estimate.
  • 4.2 Convergence in Finite Number of Splits: The refinement error width converges linearly to 0 as N increases, allowing arbitrary accuracy for sufficiently large N.This convergence follows from the Lipschitz continuity of the interval extension.

5 Methodology

ReluVal checks DNN security properties by propagating symbolic intervals, refining uncertain input ranges, and using influence and monotonicity to tighten output estimates. It can return secure, insecure, or timeout outcomes based on interval verification and concrete sampling.

  • Symbolic Interval Propagation: ReluVal propagates input ranges layer by layer, using symbolic interval analysis to tighten output estimates and assess security properties.Linear transformations retain symbolic equations, while ReLU nonlinearity is handled through concretization when necessary.
  • Symbolic Interval Propagation: Symbolic propagation can perfectly eliminate input-dependency errors for networks consisting only of linear transformations.For networks with ReLUs, concretization introduces the remaining over-approximation.
  • Iterative Interval Refinement: ReluVal refines loose output intervals by repeatedly bisecting input ranges into subintervals and reapplying symbolic interval analysis.Each bisection creates two child intervals whose combined bounds determine the parent interval’s output bound.
  • Iterative Interval Refinement: ReluVal samples points in potentially violating subintervals, reports concrete adversarial examples when found, and otherwise continues refinement toward secure or insecure conclusions.The system may also classify subintervals as securely verified or definitely containing adversarial examples.
  • Influence Analysis: Influence analysis selects the input feature with the largest gradient-based smear value for splitting, prioritizing features estimated to affect outputs most strongly.The smear function combines gradient intervals with input-feature widths.
  • Monotonicity: Monotonicity checking can replace an input interval with endpoint values when its output derivative remains strictly positive or negative throughout the interval.Empirical results indicate this reduces the number of splits needed for different security properties.

6 Implementation

ReluVal implements interval-based verification with parallelizable refinement on a multicore CPU system. It uses outward rounding to preserve sound overestimation, while finite precision remains an implementation concern addressed by the chosen rounding strategy.

  • Setup and Parallelization: ReluVal is implemented in C with OpenBLAS and evaluated on a Linux server with 16 CPU cores and 256GB memory.Its interval-arithmetic verification workload is highly parallelizable because newly created input ranges can be checked independently during refinement.
  • Setup and Parallelization: Unbalanced bisection trees and unpredictable refinement depth complicate parallel scheduling and can leave workers idle or impose scheduling overhead.These challenges arise because different subintervals may require substantially different computation times.
  • Numerical Precision: 32-bit floating-point rounding can collapse small intervals to zero and accumulate output errors across layers.The paper reports that some adversarial examples from Reluplex are false positives caused by rounding problems.
  • Numerical Precision: ReluVal uses outward rounding so every computed interval remains a sound overestimation of the true output range.The authors found 32-bit precision sufficient for verifying ACAS Xu models and note that 64-bit double precision is extendable.

7 Evaluation

ReluVal is evaluated on ACAS Xu and MNIST models, outperforming Reluplex and gradient-based attacks while isolating adversarial input ranges. Its optimizations substantially reduce interval-refinement costs.

  • Evaluation Setup: ReluVal evaluates forty-five ACAS Xu collision-avoidance models and a two-hidden-layer MNIST network with 98.28% classification accuracy.The ACAS Xu networks use five inputs, five outputs, and six hidden layers of fifty neurons; the MNIST model has 784 inputs, 10 outputs, and two 512-neuron hidden layers.
  • Performance on ACAS Xu Models: 200×: ReluVal achieves up to 200× speedup over Reluplex and outperforms it on all fifteen ACAS Xu security properties.The comparison includes ten properties from Reluplex and five additional properties; ReluVal terminates substantially sooner when Reluplex times out.
  • Performance on ACAS Xu Models: 61.2%: CW misses adversarial inputs on that percentage of models, whereas ReluVal does not require seed inputs and fully explores the input space.The comparison uses forty adversarial ACAS Xu properties.
  • Performance on ACAS Xu Models: 262,144 sub-intervals: for property S1, ReluVal proves 163,915 safe and separates a non-adversarial range ρ = [400,6402.36] from an adversarial range ρ = [6402.36,10000].The ranges are split to precision e−6.
  • Preliminary Tests on MNIST Model: 956 images are safe for |X|∞≤1 and 721 for |X|∞≤2 among 1000 MNIST test images; the safe percentage drops quickly to 0 as the norm increases.More timeouts occur as the L∞ norm increases.
  • Optimizations: 42.06% and 49.28%: symbolic interval analysis reduces the deepest and average bisection-tree depths, while influence analysis cuts running time by up to 96.04% and monotonicity by 16.91%.Influence analysis also reduces average depth by 10.85%; the comparisons use naive interval analysis or sequential splitting baselines as specified.

8 Related Work

Related work includes adversarial attacks, solver-based verification, convex and zonotope relaxations, dual optimization, MILP methods, black-box verification, and interval optimization. These approaches differ in whether they seek examples, formal guarantees, or output over-approximations.

  • Adversarial machine learning: Adversarial-learning methods commonly search for carefully crafted perturbations, while many defenses remain restricted to one adversary type or security property.The related work describes an ongoing competition between robust-network training and more efficient attacks.
  • DNN Verification: Prior verification methods use convex relaxations, zonotopes, Lagrange duality with gradient descent, or MILP solvers to over-approximate or optimize DNN outputs.The cited approaches target ReLU-network verification through different optimization or relaxation formulations.
  • Black-box Verification: Verivis leverages discrete image pixels for black-box verification but cannot verify the non-existence of norm-based adversarial examples.This contrasts black-box pixel discreteness with ReluVal’s stated verification scope.
  • Interval Optimization: Interval analysis provides rigorous bounds for nonlinear equations and global optimization, and neural-network computation is largely a sequence of simple linear operations.The paper positions interval arithmetic as a relevant foundation for DNN analysis.

9 Future Work and Discussion

Future work considers extending ReluVal beyond its current activation-function and norm support, while also exploring interval-based training. These directions broaden the method’s supported analysis and training settings.

  • Supporting other activation functions: ReluVal currently supports common piece-wise linear activations, while extending symbolic interval propagation to tanh and sigmoid is planned future work.The paper states that these activations satisfy the properties needed for interval extension in theory.
  • Supporting other norms besides L∞: The authors propose approximating L1 and L2 analyses with intervals, noting that safety under an L∞ bound guarantees safety for corresponding p-norm bounds.The discussion explains that perturbations bounded by other norms are subsets of those allowed by the corresponding L∞ bound.
  • Interval-based training: Future work would convert training samples into intervals and minimize losses over those intervals instead of over individual samples.This is presented as a proposed training direction rather than an evaluated capability.

10 Conclusion

ReluVal is presented as a generic interval-analysis framework for rigorously analyzing DNN computations and security properties. The evaluated system uses symbolic interval arithmetic and is reported to run 200 times faster on average than solver-based approaches.

  • ReluVal is a generic framework that uses interval analysis to understand and analyze DNN computations with rigorous guarantees.
  • ReluVal was designed, developed, and evaluated as a formal security analysis system for neural networks.
  • 200 times faster on average than current state-of-the-art solver-based approaches was ReluVal’s reported performance.
  • The paper identifies symbolic interval analysis as a promising direction for rigorously analyzing different security properties of DNNs.

A Appendix: Formal Definitions for ACAS Xu Properties φ1 to φ15

The appendix defines ACAS Xu inputs, outputs, model indexing, advisory labels, and formal properties φ1–φ15 across specified input ranges and networks. These properties constrain expected advisory scores or outputs under distance, heading, speed, vertical-separation, and previous-action conditions.

  • Formal definitions: ACAS Xu models use distance ρ, heading angles θ and ψ, ownship speed vown, intruder speed vint, and previous action aprev as indexed inputs.The models also index τ as time until loss of vertical separation, and define five advisory outputs including COC, weak, and strong turns.
  • Properties φ1–φ4: Properties φ1–φ4 constrain the COC score when the intruder is distant and slower, directly ahead and approaching, or directly ahead and moving away.The desired conditions include a fixed upper threshold, non-maximality, or non-minimality of the COC score.
  • Properties φ10–φ15: Properties φ10–φ15 cover far-away, near, slower, and vertically separated intruders, requiring particular minimal scores or strong-turn advisories.The conditions include large or small vertical separation, approach direction, previous actions, and model-specific input ranges.
Loading 1804.10829v3…