Skip to main content

Über dieses Buch

This volume constitutes the thoroughly refereed post-conference proceedings of the 10th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018, held in Oxford, UK, in July 2018.
The 19 full papers presented were carefully revised and selected from 24 submissions. The papers describe large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge as well as novel experiments and case studies evaluating verification techniques and technologies.



A Tree-Based Approach to Data Flow Proofs

In this paper, we investigate the theoretical foundation for the cost/precision trade-off of data flow graphs for verification. We show that one can use the theory of tree automata in order to characterize the loss of precision inherent in the abstraction of a program by a data flow graph. We also show that one can transfer a result of Oh et al. and characterize the power of the proof system of data flow proofs (through a restriction on the assertion language in Floyd-Hoare proofs).
Jochen Hoenicke, Alexander Nutz, Andreas Podelski

Executable Counterexamples in Software Model Checking

Counterexamples—execution traces of the system that illustrate how an error state can be reached from the initial state—are essential for understanding verification failures. They are one of the most salient features of Model Checkers, which distinguish them from Abstract Interpretation and other Static Analysis techniques by providing a user with information on how to debug their system and/or the specification. While in Hardware and Protocol verification, the counterexamples can be replayed in the system, in Software Model Checking (SMC) counterexamples take the form of a textual or semi-structured report. This is problematic since it complicates the debugging process by preventing developers from using existing processes and tools such as debuggers, fault localization, and fault minimization.
In this paper, we argue that for SMC the most useful form of a counterexample is an executable mock environment that can be linked with the code under analysis (CUA) to produce an executable that exhibits the fault witnessed by the counterexample. A mock environment is different from a unit test since it can interface with the CUA at the function level, potentially allowing it to bypass complex logic that interprets program inputs. This makes mock environments easier to construct than unit tests. In this paper, we describe the automatic environment generation process that we have developed in the SeaHorn verification framework. We identify key challenges for generating mock environments from SMC counterexamples of complex memory manipulating programs that use many external libraries and function calls. We validate our prototype on the verification benchmarks from Linux Device Drivers in SV-COMP. Finally, we discuss open challenges and suggests avenues for future work.
Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz

Extending VIAP to Handle Array Programs

In this paper, we extend our previously described fully automated program verification system called VIAP primarily for verifying the safety properties of programs with integer assignments to programs with arrays. VIAP is based on a recent translation of programs to first-order logic proposed by Lin [1] and directly calls the SMT solver Z3. It relies more on reasoning with recurrences instead of loop invariants. In this paper, we extend it to programs with arrays. Our extension is not restricted to single dimensional arrays but general and works for multidimensional and nested arrays as well. In the most recent SV-COMP 2018 competition, VIAP with array extension came in second in the ReachSafety-Arrays sub-category, behind VeriAbs.
Pritom Rajkhowa, Fangzhen Lin

Lattice-Based Refinement in Bounded Model Checking

In this paper we present an algorithm for bounded model-checking with SMT solvers of programs with library functions—either standard or user-defined. Typically, if the program correctness depends on the output of a library function, the model-checking process either treats this function as an uninterpreted function, or is required to use a theory under which the function in question is fully defined. The former approach leads to numerous spurious counter-examples, whereas the later faces the danger of the state-explosion problem, where the resulting formula is too large to be solved by means of modern SMT solvers.
We extend the approach of user-defined summaries and propose to represent the set of existing summaries for a given library function as a lattice of subsets of summaries, with the meet and join operations defined as intersection and union, respectively. The refinement process is then triggered by the lattice traversal, where in each node the SMT solver uses the subset of SMT summaries stored in this node to search for a satisfying assignment. The direction of the traversal is determined by the results of the concretisation of an abstract counterexample obtained at the current node. Our experimental results demonstrate that this approach allows to solve a number of instances that were previously unsolvable by the existing bounded model-checkers.
Karine Even-Mendoza, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina

Verified Certificate Checking for Counting Votes

We introduce a new framework for verifying electronic vote counting results that are based on the Single Transferable Vote scheme (STV). Our approach frames electronic vote counting as certified computation where each execution of the counting algorithm is accompanied by a certificate that witnesses the correctness of the output. These certificates are then checked for correctness independently of how they are produced. We advocate verification of the verifier rather than the software used to produce the result. We use the theorem prover HOL4 to formalise the STV vote counting scheme, and obtain a fully verified certificate checker. By connecting HOL4 to the verified CakeML compiler, we then extract an executable that is guaranteed to behave correctly with respect to the formal specification of the protocol down to machine level. We demonstrate that our verifier can check certificates of real-size elections efficiently. Our encoding is modular, so repeating the same process for another different STV scheme would require a minimal amount of additional work.
Milad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish

Program Verification in the Presence of I/O

