Deductive Software Verification – The KeY Book

This chapter presents syntax, a calculus, and semantics of first-order logic. This is done first for a basic, typed first-order logic, and then for a richer logic tailored to the verification of Java programs.

In this chapter, we introduce an instance of dynamic logic, called JavaDL, that allows us to reason about Java programs. Dynamic logic extends first-order logic and makes it possible to consider several program states in a single formula. Its principle is the formulation of assertions about program behavior by integrating programs and formulas within a single language. We present a sequent calculus for JavaDL, which is used in the KeY System for verifying Java programs. Deduction in this calculus is based on symbolic program execution and simple program transformations and is, thus, close to a programmer's understanding of Java. Besides rules for symbolic execution, the calculus contains rules for program abstraction and modularization, including invariant rules for reasoning about loops and rules that replace a method invocation by the method's contract.

This chapter covers the formalism of taclets by which inference rules can be formulated for the JavaDL sequent calculus employed in KeY. After an introductory tutorial, the syntax and semantics of the taclet language are described. Finally, techniques are presented to mechanically prove taclet soundness by deriving formulas from taclets whose validity entails the soundness.

For a program verification tool to be useful it needs to be able to reason about at least the most important data types, both abstract data types, as well as those built into the programming language. This chapter presents how the theories of some data structures are realized in KeY's logic: finite sequences, Java strings, and Java integer data types.

