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 preverification of the inlined class files. This is a part of the deployment of a MIDlet. It minimizes the burden of the byte-code verification for a limited java-device such as a cell-phone.

Tool output:

PREVERIFYING CLASS FILES... EXECUTING: wtk2.5.1/bin/preverify
    -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
    -d ../preverifiedclasses SecState
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
EXECUTING: wtk2.5.1/bin/preverify -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
    -d ../preverifiedclasses s3mstest.wormgame.WormLink
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
EXECUTING: wtk2.5.1/bin/preverify -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
    -d ../preverifiedclasses s3mstest.wormgame.Worm
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
EXECUTING: wtk2.5.1/bin/preverify -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
    -d ../preverifiedclasses s3mstest.wormgame.ScoreSender
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
EXECUTING: wtk2.5.1/bin/preverify -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
    -d ../preverifiedclasses s3mstest.wormgame.WormPit
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
EXECUTING: wtk2.5.1/bin/preverify -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
    -d ../preverifiedclasses s3mstest.wormgame.WormScore
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
EXECUTING: wtk2.5.1/bin/preverify -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
    -d ../preverifiedclasses s3mstest.wormgame.WormMain
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
EXECUTING: wtk2.5.1/bin/preverify -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
    -d ../preverifiedclasses s3mstest.wormgame.WormFood
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
EXECUTING: wtk2.5.1/bin/preverify -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
    -d ../preverifiedclasses s3mstest.wormgame.WormException
EXECUTION WD: wizard_workdir/inlinedfiles
EXECUTION SUCCESSFUL.
DONE

View the preverified class files here:

Proceed to next step: Generate proof >>