-
Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study
Authors:
Rafael Sá Menezes,
Edoardo Manino,
Fedor Shmarov,
Mohannad Aldughaim,
Rosiane de Freitas,
Lucas C. Cordeiro
Abstract:
Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significan…
▽ More
Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. In more detail, we quantify the benefits of interval analysis on two benchmarks: the Intel Core Power Management firmware and 9537 programs in the ReachSafety category of the International Competition on Software Verification. Our results show that interval analysis is essential in solving 203 unique benchmarks.
△ Less
Submitted 21 June, 2024;
originally announced June 2024.
-
ESBMC v7.4: Harnessing the Power of Intervals
Authors:
Rafael Menezes,
Mohannad Aldughaim,
Bruno Farias,
Xianzhiyu Li,
Edoardo Manino,
Fedor Shmarov,
Kunjian Song,
Franz Brauße,
Mikhail R. Gadelha,
Norbert Tihanyi,
Konstantin Korovin,
Lucas C. Cordeiro
Abstract:
ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backw…
▽ More
ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backward contractors, and particular optimizations related to singleton intervals because of their ubiquity. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.
△ Less
Submitted 22 December, 2023;
originally announced December 2023.
-
NeuroCodeBench: a plain C neural network benchmark for software verification
Authors:
Edoardo Manino,
Rafael Sá Menezes,
Fedor Shmarov,
Lucas C. Cordeiro
Abstract:
Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal, they cannot prove the absence of software faults in the network implementation. This paper presents NeuroCodeBench - a verification benchmark for neural network code written in plain C. It contains 32 neural networks wi…
▽ More
Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal, they cannot prove the absence of software faults in the network implementation. This paper presents NeuroCodeBench - a verification benchmark for neural network code written in plain C. It contains 32 neural networks with 607 safety properties divided into 6 categories: maths library, activation functions, error-correcting networks, transfer function approximation, probability density estimation and reinforcement learning. Our preliminary evaluation shows that state-of-the-art software verifiers struggle to provide correct verdicts, due to their incomplete support of the standard C mathematical library and the complexity of larger neural networks.
△ Less
Submitted 7 September, 2023;
originally announced September 2023.
-
Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs
Authors:
Fatimah K. Aljaafari,
Rafael Menezes,
Edoardo Manino,
Fedor Shmarov,
Mustafa A. Mustafa,
Lucas C. Cordeiro
Abstract:
Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially with the number of program threads and statements. We propose and evaluate EBF (Ensembles of Bounded Model Checking with Fuzzing) -- a technique that combines Bounded Model Checking (BMC) and Gray-Box Fuzzing (GBF) to find…
▽ More
Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially with the number of program threads and statements. We propose and evaluate EBF (Ensembles of Bounded Model Checking with Fuzzing) -- a technique that combines Bounded Model Checking (BMC) and Gray-Box Fuzzing (GBF) to find software vulnerabilities in concurrent programs. Since there are no publicly-available GBF tools for concurrent code, we first propose OpenGBF -- a new open-source concurrency-aware gray-box fuzzer that explores different thread schedules by instrumenting the code under test with random delays. Then, we build an ensemble of a BMC tool and OpenGBF in the following way. On the one hand, when the BMC tool in the ensemble returns a counterexample, we use it as a seed for OpenGBF, thus increasing the likelihood of executing paths guarded by complex mathematical expressions. On the other hand, we aggregate the outcomes of the BMC and GBF tools in the ensemble using a decision matrix, thus improving the accuracy of EBF. We evaluate EBF against state-of-the-art pure BMC tools and show that it can generate up to 14.9% more correct verification witnesses than the corresponding BMC tools alone. Furthermore, we demonstrate the efficacy of OpenGBF, by showing that it can find 24.2% of the vulnerabilities in our evaluation suite, while non-concurrency-aware GBF tools can only find 0.55%. Finally, thanks to our concurrency-aware OpenGBF, EBF detects a data race in the open-source wolfMqtt library and reproduces known bugs in several other real-world programs, which demonstrates its effectiveness in finding vulnerabilities in real-world software.
△ Less
Submitted 20 October, 2022; v1 submitted 13 June, 2022;
originally announced June 2022.
-
Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems
Authors:
Fedor Shmarov,
Sadegh Soudjani,
Nicola Paoletti,
Ezio Bartocci,
Shan Lin,
Scott A. Smolka,
Paolo Zuliani
Abstract:
We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochastic disturbances. Our method derives digital controllers such that the corresponding closed-loop system, modeled as a sampled-data stochastic control system, satisfies a safety specification with probability above a give…
▽ More
We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochastic disturbances. Our method derives digital controllers such that the corresponding closed-loop system, modeled as a sampled-data stochastic control system, satisfies a safety specification with probability above a given threshold. The proposed synthesis method alternates between two steps: generation of a candidate controller pc, and verification of the candidate. pc is found by maximizing a Monte Carlo estimate of the safety probability, and by using a non-validated ODE solver for simulating the system. Such a candidate is therefore sub-optimal but can be generated very rapidly. To rule out unstable candidate controllers, we prove and utilize Lyapunov's indirect method for instability of sampled-data nonlinear systems. In the subsequent verification step, we use a validated solver based on SMT (Satisfiability Modulo Theories) to compute a numerically and statistically valid confidence interval for the safety probability of pc. If the probability so obtained is not above the threshold, we expand the search space for candidates by increasing the controller degree. We evaluate our technique on three case studies: an artificial pancreas model, a powertrain control model, and a quadruple-tank process.
△ Less
Submitted 10 January, 2019;
originally announced January 2019.
-
Automated Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems
Authors:
Fedor Shmarov,
Nicola Paoletti,
Ezio Bartocci,
Shan Lin,
Scott A. Smolka,
Paolo Zuliani
Abstract:
We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particul…
▽ More
We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particular, we consider hybrid systems with nonlinear dynamics (Lipschitz-continuous ordinary differential equations) and random parameters, and we synthesize PID controllers such that the resulting closed-loop systems satisfy safety and performance constraints given as probabilistic bounded reachability properties. Our technique leverages SMT solvers over the reals and nonlinear differential equations to provide formal guarantees that the synthesized controllers satisfy such properties. These controllers are also robust by design since they minimize the probability of reaching an unsafe state in the presence of random disturbances. We apply our approach to the problem of insulin regulation for type 1 diabetes, synthesizing controllers with robust responses to large random meal disturbances, thereby enabling them to maintain blood glucose levels within healthy, safe ranges.
△ Less
Submitted 7 September, 2017; v1 submitted 17 July, 2017;
originally announced July 2017.
-
ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems
Authors:
Fedor Shmarov,
Paolo Zuliani
Abstract:
We present ProbReach, a tool for verifying probabilistic reachability for stochastic hybrid systems, i.e., computing the probability that the system reaches an unsafe region of the state space. In particular, ProbReach will compute an arbitrarily small interval which is guaranteed to contain the required probability. Standard (non-probabilistic) reachability is undecidable even for linear hybrid s…
▽ More
We present ProbReach, a tool for verifying probabilistic reachability for stochastic hybrid systems, i.e., computing the probability that the system reaches an unsafe region of the state space. In particular, ProbReach will compute an arbitrarily small interval which is guaranteed to contain the required probability. Standard (non-probabilistic) reachability is undecidable even for linear hybrid systems. In ProbReach we adopt the weaker notion of delta-reachability, in which the unsafe region is overapproximated by a user-defined parameter (delta). This choice leads to false alarms, but also makes the reachability problem decidable for virtually any hybrid system. In ProbReach we have implemented a probabilistic version of delta-reachability that is suited for hybrid systems whose stochastic behaviour is given in terms of random initial conditions. In this paper we introduce the capabilities of ProbReach, give an overview of the parallel implementation, and present results for several benchmarks involving highly non-linear hybrid systems.
△ Less
Submitted 5 March, 2015; v1 submitted 29 October, 2014;
originally announced October 2014.
-
Probabilistic bounded reachability for hybrid systems with continuous nondeterministic and probabilistic parameters
Authors:
Fedor Shmarov,
Paolo Zuliani
Abstract:
We develop an algorithm for computing bounded reachability probability for hybrid systems, i.e., the probability that the system reaches an unsafe region within a finite number of discrete transitions. In particular, we focus on hybrid systems with continuous dynamics given by solutions of nonlinear ordinary differential equations (with possibly nondeterministic initial conditions and parameters),…
▽ More
We develop an algorithm for computing bounded reachability probability for hybrid systems, i.e., the probability that the system reaches an unsafe region within a finite number of discrete transitions. In particular, we focus on hybrid systems with continuous dynamics given by solutions of nonlinear ordinary differential equations (with possibly nondeterministic initial conditions and parameters), and probabilistic behaviour given by initial parameters distributed as continuous (with possibly infinite support) and discrete random variables. Our approach is to define an appropriate relaxation of the (undecidable) reachability problem, so that it can be solved by $δ$-complete decision procedures. In particular, for systems with continuous random parameters only, we develop a validated integration procedure which computes an arbitrarily small interval that is guaranteed to contain the reachability probability. In the more general case of systems with both nondeterministic and probabilistic parameters, our procedure computes a guaranteed enclosure for the range of reachability probabilities. We have applied our approach to a number of nonlinear hybrid models and validated the results by comparison with Monte Carlo simulation.
△ Less
Submitted 11 May, 2015; v1 submitted 7 June, 2014;
originally announced June 2014.
