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

如今，移动的代码的使用在计算场景中（例如，在www和电话应用中）是广泛的。移动的代码的好处之一是允许可扩展性，其中一段代码从源节点迁移到目标节点，并链接到目标的运行时环境以服务于其目的。移动的计算的这种开放特性引入了主要的安全问题：访问控制、数据隐私（保密）和可用性。然而，当前的系统和编程语言缺乏识别和检测潜在恶意移动的软件的理论基础。本研究计划开发的基本技术，以解决三个安全问题有关移动的程序使用定义良好的数学模型，类型演算的移动的processes，并将其应用到一个移动的language design.First，我们开发了一个统一的框架，可以确保活动性和保密性的各种编程语言的基础上的并发进程演算，称为π演算。然后，我们扩展其理论的移动性使用高阶π演算，以及将访问控制。最后，我们通过设计一个移动的编程语言及其类型系统，将这些基础理论应用到真实的软件开发中，以证明这些理论的相关性，该语言及其类型系统可以确保完整性、保密性和活性。类型系统的正确性是通过转换成移动的进程来证明的。

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.