基于Agent的移动计算及其安全性研究

摘要

随着近来计算机网络技术、通信技术的飞速发展,基于因特网的全球性的计算平台已经建立起来；同时,由于高速无线通信技术的出现以及器件快速小型化,许多便携式设备如：笔记本电脑,移动电话,PDA,以及各种信息家电也接入到网络中来。以并发性、移动性、分布性、实时性、异构性和互操作性为主要特征的移动计算系统已经成为计算机技术领域的一个研究热点,很多研究成果已经在实际信息系统的开发中得到广泛应用。对于移动计算而言,安全性是移动计算能否成功应用的关键问题。本文研究基于agent的移动计算系统的形式化理论和技术,并在形式化模型基础上深入研究了基于agent的移动计算系统的安全性理论和技术,包括静态安全性分析,安全信息流分析和基于安全自动机的动态监测技术,最后探讨了基于agent的移动基础设施和消息传递算法。主要工作包括以下六个方面：(1)首先对移动计算系统中的安全要求、安全威胁和安全机制进行了讨论,提出了移动计算的统一安全框架,并指出在移动计算中可以在统一的形式化计算模型中描述移动计算系统并设计和表示不同的安全机制。(2)在基于进程代数的π演算框架下,通过引入位置、计算边界和限制区域,建立了一个扩展的π演算模型：Confined-π演算。并在限制声明的基础上对进程的行为进行了规范,使得安全策略通过由计算边界定义的格和限制区域的包含关系编码到Confined-π演算中。(3)在Confined-π演算平台上,从静态分析的角度考查了实现移动计算系统静态安全性分析的方法。通过在Confined-π演算中引入带安全标记(计算边界标记和限制区域标记)的类型系统,移动计算的安全要求,如限制agent移动和通信等,被转换成类型系统中的形式化特性,从而将移动计算系统中的一些安全性问题转化成基于类型的静态分析问题。

目录

摘要

ABSTRACT

英语缩略语表

第一章 绪论

1.1 引言

1.2 基于Agent 的移动计算与π演算

1.3 移动计算环境下的安全性

1.3.1 基于类型系统的静态分析理论与技术

1.3.2 移动计算中的安全信息流分析技术

1.3.3 移动计算环境下的安全策略与动态监测技术

1.4 本文的主要工作

第二章 移动计算的安全威胁和要求以及安全机制

2.1 计算系统模型及移动计算环境下的安全框架

2.2 移动计算环境下的安全要求与安全威胁

2.3 移动计算中的安全机制

2.4 小结

第三章 基于Agent 的安全移动计算模型

3.1 引言

3.2 移动计算的计算边界及限制区域

3.2.1 移动计算的计算边界

3.2.2 移动计算的限制区域

3.3 限制Agent：Confined-π计算模型

3.3.1 Confined-π的语法

3.3.2 Confined-π的操作语义

3.3.3 Confined-π演算迁移系统的基本性质

3.4 举例

3.5 小结

第四章 类型系统

4.1 类型语法与类型的运算

4.2 Confined-π演算的类型系统

4.3 类型系统的性质

4.4 小结

第五章 Confined-π演算中的等价关系及安全信息流分析

5.1 引言

5.2 非类型约束的进程等价

5.3 具有类型约束的进程等价

5.4 Confined-π演算中的安全信息流分析

5.4.1 Confined-π演算中的安全结构

5.4.2 Confined-π演算中的非干扰安全性

5.5 小结

第六章 安全策略的进程表示

6.1 引言

6.2 移动计算系统中安全性的形式化描述

6.3 安全自动机及其进程描述

6.3.1 安全自动机的定义

6.3.2 安全自动机的进程表示

6.4 移动计算系统安全属性的判定

6.5 Confined-π演算中安全策略的表达及实施

6.6 小结

第七章 基于Agent 的移动计算中的基础设施设计与算法

7.1 引言

7.2 移动基础设施统一框架

7.3 支持Agent 移动的消息传递算法

7.3.1 算法的提出

7.3.2 通信过程与算法

7.4 小结

第八章 研究工作总结与展望

8.1 研究工作总结

8.2 研究展望

参考文献

致谢

攻读博士学位期间发表和录用的学术论文目录

攻读博士学位期间参加的科研项目