This is a follow-up post to the blog about the verification of TimSort. Many people have asked how KeY actually works and which resources are available. In this brief post we answer some of the questions about KeY that came up in the discussions. We also provide pointers to documentation, case studies and technical papers.
The KeY project was started in the late 1990s at University of Karlsruhe (now: Karlsruhe Institute of Technology) with the aim to develop a tool for formal specification and verification of Java that would be useful not only to the formal methods specialist, but for ordinary software developers as well. This was an ambitious and long-term goal. After more than 15 years of research and tool development, it has been partially reached, as we explain below. For example, KeY not only includes a formal verification tool, but also a debugger with novel features and an automated test case generator. In the meantime, KeY is developed and maintained at three sites. In addition to Karlsruhe, these are Technische Universität Darmstadt and Chalmers University of Technology.
The core of KeY is a software verification tool based on symbolic execution and invariant reasoning.
Symbolic Execution
To execute a program symbolically means to interpret it with unknown, non-initialized start values or parameters. Look at the code snippet below:
// int x, y, z;
x = y - x;
y = y - x;
x = x + y;
z = x / y
Its effect is to swap the values of x and y without allocating a temporary variable and then to assign the result of dividing x by y to z. Assume for simplicity that x and y are mathematical integers without overflow. After the variable declaration, x and y are initialized with unknown integer values, say x0 and y0, respectively. Symbolic execution of the first assignment updates the value of x to y0–x0. When executing the second assignment, this is the value that x has on the right hand side. Therefore, the new value of y is: y0–(y0–x0) = x0, and so on.
When computing the last statement z = x/y, an ArithmeticException might be thrown depending on whether the initial value x0 of x (and current value of y) was zero or not. As no further information is available, symbolic execution has to consider both possibilities and thus splits the execution. Consequently, the result of symbolic execution typically is a tree such as this one:
One great feature of symbolic execution is that it can start at any code location and that no fixture or initial state is necessary. The main drawback is that symbolic execution splits quite a lot, at least at every explicit case distinction, but also, for example, at each object access of the form o.n, because the behavior of that code differs, depending on whether o is null or not.
Loop Invariants
Symbolic execution hits a problem when it encounters a loop such this one:
for (int i = 0; i < a.length; i++) { a[i] = i }
If a is an arbitrary array (for sake of presentation assume a!=null), then we don’t know the value of a.length. We can unwind the loop body one or more times, but it is not clear when to stop. KeY uses loop invariants to deal with this situation. A loop invariant is a property that holds (i) when the loop is encountered and (ii) is preserved by any execution of the loop guard and body. In the example above, a typical loop invariant in the Java Modeling Language [JML] notation) might be:
loop_invariant (i >= 0 && i <= a.length && (\forall int j; 0<= j && j < i; a[j] = j ))
It gives the bounds of the loop counter and tells that the array has been partially initialized up to the current value of the loop counter. Since at the exit of the loop we know i==a.length, we can deduce that after the loop finishes, the array is fully initialized. This fact can then be used during the analysis of any remaining code that comes after the loop. In simple cases (such as the one above), loop invariants can be derived automatically, but in general the designer must supply a suitable invariant. Our analysis of the TimSort bug showed that it is easy to make subtle errors when writing loop invariants. This is why a verification system such as KeY is useful to confirm (or refute!) one’s intuition.
Design-by-Contract
To render symbolic execution feasible, it has to be broken down into manageable pieces that are analyzed separately. In Java the most natural granule of analysis is that of a method.
In KeY we follow a specification methodology called design-by-contract (originally suggested by Bertrand Meyer for runtime assertion checking of Eiffel programs). The precise effect of each method is captured in a contract written in JML. Expressions of JML are written in structured Java comments, next to the declaration they relate to. For instance, a contract for the method binarySearch(int[], int) of class Arrays can be written as follows:
/*@ public normal_behaviour @ requires @ (\forall int x; (\forall int y; @ 0 <= x && x < y && y < a.length; a[x] <= a[y])); @ ensures @ ((\exists int x; 0 <= x && x < a.length; a[x] == v) ? @ a[\result] == v : \result ==-1); @*/ static /*@ pure @*/ int binarySearch(int[] a, int v) { … }
Method binarySearch(int[], int) implements a simple binary search for arrays. The keyword normal_behaviour requires the method to terminate normally (i.e., without throwing an uncaught top level exception) if the caller of the method guarantees that at invocation time the method’s precondition (boolean JML expression after requires) is satisfied. Here the precondition states that array a is sorted in ascending order. In this case the method contract ensures that the result of the method is -1 if a does not contain element v or otherwise the index of element v in a. The specification modifier /*@ pure @*/ states that the method is not allowed to change the heap.
Formal Verification
JML annotations, Java programs, and the rules of symbolic execution are all translated automatically to formulas and rules of the program logic that is used by KeY. It is not necessary to understand the details of this. Suffice it to say, when loading a class, annotated with JML contracts, into KeY, a proof obligation formula is generated and loaded into its theorem prover. Then the user selects a method and its contract and attempts to show its validity.
If the theorem prover can show the validity of the proof obligation formula relating to a given contract and method, then we know the following is true: if the method is started in any Java state that satisfies the requires clause, then upon termination, the final state satisfies the ensures clause.
KeY’s theorem prover provides a high degree of automation, but allows also interactions by the user in case a proof cannot be found automatically. Most often, interactions with the prover consist in providing additional annotations such as invariants.
If no proof is found, then the failed proof needs to be analysed as to whether the specification is too weak or wrong, the program is buggy or the automation is not powerful enough and further interaction by the user is required.
Understanding failed proofs is thus crucial for identifying a problem. To help this process, KeY provides several options to inspect a proof object:
- in the KeY theorem prover itself (this requires an understanding of KeY’s program logic)
- in the symbolic execution debugger (SED) which renders a KeY proof situation inside the Eclipse debugger. This is a view which is familiar to most (Java) developers and easier accessible than using the theorem prover directly.
- through counter example generation, which (if successful) provides concrete input values that lead to a violation of the property whose prove attempt failed.
Beyond Formal Verification
KeY is not merely a deductive verification tool only usable by specialists in formal methods, but it has developed into a versatile tool for static analysis of programs. Current research covers these areas
- generate test cases automatically that are guaranteed to satisfy certain coverage criteria
- generate counter examples to understand failed proofs
- symbolic state debugging going beyond omniscient debuggers and requiring no fixtures
- information flow analysis and leak detection/exploit generation
- automatic specification generation
In the context of the Envisage Project we develop a variant of KeY which is able to verify that an ABS program satisfies its specification. ABS is an executable specification/modelling language for distributed and concurrent systems which has been designed to be formally analysable using a variety of methods. A number of backends exists to generate executable Java/Haskell/Erlang/Maude code from a given ABS model. In particular, we are interested to verify that a given model satisfies certain properties stated as part of a service level agreement.
Resources
- There is a recent overview paper on KeY at http://link.springer.com/chapter/10.1007%2F978-3-319-12154-3_4 (Free preprint: http://wwwhome.ewi.utwente.nl/~mostowskiwi/papers/key2014.pdf)
- The KeY Quicktour provides a first introduction into KeY along a small example. PDF docs and all source files are available at http://www.key-project.org/download/quicktour/quicktour-2.0.zip
- The Symbolic Execution Debugger is an Eclipse-plugin that works like a debugger and one needs no prior knowledge about formal methods to use it. A tutorial and download link is at http://www.key-project.org/eclipse/SED/index.html
- The most extensive documentation on KeY is the KeY Book (see http://link.springer.com/book/10.1007%2F978-3-540-69061-0; accessible for free from many university networks), but it is a bit outdated. We are in the final stages of writing the 2nd edition which is due this summer.
FAQ
We are grateful for further questions to make this FAQ more complete/useful!
Do you support integer overflow?
Yes. KeY supports three kinds of semantics for integer operations occurring in programs (including Java’s), which can be selected in KeY via (Options > Taclet Options > integerSemantics):
- Ignoring overflow (default): This option treats integers in programs as mathematical integers, i.e., without overflow. It is for instance used for teaching purposes to simplify writing specifications. This option is neither sound nor complete.
- Java semantics: This option models the Java semantics faithfully using modulo arithmetic. This option is sound and complete.
- Checking overflow: Using this semantics one has to prove that an arithmetic operation does not overflow (or that an overflow is irrelevant for the property to be proven). This option is sound, but not complete, i.e., programs relying on an overflow to happen won’t be provable.
What are the Java language features you support?
We currently support sequential Java without multi-threading, garbage collection and floating point operations (initial support for floating points is currently implemented). When activating the JavaCard mode in KeY, all JavaCard features are supported, including atomic transactions. At the moment KeY does not support generics, a tool removing generics is available on request. In the future, the generics removal is planned to be transparent from the user.
Best regards,
Reiner Hähnle and Richard Bubel with help from Stijn de Gouw
Acknowledgements:
Partly funded by the EU project FP7-610582 ENVISAGE: Engineering Virtualized Services (http://www.envisage-project.eu).
This blog would never have gotten written without the enthusiastic support and gentle pushing of Amund Tveit!
One thought on “KeY: Deductive Verification of Software”