【摘要】 机密性和完整性是移动计算的两个重要特性,如何保障机密性和完整性是移动计算的重大挑战.利用π演算能有效建模移动并发系统的特征,借鉴程序语言中不同类型变量之间的赋值方式,提出基于混杂类型检测的安全π演算(Hybrid Typed Securityπ,πHTS).根据πHTS利用静态类型检测保障低机密级信息只能向同等或更高机密级流动,高完整级信息只能向同等或更低完整级流动,针对机密性和完整性在信息流向上的相反性,提出了基于强制类型转化的有效动态转换框架.πHTS将静态检测和动态检测有机地整合在一起,形成了一种统一的安全形式模型.它能同时保障移动计算中的机密性和完整性,具有较好的可用性.更多还原

【Abstract】 Confidentiality and integrity,together with their security model,are two key issues for mobile computing.In order to satisfy these two security properties,BLP model for confidentiality and Biba model for integrity are often employed.But due to their conflict,a simple composition of the two models cannot meet the two requirements simultaneously.In this paper,πHTS(Hybrid Typed Securityπ)is proposed,where static type checking is used to guarantee that information flows from the high-level confidentiality into the low-level confidentiality and from the low-level integrity into the high-level integrity.To address the conflict between BLP model and Biba model,a new frame based type conversion and dynamic checking is proposed.An example demonstrates that our method is efficient.πHTS unifies static type checking and dynamic checking and forms a general formal frame,and provides both confidentiality and integrity.更多还原