Search

Merging execution paths is a powerful technique for reducing path explosion in symbolic execution. One approach, introduced and dubbed “veritesting” by Avgerinos et al., works by translating abounded control flow region into a single constraint. This approach is a convenient way to achieve path merging as a modification to a pre-existing single-path symbolic execution engine. Previous work evaluated this approach for symbolic execution of binary code, but different design considerations apply when building tools for other languages. In this paper, we extend the previous approach for symbolic execution of Java. Because Java code typically contains many small dynamically dispatched methods, it is important to include them in multi-path regions; we introduce dynamic inlining of method-regions to do so modularly. Java’s typed memory structure is very different from the binary representation, but we show how the idea of static single assignment (SSA) form can be applied to object references to statically account for aliasing. We have implemented our algorithms in Java Ranger, an extension to the widely used Symbolic Pathfinder tool. In a set of nine benchmarks, Java Ranger reduces the running time and number of execution paths by a total of 38% and 71% respectively as compared to SPF. Our results are a significant improvement over the performance of JBMC, a recently released verification tool for Java bytecode. We also participated in a static verification competition at a top theory conference where other participants included state-of-the-art Java verifiers. JR won first place in the competition’s Java verification track.

Path-merging is a known technique for accelerating symbolic execution. One technique, named “veritesting” by Avgerinos et al. uses summaries of bounded control-flow regions and has been shown to accelerate symbolic execution of binary code. But, when applied to symbolic execution of Java code, veritesting needs to be extended to summarize dynamically dispatched methods and exceptional control-flow. Such an extension of veritesting has been implemented in Java Ranger by implementing as an extension of Symbolic PathFinder, a symbolic executor for Java bytecode. In this paper, we briefly describe the architecture of Java Ranger and describe its setup for SV-COMP 2020.

Scaling symbolic execution to industrial-sized programs is an important open research problem. Veritesting is a promising technique that improves scalability by combining the advantages of static symbolic execution with those of dynamic symbolic execution. The goal of veritesting is to reduce the number of paths to explore in symbolic execution by creating formulas describing regions of code using disjunctive formulas. In previous work, veritesting was applied to binary-level symbolic execution. Integrating veritesting with Java bytecode presents unique challenges: notably, incorporating non-local control jumps caused by runtime polymorphism, exceptions, native calls, and dynamic class loading. If these language features are not accounted for, we hypothesize that the static code regions described by veritesting are often small and may not lead to substantial reduction in paths. We examine this hypothesis by running a Soot-based static analysis on six large open-source projects used in the Defects4J collection. We find that while veritesting can be applied in thousands of regions, allowing static symbolic execution involving non-local control jumps amplifies the performance improvement obtained from veritesting. We hope to use these insights to support efficient veritesting in Symbolic PathFinder in the near future. Toward this end, we brie y address some engineering challenges to add veritesting into SPF.

JKind is an open-source industrial model checker developed by Rockwell Collins and the University of Minnesota. JKind uses multiple parallel engines to prove or falsify safety properties of infinite state models. It is portable, easy to install, performance competitive with other state-of-the-art model checkers, and has features designed to improve the results presented to users: inductive validity cores for proofs and counterexample smoothing for test-case generation. It serves as the back-end for various industrial applications.

Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quality of complex embedded systems. Given appropriate architectural descriptions, assume/guarantee contracts, and compositional reasoning rules, these techniques can be used to prove important safety properties about the architecture prior to system construction. For these proofs to be meaningful, each leaf-level component contract must be realizable; i.e., it is possible to construct a component such that for any input allowed by the contract assumptions, there is some output value that the component can produce that satisfies the contract guarantees. We have recently proposed ini¾ź[1] a contract-based realizability checking algorithm for assume/guarantee contracts over infinite theories supported by SMT solvers such as linear integer/real arithmetic and uninterpreted functions. In that work, we used an SMT solver and an algorithm similar to k-induction to establish the realizability of a contract, and justified our approach via a hand proof. Given the central importance of realizability to our virtual integration approach, we wanted additional confidence that our approach was sound. This paper describes a complete formalization of the approach in the Coq proof and specification language. During formalization, we found several small mistakes and missing assumptions in our reasoning. Although these did not compromise the correctness of the algorithm used in the checking tools, they point to the value of machine-checked formalization. In addition, we believe this is the first machine-checked formalization for a realizability algorithm.

