You are here
JavaMC - Proof-carrying Java Code
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.
Customer: Robert Atkey, for ReQueST project.
Case statement: See URL.
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.
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.
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. |