论文研究 基于操作语义的磁臂隐通道分析.pdf

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