中文摘要：

深入分析磁臂隐通道的产生及产生的原因,发现目前基于系统顶级描述和基于系统源代码搜索方法难以找出这类隐通道,提出一种基于操作语义的方法来研究磁臂隐通道,将磁臂调度过程中的进程看做一个抽象机,以Plotkin的结构化操作语义给出电梯调度算法的推导规则;根据推导规则得到进程抽象机所有状态以及进程抽象机状态的动态变化历史,这样就构成完整的信息传导操作语义模型。研究与分析两个高低安全级进程抽象机状态变迁及状态变迁序列,从而找到其中存在的磁臂隐通道。

英文摘要：

Analyzed how covert channels produced in disk arm thoroughly, and found that it＇ s very difficult to detect this kind of covert channels based on the methods of searching for system source code and system top level description at present. This paper proposed a method based on the operational semantics to study covert channels in disk arm. Considering process scheduling in disk arm as an abstract machine, it produced the inferential reasoning rule of elevator scheduling algorithm by the Plotkin＇ s structured operational semantics, and obtained all the states of the abstract machine, as well as the states of dynamic-change history of the abstract machine according to these rules, all of which constituted the integral information conduction operational semantics model. Studied and analyzed the states tranforation and tranforation sequences on high and low security levels of the abstract machine, which could find covert channels in disk arm.