安全移动资源的语义、类型系统及其代数性质的研究

摘要

移动资源演算(MR)是一种用于描述携带资源的移动系统及其交互的形式化方法，它隶属于灰箱演算的一支。灰箱演算由Cardelli提出，最初被称为移动灰箱演算(MA)，本文将绝大部分由灰箱演算发展而形成的进程代数系统称为类灰箱演算。本文以移动资源演算的一个变体——安全移动资源演算(SR)作为研究对象，从操作语义、类型系统、进程等价性和表达能力等方面对其进行了研究。 首先，本文在分析现有移动资源演算及相关的类灰箱演算(诸如移动灰箱MA，安全灰箱演算SA，盒灰箱BA等)不足的基础上，提出通过增加协动作并限制协动作的实施对象来提高安全性的思想，并以此为指导给出SR的语法和归约语义。 其次，本文研究了SR的类型问题，提出一套可以解决移动资源演算中存在的进程干扰问题的位置类型系统(L-S)。由于在移动资源演算中引入了灰箱路径作为能力操作对象的语义，因而进程的干扰问题变得更错综复杂，而且原先类灰箱演算干扰问题相关研究成果以及解决方法无法妥善地解决基于灰箱路径的操作语义所带来的相关问题，进程在不同层次的灰箱结构中对同一灰箱路径的访问无法通过已有的系统得到控制。本文利用对携有灰箱路径的能力设定相应的位置类型，进而为携有相关路径的进程记录其访问目的的类型值，配合特殊的位置类型构造，表示位于不同的灰箱层次内进程的访问地点的特性，解决了移动资源演算的巢式干扰问题。L-S系统可以有效地追踪进程的访问地点，并支持子类型关系，该系统还可以和传统的类型属性，如移动性和线程数，构成复合类型系统。 再次，本文参照Levi研究SA，以及Godskesen研究MR等价性使用的方法，对SR进行了类似的研究。首先引入SR进程的标号动作和固化结果，用于将进程中可能参与归约的部分与剩余的部分分开。在标号动作和固化结果的基础上，按照进程的归约特性给出SR基于提交关系的标号转移语义，并逐一分析这些规则与归约规则的对应关系，并证明标号转移语义和归约语义的等价性。在标号转移语义的基础上，研究了判定进程观察互模拟等价的一般方法，得出SR进程的观察互模拟等价关系与标号互模拟等价关系是同一关系的结论，并给出SR进程与上下文(含路径上下文)发生交互的各种可能，作为判定进程等价的一般性结论。 此后，本文综合类型系统和等价性判定的结论，给出用于判定进程等价的一些代数定律，同时使用这些定律证明移动资源的线性特征和数字签名卡例子在给定条件下的正确性。这些例子不仅示意了等价性定律的具体使用方法，同时也体现了SR较之MR在安全性方面的优越性。 最后，本文利用上述等价性定律给出并证明了SR演算翻译π演算的一个方案，弥补了移动资源演算作为灰箱演算的一个分支，到目前为止尚缺乏对表达能力的研究，有力地说明SR在提高安全性的同时，没有失去灰箱演算应有的表达能力。本文的主要创新性体现在以下几个方面。 (一)对利用新增的可供三方同步的协动作，以及相关的能力参数加强移动资源演算安全性这一命题进行了研究，提出了移动资源演算的变体SR。通过利用协动作参数加强交互双方的彼此控制，SR在安全控制方面比起MR来有一定优势。同时，对协动作参数进行控制后，SR并没有丧失MR所具有的表达能力。 (二)针对移动资源演算中存在的进程干扰问题给出了支持访问位置类型特性的类型系统L-S。该系统通过区分不同灰箱层次(即不同灰箱路径)下进程的位置类型，可以精确地避免不同的进程对同一访问地点产生非朴素干扰的现象，并支持子类型关系。考虑到L-S系统的独立性，L-S在设计时还考虑到和传统类型属性整合的可能性，并给出了复合类型系统的框架。 (三)有别于Gordon和Cardelli基于硬化关系的上下文等价方法，本文借鉴Levi和Sangiorgi基于固化结果和提交关系所引入的标号互模拟等价性，给出了SR中判定进程等价性的一般性方法；同时结合位置类型系统，证明了在给出的类型环境Г下SR进程的等价性定律。 (四)本文借助自行推导的SR进程的等价性定律完成对π演算翻译的代数方法证明，较之Zimmer的证明方法来得更为简明。另外，本文将前人对移动资源演算以及相关的类灰箱演算的语义、等价性、表达能力等方面的研究成果结合本文SR演算在这些方面的研究和探索进行了贯穿和融合。

目录

文摘

英文文摘

论文说明：文中用到的符号及含义、上海交通大学学位论文答辩决议书

上海交通大学学位论文原创性声明及版权使用授权书

第一章概述

第二章安全移动资源演算

第三章位置类型系统与SR巢式干扰

第四章标号转移语义

第五章等价性判定

§5.1观察互模拟等价

§5.2标号互模拟等价

§5.3两种等价关系之间的联系

§5.4应用举例

§5.5等价性定律

本章小结

第六章π演算的翻译

第七章结语

参考文献

致谢

攻读学位期间发表的学术论文目录