KTH Demo: Proof Generation

The demo pages

These pages demonstrate the proof generation / verification tools of the tool suite developed at KTH.

Here you can download the prototype description report.

The Tool Components

The tool is divided into two parts. One part for the producer side and one part for the consumer side. The producer tool automates the code rewriting, proof generation and packaging. The consumer tool parses and verifies the proofs.

Producer side

The producer side of the tool is a Java-based desktop application. The components with corresponding input and output are illustrated in the figure below. A screen shot of the user interface can be found under the download section.

Consumer side

The consumer part of the tool is a Java MIDlet application that runs on a regular CLDC-1.1 enabled mobile device. The components with corresponding input and output are illustrated in the figure below.

About the demo

The online demo is divided into the several steps shown in the menu to the left. The actual proof generation is performed in the fifth step which can be accessed directly by clicking the "Generate proof" menu item.

The WormGame

The WormGame is a simple MIDlet which contains a traditional game of 'snake'. The game has two relevant functions: View highscore and Upload highscore. View highscore reads the current highscore list from the local record store and upload highscore sends the highscore to the highscore server.

The Policy

The conspec policy used in the demo forbids opening any DataOutputStream connections after opening a local RecordStore.

What is demonstrated

The demo shows how the producer tool is used to generate, package and deploy a program together with a policy adherence proof. It then displays some screen shots from the consumer-side tool which shows how the proof is verified.