| EPSRC Reference: |
GR/S55545/01 |
| Title: |
Towards Semantics-Preserving Secure Language Infrastructure: Foundations & Applications to Secure Information Flow |
| Principal Investigator: |
Honda, Dr KH |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Queen Mary University of London |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 July 2003 |
Ends: |
31 December 2006 |
Value (£): |
183,469
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| Communications |
Information Technologies |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
At the practical level, this research aims at developing a general technical foundation by which a producer of software can verify its safety by checking its souce code, which is then compiled into an executable code with a safety proof so that a user can check the safety of the delivered code solely by verifying the executable code combined with the safety proof. In particular it should treat not only simple properties such as type-safety but also advanced properties such as various security concerns. Built on the research on proof-carrying coe (PCC), a central technical contribution of the project is to allow safety properties in a high-level code to be carried down to the low-level code throughout the compilation process, which has been difficult due to the use of function-based intermediate languages in existing PCC technologies. Capitalising on our recent work on the faithful embedding of lambda-calculi in the pi-calculus, we develop low-level pi-calculi which preserve all benefits of existing intermediate languages and which, in addition, allows more flexible representation of intermediate code. Among others it is now feasible, aided by powerful type structure, to preserve semantics while compiling source code to intermedaite code and, in effect, to the target code. We extend the pi-calculus with low-level operations and advanced type structure. and use the resulting calculus to construct a prototype semantic preserving compiler with end-to-end secure information flow assurance.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
|