English language requirements are often used to specify the behavior of complex cyber-physical systems. The process of transforming these requirements to a formal specification language is often challenging, especially if the specification language does not contain constructs analogous to those used in the original requirements. For example, requirements often contain real-time constraints, but many specification languages for model checkers have discrete time semantics. Work in specification patterns helps to bridge these gaps, allowing straightforward expression of common requirements patterns in formal languages. In this work we demonstrate how we support real-time specification patterns in the Assume Guarantee Reasoning Environment AGREE using observers. We demonstrate that there are subtle challenges, not mentioned in previous literature, to express real-time patterns accurately using observers. We then demonstrate that these patterns are sufficient to model real-time requirements for a real-world avionics system.

Guardol is a domain-specific language focused on the creation of high-assurance network guards and the specification of guard properties. The Guardol system generates Ada code from Guardol programs and also provides specification and automated verification support. Guard programs and specifications are translated to higher order logic, then deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.

This paper describes an extension to Lustre to support the analysis of globally asynchronous, locally synchronous (GALS) architectures. This extension consists of constructs for directly specifying the timeout automata used to describe asynchronous communication between processes represented by Lustre nodes. It is implemented using an extensible language framework based on attribute grammars that allows such extensions to be modularly defined so that they may be more easily composed with other language extensions.

Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quality of complex embedded systems. Given appropriate architectural descriptions and compositional reasoning rules, these techniques can be used to prove important safety properties about the architecture prior to system construction. Such proofs build from “leaf-level” assume/guarantee component contracts through architectural layers towards top-level safety properties. The proofs are built upon the premise that each leaf-level component contract is realizable; i.e., it is possible to construct a component such that for any input allowed by the contract assumptions, there is some output value that the component can produce that satisfies the contract guarantees. Without engineering support it is all too easy to write leaf-level components that can’t be realized. Realizability checking for propositional contracts has been well-studied for many years, both for component synthesis and checking correctness of temporal logic requirements. However, checking realizability for contracts involving infinite theories is still an open problem. In this paper, we describe a new approach for checking realizability of contracts involving theories and demonstrate its usefulness on several examples.

Arguments about the safety, security, and correctness of a complex system are often made in the form of an assurance case. An assurance case is a structured argument, often represented with a graphical interface, that presents and supports claims about a system's behavior. The argument may combine different kinds of evidence to justify its top level claim. While assurance cases deliver some level of guarantee of a system's correctness, they lack the rigor that proofs from formal methods typically provide. Furthermore, changes in the structure of a model during development may result in inconsistencies between a design and its assurance case. Our solution is a framework for automatically generating assurance cases based on 1) a system model specified in an architectural design language, 2) a set of logical rules expressed in a domain specific language that we have developed, and 3) the results of other formal analyses that have been run on the model. We argue that the rigor of these automatically generated assurance cases exceeds those of traditional assurance case arguments because of their more formal logical foundation and direct connection to the architectural model., 9 pages, accepted to HILT 2014

Autonomy is increasingly important in missions to remote locations (e.g., space applications and deep sea exploration) since limited bandwidth and communication delays make detailed instructions from a remote base (e.g., Earth or a land base) impractical. The planning systems used for autonomous operation are difficult to verify and validate because they must create plans for use in a specific environment and the correct behavior might not be easy to define. To explore verification and validation of planning systems, we have developed a verification framework for the PLEXIL plan execution language. The framework allows us to perform verification and test case generation using Java Symbolic PathFinder. Using this framework, we have performed verification, bounded verification and test-case generation for NASA-relevant PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in the definition of the If/Then/Else construct in the Extended PLEXIL language that could lead to plan deadlocks, and one in the semantics of the core language that could cause the PLEXIL executive to crash.

Systems are naturally constructed in hierarchies in which design choices made at higher levels of abstraction ``flow down'' to requirements on system components at lower levels of abstraction. Thus, whether an aspect of the system is a design choice or a requirement depends largely on one's vantage point within the hierarchy of system components. Furthermore, systems are often constructed middle-out rather than top-down; compatibility with existing systems and architectures, or availability of specific components influences high-level requirements. We believe that requirements and architectural design should be more closely aligned: that requirements models must account for hierarchical system construction, and that architectural design notations must better support specification of requirements for system components.In this presentation, I describe tools supporting iterative development of architecture and verification based on software models. We represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe requirements at different levels of abstraction for compositional verification. To describe and verify component-level behavior, we use Simulink and Stateflow and multiple analysis tools.

