Software Security, Autumn 2020

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

Doing it is obligatory and required to pass the course. You can do them individually or in pars.

There will be the opportunity to get help doing this assignment in a special lab session slot; time and place will be discussed in class. 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

Hand your solutions (ie. the annotated Java files) in via Brightspace (for the 6 EC NWI-ISOFSE course). Irregardless of whether you do it individually or as a pair, you have to join one of the "pair or individual assignments" groups in Brightspace and hand is it as this Brightspace group. 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: Upload your solutions as the annotated files, named BagYourName.java and AmountYourName.java, where YourName is your full name(s), and ALSO put your names IN the Java files , as comments in the code. Do not zip or tar these documents, to save us a lot of hassle 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 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. The technology behind this tool is similar to that of the VCC tool used for the verification of the Hyper-V hypervisor at Microsoft.

Running ESC/Java2

• central Linux servers (lilo.science.ru.nl and stitch.science.ru.nl) NB THE EASIEST OPTION, if you're not scared by the Linux command line

  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

  You can SSH to lilo.science.ru.nl or stitch.science.ru.nl and run the tool there. For this you need your faculty (Science) login, which - unfortunately - is different from your Brightspace login. All students have a science login, even if you do not know it: check with the Student Help Desk.

  For the Linux-challenged: you can SSH to the Linux servers from any Windows PC above using putty (download here) or bitvise ssh client (aka tunnelier) (download here). Tunnelier is more convenient, as it also provides the possibility to copy files over between the machines (using sftp). There are two ways to then do the assignment:

  1. Open two SSH terminal windows on lilo3 (or stitch), one to run ESC/Java2 from the command-line as explained above, and one to edit the files Amount.java and Bag.java, using a simple comand-line editor like pico.
  2. Simply edit the files on your local machine, and then copy them over to lilo3 with sftp using tunnelier, and open one SSH terminal window on lilo3 to run ESC/Java2 on the file, as explained above.

• Linux PCs in terminal rooms in Huygens building.

  Start up in Ubuntu Linux, and follow instructions as above.

• Windows PCs in terminal rooms in Huygens building.

  On any of the Windows machines in the computer rooms in the Huygens building, ESC/Java2 is installed in T:\softwaresecurity. To run the tool on some file A.java, open a command window by selecting

     Start -> (All) 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 it on your own Windows machine

  Download and unpack ESC.zip. You will have to edit escj.bat, replacing T:\softwaresecurity\ESC by the full path of the unpacked ESC directory from the zip file. The last line of escj.bat should execute

     "ESC_DIR\j2sdk1.4.2_12\bin\Java.exe" -Dsimplify="ESC\Simplify-1.5.4.exe"
     -classpath "ESC_DIR\esctools2.jar" escjava.Main -classpath
     "ESC_DIR\jmlspecs.jar" -classpath . %ESCJ_STDARGS% %ESCJ_ARGS%

  where ESC_DIR is the directory into which you unpacked the zip.
  Alternatively, you can try this improved batch file which automatically looks for a correct Java version.

The assignment

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,

• 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. 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.

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 key step in these exercise, as is the case in most verification, is to discover and specify the relevant object invariant. (For the verification of the seL4 microkernel, it was estimated that as much as 80% of the proof effort goes into the verification of invariants about data structures.)

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. If you get a long and confusing error message about invariants from ESC/Java2 this is typically a sign that a method may break an invariant of another object (ie. not "this"), eg. an object that is passed in as a parameter or an object that is newly constructed in the method.

Reflection

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
   • 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?