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