ZHANG Xing1, CHEN You-lei2, SHEN Chang-xiang2. Non-interference trusted model based on processes[J]. 2009, 30(3): 6-11.DOI:
基于进程的无干扰可信模型
摘要
提出了一种适应于可信计算平台系统设计的抽象模型
该模型借鉴信息流的基本无干扰理论
利用进程代数和逻辑推理方法
将系统抽象为进程、动作、状态和输出
形式化地定义了进程运行可信
给出进程运行可信的条件和性质
推出进程运行可信隔离定理
在进程运行可信基础上给出系统运行可信的定义
并证明了系统运行可信判定定理。该模型建立在逻辑推理基础上
不依赖于特定的安全机制和实现方法
任何一种符合这个模型的实现方法
都可以达到系统运行可信的目标。
Abstract
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 definition 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.