No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks

TL;DR

This paper demonstrates that current neural network verification methods fail to ensure safety in real-world deployment due to the gap between theoretical and practical soundness, highlighting vulnerabilities to environment-specific attacks.

Contribution

The paper reveals the disconnect between theoretical and practical soundness in neural network verification and introduces deployment-specific attacks exposing verifier vulnerabilities.

Findings

All tested verifiers are vulnerable to deployment-specific attacks.

Theoretical soundness does not guarantee practical safety in neural network deployment.

Verifiers can be misled by environment-aware adversarial networks.

Abstract

The ultimate goal of verification is to guarantee the safety of deployed neural networks. Here, we claim that all the state-of-the-art verifiers we are aware of fail to reach this goal. Our key insight is that theoretical soundness (bounding the full-precision output while computing with floating point) does not imply practical soundness (bounding the floating point output in a potentially stochastic environment). We prove this observation for the approaches that are currently used to achieve provable theoretical soundness, such as interval analysis and its variants. We also argue that achieving practical soundness is significantly harder computationally. We support our claims empirically as well by evaluating several well-known verification methods. To mislead the verifiers, we create adversarial networks that detect and exploit features of the deployment environment, such as the order and precision of floating point operations. We demonstrate that all the tested verifiers are vulnerable to our new deployment-specific attacks, which proves that they are not practically sound.