  Occlusion is a prevalent and easily realizable semantic perturbation to deep
neural networks (DNNs). It can fool a DNN into misclassifying an input image by
occluding some segments, possibly resulting in severe errors. Therefore, DNNs
planted in safety-critical systems should be verified to be robust against
occlusions prior to deployment. However, most existing robustness verification
approaches for DNNs are focused on non-semantic perturbations and are not
suited to the occlusion case. In this paper, we propose the first efficient,
SMT-based approach for formally verifying the occlusion robustness of DNNs. We
formulate the occlusion robustness verification problem and prove it is
NP-complete. Then, we devise a novel approach for encoding occlusions as a part
of neural networks and introduce two acceleration techniques so that the
extended neural networks can be efficiently verified using off-the-shelf,
SMT-based neural network verification tools. We implement our approach in a
prototype called OccRob and extensively evaluate its performance on benchmark
datasets with various occlusion variants. The experimental results demonstrate
our approach's effectiveness and efficiency in verifying DNNs' robustness
against various occlusions, and its ability to generate counterexamples when
these DNNs are not robust.
