可信应用环境的安全性验证方法  

Security Verification Method of Trusted Application Environment

作　　者：陈亚莎[1] 胡俊[2] 沈昌祥[2] 

机构地区：[1]海军工程大学电气与信息工程学院,武汉430033 [2]北京工业大学计算机学院,北京100124

出　　处：《计算机工程》2011年第23期152-154,共3页Computer Engineering

基　　金：国家"863"计划基金资助重点项目(2009AA01Z437);国家"973"计划基金资助项目(2007CB311100)

摘　　要：针对可信应用环境的安全性验证问题,利用通信顺序进程描述系统应具有的无干扰属性,基于强制访问控制机制对系统中的软件包进行标记,并对系统应用流程建模。将该模型输入FDR2中进行实验,结果证明,系统应用在运行过程中达到安全可信状态,可以屏蔽环境中其他应用非预期的干扰。Aiming at security verification problem of trusted application environment,this paper uses Communicating Sequential Processes（CSP） to describe non-interference performance of the system.Based on mandatory access control mechanism,it tags all software packages in the system,and models system application processes.The model is input into FDR2 to do experiment,whose result shows that the application execution process is secure and trusted,which can resist unexpected interference from other applications.

关 键 词：无干扰 通信顺序进程 形式化描述 形式化验证 可信计算 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]