ESC/Java2 assignment

Software Security, Spring 2011

Exercise 3: Program verification with ESC/Java2

Purpose of this exercise is to get a taste of how formal program verification can be used to certify properties of code. We use the program verification tool ESC/Java2 to verify (and debug) some pieces of Java code.

It is an individual exercise. It won't be marked, but doing it is obligatory and required to pass the course.

There will be the opportunity to get help doing this assignment on May 27 in HG00.023, 10:30-12:30 and 13:30-15:30. Fabian van den Broek and Wojciech Mostowksi will be there to help. For non-Nijmegen students we will provide user accounts.

NB have a look at the Java code samples and a first stab at the exercise before showing up here, so that you can make the most of the available help. It should then not be a problem to finish the exercise well within 2 hours.

Handing in the assignment

Easiest way is simply to show Fabian or Wojciech that you have completed the exercises at the end of the practicum session.

Otherwise, email your solutions (ie. the annotated Java files) to Fabian van den Broek (f.vandenbroek at cs.ru.nl) with subject [SS] ESC by June 3. NB Provide the annotated files in two attachements, named BagYourName.java and AmountYourName.java, where YourName is your full name, and also put your name in the Java file. Please don't zip or tar these attachments, to save us a lot of unzipping and untarring.

Background: The program verification tool ESC/Java2

ESC/Java2 is an automated program verification tool (aka extended static checker) for Java programs. It implements a Hoare logic for reasoning over Java programs that have been annotated with JML specifications. These specifications express for instance preconditions, postconditions, and invariants, and can be added as assertions to the program code. Essentially, ESC/Java2 computes weakest preconditions of methods, and then sends the resulting proof obligiations to the automated theorem prover Simplify. The user never get to see these proof obligations or the back-end theorem prover; instead, the tool gives feedback over which assertions it could not prove.

Running ESC/Java2

ESC/Java2 is available on the central Linux machines and on the Windows PCs in the terminal rooms. You can also download it on your own machine. Instructions for this:

central Linux servers (lilo.science.ru.nl and stitch.science.ru.nl)
ESC/Java2 is installed in /vol/practica/softwaresecurity. To run the tool on some file A.java, give the command
/vol/practica/softwaresecurity/ESCJava/escjava2 A.java
Windows PCs in terminal rooms
ESC/Java2 is installed in T:\softwaresecurity. To run the tool on some file A.java, open a command window by selecting
Start -> Programs -> Accessories -> Command Prompt
then go to the directory where A.java is (using cd) and type in the command
T:\softwaresecurity\ESC\escj.bat A.java
Installing on your own machine
If you prefer running the tool on your own computer, ESC/Java2 can be downloaded here. (Don't be scared to give your email address; we won't use it to spam you.) Just get binary of the latest release. The tool runs on just about any platform: Windows, Mac, Linux and UNIX, and comes with lots of documentation. I always use it from the command line, but there is also a simple Swing GUI front-end.
If you're using Windows, you will have to edit escj.bat to provide the correct path names: the last line of escj.bat should be
"C:\j2sdk1.4.2_12\bin\Java.exe" -Dsimplify="C:\ESCJava 2\Simplify-1.5.4.exe" -classpath "C:\ESCJava 2\esctools2.jar" escjava.Main -classpath "C:\ESCJava 2\jmlspecs.jar" -classpath . %ESCJ_STDARGS% %ESCJ_ARGS%
if you installed ESC/Java2 in "C:\ESCJava 2" and Java in "C:\j2sdk1.4.2_12"
If you're using Linux or MacOS, use the script escjava2 to run the tool.
As cool Eclipse plugin: You can also try to install ESC/Java2 as Eclipse plug-in.

The assignment

For the assignment, you should specify the two classes

with JML and run ESC/Java2 to verify these specifications. Simply put, you have to run ESC/Java2 on these files, and, if the tool produces some warning,

either add annotation to the code (eg to document invariants, preconditions, or postconditions)
or fix bugs in the code

to make the warning go away. You have to use your own best judgement to choose between these two options, but there are some deliberate bugs in the code for you to detect, with the help of the tool.

For Amount.java you must also try to formalise the informal invariant that is discussed in the file in JML, which should reveal some problems in the code.

In the end, ESC/Java2 should run without any complaints on the annotated code. ESC/Java2 complains (among other things) if it thinks a runtime exception may occur, say a NullPointerException, so if ESC/Java2 runs without complaints this means it has verified that no runtime exceptions can occur.

More detailed instructions are given in the Java files. Read these!

The only JML keywords you'll need to use for this are requires, invariant, and ensures. If you want, you can also use non_null as an abbreviation and experiment with other features.

The ESC/Java2 tool has many command line options. The most useful ones are

escjava2 -suggest
For every warning the tool then tries to suggest an annotation that will suppress the warning.
escjava2 -routine
The tool then checks just the named routine; e.g. escjava2 -routine arraycopy Bag.java only checks method arraycopy in Bag.java

Some hints to keep you out of trouble with the tool:

Only look at the first warning that ESC/Java2 produces, and ignore the others, until you've managed to get rid of this first one.
The only JML keywords you'll need are requires, invariant, and ensures. If you want, you can also use non_null as an abbreviation and experiment with other features.
Don't use the Java shorthand x+=10 for x = x+10.
Whenever possible, split invariants than contain conjunctions into several smaller invariants. The tool then provides better feedback. So instead of
   //@ invariant A && B;
write
   //@ invariant A;
   //@ invariant B;
The same goes for preconditions (aka requires clauses).
If the tool complains of invariant violations, it produces a lot of information that is hard to interpret. The crucial information to look at is
- the line number saying which invariant is violated, and
- the line number saying where this invariant is violated.
NB beware that calling a method on some object may break the invariant of another object. For instance, in the taxpayer exercise, calling a method on a TaxPayer may break the invariant of his or her spouse.

Reflection

Some questions to consider

In the end, do you think that you found all problems? Are you certain now that the code is correct?
Can you think of ways in which the tool or the specification language could be improved?
Instead of the tool we used, can you think of other ways (formal or informal, tool-supported or not) to find the problems that the tool found? If so, would these alternatives
- find fewer of the problems, the same, or more?
- find problems sooner or later than the current approach?
- require more work or less work?
- provide you with more confidence or less confidence that the code is correct?