Details of Grant 

EPSRC Reference:	GR/T03215/01
Title:	Type-Based Security for Mobile Computing: Integrity, Secrecy and Liveness
Principal Investigator:	Yoshida, Professor N
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computing
Organisation:	Imperial College London
Scheme:	Standard Research (Pre-FEC)
Starts:	01 October 2006	Ends:	31 October 2009	Value (£):	161,860
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	Communications
Related Grants:
Panel History:	Panel Date Panel Name Outcome 19 Apr 2004 ICT Fellowships 2004 - ARF Interview Panel Deferred 18 Mar 2004 ICT Fellowships 2004 Sift Panel Deferred
Summary on Grant Application Form
Nowadays the use of mobile code is widespread through computing scenes, e.g. in www and telephony applications. One of benefits of mobile code is to allow extensibility, where a piece of code migrates from a source node to a target node and gets linked to the run-time environment of the target to serve its purpose. Such an open characteristic of mobile computing introduces the main security issues: access control, privacy of data (secrecy), and availability. However, current systems and programming languages lack a theoretical base to identify and detect potentially malicious mobile software. This research proposal develops fundamental technologies to solve three security issues concerning mobile programs using well-defined mathematical models, typed calculi of mobile processes, and applies them to a mobile language design.First we develop a uniform framework for the various programming languages which can ensure liveness and secrecy based on a concurrent process calculus, called the pi-calculus. Then we extend its theory to mobility using the higher-order pi-calculus, as well as incorporating the access control. Finally we demonstrate the relevance of these foundational theories by applying them to the real software development by designing a mobile programming language and its type system which can ensure integrity, secrecy and liveness. The correctness of the type system is proved via translation into mobile processes.
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