Abstract
Due to the increasing usage of machine learning (ML) techniques in security-and safety-critical domains, such as autonomous systems and medical diagnosis,ensuring correct behavior of ML systems, especially for different corner cases,is of growing importance. In this paper, we propose a generic framework forevaluating security and robustness of ML systems using different real-worldsafety properties. We further design, implement and evaluate VeriVis, ascalable methodology that can verify a diverse set of safety properties forstate-of-the-art computer vision systems with only blackbox access. VeriVisleverage different input space reduction techniques for efficient verificationof different safety properties. VeriVis is able to find thousands of safetyviolations in fifteen state-of-the-art computer vision systems including tenDeep Neural Networks (DNNs) such as Inception-v3 and Nvidia's Dave self-drivingsystem with thousands of neurons as well as five commercial third-party visionAPIs including Google vision and Clarifai for twelve different safetyproperties. Furthermore, VeriVis can successfully verify local safetyproperties, on average, for around 31.7% of the test images. VeriVis finds upto 64.8x more violations than existing gradient-based methods that, unlikeVeriVis, cannot ensure non-existence of any violations. Finally, we show thatretraining using the safety violations detected by VeriVis can reduce theaverage number of violations up to 60.2%.