EPSRC logo

Details of Grant 

EPSRC Reference: GR/S55538/01
Title: Towards Semantics-Preserving Secure Language Infrastructure: Foundations & Applications to Secure Information Flow
Principal Investigator: Yoshida, Professor N
Other Investigators:
Researcher Co-Investigators:
Dr M Berger
Project Partners:
Department: Dept of Computing
Organisation: Imperial College London
Scheme: Standard Research (Pre-FEC)
Starts: 07 April 2004 Ends: 06 April 2007 Value (£): 14,027
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies Communications
Related Grants:
GR/S55545/01
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: http://www.imperial.ac.uk