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
Ahern A
(2007)
Formalising Java RMI with explicit code mobility
in Theoretical Computer Science
Berger M
(2008)
Automata, Languages and Programming
BERGER M
(2007)
A logical analysis of aliasing in imperative higher-order functions
in Journal of Functional Programming
Berger M
(2007)
Programming Languages and Systems
Carbone M
(2007)
A Calculus of Global Interaction based on Session Types
in Electronic Notes in Theoretical Computer Science
Carbone M
(2008)
CONCUR 2008 - Concurrency Theory
Carbone M
(2007)
Programming Languages and Systems
Carbone M
(2008)
Theoretical Aspects of Communication-Centred Programming
in Electronic Notes in Theoretical Computer Science
Crafa S
(2007)
CONCUR 2007 - Concurrency Theory
Dezani-Ciancaglini M
(2006)
ECOOP 2006 - Object-Oriented Programming
Gardner P
(2006)
Editorial
in Theoretical Computer Science
Honda K
(2007)
Web Services, Mobile Processes and Types
in ulletin of the EATCS
Honda K
(2008)
Multiparty asynchronous session types
in ACM SIGPLAN Notices
Honda K
(2006)
Automata, Languages and Programming
Honda K
(2008)
Multiparty asynchronous session types
Mario Coppo
(2007)
Asynchronous Session Types and Progress for Object-Oriented Languages
in Formal Methods for Open Object-Based Distributed Systems
Mostrous D
(2007)
Typed Lambda Calculi and Applications
Varacca D
(2006)
Typed Event Structures and the p-Calculus
in Electronic Notes in Theoretical Computer Science
Varacca D
(2007)
Probabilistic p-Calculus and Event Structures
in Electronic Notes in Theoretical Computer Science
Yoshida N
(2007)
Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication
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
Yoshida N
(2007)
Foundations of Software Science and Computational Structures
Yoshida N
(2006)
Type-Based Security for Mobile Computing Integrity, Secrecy and Liveness
in Electronic Notes in Theoretical 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 |