Isabelle在分析安全操作系统状态机模型中的应用  

Application of Isabelle in analyzing secure operating system state-machine models

作　　者：陈坤[1] 贺也平[2] 

机构地区：[1]中国科学院研究生院,北京100080 [2]中国科学院软件研究所基础软件工程技术中心,北京100080

出　　处：《计算机工程与设计》2008年第3期580-582,730,共4页Computer Engineering and Design

基　　金：国家自然科学基金面上项目(60573042);北京市自然科学基金项目(4052016)

摘　　要：为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观、简洁的问题,提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数,以及模型中的安全不变量和状态迁移规则进行形式化描述的新方法。通过实际验证一种典型的安全操作系统状态机模型——可信进程模型,总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略。The existing formal frame for state-machine model has trouble in concisely and specifically analyzing secure operating system state-machine models. To solve this problem, a method of using Isabelle to formally describe types, variables, constants, relations, mappings and functions in secure operating system state-machine models and secure invariants and state transition operations in the models is introduced. Thenaftertheverificationofarepresentativemodeltrustedprocessmodel, an effective strategy ofIsabelle assisted formal design, analysis, verification of secure operating system state-machine models is concluded.

关 键 词：形式化 Isabelle工具 状态机模型 安全操作系统 可信进程模型 

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