论文部分内容阅读
安全操作系统的设计和实现过程中对形式化方法有很高的要求。在各种形式化验证方法中，模型检验以其自动化程度高并且能够提供验证反例帮助纠错而受到人们的关注。如何定义和选择要验证的属性，如何对验证系统重构，以使安全属性的验证更加方便是使用模型检验进行形式化验证需要考虑的问题。
微内核因其结构高度模块化，易验证，具有较强的灵活性和可靠性而适合作为安全操作系统的内核结构。L4是第二代微内核的典型代表。本文针对L4内核中与系统安全性关系密切的内存管理功能，运用模型检验的方法进行了一系列形式化验证和改进工作。研究和探讨针对该问题的系统抽象描述，以及在该抽象层次上系统安全属性的定义。通过分析验证反馈结果提出了安全性改进方案。这些工作主要包括：
1)分析各类形式化方法，选择SPIN作为形式化验证工具。
总结了目前操作系统安全性验证主要的形式化方法，分析了定理证明和模型检验方法各自的优缺点。针对L4内存地址映射操作的特点，选择了SPIN作为形式化验证工具。
2)针对L4内存管理模块形式化建模
研究分析了L4内存管理的分层映射模型，运用SPIN模型描述语言Promela构建了L4内存管理的形式化模型，对L4内核API提供的几个基本的地址空间操作原语进行形式化描述。
3)安全属性验证与实现修正方案
总结提出了系统在多个用户进程并发执行时，地址空间映射关系应满足的一些安全属性，并运用时序逻辑公式将这些安全属性描述为系统不变量。
应用模型检验工具SPIN对这些安全属性进行了验证，从中发现了grant操作可能产生的安全性问题，并提出了实现修正方案。