-
Provably Safe Neural Network Controllers via Differential Dynamic Logic
Authors:
Samuel Teuber,
Stefan Mitsch,
André Platzer
Abstract:
While neural networks (NNs) have potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of NN based control systems (NNCSs) poses significant challenges for the practical use of NNs, especially when safety is needed for unbounded time horizons. One reason is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably S…
▽ More
While neural networks (NNs) have potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of NN based control systems (NNCSs) poses significant challenges for the practical use of NNs, especially when safety is needed for unbounded time horizons. One reason is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first general approach that allows reusing control theory results for NNCS verification. By joining forces, we exploit the efficiency of NN verification tools while retaining the rigor of differential dynamic logic (dL). Based on provably safe control envelopes in dL, we derive specifications for the NN which is proven via NN verification. We show that a proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS.
The NN verification properties resulting from hybrid systems typically contain nonlinear arithmetic and arbitrary logical structures while efficient NN verification merely supports linear constraints. To overcome this divide, we present Mosaic: An efficient, sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic partitions complex verification queries into simple queries and lifts off-the-shelf linear constraint tools to the nonlinear setting in a completeness-preserving manner by combining approximation with exact reasoning for counterexample regions. Our evaluation demonstrates the versatility of VerSAILLE and Mosaic: We prove infinite-time safety on the classical Vertical Airborne Collision Avoidance NNCS verification benchmark for two scenarios while (exhaustively) enumerating counterexample regions in unsafe scenarios. We also show that our approach significantly outperforms State-of-the-Art tools in closed-loop NNV.
△ Less
Submitted 14 June, 2024; v1 submitted 16 February, 2024;
originally announced February 2024.
-
Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis
Authors:
Florian Lanzinger,
Christian Martin,
Frederik Reiche,
Samuel Teuber,
Robert Heinrich,
Alexander Weigl
Abstract:
Most formal methods see the correctness of a software system as a binary decision. However, proving the correctness of complex systems completely is difficult because they are composed of multiple components, usage scenarios, and environments. We present QuAC, a modular approach for quantifying the correctness of service-oriented software systems by combining software architecture modeling with de…
▽ More
Most formal methods see the correctness of a software system as a binary decision. However, proving the correctness of complex systems completely is difficult because they are composed of multiple components, usage scenarios, and environments. We present QuAC, a modular approach for quantifying the correctness of service-oriented software systems by combining software architecture modeling with deductive verification. Our approach is based on a model of the service-oriented architecture and the probabilistic usage scenarios of the system. The correctness of a single service is approximated by a coverage region, which is a formula describing which inputs for that service are proven to not lead to an erroneous execution. The coverage regions can be determined by a combination of various analyses, e.g., formal verification, expert estimations, or testing. The coverage regions and the software model are then combined into a probabilistic program. From this, we can compute the probability that under a given usage profile no service is called outside its coverage region. If the coverage region is large enough, then instead of attempting to get 100% coverage, which may be prohibitively expensive, run-time verification or testing approaches may be used to deal with inputs outside the coverage region. We also present an implementation of QuAC for Java using the modeling tool Palladio and the deductive verification tool KeY. We demonstrate its usability by applying it to a software simulation of an energy system.
△ Less
Submitted 25 January, 2024;
originally announced January 2024.
-
An Information-Flow Perspective on Algorithmic Fairness
Authors:
Samuel Teuber,
Bernhard Beckert
Abstract:
This work presents insights gained by investigating the relationship between algorithmic fairness and the concept of secure information flow. The problem of enforcing secure information flow is well-studied in the context of information security: If secret information may "flow" through an algorithm or program in such a way that it can influence the program's output, then that is considered insecu…
▽ More
This work presents insights gained by investigating the relationship between algorithmic fairness and the concept of secure information flow. The problem of enforcing secure information flow is well-studied in the context of information security: If secret information may "flow" through an algorithm or program in such a way that it can influence the program's output, then that is considered insecure information flow as attackers could potentially observe (parts of) the secret.
There is a strong correspondence between secure information flow and algorithmic fairness: if protected attributes such as race, gender, or age are treated as secret program inputs, then secure information flow means that these ``secret'' attributes cannot influence the result of a program. While most research in algorithmic fairness evaluation concentrates on studying the impact of algorithms (often treating the algorithm as a black-box), the concepts derived from information flow can be used both for the analysis of disparate treatment as well as disparate impact w.r.t. a structural causal model.
In this paper, we examine the relationship between quantitative as well as qualitative information-flow properties and fairness. Moreover, based on this duality, we derive a new quantitative notion of fairness called fairness spread, which can be easily analyzed using quantitative information flow and which strongly relates to counterfactual fairness. We demonstrate that off-the-shelf tools for information-flow properties can be used in order to formally analyze a program's algorithmic fairness properties, including the new notion of fairness spread as well as established notions such as demographic parity.
△ Less
Submitted 15 December, 2023;
originally announced December 2023.
-
Geometric Path Enumeration for Equivalence Verification of Neural Networks
Authors:
Samuel Teuber,
Marko Kleine Büning,
Philipp Kern,
Carsten Sinz
Abstract:
As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivalence which aims to prove that two NNs (e.g. an original and a compressed version) show equivalent behavior. Two approaches have been proposed for this problem: Mixed integer linear…
▽ More
As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivalence which aims to prove that two NNs (e.g. an original and a compressed version) show equivalent behavior. Two approaches have been proposed for this problem: Mixed integer linear programming and interval propagation. While the first approach lacks scalability, the latter is only suitable for structurally similar NNs with small weight changes.
The contribution of our paper has four parts. First, we show a theoretical result by proving that the epsilon-equivalence problem is coNP-complete. Secondly, we extend Tran et al.'s single NN geometric path enumeration algorithm to a setting with multiple NNs. In a third step, we implement the extended algorithm for equivalence verification and evaluate optimizations necessary for its practical use. Finally, we perform a comparative evaluation showing use-cases where our approach outperforms the previous state of the art, both, for equivalence verification as well as for counter-example finding.
△ Less
Submitted 13 December, 2021;
originally announced December 2021.
-
An Incremental Abstraction Scheme for Solving Hard SMT-Instances over Bit-Vectors
Authors:
Samuel Teuber,
Marko Kleine Büning,
Carsten Sinz
Abstract:
Decision procedures for SMT problems based on the theory of bit-vectors are a fundamental component in state-of-the-art software and hardware verifiers. While very efficient in general, certain SMT instances are still challenging for state-of-the-art solvers (especially when such instances include computationally costly functions). In this work, we present an approach for the quantifier-free bit-v…
▽ More
Decision procedures for SMT problems based on the theory of bit-vectors are a fundamental component in state-of-the-art software and hardware verifiers. While very efficient in general, certain SMT instances are still challenging for state-of-the-art solvers (especially when such instances include computationally costly functions). In this work, we present an approach for the quantifier-free bit-vector theory (QF_BV in SMT-LIB) based on incremental SMT solving and abstraction refinement. We define four concrete approximation steps for the multiplication, division and remainder operators and combine them into an incremental abstraction scheme. We implement this scheme in a prototype extending the SMT solver Boolector and measure both the overall performance and the performance of the single approximation steps. The evaluation shows that our abstraction scheme contributes to solving more unsatisfiable benchmark instances, including seven instances with unknown status in SMT-LIB.
△ Less
Submitted 23 August, 2020;
originally announced August 2020.
-
A Question of Context: Enhancing Intrusion Detection by Providing Context Information
Authors:
Simon Duque Anton,
Daniel Fraunholz,
Stephan Teuber,
Hans Dieter Schotten
Abstract:
Due to the fourth industrial revolution, and the resulting increase in interconnectivity, industrial networks are more and more opened to publicly available networks. Apart from the huge benefit in manageability and flexibility, the openness also results in a larger attack surface for malicious adversaries. In comparison to office environments, industrial networks have very high volumes of data. I…
▽ More
Due to the fourth industrial revolution, and the resulting increase in interconnectivity, industrial networks are more and more opened to publicly available networks. Apart from the huge benefit in manageability and flexibility, the openness also results in a larger attack surface for malicious adversaries. In comparison to office environments, industrial networks have very high volumes of data. In addition to that, every delay will most likely lead to loss of revenue. Hence, intrusion detection systems for industrial applications have different requirements than office-based intrusion detection systems. On the other hand, industrial networks are able to provide a lot of contextual information due to manufacturing execution systems and enterprise resource planning. Additionally, industrial networks tend to be more uniform, making it easier to determine outliers. In this work, an abstract simulation of industrial network behaviour is created. Malicious actions are introduced into a set of sequences of valid behaviour. Finally, a context-based and context-less intrusion detection system is used to find the attacks. The results are compared and commented. It can be seen that context information can help in identifying malicious actions more reliable than intrusion detection with only one source of information, e.g. the network.
△ Less
Submitted 28 May, 2019;
originally announced May 2019.