Semantics, Verified Library Routines, and Verified Applications
Software verification tools that build machine-checked proofs of functional correctness usually focus on the algorithmic content of the code. Their proofs are not grounded in a formal semantic model of the environment that the program runs in, or the program’s interaction with that environment. As a result, several layers of translation and wrapper code must be trusted. In contrast, the CakeML project focuses on end-to-end verification to replace this trusted code with verified code in a cost-effective manner.
In this paper, we present infrastructure for developing and verifying impure functional programs with I/O and imperative file handling. Specifically, we extend CakeML with a low-level model of file I/O, and verify a high-level file I/O library in terms of the model. We use this library to develop and verify several Unix-style command-line utilities: cat, sort, grep, diff and patch. The workflow we present is built around the HOL4 theorem prover, and therefore all our results have machine-checked proofs.
Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho

TWAM: A Certifying Abstract Machine for Logic Programs

Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a typed compiler for an idealized logic programming language we call T-Prolog. The crux of our approach is a new certifying abstract machine which we call the Typed Warren Abstract Machine (TWAM). The TWAM has a dependent type system strong enough to show programs obey a semantics based on provability in first-order logic (FOL). We present a soundness metatheorem which (going beyond the guarantees provided by most typed compilers) constitutes a partial behavior correctness guarantee: well-typed TWAM programs are sound proof search procedures with respect to a FOL signature. We argue why this guarantee is a natural choice for significant classes of logic programs. This metatheorem justifies our design and implementation of a certifying compiler from T-Prolog to TWAM.
Brandon Bohrer, Karl Crary

A Java Bytecode Formalisation

This paper presents the first Coq formalisation of the full Java bytecode instruction set and its semantics. The set of instructions is organised in a hierarchy depending on how the instructions deal with the runtime structures of the Java Virtual Machine such as threads, stacks, heap etc. The hierarchical nature of Coq modules neatly reinforces this view and facilitates the understanding of the Java bytecode semantics. This approach makes it possible to both conduct verification of properties for programs and to prove metatheoretical results for the language. Based upon our formalisation experience, the deficiencies of the current informal bytecode language specification are discussed.
Patryk Czarnik, Jacek Chrząszcz, Aleksy Schubert

Formalising Executable Specifications of Low-Level Systems

