摘要: 针对可信应用环境的安全性验证问题,利用通信顺序进程描述系统应具有的无干扰属性,基于强制访问控制机制对系统中的软件包进行标记,并对系统应用流程建模。将该模型输入FDR2中进行实验,结果证明,系统应用在运行过程中达到安全可信状态,可以屏蔽环境中其他应用非预期的干扰。
关键词:
无干扰,
通信顺序进程,
形式化描述,
形式化验证,
可信计算
Abstract: 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.
Key words:
non-interference,
Communicating Sequential Processes(CSP),
formal description,
formal verification,
trusted computing
中图分类号:
陈亚莎, 胡俊, 沈昌祥. 可信应用环境的安全性验证方法[J]. 计算机工程, 2011, 37(23): 152-154.
CHEN E-Sha, HU Dun, CHEN Chang-Xiang. Security Verification Method of Trusted Application Environment[J]. Computer Engineering, 2011, 37(23): 152-154.