摘要
提出了一种适应于可信计算平台系统设计的抽象模型,该模型借鉴信息流的基本无干扰理论,利用进程代数和逻辑推理方法,将系统抽象为进程、动作、状态和输出,形式化地定义了进程运行可信,给出进程运行可信的条件和性质,推出进程运行可信隔离定理,在进程运行可信基础上给出系统运行可信的定义,并证明了系统运行可信判定定理。该模型建立在逻辑推理基础上,不依赖于特定的安全机制和实现方法,任何一种符合这个模型的实现方法,都可以达到系统运行可信的目标。
A novel abstract model for the design of trusted computing platform system was proposed. By using the basic idea of non-interference theory as reference and introduces the reasoning method of process algebra, thus abstracting the system as processes, actions, states and outputs, and giving the formal definition of the trusted of process running. Process isolation trusted theorem was verified formally. Furthermore, by associating process with system state, the defini- tion and the theorem of system running trusted was proposed. The model was established by logic reasoning and independent of special security mechanism and enforcement. The trust of the running system can be realized by any method which satisfies the conditions of the model.
出处
《通信学报》
EI
CSCD
北大核心
2009年第3期6-11,共6页
Journal on Communications
基金
国家重点基础研究发展计划("973"计划)基金资助项目(2007CB311100)
国家高技术研究发展计划("863"计划)基金资助项目(2006AA01Z440)
北京市科技计划基金资助项目(Z07000100720706)~~
关键词
可信
无干扰
进程运行可信
系统运行可信
trusted
non-interference
process running trusted
system running trusted
