KTH Demo: Proof Generation

Overview

Online Demo
Load Java-source files
Compile class files
Inline class files
Preverify class files
Generate proof
Package into .jad/.jar
Verify policy adherence

Offline Demo
Download executable

Demo Videos
Developers Perspective
Users Perspective (fail)
Users Perspective (success)

This step performs the inlining of the compiled class files.

It is not required that this step is performed by our reference implementation of the inliner. As long as the resulting program does not violate the policy (and the security invariant holds before / after each method) the proof generation should not have any problem when generating a proof.

The policy used is the "don't send after read"-policy displayed below.

Policy:

SCOPE Session
SECURITY STATE boolean haveRead = false;
BEFORE javax.microedition.rms.RecordStore.openRecordStore(java.lang.String name, boolean createIfNecessary)
PERFORM
true -> {haveRead = true;}

BEFORE javax.microedition.io.Connector.openDataOutputStream(java.lang.String url)
PERFORM
haveRead == false -> {haveRead = true;}

View / download the policy here.

Tool output:

COPYING CLASS FILES INTO INLINER WORKING DIR...
    Copying s3mstest/wormgame/WormLink.class to inliner/classfiles
    Copying s3mstest/wormgame/Worm.class to inliner/classfiles
    Copying s3mstest/wormgame/ScoreSender.class to inliner/classfiles
    Copying s3mstest/wormgame/WormPit.class to inliner/classfiles
    Copying s3mstest/wormgame/WormScore.class to inliner/classfiles
    Copying s3mstest/wormgame/WormMain.class to inliner/classfiles
    Copying s3mstest/wormgame/WormFood.class to inliner/classfiles
    Copying s3mstest/wormgame/WormException.class to inliner/classfiles
