Deductive program verification is a difficult task: in general, user guidance is required to control the proof search and construction. Providing the right guiding information is challenging for users and usually requires several reiterations. Supporting the user in this process can considerably reduce the effort of program verification.
Many real world communication protocols exchange complex messages, consisting of multiple nested fields, some could have values that depend on other fields. To properly test an implementation, it is not sufficient to only explore different orders of message exchanges. We also need to test if the implementation produces correctly formatted messages, and responds correctly when it receives different variations of every message type. This paper presents a light weight model based testing tool called APSL. Models are described as labelled transitions systems, from which abstract test sequences can be generated. APSL’s main contribution is in its language for describing complex message formats, text-based or binary, allowing APSL to automatically concretize abstract test sequences, and check incoming messages for their type and format conformance. Testing works out thus of the box: developers do not need to first write a dedicated concretization layer, which would otherwise require substantial investment.
We present KERIS, a configurable, non-centralized server-based framework which enables the combinatorial testing of the Linux kernel's system call interface. The tool constitutes an improvement over our previously developed tool called ERIS by incorporating dynamic memory analysis capabilities among other improvements. The testing framework is designed to offer large-scale automation and requires only minimal high-level input from the user. Several experiments performed with KERIS demonstrate the capabilities of finding and reproducing Linux kernel bugs in an automated manner.
This paper introduces VeriDAG, a verification tool for directed acyclic graphs that represent concurrent programs under memory consistency models. VeriDAG has two novel aspects. First, VeriDAG does not handle concurrent programs directly, but operates on directed acyclic graphs whose edges denote dependencies between instructions in the concurrent programs. This provides software model checking under various memory consistency models by replacing the definitions of edge connections, whereas many model checkers are specific to certain memory consistency models. Second, an engine for exploring execution traces is fully implemented in Haskell with manageable exploration strategies. In contrast, similar model checkers use external engines such as SMT solvers and model checkers that ignore relaxed memory consistency models. Thus, VeriDAG provides a research framework on which we can design new memory consistency models and apply exploration strategies for execution traces under memory consistency models. As evidence, this paper compares VeriDAG with an existing model checker, and implements reordering controls, which are heuristic searches for counterexample detection in directed model checking.
Mobile applications are being used every day by more than half of the world’s population to perform a great variety of tasks. With the increasingly widespread usage of these applications, the need arises for efficient techniques to test them. Many frameworks allow automating the process of application testing, however existing frameworks mainly rely on the application developer for providing testing scripts for each developed application, thus preventing reuse of these tests for similar applications. In this demonstration, we present a novel tool for the automation of testing Android applications by leveraging machine learning techniques and reusing popular test scenarios. We discuss and demonstrate the potential benefits of our tool in an empirical study where we show it outperforms standard methods in realistic settings.
In this paper we provide a concise survey of our work devoted to applying formal methods to check the safety of adaptive cyber-physical systems.
We present an algorithm for synthesising a controller (supervisor) for a discrete event system (DES) based on the property-directed reachability (PDR) model checking algorithm. The discrete event systems framework is useful in both software, automation and manufacturing, as problems from those domains can be modelled as discrete supervisory control problems. As a formal framework, DES is also similar to domains for which the field of formal methods for computer science has developed techniques and tools. In this paper, we attempt to marry the two by adapting PDR to the problem of controller synthesis. The resulting algorithm takes as input a transition system with forbidden states and uncontrollable transitions, and synthesises a safe and minimally-restrictive controller, correct-by-design. We also present an implementation along with experimental results, showing that the algorithm has potential as a part of the solution to the greater effort of formal supervisory controller synthesis and verification.
Modern web browsers allow asynchronous loading of JavaScript scripts in order to speed up parsing a web page. Instead of blocking until a script has been downloaded and evaluated, the async and defer tags in a script allow the browser to download the script in a background task, and either evaluate it as soon as it is available (for async) or evaluate it in load-order at the end of parsing (for defer). While asynchronous loading can significantly speed up the time-to-render, i.e., the time that passes until the first page elements are displayed on-screen, the specification for correct loading is complex and the programmer is responsible for understanding the circumstances under which a script can be loaded asynchronously in either mode without breaking page functionality. As a result, many complex web applications do not take full advantage of asynchronous loading. We present an automatic analysis of web pages which identifies which scripts may be safely deferred, that is, deferred without any observable behavior on the page. Our analysis defers a script if every other script that has a transitive read or modification dependency does not access the DOM. We approximate access and modification sets using a dynamic analysis. On a corpus of 462 professionally developed web pages from Fortune 500 companies, we show that on average, we can identify two or three scripts to defer (mean; median: 1). On 18 pages, we find at least 11 deferrable scripts. Deferring these scripts can have notable impact on time-to-render: in 49 pages, we could show that the median improvement in time-to-render was at least 100 ms, with improvements up to 890 ms.
In this paper, we present RATCOP, a static analysis tool for efficiently computing relational invariants in race free shared-variable multi-threaded Java programs. The tool trades the standard sound-at-all-program-points guarantee for gains in efficiency. Instead, it computes sound facts for a variable only at program points where it is “relevant”. In our experiments, RATCOP was fairly precise while being fast. As a tool, RATCOP is easy-to-use, and easily extensible.
CPS plays important roles along with popularization. In this study, we handle an autonomous robot which estimates its position by observations in discrete two-dimensional field. Probabilistic behaviors are modeled in MDPs, and model checking results validate robot’s design.
Previous work on equivalence checking for synthesis and translation validation has usually verified programs across selected optimizations, disabling the ones that exploit undefined behaviour. On the other hand, modern compilers extensively exploit language level undefined behaviour for optimization. Previous work on equivalence checking for translation validation and synthesis yields poor results, when such optimizations relying on undefined behaviour are enabled. We extend previous work on simulation-based equivalence checking, by adding a framework for reasoning about language level undefined behaviour. We implement our ideas in a tool to compare equivalence across compiler optimizations produced by GCC and LLVM. Testing these compiler optimizations on programs taken from the SPEC integer benchmark suite, we find that modeling undefined behaviour semantics improves success rates for equivalence checking by 31 percentage points (from 50
We consider the task of analyzing message-passing programs by observing their run-time behavior. We introduce a purely library-based instrumentation method to trace communication events during execution. A model of the dependencies among events can be constructed to identify potential bugs. Compared to the vector clock method, our approach is much simpler and has in general a significant lower run-time overhead. A further advantage is that we also trace events that could not commit. Thus, we can infer more alternative communications. This provides the user with additional information to identify potential bugs. We have fully implemented our approach in the Go programming language and provide a number of examples to substantiate our claims.
Formal verification of asynchronous circuits is known to be challenging due to highly non-deterministic behavior exhibited in these systems. One of the main challenges is that it is very difficult to come up with a systematic approach to establishing invariance properties, which are crucial in proving the correctness of circuit behavior. Non-determinism also results in asynchronous circuits having a complex state space, and hence makes the verification task much more difficult than in synchronous circuits. To ease the verification task by reducing non-determinism, and consequently reducing the complexity of the set of execution paths, we impose design restrictions to prevent communication between a module M and other modules while computations are still taking place that are internal to M. These restrictions enable our verification framework to verify loop invariants efficiently via induction and subsequently verify the functional correctness of asynchronous circuit designs. We apply a link-joint paradigm to model asynchronous circuits. Our framework applies a hierarchical verification approach to support scalability. We demonstrate our framework by modeling and verifying the functional correctness of a 32-bit asynchronous serial adder.
Temporal synthesis is the automated design of a system that interacts with an environment, using the declarative specification of the system's behavior. A popular language for providing such a specification is Linear Temporal Logic, or LTL. LTL synthesis in the general case has remained, however, a hard problem to solve in practice. Because of this, many works have focused on developing synthesis procedures for specific fragments of LTL, with an easier synthesis problem. In this work, we focus on Safety LTL, defined here to be the Until-free fragment of LTL in Negation Normal Form~(NNF), and shown to express a fragment of safe LTL formulas. The intrinsic motivation for this fragment is the observation that in many cases it is not enough to say that something "good" will eventually happen, we need to say by when it will happen. We show here that Safety LTL synthesis is significantly simpler algorithmically than LTL synthesis. We exploit this simplicity in two ways, first by describing an explicit approach based on a reduction to Horn-SAT, which can be solved in linear time in the size of the game graph, and then through an efficient symbolic construction, allowing a BDD-based symbolic approach which significantly outperforms extant LTL-synthesis tools.
Understanding malware behavior is critical for cybersecurity. This is still largely done through expert manual analysis of the malware code/binary. In this work, we introduce a fully automated method for malware analysis that utilizes memory traces of program execution. Given both benign and malicious execution traces of a program, the method identifies memory segments specific to the malware attack, and then uses them to localize the attack in the source code. We evaluated our method on the RIPE benchmark for memory corruption malware attacks and demonstrated its ability to: (i) perform diagnosis by identifying the program location of both code corruption (e.g. buffer overflow location) and attack execution (e.g. control flow to payload), (ii) recognize the characteristics of different attacks.
The system designers need in various design tools which could help them both for estimation of possible threats to the security and select one or another ways of their neutralization. There are many approaches to the evaluation (verification) of the degree of protection of programs against possible attacks.
The classical approach to solving the satisfiability problem of propositional logic prunes unsatisfiable branches from the search space. We prune more agressively by also removing certain branches for which there exist other branches that are more satisfiable. This is achieved by extending the popular conflict-driven clause learning (CDCL) paradigm with so-called 𝖯𝖱 -clause learning. We implemented our new paradigm, named satisfaction-driven clause learning (SDCL), in the SAT solver Lingeling. Experiments on the well-known pigeon hole formulas show that our method can automatically produce proofs of unsatisfiability whose size is cubic in the number of pigeons while plain CDCL solvers can only produce proofs of exponential size.
Interpolation is becoming a standard technique for over-approximating state spaces in software model checking with Satisfiability Modulo Theories (SMT). In particular when modelling programs with linear arithmetics, the standard state-of-the-art technique might provide either interpolants that are too specific or too generic to be useful for a given application. In this work we introduce the SI-LRA interpolation system for linear real arithmetics that allows the tuning of interpolants based on shifting between the primal and dual interpolants. We prove a strength relation between the interpolants constructed by SI-LRA, and integrate SI-LRA into a propositional interpolator in an SMT solver. Our evaluation, performed using a state-of-the-art software model checker, reveals that correct tuning with SI-LRA can reduce the number of needed refinements by up to one third and provide lower runtimes.
The paper presents MicroTESK, a tool that automates construction of test program generators for microprocessors. A constructed generator consists of the core that implements architecture-independent generation methods and the model that holds information required to generate tests for the corresponding architecture. The tool extracts this information from formal specifications of the instruction set architecture. The extracted information is used in multiple ways: (1) to get the assembly format of the instructions; (2) to build the coverage model of the instruction set architecture; (3) to construct the instruction set simulator used as a reference model. Test programs are created on the basis of test templates provided by users. Flexible architecture of the tool facilitates integration of new test generation engines. MicroTESK has been applied to the ARMv8, MIPS64, PowerPC, RISC-V, and x86 architectures.
