Sound Verification of Deployed Neural Networks

Verification methods aim at mathematically proving desirable properties of neural networks, such as robustness to adversarial perturbations. A verifier is sound if and only if it never claims that a neural network has the desired property when it does not. It was shown recently that none of the currently known verifiers that are claimed to be sound are guaranteed to be sound when considering the deployed version of the verified network. Due to this, all the known verifiers are vulnerable to certain backdoor attacks, where an adversarial network passes verification, but in reality, it exhibits adversarial behavior in specific deployment environments. So far, it has been suspected that sound verification is prohibitively expensive if we wish to verify all possible executions—including parallel and stochastic ones—in deployment. We show that efficient and practically sound verifiers can be designed using a bound on the so-called backward error. Using this bounding technique, we propose two verifiers: one based on interval bound propagation, and one using symbolic propagation. Both verifiers are proven to remain sound even if the deployment environment randomly selects a valid expression tree (an ordering and parenthesizing of the arithmetic operations) to compute the network, and even if numeric underflow or overflow occurs in any valid expression tree. This is especially interesting in the case of symbolic propagation, where the expression tree used by the verifier is completely different from the one used in deployment. We demonstrate empirically that our techniques introduce only a limited performance overhead while detecting all the known verifier backdoor attacks.