ESC/Java2 assignment

Software Security, Autumn 2018

Exercise 3: Java Program verification with ESC/Java2 (or OpenJML)

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 will be marked (with ok/pass/not ok scores), and doing it is obligatory and required to pass the course.

There will be the opportunity to get help doing this assignment in a special lab session slot; time and place will be announced by email and Blackboard.

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 in a couple of hours.

Handing in the assignment

Email your solutions (ie. the annotated Java files) to erikpoll at cs.ru.nl with subject JML. Please mark any lines in the code that you have changed, with a comment like // CHANGED . Restrict changes in the code to the minimum that is required to correct things.

NB follow these instructions for handing in to the letter: Provide the annotated files in two attachments, named BagYourName.java and AmountYourName.java, where YourName is your full name, and also put your name in the Java files. Don't zip or tar these attachments, to save us a lot of hassle unzipping and untarring. Anything handed it that does not comply with these instructions won't be marked.

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 an automated theorem prover. 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

You can use ESC/Java2 remotely on the central Linux servers, or on PCs in the terminal rooms, either under Windows or Linux. You can also download it on your own machine, but if you run into hassle with installing, using one of the options above is probably easier. Instructions for this:

The assignment

Below a precise description of what you should do:
You should specify the two classes
  1. Bag.java
  2. Amount.java
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, to make the warning go away. You have to use your own best judgement to choose between these two options. There are some deliberate bugs in the code for you to detect, with the help of the tool. Don't change the code when there is no real bug in it.

For Amount.java you must also formally specify the invariants that are discussed in the file in JML, which will reveal some additional 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

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

Reflection

Some questions to consider. (You don't have to hand this in! But I might ask for an intelligent response to these questions at the exam.)
  1. In the end, do you think that you found all problems? Are you certain now that the code is correct?
  2. Can you think of ways in which the tool or the specification language could be improved?
  3. 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