Type-Based Security for Mobile Computing: Integrity, Secrecy and Liveness
Lead Research Organisation:
Imperial College London
Department Name: Computing
Abstract
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.
Organisations
People |
ORCID iD |
Nobuko Yoshida (Principal Investigator) |
Publications
Honda K
(2008)
Multiparty asynchronous session types
Carbone M
(2008)
Theoretical Aspects of Communication-Centred Programming
in Electronic Notes in Theoretical Computer Science
Yoshida N
(2008)
Logical Reasoning for Higher-Order Functions with Local State
in Logical Methods in Computer Science
Description | See GR/T03208/01 |
Exploitation Route | See GR/T03208/01 |
Sectors | Digital/Communication/Information Technologies (including Software),Security and Diplomacy |
URL | http://www.doc.ic.ac.uk/~yoshida/advance |
Description | This section should be the same as GR/T03208/01 |
First Year Of Impact | 2009 |
Sector | Digital/Communication/Information Technologies (including Software),Security and Diplomacy |
Impact Types | Policy & public services |