Formal Security Analysis of Neural Networks using Symbolic Intervals

Abstract

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.

arXiv commentAccepted to USENIX Security 2018

References in corpus (6)

• DeepXplore: Automated Whitebox Testing of Deep Learning Systems
• Delving into Transferable Adversarial Examples and Black-box Attacks
• Adversarial Machine Learning at Scale
• A Dual Approach to Scalable Verification of Deep Networks
• Provably Minimally-Distorted Adversarial Examples
• Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems

Cited by in corpus (62)

• On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models
• Testing Deep Neural Networks
• How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review
• Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
• Software Engineering for AI-Based Systems: A Survey
• Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective
• A Survey of Safety and Trustworthiness of Deep Neural Networks: Verification, Testing, Adversarial Attack and Defence, and Interpretability
• Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems
• Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes
• Arms Race in Adversarial Malware Detection: A Survey
• Branch and Bound for Piecewise Linear Neural Network Verification
• Robustness Verification for Transformers
• DNNV: A Framework for Deep Neural Network Verification
• Algorithms for Verifying Deep Neural Networks
• HYDRA: Pruning Adversarially Robust Neural Networks
• Learning Security Classifiers with Verified Global Robustness Properties
• Parallelization Techniques for Verifying Neural Networks
• Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability
• Fast Neural Network Verification via Shadow Prices
• Interval Universal Approximation for Neural Networks
• Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation
• Improving adversarial robustness of deep neural networks by using semantic information
• Model Assertions for Monitoring and Improving ML Models
• Curriculum Learning for Safe Mapless Navigation
• Towards Security Threats of Deep Learning Systems: A Survey
• Scalable Verification of GNN-based Job Schedulers
• Generating Probabilistic Safety Guarantees for Neural Network Controllers
• Input Validation for Neural Networks via Runtime Local Robustness Verification
• Towards Scalable Verification of Deep Reinforcement Learning
• On Tractable Representations of Binary Neural Networks
• Better the Devil you Know: An Analysis of Evasion Attacks using Out-of-Distribution Adversarial Examples
• Refactoring Neural Networks for Verification
• ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
• On Training Robust PDF Malware Classifiers
• Almost Tight L0-norm Certified Robustness of Top-k Predictions against Adversarial Perturbations
• POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems
• OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems
• DeepSearch: A Simple and Effective Blackbox Attack for Deep Neural Networks
• Scalable Verification of Quantized Neural Networks (Technical Report)
• Taking Care of The Discretization Problem: A Comprehensive Study of the Discretization Problem and A Black-Box Adversarial Attack in Discrete Integer Domain
• Pruning and Slicing Neural Networks using Formal Verification
• Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs
• Computing Linear Restrictions of Neural Networks
• Fast Geometric Projections for Local Robustness Certification
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification
• D-square-B: Deep Distribution Bound for Natural-looking Adversarial Attack
• SOCRATES: Towards a Unified Platform for Neural Network Analysis
• nn-dependability-kit: Engineering Neural Networks for Safety-Critical Autonomous Driving Systems
• Simplifying Neural Networks using Formal Verification
• Grand Challenges in Resilience: Autonomous System Resilience through Design and Runtime Measures
• Towards Safety Verification of Direct Perception Neural Networks
• Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool
• Continuous Safety Verification of Neural Networks
• Probabilistic Safety for Bayesian Neural Networks
• Neural Network Repair with Reachability Analysis
• Reachability Analysis of Neural Networks with Uncertain Parameters
• Using Quantifier Elimination to Enhance the Safety Assurance of Deep Neural Networks
• Interval Deep Learning for Uncertainty Quantification in Safety Applications
• Reducing Neural Network Parameter Initialization Into an SMT Problem
• Expected Tight Bounds for Robust Training
• Reconciling Spatial and Temporal Abstractions for Goal Representation
• Boosting the Robustness Verification of DNN by Identifying the Achilles's Heel