Complex systems are by necessity hierarchically organized. Decomposition into subsystems allows for intellectual control, as well as enabling different subsystems to be created by distinct teams. This decomposition affects both requirements and architecture. The architecture describes the structure and this affects how requirements ``flow down'' to each subsystem. Moreover, discoveries in the design process may affect the requirements. Demonstrating that a complex system satisfies its requirements when the subsystems are composed is a challenging problem. In this paper, we present a medical device case example where we apply an iterative approach to architecture and verification based on software architectural models. We represent the hierarchical composition of the system in the Architecture Analysis and Design Language (AADL), and use an extension to the AADL language to describe the requirements at different levels of abstraction for compositional verification. The component-level behavior for the model is described in Simulink/Stateflow. We assemble proofs of system level properties by using the Simulink Design Verifier to establish component-level properties and an open-source plug-in for the OSATE AADL environment to perform the compositional verification of the architecture. This combination of verification tools allows us to iteratively explore design and verification of detailed behavioral models, and to scale formal analysis to large software systems.

Symbolic execution is a program analysis technique that attempts to explore all possible paths through a program by using symbolic values rather than actual data values as inputs. When applied to Statecharts, a model-based formalism for reactive systems, symbolic execution can determine all feasible paths through a model up to a specified bound and generate input sequences exercising these paths. The main drawback of this method is its computational expense. This paper describes two efforts to improve the performance of symbolic execution within our previously developed framework for Statechart analysis. One method is a multithreaded symbolic execution engine targeted directly at our framework. A second, orthogonal, method is program specialization with respect to a particular model and Statechart semantics, which uses symbolic execution to rewrite the original code into an equivalent form that has fewer instructions and is easier to analyze.

Statecharts is a model-based formalism for simulating and analyzing reactive systems. In our previous work, we developed Polyglot, a unified framework for analyzing different semantic variants of Statechart models. However, for systems containing communicating, asynchronous components deployed on a distributed platform, additional features not inherent to the basic Statecharts paradigm are needed. These include a connector mechanism for communication, a scheduling framework for sequencing the execution of individual components, and a method for specifying verification properties spanning multiple components. This paper describes the addition of these features to Polyglot, along with an example NASA case study using these new features. Furthermore, the paper describes on-going work on modeling Plexil execution plans with Polyglot, which enables the study of interaction issues for future manned and unmanned missions.

Guardol is a domain-specific language designed to facilitate the construction of correct network guards operating over tree-shaped data. The Guardol system generates Ada code from Guardol programs and also provides specification and automated verification support. Guard programs and specifications are translated to higher order logic, then deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.

In large programs such as NASA Exploration, multiple systems that interact via safety-critical protocols are already designed with different Statechart variants. To verify these safety-critical systems, a unified framework is needed based on a formal semantics that captures the variants of Statecharts. We describe Polyglot, a unified framework for the analysis of models described using multiple State-chart formalisms. In this framework, Statechart models are translated into Java and analyzed using pluggable semantics for different variants operating in a polymorphic execution environment. The framework has been built on the basis of a parametric formal semantics that captures the common core of Statecharts with extensions for different variants, and addresses previous limitations. Polyglot has been integrated with the Java Pathfinder verification tool-set, providing analysis and test-case generation capabilities. We describe the application of this unified framework to the analysis of NASA/JPL's MER Arbiter whose interacting components were modeled using multiple Statechart formalisms.

Information flow modeling describes how information can be transferred between different locations within a software and/or hardware system. In this chapter, we define a notion of information flow based on traces that is useful for describing flow relations for synchronous dataflow languages such as SimulinkⓇ (The Mathworks, Inc.) and SCADE™ (Esterel Technologies, Inc.) that are often used for hardware/software codesign. We then define an automated method for analyzing information flow properties of Simulink models using model checking. This method is based on creating a flow model that tracks information flow throughout the model. Often, information flow properties are defined in terms of some form of noninterference, which states informally that objects in one security domain cannot perceive the actions of objects within another domain. We demonstrate that this method preserves the GWV functional notion of noninterference. We then describe how this proof relates to the GWV theorem and provide some insight into the relationship of the flow model and the flow graphs used in GWVr1. Finally, we demonstrate our analysis technique by analyzing the architecture of the Turnstile high-assurance cross-domain guard platform using our Gryphon translation framework and the Prover™ model checker.