DONE
EXECUTING: /usr/lib/jvm/java-1.5.0-sun/bin/java -classpath .: wtk2.5.1/lib/cldcapi10.jar: wtk2.5.1/lib/cldcapi11.jar: wtk2.5.1/lib/j2me-ws.jar: wtk2.5.1/lib/j2me-xmlrpc.jar: wtk2.5.1/lib/jsr082.jar: wtk2.5.1/lib/jsr179.jar: wtk2.5.1/lib/jsr180.jar: wtk2.5.1/lib/jsr184.jar: wtk2.5.1/lib/jsr211.jar: wtk2.5.1/lib/jsr226.jar: wtk2.5.1/lib/jsr229.jar: wtk2.5.1/lib/jsr234.jar: wtk2.5.1/lib/jsr238.jar: wtk2.5.1/lib/jsr239.jar: wtk2.5.1/lib/jsr75.jar: wtk2.5.1/lib/midpapi10.jar: wtk2.5.1/lib/midpapi20.jar: wtk2.5.1/lib/midpapi21.jar: wtk2.5.1/lib/mmapi.jar: wtk2.5.1/lib/satsa-apdu.jar: wtk2.5.1/lib/satsa-crypto.jar: wtk2.5.1/lib/satsa-jcrmi.jar: wtk2.5.1/lib/satsa-pki.jar: wtk2.5.1/lib/wma11.jar: wtk2.5.1/lib/wma20.jar Main -verbose policy.txt classfiles/s3mstest/wormgame/ScoreSender.class classfiles/s3mstest/wormgame/WormScore.class
EXECUTION WD: inliner
Inlining s3mstest/wormgame/ScoreSender
  Visiting (Ljavax/microedition/midlet/MIDlet;I)V
    Found invokespecial java/lang/Thread.()V
  Visiting run()V
    Found invokespecial java/lang/StringBuffer.()V
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(I)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.toString()L java/lang/String;
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/String;)V
    Found invokestatic javax/microedition/io/Connector.openDataOutputStream(Ljava/lang/String;)L java/io/DataOutputStream;
      Inserting javax/microedition/io/Connector.openDataOutputStream(Ljava/lang/String;)L java/io/DataOutputStream; policy code.
    Found invokespecial java/lang/StringBuffer.()V
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(I)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.toString()L java/lang/String;
    Found invokevirtual java/lang/String.getBytes()[B
    Found invokevirtual java/io/DataOutputStream.write([B)V
    Found invokevirtual java/io/DataOutputStream.write(I)V
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/Object;)V
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/String;)V
    Found invokevirtual javax/microedition/midlet/MIDlet.notifyDestroyed()V
    Found invokespecial java/lang/StringBuffer.()V
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/Object;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.toString()L java/lang/String;
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/String;)V
Wrote inlined/classfiles/s3mstest/wormgame/ScoreSender.class
Inlining s3mstest/wormgame/WormScore
  Visiting ()V
    Found invokespecial java/lang/Object.()V
  Visiting openHighScoreStore()L javax/microedition/rms/RecordStore;
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/String;)V
    Found invokestatic javax/microedition/rms/RecordStore.openRecordStore(Ljava/lang/String;Z)L javax/microedition/rms/RecordStore;
      Inserting javax/microedition/rms/RecordStore.openRecordStore(Ljava/lang/String;Z)L javax/microedition/rms/RecordStore; policy code.
    Found invokespecial java/lang/StringBuffer.()V
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/Object;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.toString()L java/lang/String;
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/String;)V
  Visiting getHighScoreName(I)L java/lang/String;
    Found invokestatic s3mstest/wormgame/WormScore.openHighScoreStore()L javax/microedition/rms/RecordStore;
    Found invokevirtual javax/microedition/rms/RecordStore.getNumRecords()I
    Found invokevirtual javax/microedition/rms/RecordStore.getRecord(I)[B
    Found invokespecial java/io/ByteArrayInputStream.([B)V
    Found invokespecial java/io/DataInputStream.(Ljava/io/InputStream;)V
    Found invokevirtual java/io/DataInputStream.readShort()S
    Found invokevirtual java/io/DataInputStream.readUTF()L java/lang/String;
    Found invokevirtual java/io/DataInputStream.close()V
    Found invokevirtual javax/microedition/rms/RecordStore.closeRecordStore()V
    Found invokespecial java/lang/StringBuffer.()V
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/Object;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.toString()L java/lang/String;
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/String;)V
  Visiting getHighScore(I)S
    Found invokestatic s3mstest/wormgame/WormScore.openHighScoreStore()L javax/microedition/rms/RecordStore;
    Found invokevirtual javax/microedition/rms/RecordStore.getNumRecords()I
    Found invokevirtual javax/microedition/rms/RecordStore.getRecord(I)[B
    Found invokespecial java/io/ByteArrayInputStream.([B)V
    Found invokespecial java/io/DataInputStream.(Ljava/io/InputStream;)V
    Found invokevirtual java/io/DataInputStream.readShort()S
    Found invokevirtual java/io/DataInputStream.close()V
    Found invokevirtual javax/microedition/rms/RecordStore.closeRecordStore()V
    Found invokespecial java/lang/StringBuffer.()V
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/Object;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.toString()L java/lang/String;
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/String;)V
  Visiting setHighScore(IILjava/lang/String;)V
    Found invokespecial java/io/ByteArrayOutputStream.()V
    Found invokespecial java/io/DataOutputStream.(Ljava/io/OutputStream;)V
    Found invokevirtual java/io/DataOutputStream.writeShort(I)V
    Found invokevirtual java/io/DataOutputStream.writeUTF(Ljava/lang/String;)V
    Found invokevirtual java/io/ByteArrayOutputStream.toByteArray()[B
    Found invokevirtual java/io/DataOutputStream.close()V
    Found invokestatic s3mstest/wormgame/WormScore.openHighScoreStore()L javax/microedition/rms/RecordStore;
    Found invokevirtual javax/microedition/rms/RecordStore.setRecord(I[BII)V
    Found invokevirtual javax/microedition/rms/RecordStore.closeRecordStore()V
    Found invokespecial java/lang/StringBuffer.()V
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/String;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.append(Ljava/lang/Object;)L java/lang/StringBuffer;
    Found invokevirtual java/lang/StringBuffer.toString()L java/lang/String;
    Found invokevirtual java/io/PrintStream.println(Ljava/lang/String;)V
Wrote inlined/classfiles/s3mstest/wormgame/WormScore.class
Wrote inlined/classfiles/s3mstest/wormgame/SecState.class
EXECUTION SUCCESSFUL.
COPYING INLINED FILES BACK INTO WORKING DIR...
    Copying s3mstest/wormgame/ScoreSender.class to wizard_workdir/inlinedfiles
    Copying s3mstest/wormgame/WormScore.class to wizard_workdir/inlinedfiles
DONE

View the inlined files here:

Proceed to next step: Preverify class files >>