Formal models of low-level applications rely often on the distinction between executable layer and underlying hardware abstraction. This is also the case for the model of Pip, a separation kernel formalised and verified in Coq using a shallow embedding. DEC is a deeply embedded imperative typed language with primitive recursion and specified in terms of small-step semantics, which we developed in Coq as a reified counterpart of the shallow embedding used for Pip. In this paper, we introduce DEC and its semantics, we present its interpreter based on the type soundness proof and extracted to Haskell, we introduce a Hoare logic to reason about DEC code, and we use this logic to verify properties of Pip as a case study, comparing the new proofs with those based on the shallow embedding. Notably DEC can import shallow specifications as external functions, thus allowing for reuse of the abstract hardware model (DEC can be found at https://​github.​com/​2xs/​dec.​git [1]).
Paolo Torrini, David Nowak, Narjes Jomaa, Mohamed Sami Cherif

A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars

Augmented Backus-Naur Form (ABNF) is a standardized formal grammar notation used in several Internet syntax specifications. This paper describes (i) a formalization of the syntax and semantics of the ABNF notation and (ii) a verified parser that turns ABNF grammar text into a formal representation usable in declarative specifications of correct parsing of ABNF-specified languages. This work has been developed in the ACL2 theorem prover.
Alessandro Coglio

Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing Between Black-Box Components

Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and required by law. It is therefore desirable to have formal methods that provide guarantees that certain privacy-relevant properties hold. We propose an approach that can be used to design a privacy-compliant architecture without needing to know the source code or internal structure of any individual component. We model an architecture as a set of agents or components that pass messages to each other. We present in this paper algorithms that take as input an architecture and a set of privacy constraints, and output an extension of the original architecture that satisfies the privacy constraints.
Robin Adams, Sibylle Schupp

SideTrail: Verifying Time-Balancing of Cryptosystems

Timing-based side-channel attacks are a serious security risk for modern cryptosystems. The time-balancing countermeasure used by several TLS implementations (e.g. s2n, GnuTLS) ensures that execution timing is negligibly influenced by secrets, and hence no attacker-observable timing behavior depends on secrets. These implementations can be difficult to validate, since time-balancing countermeasures depend on global properties across multiple executions. In this work we introduce the tool SideTrail, which we use to prove the correctness of time-balancing countermeasures in s2n, the open-source TLS implementation used across a range of products from AWS, including S3. SideTrail is used in s2n’s continuous integration process, and has detected three side-channel issues that the s2n team confirmed and repaired before the affected code was deployed to production systems.
Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCarthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran

Towards Verification of Ethereum Smart Contracts: A Formalization of Core of Solidity

Solidity is the most popular programming language for writing smart contracts on the Ethereum platform. Given that smart contracts often manage large amounts of valuable digital assets, considerable interest has arisen in formal verification of Solidity code. Designing verification tools requires good understanding of language semantics. Acquiring such an understanding in case of Solidity is difficult as the language lacks even an informal specification.
In this work, we evaluate the feasibility of formalization of Solidity and propose a formalization of a small subset of Solidity that contains its core data model and some unique features, such as function modifiers.
Jakub Zakrzewski

Relational Equivalence Proofs Between Imperative and MapReduce Algorithms

Distributed programming frameworks like MapReduce, Spark and Thrill, are widely used for the implementation of algorithms operating on large datasets. However, implementing in these frameworks is more demanding than coming up with sequential implementations. One way to achieve correctness of an optimized implementation is by deriving it from an existing imperative sequential algorithm description through a sequence of behavior-preserving transformations.
We present a novel approach for proving equivalence between imperative and deterministic MapReduce algorithms based on partitioning the equivalence proof into a sequence of equivalence proofs between intermediate programs with smaller differences. Our approach is based on the insight that proofs are best conducted using a combination of two kinds of steps: (1) uniform context-independent rewriting transformations; and (2) context-dependent flexible transformations that can be proved using relational reasoning with coupling invariants.
We demonstrate the feasibility of our approach by evaluating it on two prototypical algorithms commonly used as examples in MapReduce frameworks: k-means and PageRank. To carry out the proofs, we use a higher-order theorem prover with partial proof automation. The results show that our approach and its prototypical implementation enable equivalence proofs of non-trivial algorithms and could be automated to a large degree.
Bernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich, Alexander Weigl

Practical Methods for Reasoning About Java 8’s Functional Programming Features

We describe new capabilities added to the Java Modeling Language and the OpenJML deductive program verification tool to support functional programming features introduced in Java 8. We also report on the application of the extensions to a secure streaming protocol library developed by Amazon Web Services and used as a foundation by services it provides. We found that the application under study used a small set of functional programming idioms; methods using these idioms could be verified by techniques that used only first-order logic and did not need all the features that might be required for full generality of functional programming.
David R. Cok, Serdar Tasiran

Verification of Binarized Neural Networks via Inter-neuron Factoring

(Short Paper)
Binarized Neural Networks (BNN) have recently been proposed as an energy-efficient alternative to more traditional learning networks. Here we study the problem of formally verifying BNNs by reducing it to a corresponding hardware verification problem. The main step in this reduction is based on factoring computations among neurons within a hidden layer of the BNN in order to make the BNN verification problem more scalable in practice. The main contributions of this paper include results on the NP-hardness and hardness of PTAS approximability of this essential optimization and factoring step, and we design polynomial-time search heuristics for generating approximate factoring solutions. With these techniques we are able to scale the verification problem to moderately-sized BNNs for embedded devices with thousands of neurons and inputs.
Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang, Harald Ruess

The Map Equality Domain

We present a method that allows us to infer expressive invariants for programs that manipulate arrays and, more generally, data that are modeled using maps (including the program memory which is modeled as a map over integer locations). The invariants can express, for example, that memory cells have changed their contents only at locations that have not been previously allocated by another procedure. The motivation for the new method stems from the fact that, although state-of-the-art SMT solvers are starting to be able to check the validity of more and more complex invariants, there is not much work yet on their automatic inference. We present our method as a static analysis over an abstract domain that we introduce, the map equality domain. The main challenge in the design of the method lies in scalability; given the expressiveness of the invariants, it is a priori not clear that a corresponding static analysis can be made scalable. Preliminary experiments with a prototypical implementation of the method allow us to cautiously conclude that may indeed be the case.
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski

Loop Detection by Logically Constrained Term Rewriting

Logically constrained rewrite systems constitute a very general rewriting formalism that can capture simplification processes in various domains as well as computation in imperative programs. In both of these contexts, nontermination is a critical source of errors. We present new criteria to find loops in logically constrained rewrite systems which are implemented in the tool Ctrl. We illustrate the usefulness of these criteria in three example applications: to find loops in LLVM peephole optimizations, to detect looping executions of C programs, and to establish nontermination of integer transition systems.
Naoki Nishida, Sarah Winkler

Store Buffer Reduction in the Presence of Mixed-Size Accesses and Misalignment

Naïve programmers believe that a multi-threaded execution of their program is some simple interleaving of steps of individual threads. To increase performance, modern Intel and AMD processors make use of store buffers, which cause unexpected behaviors that can not be explained by the simple interleaving model.
Programs that in the simple interleaving model obey one of various programming disciplines do not suffer from these unexpected behaviors in the presence of store buffers. These disciplines require that the program does not make use of several concrete features of modern processors, such as mixed-size/misaligned memory accesses and inter-processor interrupts. A common assumption is that this requirement is posed only to make the formal description and soundness proof of these disciplines tractable, but that the disciplines can be extended to programs that make use of these features with a lot of elbow grease and straightforward refinements of the programming discipline.
In this paper we discuss several of such features where that assumption is correct and two such features where it is not, namely mixed-size/misaligned accesses and inter-processor interrupts. We base our discussion on two programming disciplines from the literature. We present solutions and discuss some context, including a claim in the C11 standard that contradicts our findings.
Our work is based directly on the roughly 500 page PhD thesis of the author, which includes a formal treatment of the extensions and a detailed soundness proof.
Jonas Oberhauser


Weitere Informationen

Premium Partner