基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究  

Research on Isolation Semantics Description Based on Noninterference Theory and Automated Isolation Strategy Verification Scheme

作　　者：崔隽[1,2] 黄皓[1,2] 陈志贤[1,2,3] 

机构地区：[1]南京大学软件新技术国家重点实验室,南京210093 [2]南京大学计算机科学与技术系,南京210093 [3]南京工业大学信息学院,南京210009

出　　处：《计算机科学》2010年第6期147-154,共8页Computer Science

基　　金：863国家高技术研究发展计划(No:2007AA01Z409)资助

摘　　要：隔离有助于阻止信息泄露或被篡改、错误或失败被传递等。利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程CSP来定义上述隔离语义,并给出一个系统满足给定隔离策略的判定断言,以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证。以基于虚拟机的文件服务监控器为例,展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略。Processes or modules isolation helps protect information from being revealed or modified and prevent processes or modules from passing error or failure to others. We proposed the semantics of isolation by noninterference theory, for the purpose of analyzing and designing isolation strategies in software systems;we also specified the semantics of isolation and its determine conditions by Communicating Sequential Process（CSP） in order for automated formal verification of isolation strategies in systems in formal verification tool FDR2. And in this paper, with an example of file system monitor in a virtual machine, we illustrated how to specify a system or a isolation strategy by CSP formulation and how to verify given isolation strategies in a system automatically in FDR2.

关 键 词：不干扰模型 进程隔离 通信顺序进程 形式化验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]