Type-Based Security for Mobile Computing: Integrity, Secrecy and Liveness

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.