作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2011, Vol. 37 ›› Issue (23): 152-154. doi: 10.3969/j.issn.1000-3428.2011.23.052

• 安全技术 • 上一篇    下一篇

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

陈亚莎1,胡 俊2,沈昌祥2   

  1. (1. 海军工程大学电气与信息工程学院,武汉 430033;2. 北京工业大学计算机学院,北京100124)
  • 收稿日期:2011-05-05 出版日期:2011-12-05 发布日期:2011-12-05
  • 作者简介:陈亚莎(1983-),女,博士研究生,主研方向:可信计算,信息安全,形式化验证;胡 俊,讲师;沈昌祥,教授、博士生导师、中国工程院院士
  • 基金资助:
    国家“863”计划基金资助重点项目(2009AA01Z437);国家“973”计划基金资助项目(2007CB311100)

Security Verification Method of Trusted Application Environment

CHEN Ya-sha 1, HU Jun 2, SHEN Chang-xiang 2   

  1. (1. Department of Electrical and Information Engineering, Naval University of Engineering, Wuhan 430033, China; 2. Institute of Computer Science, Beijing University of Technology, Beijing 100124, China)
  • Received:2011-05-05 Online:2011-12-05 Published:2011-12-05

摘要: 针对可信应用环境的安全性验证问题,利用通信顺序进程描述系统应具有的无干扰属性,基于强制访问控制机制对系统中的软件包进行标记,并对系统应用流程建模。将该模型输入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

中图分类号: