摘要
隔离有助于阻止信息泄露或被篡改、错误或失败被传递等。利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程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.
出处
《计算机科学》
CSCD
北大核心
2010年第6期147-154,共8页
Computer Science
基金
863国家高技术研究发展计划(No:2007AA01Z409)资助
关键词
不干扰模型
进程隔离
通信顺序进程
形式化验证
Noninterference model, Processes isolation, Communicating sequential processes, Formal verification
