隐通道传递信息机理的研究

可信计算机系统中一些隐蔽数据流避开了安全机制的监控，造成信息的泄漏。本文通过对这种隐蔽流泄漏信息的机理进行分析和抽象，提出了一个通道元模型。将每一类通道元看成一个有限状态机，以Plotkin的结构化操作语义等为基础，计算出状态机的状态变化序列。通过对不满足隐通道定义的状态变迁序列的归纳，得到了抽象机中安全状态转移的约束条件，找出两个通道元通过共享客体泄露信息的工作机理，从而开发出一种基于操作语义的隐通道标识方法。对电梯调度算法模型进行实验，可有效地标识出存在的隐通道。

On the Principle of Information Transfer in Covert Channel

Some covert information flow evades the inspection of security mechanism in trusted computer system, which results in information leakage. The atomic channel model was established by analyzing and abstracting the principle of covert information flow. A finite state machine was used to describe an atomic channel model. Based on the structured operational semantics proposed by Plotkin we can compute sequences of states. By reasoning on state sequences against the definition of covert channel, restriction conditions of secure state translation were gained, and the principle of information leakage in two atomic channel models sharing an object was found. Consequently a covert channel identification method based on operational semantics was proposed. The experiment on elevator dispatch algorithm showed that our method could search for covert channels efficiently.