Recent advances in modeling languages have made it feasible to formally specify and analyze the behavior of large system components. Synchronous data flow languages, such as Lustre, SCR, and RSML are well suited to this task, and commercial versions of these tools such as SCADE and Simulink are growing rapidly in popularity among designers of safety critical systems, largely due to their ability to automatically generate code from the models. At the same time, advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This report describes how such formal verification tools have been applied to the FCS 5000, a new family of Flight Control Systems being developed by Rockwell Collins Inc.

Assurance that a formal specification (system specification or software specification) possesses desired properties can be achieved through (1) manual inspections, (2) formal verification of the desired properties, or (3) simulation and testing of the specification. To achieve the high level of confidence in the correctness required in a safety-critical system, all three approaches must be used in concert. We have developed an specification language, called RSML/sup -e/, and an environment, called NIMBUS, which provides support for all these activities. The three V&V techniques fill complementary roles within the validation and verification process. Manual inspections and visualization provide the specification team, customers, and regulatory representatives the means to informally verify that the behavior described formally matches the desired "real world" behavior of the system. RSML/sup -e/ is a fully formal, synchronous, data-flow language. NIMBUS supports large-scale, distributed simulation of specifications through communications over Microsoft's distributed COM or OMG's CORBA.

Automated translation, or code generation, of a formal requirements model to production code can alleviate many of the problems associated with design and implementation. In this paper, we outline the requirements of such code generation to obtain a high level of confidence in the correctness of the translation process. We then describe a translator for a state-based modeling language called RSML (Requirements Specification Modeling Language) that largely meets these requirements.

Although autocoding techniques promise large gains in software development productivity, their "real-world" application has been limited, particularly in safety-critical domains. Often, the major impediment is the missing trustworthiness of these systems: demonstrating - let alone formally certifying - the trustworthiness of automatic code generators is extremely difficult due to their complexity and size. We develop an alternative product-oriented certification approach which is based on five principles: (1) trustworthiness of the generator is reduced to the safety of each individual generated program; (2) program safety is defined as adherence to an explicitly formulated safety policy; (3) the safety policy is formalized by a collection of logical program properties; (4) Hoare-style program verification is used to show that each generated program satisfies the required properties; (5) the code generator itself is extended to automatically produce the code annotations required for verification. The approach is feasible because the code generator has full knowledge about the program under construction and about the properties to be verified. It can thus generate all auxiliary code annotations a theorem prover needs to discharge all emerging verification obligations fully automatically. Here we report how this approach is used in a certification extension for AutoBayes, an automatic program synthesis system which generates data analysis programs (e.g., for clustering and time-series analysis) from declarative specifications. In particular, we describe how a variable-initialization-before-use safety policy can be encoded and certified.

Formal specifications can be hundreds of pages in length-a reflection of the size and complexity of the systems being specified. Lengthy documents are difficult to read understand, and use. Program slicing was developed to address these issues for programs. The authors apply similar techniques to formal specifications expressed as hierarchical state machines. They present a two tiered approach to slicing (or simplification) of hierarchical state machines. They have applied their techniques to a large case study and present empirical data highlighting the reduction and simplification capabilities of their approach to large specifications.

Code certification is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be defined and formalized via properties, e.g., operator safety or memory safety. Its basic idea is to require code producers to provide formal proofs that their code satisfies these quality properties. The proofs serve as certificates which can be checked independently, by the code consumer or by certification authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code [6].

We are attempting to create a translator for a formal state-based specification language (RSML-e) that is suitable for use in safety-critical systems. For such a translator, there are two main concerns: the generated code must be shown to be semantically equivalent to the specification, and it must be fast enough to be used in the intended target environment. We address the first concern by providing a formal proof of the translation, and by keeping the implementation of the tool as simple as possible. The second concern is addressed through a variety of methods: (1) decomposing a specification into parallel subtasks, (2) providing provably-correct optimizations, and (3) making worst-case performance guarantees on the generated code.

Code certification is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satisfies certain quality properties. These proofs serve as certificates that can be checked independently. Since code certification uses the same underlying technology as program verification, it requires detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding annotations to the code is time-consuming and error-prone. We address this problem by combining code certification with automatic program synthesis. Given a high-level specification, our approach simultaneously generates code and all annotations required to certify the generated code. We describe a certification extension of AutoBayes, a synthesis tool for automatically generating data analysis programs. Based on built-in domain knowledge, proof annotations are added and used to generate proof obligations that are discharged by the automated theorem prover E-SETHEO. We demonstrate our approach by certifying operator- and memory-safety on a data-classification program. For this program, our approach was faster and more precise than PolySpace, a commercial static analysis tool.