一种面向移动计算的机密性与完整性模型  

A Security Model for Confidentiality and Integrity in Mobile Computing

作　　者：郭云川[1,2] 方滨兴[1] 殷丽华[1] 周渊[3] 

机构地区：[1]中国科学院信息工程研究所,北京100093 [2]广西可信软件重点实验室(桂林电子科技大学),广西桂林541004 [3]国家计算机网络应急技术处理协调中心,北京100029

出　　处：《计算机学报》2013年第7期1424-1433,共10页Chinese Journal of Computers

基　　金：国家"八六三"高技术研究发展计划项目基金(2013AA014002);国家自然科学基金(61100186;61070186;61063002;61262008);广西混杂计算与集成电路设计分析重点实验室(HCIC201107)资助~~

摘　　要：机密性和完整性是移动计算的两个重要特性,如何保障机密性和完整性是移动计算的重大挑战.利用π演算能有效建模移动并发系统的特征,借鉴程序语言中不同类型变量之间的赋值方式,提出基于混杂类型检测的安全π演算(Hybrid Typed Securityπ,πHTS).根据πHTS利用静态类型检测保障低机密级信息只能向同等或更高机密级流动,高完整级信息只能向同等或更低完整级流动,针对机密性和完整性在信息流向上的相反性,提出了基于强制类型转化的有效动态转换框架.πHTS将静态检测和动态检测有机地整合在一起,形成了一种统一的安全形式模型.它能同时保障移动计算中的机密性和完整性,具有较好的可用性.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 confi- dentiality 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, hilTS（ Hybrid Typed Security n） is proposed, where static type checking is used to guar- antee 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 pro- posed. 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.

关 键 词：机密性 完整性 混杂类型检测 移动计算 移动互联网 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]