  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.