In this chapter, we present a framework to integrate abstract interpretation into JavaDL. Our abstraction does not act directly on target programs, but on their symbolic state representation (JavaDL's updates). Unlike counter example guided abstraction-refinement (CEGAR) loops, we start with a fully precise representation and use abstraction only incrementally on demand, for example, to enforce termination of symbolic execution of a loop. Incremental means two things: use abstractions that are not coarser than necessary and apply abstraction to as few program locations as possible. This allows us to become fully-automatic, as for instance, no loop invariants need to be provided, but to maintain high precision.

This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It appears in a book about the KeY approach and tool for the verification of Java software, because JML is the dominating starting point of KeY style Java verification. However, this chapter does not depend on any specific tool nor verification methodology in any way. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular.

The calculus of the KeY prover operates on the logic JavaDL while Java programs are specified using the Java Modeling Language (JML). This chapter builds a formal bridge between the two logical languages by providing a denotational formal semantics for JML, translating expressions and contracts to formulas in JavaDL. Proof obligations which entail the correctness of contracts are defined for functional and dependency contracts. The issue of well-definedness of JML contracts is discussed and a formulation of a proof condition is presented.

In this chapter, concepts already addressed in previous chapters are reconsidered and extended to cater for modularity. In particular, it is shown how method contracts can be used in proofs (as opposed to being verified themselves). Another central topic is nonfunctional framing information, i.e., information on what locations a method may write to or read from. But, there are also items that are discussed here in depth for the first time: model methods, an abstraction of Java methods that are only used in specification, verification of recursive methods, and object invariants. For any of the arising proof obligations the calculus rules needed to dispatch them are shown.

This chapter presents the extension of KeY and JavaDL to handle a particular and peculiar dialect of Java, namely Java Card, for programming smart cards. The necessary extensions to the logic and the specification language are discussed, followed by a number of small case studies. The chapter is concluded with applications of the ideas presented here to on-going and future research, in particular in reasoning about concurrent Java programs.

This chapter presents the usage and different use cases of the Symbolic Execution Debugger (SED), an interactive debugger based on symbolic execution. In addition, the extendable architecture of the SED and the underlying symbolic execution engine based on KeY are discussed.

KeYTestGen is a white-box test generator for Java methods based on KeY's program analysis and symbolic execution. KeYTestGen generates a JUnit test harness (test driver) which does not only initialize method parameters but also the global state that is defined by the (potentially private) fields of objects and classes. For example, a complex linked data structure may be created as test input. The tests can satisfy different test criteria such as branch coverage, path coverage, and MC/DC coverage. The user may also provide a specification in the Java Modeling Language (JML) from which a test oracle can be generated or which can be used as an abstraction for a loop or method call. KeYTestGen can be used either as a simple stand-alone tool not requiring expert knowledge or it can be used in an advanced way to support and complement formal verification.

Information flow analysis detects and controls how sensitive information is propagated through an application. We give a formal model of what it means for sensitive information to be revealed, as well as an extension of JML that allows for the specification of information flow concerns. We present an approach by which we can verify these JML contracts using KeY. It is based on two symbolic executions of the program.

This chapter consists of two parts: The first describes how to interleave symbolic execution with partial evaluation to render the representation of proof trees more compact. Besides saving proof effort, it helps a human user to navigate and comprehend a given proof situation better. The second part is about verifiably correct compilation. Instead of verifying a compiler, we use the verification engine of KeY to prove for a given program on the fly that it is correctly compiled through a sound program transformation. Program behavior of the source code is provably preserved at the level of the target language: source and compiled program terminate in states in which the values of a user-specified region of the heap are equivalent. We give a proof-of-concept of the approach in realizing a partial evaluator, i.e., a source-to-source compiler.

This chapter is a self-contained introduction into the usage of the KeY prover, a tool for proving formulas of a program logic called Java Dynamic Logic. It does not assume the reader to have read any other chapter of the book in advance. Here, we discuss the usage of the KeY prover in isolation. For a tutorial on the most common context of the prover, i.e., the KeY verification process, we refer to the chapter `Formal Verification with KeY: A Tutorial'. The present chapter takes entirely the user's perspective on the KeY prover, and the GUI plays an important role. However, we do not only introduce the various ways of using, and interacting with, the KeY prover. Rather, the various visible artifacts the prover acts on, in particular the logic and the taclet language, are introduced on the side, on demand, and example driven, in a light-weight manner. This chapter is meant to be read with the KeY system up and running, such that every step can be tried out immediately in the system. The concepts that will be introduced along with the usage of the prover include KeY problem files, propositional, first-order, and dynamic logic, sequent calculus, proof construction, proof navigation and manipulation, taclets, interactive and automated proving, quantifier instantiation, and symbolic execution. Most of these topics are discussed in much greater detail in other chapters within this book, but appear here in the context of using the KeY prover.

This chapter gives a systematic tutorial introduction on how to perform formal program verification with the KeY system. It illustrates a number of complications and pitfalls, notably programs with loops, and shows how to deal with them. After working through this tutorial, you should be able to formally verify with KeY the correctness of simple Java programs, such as standard sorting algorithms, gcd, etc.

This chapter targets the teaching of formal methods to Bachelor students who come into contact with formal methods for the first time. We introduce a program logic and a tool based on KeY that has been designed specifically for teaching purposes. We designed a calculus to realize a forward symbolic execution style of reasoning in the same spirit as the JavaDL calculus, but we stay close to the formalism used in a Hoare-style calculus, such that students are not inhibited from using standard text books.

With this tool students can now easily check intermediate steps in their solution, e.g., if they work with a correct loop invariant. Instructors can easily establish the correctness of electronically submitted assignments.

Electronic voting (e-voting) systems that are used in public elections need to fulfill a broad range of strong requirements concerning both safety and security. Among those requirements are reliability, robustness, privacy of votes, coercion resistance, and universal verifiability. Bugs in or manipulations of an e-voting system can have considerable influence on society. Therefore, e-voting systems are an obvious target for software verification. This case study proves the preservation of privacy of votes for a basic electronic voting system. Altogether the considered code comprises eight classes and thirteen methods in about 150 lines of code of a rich fragment of Java.

We discuss a mechanized correctness proof in KeY of Counting sort and Radix sort. Counting sort is an unusual sorting algorithm in the sense that it is based on arithmetic rather than comparisons. Radix sort is tailored to sorting arrays of large numbers. It uses an auxiliary sorting algorithm, such as Counting sort, to sort the digits of the large numbers one-by-one. The correctness of Radix sort requires the stability of the auxiliary sorting algorithm. Stability here means that the order between different occurrences of the same number is preserved. The correctness proof of Counting sort includes a proof of its stability.