You are here

JavaMC - Proof-carrying Java Code

Project ID: 
90
Current stage: 
Manager: 
Unit: 
What: 

Description: Develop and enhance a system for verification of 'mobile' (web-transferable) code, utilising and/or enhancing the JavaMC code base.

Deliverables: All deliverables are to be produced in Java.
A simple lightweight web service which allows the transport of mobile code.
An extension to the provided JavaMC code which allows information to be sent and received from a prover for the purposes of code verification.
A configurable byte-code modification engine which allows instrumentation of code to be verified.
An extension or rewrite of the example 'photo server' web application for demonstration of the above.

Why: 

Customer: Robert Atkey, for ReQueST project.

Case statement: See URL.

When: 

Status: Final Report

Timescales: 3 months, spread over 1 year (March 2008 - March 2009).
Timescales of the deliverables to be confirmed.

Priority: High priority alongside Proof-General.
As usual, other duties could take priority for short periods of time.

Time: 3 months' CO effort, spread over March 2008 - March 2009.

How: 

Proposal: Pre-approved as this effort is funded directly.

Resources: 1 x Computing Officer with part-time effort.
Project uses the Informatics subversion repository.

Plan: Complete deliverables as appropriate to overall development, and according to feedback.

Other: 

Dependencies: No strict dependencies, except requiring periodic input from the customer.

Risks: Risk of slippage due to other tasks. Unlikely due to generous real-timeframe, but could contend with Proof General development.

URL: http://groups.inf.ed.ac.uk/request/

Milestones

Proposed date Achieved date Name Description
2009-01-20 Investigation Investigate current system, examine technologies used
2009-05-01 Test Service Prepare a replacement example service based on the photo server example
2009-03-01 Extend Service Extend web service with a usable API
2009-04-01 External Prover Implement simple interface for an external application to verify submitted code
2009-02-01 Byte-code analy Implement enhanced byte-code checking routines
2009-01-10 2009-01-10 Aborted Funding for this project has been withdrawn.