Symbolic reachability analysis using rewriting with Satisfiability Modulo Theories (SMT) has been used to model different systems, including a variety of security protocols. Recently, it has also been used to analyze systems modeled using Parametric Timed Automata (PTAs). These techniques are based on reachability in a finite state graph generated from symbolic initial states where each generated state is constrained by an SMT expression checked for satisfiability. In this work, by rewriting with SMT but by narrowing with SMT. we use narrowing with SMT instead of rewriting with SMT. Narrowing with SMT allows a greater generalization, since (i) an infinite number of initial states may be represented by a finite number of states with variables, not only SMT variables, and (ii) an infinite state graph from an initial state may be represented by a finite state graph from another initial state with variables, not only SMT variables. We use graph search pruning techniques via irreducible terms and SMT constraints on conditional rules. This is supported by a novel folding SMT narrowing technique to represent infinite computations in a finite way. Additionally, we present a new textual user interface that allows the use of the algorithm in a simpler and more readable way.
Fault trees (FTs) are hierarchical diagrams used to model the propagation of faults in a system. Fault tree analysis (FTA) is a widespread technique that allows to identify the key factors that contribute to system failure. In recent work we introduced BFL , a Boolean Logic for Fault trees. BFL can be used to formally define simple yet expressive properties for FTA, e.g.: 1) we can set evidence to analyse what-if scenarios; 2) check whether two elements are independent or if they share a child that can influence their status; 3) and set upper/lower boundaries for failed elements. Furthermore, we provided algorithms based on binary decision diagrams (BDDs) to check BFL properties on FTs. In this work, we evaluate usability of a different approach by employing quantified Boolean formulae (QBFs) instead of BDDs. We present a translation from BFL to QBF and provide an implementation—making it the first tool for checking BFL properties—that builds on top of the Z3 solver. We further demonstrate its usability on a case study FT and investigate runtime, memory consumption and scalability on a number of benchmark FTs. Lastly, qualitative differences from a BDD-based approach are discussed.
Mechanical ventilators are increasingly used for life support of critically ill patients. In this sense, despite recent technological advances, the accurate specification of their properties remains challenging, and the use of formal tools is limited. This work focuses on verifying the properties of the architecture of a mechanical ventilator using UPPAAL as a modeling tool. As a result, the system requirements and specification of a functional prototype were verified and improved using the formal model of a mechanical ventilator. This approach provides a valuable means of ensuring the correctness and reliability of mechanical ventilator systems.
We propose a quantitative risk assessment approach for the design of an obstacle detection function for low-speed freight trains with grade of automation 4. In this five-step approach, starting with single detection channels and ending with a three-out-of-three model comprised of three independent dual-channel modules and a voter, we exemplify a probabilistic assessment, using a combination of statistical methods and parametric stochastic model checking. We illustrate that, under certain not unreasonable assumptions, the resulting hazard rate becomes acceptable for the discussed application setting. The statistical approach for assessing the residual risk of misclassifications in convolutional neural networks and conventional image processing software suggests that high confidence can be placed into the safety-critical obstacle detection function, even though its implementation involves realistic machine learning uncertainties.
Both Rust and SPARK are memory-safe programming languages and feature stronger safety guarantees than other popular programming languages for embedded software. However, modern systems often combine software written in multiple programming languages using the Foreign Function Interface (FFI). When using safety-oriented programming languages such as Rust and SPARK, maintaining compile-time safety guarantees across a language boundary is a challenge. The objective of this study is to explore if/how the inherent safety guarantees of these languages are preserved, and their potential benefits when establishing a library interface between them. In particular, we apply our method to the BBQueue circular buffer library that features complex ownership hand-over patterns when using FFI. Results reveal that most of the inherent consistency and safety features of these languages can be maintained. Yet, special caution is required at the FFI boundary to prevent potential vulnerabilities.
Signal temporal logic (STL) is a temporal logic formalism for specifying properties of continuous signals. STL has been widely used for specifying, monitoring, and testing properties of hybrid systems that exhibit both discrete and continuous behavior. However, model checking techniques for hybrid systems have been primarily limited to invariant and reachability properties. This is mainly due to the intrinsic nature of hybrid systems, which involve uncountably many signals that continuously change over time. For hybrid systems, checking whether all possible behaviors satisfy an STL formula requires a certain form of abstraction and discretization, which has not been developed for general STL properties. In this talk, I introduce bounded model checking algorithms and tools for general STL properties of hybrid systems. Central to our technique is a novel logical foundation for STL: (i) a syntactic separation of STL, which decomposes an STL formula into components, with each component relying exclusively on separate segments of a signal, and (ii) a signal discretization, which ensures a complete abstraction of a signal, given by a set of discrete elements. With this new foundation, the STL model checking problem can be reduced to the satisfiability of a first-order logic formula. This allows us to develop the first model checking algorithm for STL that can guarantee the correctness of STL up to given bound parameters, and a pioneering bounded model checker for hybrid systems, called STLmc.
We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the total execution time. The system, here modelled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both public and private corresponding runs. We focus on the untimed control problem: exhibiting a controller, ie a set of allowed actions, such that the system restricted to those actions is fully timed-opaque. We first show that this problem is not more complex than the full timed opacity problem, and then we propose an algorithm, implemented and evaluated in practice.
Robots and other cyber-physical systems are held to high standards of safety and reliability, and thus one must be confident in the correctness of their software. Formal verification can provide such confidence, but programming languages that lend themselves well to verification often do not produce executable code, and languages that are executable do not typically have precise enough formal semantics. We present MARVeLus, a stream-based approach to combining verification and execution in a synchronous programming language that allows formal guarantees to be made about implementation-level source code. We then demonstrate the end-to-end process of developing a safe robotics application, from modeling and verification to implementation and execution.
Functional Block Diagrams (FBD) are commonly used as a graphical representation for probabilistic risk assessment in a wide range of complex engineering applications. An FBD models the stochastic behavior and cascading dependencies of system components or subsystems. Within FBD-based safety analysis, Event Trees (ET) dependability modeling techniques are typically used to associate all possible risk events to each subsystem. In this paper, we conduct the formal modeling and probabilistic risk assessment of a nuclear power plant in the HOL4 theorem prover. Using an FBD modeling in HOL4 of the nuclear Boiling Water Reactor (BWR), we formally determine all possible classes of accident events that can occur in the BWR. We compare our formal analysis in HOL4 with those obtained analytically and by simulation using Matlab and the specialized Isograph tool. Experimental results showed the superiority of our approach in terms of scalability, expressiveness, accuracy and CPU time.
This paper presents a rewriting logic semantics for parametric timed automata (PTAs) and shows that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We then refine standard Maude-with-SMT reachability analysis so that the analysis terminates when the symbolic state space of the PTA is finite. We show how we can synthesize parameters with our methods, and compare their performance with Imitator, a state-of-the-art tool for PTAs. The practical contributions are two-fold: providing new analysis methods for PTAs---e.g. allowing more general state properties in queries and supporting reachability analysis combined with user-defined execution strategies---not supported by Imitator, and developing symbolic analysis methods for real-time rewrite theories.
Security-critical applications often rely on memory isolation mechanisms to ensure integrity of critical data (e.g., keys) and program instructions (e.g., implementing an attestation protocol). These include software-based security microvisor (SµV) or hardware-based (e.g., TrustLite or SMART). Here, we must guarantee that none of the assembly-level instructions corresponding to a program violate the imposed memory access restrictions. We demonstrate our approach on two architectures (SµV and TrustLite) on which remote attestation protocols are implemented. We extend an approach based on the Binary Analysis Platform (BAP) to generate compiled assembly for a given C program, which is translated to an assembly intermediate language (BIL) and ultimately to Isabelle/HOL theories. In our extension, we develop an adversary model and define conformance predicates imposed by an architecture. We generate a set of programs covering all possible cases in which an assembly-level instruction attempts to violate at least one of the conformance predicates. This shows that the memory access restriction of both SµV and TrustLite are dynamically maintained. Moreover, we introduce conformance predicates for assembly-level instructions that can change the control flow, which improve TrustLite’s memory protection unit.
Cooperative verification is an approach in which several verifiers help each other solving the verification problem by sharing artifacts about the verification process. There are many verification tools available, but the power of combining them is not yet fully leveraged. The problem is that in order to use verifiers 'off-the-shelf', we need clear interfaces to invoke the tools and to pass information. Part of the interfacing problem is to define standard artifacts to be exchanged between verifiers. We explain a few recent approaches for cooperative combinations and also give a brief overview of CoVeriTeam, a tool for composing verification systems from existing off-the-shelf components.
A concurrent system specified as a rewrite theory can be symbolically analyzed using narrowing-based reachability analysis. Narrowing-based approaches have been applied to formally analyze cryptographic protocols and parameterized protocols. However, existing narrowing-based techniques, based on a breadth-first-search strategy, cannot deal with generic distributed systems with objects and messages due to the symbolic state-space explosion problem. This paper proposes a heuristic search approach for narrowing-based reachability analysis to guide the search for counterexamples involving a small number of objects. As a result, our method can effectively find a counterexample if an error state is reachable. We demonstrate the effectiveness of our technique using a nontrivial distributed consensus algorithm.
We present Q Framework: a verification framework used at Sandia National Laboratories. Q is a collection of tools used to verify safety and correctness properties of high-consequence embedded systems and captures the structure and compositionality of system specifications written with state machines in order to prove system-level properties about their implementations. Q consists of two main workflows: 1) compilation of temporal properties and state machine models (such as those made with Stateflow) into SMV models and 2) generation of ACSL specifications for the C code implementation of the state machine models. These together prove a refinement relation between the state machine model and its C code implementation, with proofs of properties checked by NuSMV (for SMV models) and Frama-C (for ACSL specifications).
A programmable logic controller (PLC) is widely used in industrial control systems, and Structured text (ST) is an imperative language to develop PLC programs. Because of its safety-critical nature, formally analyzing PLC programs is important, and a rewriting-based formal semantics of ST has been proposed for this purpose. This paper presents a bounded model checking technique for PLC ST programs based on the rewriting-based semantics. We apply rewriting modulo SMT to symbolically analyze LTL properties of ST programs with respect to sequences of (possibly infinite) inputs and outputs. We have demonstrated the effectiveness of our approach using a traffic light case study.
To create trustworthy programs, the 'gold standard' is specifications at a high-enough level to clearly correspond to the informal specifications, and also a refinement proof linking these high-level specifications down to, in our case, executable bytecode. The DeepSEA system demonstrates how this can be done, in the context of smart contracts on the Ethereum blockchain. A key component of this is the model of the blockchain on which the smart contracts reside. When doing proofs in DeepSEA, it is critical to have such a model, which allows for the writing of specifications at a high-level clearly corresponding to informal specifications. A candidate model for doing so and its usefulness for carrying out proofs is discussed in this paper.
Complex cyber-physical systems can be difficult to analyze for resource adequacy at the concept development stage since relevant models are hard to create. During this period, details about the functions to be executed or the platforms in the architecture are partially unknown. This is especially true for Integrated Modular Avionics (IMA) Systems, for which life-cycles span over several decades, with potential changes to functionality in the future. To support the engineers evaluating conceptual designs there is a need for tools that model resources of interest in an abstract manner and allow analyses of changing architectures in a modular and scalable way. This work presents a generic timed automata-based model of a networked IMA system abstracting complex networking and computational elements of an architecture, but representing the communication needs of each application function using UPPAAL templates. The proposed model is flexible and can be modified/extended to represent different types of network topologies and communication patterns. More specifically, the different components of the IMA network, Core Processing Modules, Network End-Systems, and Switches, are represented by different templates. The templates are then instantiated to represent a conceptual design, and fed into a model checker to verify that a given platform instance supports the desired system functions in terms of network bandwidth and buffer size adequacy - in particular, whether messages can reach their final destination on time. The work identifies the limits of the tool used for this evaluation, but the conceptual model can be carried over to other tools for further studies.
Due to major breakthroughs in software and engineering technologies, embedded systems are increasingly being utilized in areas ranging from aerospace and next-generation transportation systems, to smart grid and smart cities, to health care systems, and broadly speaking to what is known as Cyber-Physical Systems (CPS). A CPS is primarily composed of several electronic, communication and controller modules and some actuators and sensors. The mix of heterogeneous underlying smart technologies poses a number of technical challenges to the design and more severely to the verification of such complex infrastructure. In fact, a CPS shall adhere to strict safety, reliability, performance and security requirements, where one needs to capture both physical and random aspects of the various CPS modules and then analyze their interrelationship across interlinked continuous and discrete dynamics. Oftentimes however, system bugs remain uncaught during the analysis and in turn cause unwanted scenarios that may have serious consequences in safety-critical applications. In this paper, we introduce some of the challenges surrounding the design and verification of contemporary CPS with the advent of smart technologies. In particular, we survey recent developments in the use of theorem proving, a formal method, for the modeling, analysis and verification of CPS, and overview some real world CPS case studies from the automotive, avionics and healthtech domains from system level to physical components.
This study proposes a semi-automatic extraction of the formal semantics of MIPS architecture from the pseudocode description in MIPS instruction manual. Among 127 collected instructions, we focus on the 63 instructions of the CPU category. After manually preparing 21 primitive functions in the pseudocode description, their semantics are successfully generated as Java methods, which are unified to a dynamic symbolic execution tool SyMIPS. We perform an empirical study on 3219 MIPS32 IoT malware collected from ViruSign and observe that SyMIPS successfully traces 2412 samples, in which SyMIPS finds the dead conditional branch, e.g., in DDOS-Y. The rest is interrupted by either timeout, stack overflow, or exceptions, which current SyMIPS does not cover.
In this article, we describe a static program analysis to determine the lowest floating-point precisions on inputs and intermediate results that guarantees a desired accuracy of the output values. A common practice used by developers without advanced training in computer arithmetic consists in using the highest precision available in hardware (double precision on most CPU’s) which can be exorbitant in terms of energy consumption, memory traffic, and bandwidth capacity. To overcome this difficulty, we propose a new precision tuning tool for the floating-point programs integrating a static forward and backward analysis, done by abstract interpretation. Next, our analysis will be expressed as a set of linear constraints easily checked by an SMT solver.
