In this paper, we consider an analysis of temporal properties of hybrid systems based on simulations, so-called falsification of requirements. We present a novel exploration-based algorithm for falsification of black-box models of hybrid systems based on the Voronoi bias. This approach is inspired by techniques used originally in motion planning: rapidly exploring random trees. Instead of commonly employed exploration that is based on coverage of inputs, the proposed exploration algorithm aims to explore possible outputs directly. It achieves that by covering a feature space that is associated with some spatial and temporal properties of output signals. This approach also does not require robustness or other guidance metrics tied to a specific behavior that is being falsified. This allows our algorithm to falsify specifications for which robustness is not conclusive enough to guide the falsification procedure.

We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information it has declassified via assume annotations already widely used in deductive program verification; and (b) auditing the declassifications against a declarative security policy. We show how condition (a) can be enforced by an extension of the existing program logic SecCSL, and how (b) can be checked by proving a set of simple entailments. Part of the challenge is to define respective semantic soundness criteria and to formally connect these to the logic rules and policy audit. We support our methodology in an auto-active program verifier, which we apply to verify the implementations of various case study programs against a range of declassification policies.

Abstract Korn is a software verifier that infers correctness certificates and violation witnesses sutomatically using state-of-the-art Horn-clause solvers, such as Z3 and Eldarica. The solvers are used in a portfolio together with cheap random sampling where the latter can be very effective at finding counterexamples. Korn perfomend best in the sub-category of SV-COMP 2023.

The statefulness property of network protocol implementations poses a unique challenge for testing and verification techniques, including Fuzzing. Stateful fuzzers tackle this challenge by leveraging state models to partition the state space and assist the test generation process. Since not all states are equally important and fuzzing campaigns have time limits, fuzzers need effective state selection algorithms to prioritize progressive states over others. Several state selection algorithms have been proposed but they were implemented and evaluated separately on different platforms, making it hard to achieve conclusive findings. In this work, we evaluate an extensive set of state selection algorithms on the same fuzzing platform that is AFLNet, a state-of-the-art fuzzer for network servers. The algorithm set includes existing ones supported by AFLNet and our novel and principled algorithm called AFLNetLegion. The experimental results on the ProFuzzBench benchmark show that (i) the existing state selection algorithms of AFLNet achieve very similar code coverage, (ii) AFLNetLegion clearly outperforms these algorithms in selected case studies, but (iii) the overall improvement appears insignificant. These are unexpected yet interesting findings. We identify problems and share insights that could open opportunities for future research on this topic.

Abstract We present an approach to synthesize relational invariants to prove equivalences between object-oriented programs. The approach bridges the gap between recursive data types and arrays that serve to represent internal states. Our relational invariants are recursively-defined, and thus are valid for data structures of unbounded size. Based on introducing recursion into the proofs by observing and lifting the constraints from joint methods of the two objects, our approach is fully automatic and can be seen as an algorithm for solving Constrained Horn Clauses (CHC) of a specific sort. It has been implemented on top of the SMT-based CHC solver AdtChc and evaluated on a range of benchmarks.

Legion is a grey-box coverage-based concolic tool that aims to balance the complementary nature of fuzzing and symbolic execution to achieve the best of both worlds. It proposes a variation of Monte Carlo tree search (MCTS) that formulates program exploration as sequential decision-making under uncertainty guided by the best-first search strategy. It relies on approximate path-preserving fuzzing , a novel instance of constrained random testing, which quickly generates many diverse inputs that likely target program parts of interest. In Test-Comp 2020 [ 1 ], the prototype performed within 90% of the best score in 9 of 22 categories.

Concolic execution and fuzzing are two complementary coverage-based testing techniques. How to achieve the best of both remains an open challenge. To address this research problem, we propose and evaluate Legion. Legion re-engineers the Monte Carlo tree search (MCTS) framework from the AI literature to treat automated test generation as a problem of sequential decision-making under uncertainty. Its best-first search strategy provides a principled way to learn the most promising program states to investigate at each search iteration, based on observed rewards from previous iterations. Legion incorporates a form of directed fuzzing that we call approximate path-preserving fuzzing (APPFuzzing) to investigate program states selected by MCTS. APPFuzzing serves as the Monte Carlo simulation technique and is implemented by extending prior work on constrained sampling. We evaluate Legion against competitors on 2531 benchmarks from the coverage category of Test-Comp 2020, as well as measuring its sensitivity to hyperparameters, demonstrating its effectiveness on a wide variety of input programs.

We present SecCSL , a concurrent separation logic for proving expressive, data-dependent information flow security properties of low-level programs. SecCSL is considerably more expressive, while being simpler, than recent compositional information flow logics that cannot reason about pointers, arrays etc. To capture security concerns, SecCSL adopts a relational semantics for its assertions. At the same time it inherits the structure of traditional concurrent separation logics; thus SecCSL reasoning can be automated via symbolic execution. We demonstrate this by implementing SecC , an automatic verifier for a subset of the C programming language, which we apply to a range of benchmarks.

VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange.

Abstract Framing is important for specification and verification, especially in programs that mutate data structures with shared data, such as DAGs. Both separation logic and region logic are successful approaches to framing, with separation logic providing a concise way to reason about data structures that are disjoint, and region logic providing the ability to reason about framing for shared mutable data. In order to obtain the benefits of both logics for programs with shared mutable data, this paper unifies them into a single logic, which can encode both of them and allows them to interoperate. The new logic thus provides a way to reason about program modules specified in a mix of styles.

Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification-a methodology of search-based testing that employs stochastic optimization-is thus attracting attention as an alternative quality assurance method. Inspired by the recent work that advocates coverage and exploration in falsification, we introduce a two-layered optimization framework that uses Monte Carlo tree search (MCTS), a popular machine learning technique with solid mathematical and empirical foundations (e.g., in computer Go). MCTS is used in the upper layer of our framework; it guides the lower layer of local hill-climbing optimization, thus balancing exploration and exploitation in a disciplined manner. We demonstrate the proposed framework through experiments with benchmarks from the automotive domain.

Specification languages have long featured ways to describe what does not change when an imperative procedure is executed: the so-called frame problem. Solutions to the frame problem are needed for formal verification in imperative programming, as otherwise a verification would not be able to accumulate information from one statement to the next. Region logic is one of the approaches to solving the frame problem. We present a modified version of region logic with fine granularity and introduce conditional effects that allows one to specify more precise frame conditions.

This paper presents a logic that extends basic ITL with explicit, interleaved programs. The calculus is based on symbolic execution, as previously described. We extend this former work here, by integrating the logic with higher-order logic, adding recursive procedures and rules to reason about fairness. Further, we show how rules for rely-guarantee reasoning can be derived and outline the application of some features to verify concurrent programs in practice. The logic is implemented in the interactive verification environment KIV.

We present TakaTuka, a tiny Java Virtual Machine (JVM) for wireless sensor motes. TakaTuka's preliminary version successfully runs on Crossbow's mica2 motes. Furthermore, TakaTuka also runs on Windows and Unix.