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

如今，移动代码的使用通过计算场景被广泛使用，例如在WWW和电话应用中。移动代码的好处之一是允许可扩展性，其中一段代码从源节点迁移到目标节点，并链接到目标的运行时环境以实现其目的。移动计算的这种开放特性带来了主要的安全问题：访问控制、数据隐私(保密性)和可用性。然而，当前的系统和编程语言缺乏识别和检测潜在恶意移动软件的理论基础。该研究方案利用定义良好的数学模型和移动进程的类型化演算，为解决移动程序的三个安全问题提供了基础技术，并将其应用于移动语言的设计中。首先，基于并发进程演算，为各种编程语言开发了一个能够保证活动性和保密性的统一框架，称为pi演算。然后我们利用高阶pi-演算将其理论扩展到移动性，并结合访问控制。最后，通过设计一种能够保证完整性、保密性和活跃性的移动编程语言及其类型系统，将这些基本理论应用到实际的软件开发中，论证了这些基本理论的相关性。通过向移动进程的转换，证明了类型系统的正确性。

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.