PtYasm

PtYasm is an enhanced version of the Yasm software model checker which uses proof templates to prove the safety of array bounds checks. PtYasm has been evaluated on testcases derived from the Verisec suite; the complete evaluation materials are located here.

Download

PtYasm requires Java, OCaml, CIL, Apache Ant, ANLTR, and CVCL. PtYasm has only been tested on Linux, but should run on any platform for which these programs are available. Note that you must have a source distribution of CIL, since PtYasm's loop scanner is a CIL extension.

Download the PtYasm tarball, and install the supporting programs on your system.

• PtYasm tarball
• Supporting programs:
  • CVCL
  • CIL
  • Java
  • OCaml
  • Apache Ant
  • ANTLR

Installation Instructions

1. Ensure that all supporting programs are installed.
2. Download and extract the PtYasm tarball.
3. Download CVCL and make it executable using chmod u+x.
4. In the top-level directory of the extracted PtYasm tarball, edit bin/custom_env.sh to set up PtYasm's environment variables: JAVA_HOME, ANTLR_HOME, CILHOME, and CVCL_BINARY.
5. In the top-level directory of the extracted tarball, type "source ./bin/custom_env.sh `pwd`". This will set up the environment variables PtYasm needs.
6. Build CIL with the loop scanner extension. (See CIL documentation on building CIL with extensions.) Short form:
   • $ cd $CILHOME
   • $ ./configure EXTRASRCDIRS=${ROOT}/ocamlsrc EXTRAFEATURES=scanloops
   • $ make
7. Return to the top-level directory of PtYasm, and build Yasm by typing "ant -f build.xml". You should now have a working copy of PtYasm.

Running PtYasm

PtYasm has two components: the loop scanner, and Yasm. These can be run independently, or together using the ptyasm script.

To invoke the loop scanner on its own on a file called foo.c which contains exactly one assertion, type:
     $ cilly --doscanloops --save-temps --noPrintLn --dosimpleMem --domakeCFG --printCilAsIs --out=foo.cil foo.c
The loop scanner will thus produce files foo.cil and foo.abs. foo.cil is an instrumented version of foo.c, which has had its syntax lowered, and foo.abs stores the proof templates which the loop scanner suggests that Yasm use.

Now that we have foo.cil and foo.abs, we can verify an assertion. Run the script yasmpp.pl, which preprocesses foo.cil, and produces foo.ypp. To verify the safety of the assertion, Yasm attempts to verify that the line labelled ERROR is unreachable. You can invoke Yasm as:
     $ yasr -p 'EF pc = ERROR' foo.ypp --prooftemplates "foo.abs" --refiner "local-cbj-vs-i-s" --blocking
This tells Yasm to verify that ERROR is unreachable, using proof templates found in foo.abs if necessary. The last two options are optimizations, which we strongly recommend using: --refiner tells Yasm to compute transition relations coarsely, refining them when necessary, and --blocking tells Yasm to abstract basic blocks rather than individual statements.

We include a script, ptyasm, which runs all of the above steps on a single file. We also include a set of four example programs in ${ROOT}/examples. You can run them using the ptyasm script; example:
     $ ptyasm gd.c
The examples have all been tested and confirmed to run to completion using PtYasm.

Troubleshooting

• On some Linux systems, such as Ubuntu, you need both the ant ant ant-optional packages.
• If PtYasm crashes with an error message saying that it cannot allocate memory, edit bin/yasr, and reduce the values of the variables MEMORY_MIN and MEMORY_MAX.
• Due to a bug in the way Yasm treats non-deterministic assignment, if you traverse a string using a variable i, you must write the string's null terminator before initializing i.