Probabilistic verification of black-box systems

Abstract

Wir entwickeln und untersuchen eine probabilistische Prozedur zur Charakterisierung der Sicherheit von Black Box Systemen, wie neuronalen Netzwerken (NNs) oder cyber-physikalischen Systemen (CPSs). Mit einer einzigen Stichprobe von ausreichender Größe kann unsere Prozedur Spezifikationen in einer vorausgewählten Klasse identifizieren, welche das System mit hoher Wahrscheinlichkeit korrekt beschreiben. Für viele Probleme sind Lösungen basierend auf maschinellem Lernen der Stand der Technik, doch die Komplexität dieser Systeme macht formale Beweise ihrer Sicherheit oft unmöglich. Ohne Sicherheitsgarantien kann unvorhersehbares Verhalten und Manipulationsanfälligkeit in kritischen Anwendungen nicht ausgeschlossen werden. Dies ist vor allem für CPSs wichtig, welche physisch mit ihrer Umgebung interagieren. Deswegen sind Sicherheitsgarantien für den Einsatz dieser Systeme oft eine Voraussetzung. Für Black-Box Szenarien, in denen formale Methoden nicht einsetzbar sind, untersuchen wir wie probabilistische Garantien alleine durch Zufallstests gegeben werden können. Wir verwenden Methoden aus der Lerntheorie um---für eine gewählte Klasse von möglichen Spezifikationen---zu entscheiden, welche Spezifikationen das System mit großer Wahrscheinlichkeit korrekt beschreiben. Unsere Prozedur benötigt nur eine Stichprobe von ausreichender Größe um eine Aussage über die gesamte Spezifikationsklasse zu treffen. Bemerkenswerterweise ist die Größe dieser Stichprobe unabhängig von Charakteristiken des untersuchten Systems und seiner Daten und ist nur abhängig von der Komplexität der Spezifikationsklasse selbst, speziell ihrer Vapnik-Chervonenkis (VC) Dimension. Wir untersuchen die Anwendung unserer Methode in zwei praxisrelevanten Szenarien und erweitern unsere Theorie um Lösungen speziell für diese Probleme zu entwickeln. Zuerst untersuchen wir die Robustheit von NNs gegen gezielte Datenmanipulation und geben wahrscheinlich annähernd-globale Robustheitsgarantien. Diese Garantien dienen dann als scharfe untere Schranken für die Robustheit jeder Vorhersage eines NNs in Abhängigkeit der Vorhersagesicherheit. Für CPS Verifizierung selbst untersuchen wir Signal-temporale Logik (STL) als Spezifikationssprache. Erfüllt das CPS eine Bedingung für Wohlverhaltenheit, erhalten wir für jede in STL ausdrückbare Formel eine Oberschranke ihrer VC Dimension. Dadurch können wir die notwendige Stichprobengröße bestimmen, mit der jede aus den Daten gelernte Spezifikation mit hoher Wahrscheinlichkeit generalisiert. Unsere Experimente zeigen, dass unsere Theorie in die Praxis übertragbar ist und die Stichprobengrößen auch für komplexe Spezifikationsklassen noch handhabbar sind.

We devise and investigate a probabilistic procedure for verifying the safety of black-box systems like neural networks (NNs) and cyber-physical systems (CPSs). Given a large enough sample of observations, our procedure allows us to identify specifications in a chosen class that correctly characterise the system with high probability. In particular, we give guarantees for all specifications in the class without the need to resample. Machine-learning-based solutions are state of the art in many problem settings, yet their internal complexity often renders it infeasible to verify them for safety formally. Without safety guarantees, these systems might behave unpredictably and are vulnerable to manipulation in critical applications. This is especially true for CPSs, which interact with their environment physically. Because of this, guaranteed safety is often a prerequisite for the deployment of CPSs. For black-box settings where formal methods are infeasible, we investigate how to give probabilistic guarantees from random observations alone. We use tools from learning theory to decide---for a chosen class of candidate specifications---which specifications the investigated system will adhere to with high probability. Our procedure requires us to obtain only one sufficiently large sample of observations to make statements about the whole class of specifications. Remarkably, the required size of the sample is independent of any characteristics of the investigated system and observations and only depends on the complexity of the specification class itself, specifically its Vapnik-Chervonenkis (VC) dimension. We apply our verification procedure to two practically relevant settings and extend our theory to devise solutions tailored to these specific problems. We first investigate the robustness of NNs against adversarial perturbations and give probably, approximately global robustness guarantees. These guarantees then serve as sharp lower bounds for the robustness of each prediction of an NN, given its prediction confidence. To tackle CPS verification, we investigate signal temporal logic (STL) as a specification language. Assuming the CPS is well-behaved, we can provide VC dimension bounds for any parametrised formula expressible in STL. This allows us to quantify how many samples are required to mine system specifications that are guaranteed to generalise. Our experimental results show that our theory easily translates into practice and that our requirements on the sample size are manageable even for complex specification classes.