操作系统(operating system, 简称OS)作为重要的系统软件, 为上层的各种应用程序提供平台服务和安全保障.OS的正确性是信息安全的重要部分.如何说明和保证OS的正确性, 一直是学术界和工业界研究的热点.OS由于其巨大的规模和复杂性, 使得其正确性很难用定量的方法来进行描述和说明.即使经过尽可能全面的大规模测试, OS中的错误还是随着时间的推移不断地出现, 这点从目前各种主流商业OS不断发布更新补丁这一事实上可见端倪.

对于低安全性的应用环境, 使用系统测试的方法可以在一定程度上保证OS的正确性.但对于高安全性的应用场合, 采用测试的方法是不够的, 即使尽可能完整的测试用例, 也很难保证OS的实现是正确的.

形式化方法是目前公认的对OS的正确性进行验证的有效工具.对OS的形式化验证可以从两个方面进行, 包括高级语言级(如C语言)形式化验证和底层汇编语言级形式化验证.很多学者和形式化项目对高级语言级的形式化验证进行了研究^[1-3], 然而, 高级语言代码并非真正在机器上运行的机器代码, 即使高级语言层的代码经过了形式化验证, 也只能说明系统在高级语言层是可靠的, 但无法保证系统在物理机器上实际运行情况的正确性.原因在于高级语言层和机器代码层之间隔了汇编语言层, 从高级语言代码到汇编语言代码的转化是通过编译器来实现的.要说明高级语言代码和汇编语言代码的一致性, 主要有两个途径:第一是通过验证编译器的正确性来说明; 第二是通过对汇编语言代码层进行建模, 并对其语义的正确性进行验证来说明.对于第1种途径, 由于编译器的巨大规模和复杂性, 往往很难验证其正确性, 很多学者对此进行了尝试^{[4, 5]}, 从所耗费的人力和物力上来说, 使得很多的OS开发项目望而却步; 而第2种方法, 即直接对汇编语言层进行建模和验证, 由于汇编语言过于底层, 对其进行形式化验证的难度较大, 如何有效地对汇编语言代码进行建模, 便于对其语义和功效的正确性进行验证, 成为OS形式化领域的一大挑战.

同时我们认为, 不仅需要使用形式化的方法对系统实现进行验证, 对于系统设计的过程, 就需要使用严格的形式逻辑来保证设计的正确性, 从而最大程度上保证系统的正确性.本文阐述我们对于OS形式化设计和验证的方法.本文的创新点在于汇编层形式化地对系统模块的功能语义进行建模, 提出一种汇编级的系统状态模型, 该模型作为汇编语言层设计和验证的纽带, 通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域, 并以此来描述汇编层的论域.通过验证汇编层的功能模块的正确性来保证汇编语言层设计的正确性, 从而达到对系统功能实现的正确性验证.我们使用定理证明工具Isabelle/HOL^[6]来形式化地描述该系统状态模型.基于这一形式化模型, 我们在Isabelle/HOL中验证系统模块的功能语义的正确性.本文以我们实现的安全可信OS (verified secure operating system, 简称VSOS)为例阐述我们的方法, 说明这一形式化方法在对OS系统汇编层的建模和语义功效的正确性验证方面的可行性.

本文第1节介绍操作系统形式化验证领域的相关工作, 并与我们的工作进行比较.第2节介绍VSOS的整体框架.第3节以VSOS为例描述我们提出的系统状态模型.第4节描述系统状态模型在Isabelle/HOL定理证明器环境中的构建方法.第5节阐述系统初始化过程汇编级验证方法.第6节阐述系统功能模块的汇编级验证方法.第7节对我们的工作进行总结, 并对未来的工作进行展望.

1 相关工作

1978年, UCLA为PDP-11机器开发了UCLA Secure Unix^[7].在该系统中, 给出了多层规格说明.顶层规格说明描述了内核的权限访问控制模型, 抽象层规格说明主要是一些抽象的数据结构, 低层规格说明包含了在内核调用接口中要用到的所有变量对象, 最低层是内核的Pascal代码.UCLA证明了部分的抽象层次规约的一致性, 但是没有证明所有内核层次之间以及与实现的一致性.

Provably Secure Operating System (PSOS)由SRI国际组织^[8]于1973年~1980年设计, 其目的在于提供一个可证明安全性的通用OS.PSOS提出了多级分层抽象的方法, 其采用的规约和断言语言SPECIAL^[9]用于精确定义各个层次的模块以及层与层之间的抽象映射.PSOS只提供了一些简单的实例来说明实现和规约是一致的, 没有做到真正的形式化设计和验证.

1992年, 美国支持完成的LOCK项目致力于开发达到或超过A1级的安全OS, 其整个开发周期的58%的工作都被用来进行形式化安全策略模型和顶层规范的设计, 以及策略与设计之间的一致性证明.1992年~1993年间, 美国国家安全局(NSA)和安全计算公司(SCC)的研究人员在LOCK项目的基础上共同设计和实现了分布式可信Mach系统(DTMach).DTMach项目的后继项目--分布式可信OS (DTOS)^[10]最终形成了Z语言版的形式化安全策略模型(FSPM)和形式化顶层规范(FTLS)技术文档.

1995年, Charlie Landau组织了EROS^[11]项目, 它的形式化验证工作主要考虑地址转换的正确性和内核的内存使用的安全性部分.EROS的后继项目Coyotos由Hopkins在2006年组织, 设计了一种低层次的编程语言BitC, 同时给出了相应的形式语义^[12].

VFiasco项目^[13]由德累斯顿技术大学组织, 对兼容L4的OS微内核Fiasco进行形式化验证, 采用了SPIN模型检测的方法来验证IPC机制; 同时, 采用定理辅助证明工具PVS^[14]进行建模和代码验证, 对C++语言进行了部分改进加强编程语言的安全性.2008年, 文献[15]报告了VFiasco的工作在Nova Hypervisor项目中的延续, 提出了IA32处理器的模型和内存模型, 实现了将C++代码直接转换为相应PVS语意代码的工具.

Robin^[16]项目开始于2006年, 使用PVS进行了形式化描述, 验证了简单版本的x86硬件模型以及C++的子集语义的正确性.

seL4项目由澳大利亚国家ICT实验室(NICTA)在2004年~2006年实施发起, 该项目重点在形式化验证L4微内核的ARM体系结构版本, 其正确性证明采用Isabelle/HOL形式化证明辅助工具.Tuch和Klein在文献[1]中介绍了验证的工作, 验证的目标是使用Isabelle/HOL证明最终的实现符合抽象模型的预期定义.seL4致力于采用形式化方法验证OS的可靠性^[17]和完整性^[18], 并提高实际系统的运行效率^[19].

从20世纪90年代开始, Shao等人带领的Flint项目组在形式化验证方面做了大量的工作^{[2, 20]}.在安全语言方面, Flint开发了一种新的编程语言VeriML^[21], 其采用的逻辑系统lHOL^ind在lHOL逻辑^[22]的基础上加入了对数据类型的归纳定义, 提供了丰富的形式化描述能力以及类型安全特性.同时, Feng等人提出的OCAP^[23]开放逻辑框架首次成功将OS不同模块的验证逻辑结合起来, 形成一个完整的验证系统, 并保证验证模型的可扩展性.同时, Flint项目组研究了并发管理的形式化验证方法^[24], 并使用分层抽象的方法验证OS中的功能模块^[25].Flint项目组和中国科技大学陈意云教授带领的小组组建的可信软件实验室, 致力于高可信软件中的形式程序验证技术, 研究如何有效地集成形式程序验证和领域专用语言这两种软件技术, 形成提高编写健壮软件生产力和提高对它们正确性和安全性的软件开发新方法, 并构建开发基于携带证明(PCC)的大型系统软件的基础结构^[26-30].

Verisoft是一个大型的计算机系统设计开发项目, 目标在于对整个计算机系统自底向上从硬件层到应用软件层进行普适形式化证明(pervasive formal verification)^{[3, 31]}.在2007年, 其后继项目Verisoft XT正式启动.在Verisoft项目中, 普适形式化证明意味着整个项目重点关注的问题并不仅仅是编译器和机器指令模型的正确性, 而是整个系统的设计层次都要经过严格的形式化验证, 从而组成一个完整的软硬件的验证链^[32-34].

目前尚无一款通用OS或者OS内核可以认为是完全经过形式化验证的, 尽管部分小型系统接近Common Criteria的Verified指标, 但仍然需要人工地将系统的实现代码转化为定理证明器的验证代码, 或者直接在定理证明器中编写针对系统实现的验证代码, 或多或少地存在着非形式化的描述和验证.Verisoft项目是目前看来比较成功的例子, 但目前已终止, 其中, VAMOS内核的验证工作也只是在很小的范围进行.seL4项目致力于对系统代码进行完全的验证, 由于内核结构的复杂性, 其验证工作尚未完成.

从20世纪70年代到现在, OS的代码从几百行发展到现在的上万行, 验证的复杂度也上升了多个数量级, 即使是在很大程度上经过形式化设计和验证的项目, 如何将系统的实现转化为验证工具的输入, 仍然是困扰很多形式化学者的重要问题.同时, 系统运行环境和形式化验证之间存在着现实世界的非形式化和逻辑世界的形式化之间的一道鸿沟.OS的形式化设计和验证仍然是困难和费时的研究工作, 系统实现代码和验证代码量1:40以上的工作量, 导致形式化验证技术对很多的系统项目来说不得不考虑人力和物力的问题.

同时, 具有代表性的Verisoft, seL4等形式化工作在对系统进行验证的过程中都是从非常高的层次去验证系统中的功能函数的正确性, 并通过保证编译过程的正确性来说明系统整体的正确性.

VSOS强调在前期设计过程中就采用形式化的方法, 以此来保证系统在设计过程的可验证性, 同时也是为了力争做到形式化方法和理论对整个OS开发过程指导的全程化以及整个OS代码的可维、可控, 做到系统的完全自主.本文尝试从汇编级对系统建立形式化状态模型, 将该模型作为汇编语言层设计和验证的纽带, 通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域.在对系统状态和指令语义的形式化定义的基础上, 对系统的安全性(正确性)条件以命题公式的形式来表达, 并使用交互式的机械化证明的方法来验证系统的设计和实现是否满足预期的安全性(正确性)条件.验证工作的结果表明, 我们的方法是可行的和高效的.如果从系统实现的代码量和验证的代码量的比例的标准来看, 我们达到了平均情况下1:10的量; 同时, 我们的验证工作覆盖了整个微内核以及文件系统、进程管理、内存管理等微内核外围模块.

2 VSOS框架

VSOS是我们实现的安全操作系统原型, VSOS内核部分提供基本的系统服务, 如中断处理、消息处理和简单的I/O服务.其他的功能服务, 如文件管理、进程管理、内存管理等, 都采用用户态进程的方式来提供.VSOS的整体框架如图 1所示.

VSOS采用微内核架构, 只有微内核运行于特权级模式, 其他的系统功能模块和第三方的驱动程序都运行于用户级, 有效地保证了微内核运行环境的隔离性.为此, 微内核作为整个系统的可信基.如果对微内核部分进行了严格的验证, 就能够保证整个系统的核心的正确性.VSOS的微内核代码量(C语言和汇编实现)控制在10k SLOC (source lines of code)左右, 便于对其正确性进行形式化验证.

在VSOS的框架中, 进程间通信(IPC)采用消息机制实现.从功效来说, 消息处理机制是微内核将消息发送进程的消息缓冲区中的消息拷贝到消息接收进程的消息缓冲区中.消息处理需要检查目标进程的合法性, 查找内存中的发送和接收缓存.同时, 微内核将硬件中断和软件中断转换成消息, 硬件中断由硬件产生, 软件中断是用户层程序为请求系统服务而向内核传递的唯一途径.

微内核进行进程调度行为, 负责进程在就绪态、运行态和阻塞态之间的转换.

由于隔离性, 位于微内核外部的进程被禁止执行实际的I/O操作, 也不能改动系统表以及完成其他操作系统一般都有的功能.为此, 需要让微内核为驱动程序和服务器提供一组服务, 这些专门的服务是由系统任务进行处理的.系统任务作为独立的进程并被调度, 负责接收所有来自驱动程序和服务器的调用请求消息并进行转发.

微内核还负责对系统的硬件中断和系统调用(软件中断)进行处理, 包括保存进程上下文(寄存器信息)、中断处理例程以及恢复并重启进程等行为.

3 VSOS系统状态模型

本节首先分析构成VSOS系统状态模型的元素, 如软件/硬件计算单元、系统对象状态和事件.在这些元素的基础上, 我们阐述VSOS的系统状态模型.

3.1 硬件和软件计算单元

一台安装了OS和服务软件的网络服务器, 在启动后可以持续地提供约定的服务, 这是软硬件系统协同工作的结果.在描述OS的抽象模型之前, 首先分析系统软/硬件计算单元的基本要素.

现代计算机系统主要的构成部分包括存储器、算术单元(arithmetic unit)和控制单元(control unit)等.这里所讲的存储器部分包括了CPU中寄存器、缓存(cache)、传统意义上的主存、设备控制器中寄存器以及硬盘的交换区域.系统执行过程中, 算术单元所需的指令序列和数据以及计算的结果都存放在存储器中.我们这里所涉及的存储器概念与传统意义上的计算机组织结构存在一定的差别, 这主要是为了便于后续对OS抽象模型的描述.能够改变存储器中数据的主体包括CPU中的运算器(或CPU处理核中的运算器)、采用直接内存访问(direct memory access, 简称DMA)机制的系统中的设备控制器, 它们并行地改变存储器中的数据.我们将这些对象称为硬件计算单元.

CPU中, 控制器根据存储器中的数据控制着CPU中运算器的运行方式, 例如在Intel处理器上, 当EFLAG寄存器的CPL位不等于0时, 运算器不能执行SETGDT指令.同时, 由于存储器中数据(如Intel处理器中的EFLAGS寄存器)包含了对于系统中断的掩码信息, 为此, 控制器根据这些信息控制着系统从到达计算机的中断事件中选择出一组恰当的事件接下来进行处理, 从而影响着对下一组执行指令的选择.对于不同的指令, 执行所需要的时钟周期数是不同的.在每个时钟周期结束时, 有些指令可能完全执行完成, 但有些指令则需要在下一个时钟周期继续执行.同时, 在每个时钟周期结束时, 可能有多个事件到达系统.CPU中的控制器根据存储器中的当前数据以及恰好执行完指令的硬件计算单元来选择多个事件, 在下一个时钟周期进行处理.在这样一个场景下, 我们将可以在一个硬件计算单元上运行的一个指令序列称为软件计算单元, 例如进程、线程和函数对象等.

假设U是一个软件计算单元, U的只读数据对象集合表示为R(U), 对应地, U的可修改数据对象集合表示为W(U).我们将R(U) W(U)称为U的一个工作对象集合, 表示为RW(U).由于系统中存在中断机制, 软件计算单元U在执行过程中可能会被打断, 从而进入等待队列进行等待.在VSOS的设计过程中, 我们利用隔离机制保证了在U的等待过程中, 其他的软件计算单元不能访问其工作对象集合.为此, 我们可以将当前的所有软件计算单元分成两类:一类是正在运行的软件计算单元集合, 记为A_r, 这些软件计算单元都在各自对应的硬件计算单元上运行; 另一类是正在等待的软件计算单元集合, 记为A_w, 这些软件计算单元并不占有硬件计算单元, 即, 在等待队列中等待运行.所有的软件计算单元的集合表示为A, 即, A=A_r A_w.

3.2 系统对象状态

我们使用李未院士的P过程记法^[35]来描述和定义系统状态.

假设运行计算单元集合为A_r={a₁, a₂, …, a_t}, 等待计算单元集合为A_w={a_t+1, a_t+2, …, a_n}, a_i的工作对象集合为RW(a_i)={x_ij|j=1, 2, …, t_i}, 其中, i=1, 2, …, n, t_i表示a_i的工作对象的个数.对象x_ij的取值范围表示V_ij.x_ij的初始值为$s_{ij}^0$.假设a_i有m_i条指令, 在执行完k条指令后, 集合RW(a_i)中的对象x_ij的值为$s_{ij}^k$, k=1, 2, …, m_i.

因此, 工作对象集合RW(a_i)的值空间为

$ \prod\nolimits_{j = 1}^{{t_i}} {{V_{ij}}} $

(1)

表示为VRW(a_i).软件计算单元a_i的语义可以表示为映射:$\prod\nolimits_{j = 1}^{{t_i}} {{V_{ij}}} \to \prod\nolimits_{j = 1}^{{t_i}} {{V_{ij}}} .$

我们将笛卡尔积:

$ \prod\nolimits_{i = 1}^n {\prod\nolimits_{j = 1}^{{t_i}} {{V_{ij}}} } $

(2)

称为系统对象状态集合, 记为S_D.

除了公式(2)中的对象外, 系统存储器中还存在着多个空闲存储空间片段, 这些片段的位置与数量是不断变化的.为了便于分析系统对象状态, 我们对包括寄存器、缓存、内存等在内的所有存储单元在表达方式上统一进行编号, 这些编号全体属于自然数集合N, 我们将其标记为N', N' N.

每个数据对象都有自己的类型, 都对应于一个或者若干个连续的存储单元.例如, 32位的整型变量的存储单元为{ & y, & y+1, & y+2, & y+3}, 一共4个编号连续的存储单元, 我们用区间[ & y, & y+3]表示这个存储单元的集合, 下面称其为N'的子区间.如果当前系统具有n个进程{p_i|i=1, 2, …, n}, 其中, 进程p_i的工作对象集合为{x_ij|j=1, 2, …, t_i}.这些对象对应于N'的t_i个互不相交的子区间{N_ij|j=1, 2, …, t_i; i=1, 2, …, n}.除了对象{x_ij|j=1, 2, …, t_i}所占据的N'中的这些互不相交的子区间, 我们假设仍然剩余t₀个互不相交的子区间未被占用, 这些子区间表示为{N_0j|j=1, 2, …, t₀}, 对应的数据对象表示为{x_0j|j=1, 2, …, t₀}.显然, 这两部分的子区间, 即{N_ij|j=1, 2, …, t_i; i=0, 1, …, n}仍然是互不相交的, 并且$\bigcup\nolimits_{i = 0}^n {\bigcup\nolimits_{j = 1}^{{t_i}} {{N_{ij}}} } = N'$.不失一般性, 我们假设未被占用的这部分子区间{N_0j|j=1, 2, …, t₀}的取值为0, 原因在于新分配的数据对象的值都会被初始化成0.

3.3 事件

在每一个时钟周期, 每个设备都有可能产生硬件中断, 这些中断会改变正在运行的软件计算单元集合A_r; 同时, CPU的异常也会改变A_r.我们将在时钟周期中产生的软/硬件中断和异常称为当前到达事件, 记为E_a.对应地, 之前到达的事件或者等待被处理的事件称为等待事件, 记为E_w.正在被处理的事件称为运行事件, 记为E_r.显然, 系统对象状态S_D、当前到达事件E_a、等待事件E_w、正在运行的软件计算单元A_r和正在等待的软件计算单元集合A_w共同决定了接下来的E_r, E_w, A_r和A_w.

3.4 VSOS系统状态模型的框架

在以上分析的基础上, 我们认为, 计算机系统的运行过程可以被描述成一系列的计算单元并行地操作着存储器中的数据对象, 如图 2所示.

从软件的角度来说, 我们可以假设硬件计算单元以互斥的方式进行工作.因此, 影响系统运行的因素包括数据对象和存储器中的指令序列以及达到事件集合.综上所述, 在一定程度上, 计算系统和一个状态自动机(state automaton)模型是相符的^[36], 主要有以下几个理由:接受的事件对象集合对应于状态自动机的字母表(alphabet); 系统运行过程中处理的所有事件构成状态自动机接受的一个句子(sentence); 在每个时钟周期结束时, 存储器的状态和达到的事件构成状态自动机的当前状态(current state); 硬件计算单元对存储器单元的修改动作对应于状态自动机的状态转化(state transition); CPU执行halt指令的状态对应于状态自动机的终止状态(termination state).在此基础上, 我们来构建VSOS的系统状态模型.

定义1(VSOS的系统状态模型). VSOS的系统状态模型是一个状态自动机, 即A_VSOS=(S, Σ, δ, s₀, Γ), S, Σ, δ, s₀和Γ的定义如下:

(1)  系统状态:S=(S_D, A_r, A_w, E_r, E_w):

  a)  对象状态S_D:系统对象状态;

  b)  正在运行的软件计算单元集合A_r:占有硬件计算单元并正在运行的软件计算单元集合;

  c)  等待运行的软件计算单元集合A_w:正在等待占有硬件计算单元的软件计算单元集合;

  d)  运行事件E_r:被系统选中并正在处理的事件集合;

  e)  等待事件E_w:等待被处理的事件集合;

(2)  Σ是系统所接受的各种事件;

(3)  状态转化函数δ:δ(s, E_a)=s';

(4)  s₀是系统的初始状态;

(5)  Γ是系统的终止状态集合, Γ S.当系统到达Γ中的状态时, 系统就终止.

4 VSOS系统状态模型在Isabelle/HOL中的构建

上一节分析了构成VSOS系统状态模型的基本要素--硬件/软件计算单元、系统对象状态、事件, 并在这些基本要素的基础上阐述了VSOS系统状态模型.本节首先对我们采用的Isabelle/HOL环境做介绍, 并在此基础上阐述VSOS论域以及在Isabelle/HOL中形式化地构建VSOS系统状态模型的方法.

4.1 Isabelle/HOL定理证明器环境

Isabelle/HOL是一款可以对系统规格说明进行描述和验证的定理证明器.Isabelle是针对逻辑形式化理论的通用系统, Isabelle/HOL是Isabelle对于高阶逻辑(higher-order logic, 简称HOL)的规格说明和实现.在Isabelle/HOL环境中, 提供了强大的对象描述和规格说明表达的能力, 以及对于命题定理的证明方法.

Isabelle/HOL是一个类型系统, 具有多种预定的基本类型描述, 如自然数nat、整型int、列表list等.用户可以采用函数式编程(functional programming)的方式来构建新的类型, 如记录类型record和自构造数据类型datatype, 并可以构造各种函数, 如原始递归函数primrec、全函数fun, 以及各种引理lemma和定理theorem.在Isabelle/HOL环境中, 特定域(special domain)以称为理论的方式进行构造, 如theory, 为此, 每个特定域可以认为是类型、定义、函数和定理证明的集合.

在这一节, 针对下面的章节将使用到的Isabelle/HOL符号和操作进行说明.

自构造数据类型datatype可以用于构造复合的数据类型, 例如, 对于系统的运行状态级别在Isabelle/HOL中可以定义为:datatype ring=user_level|root_level, 新数据类型ring由构造子user_level和root_level组成, 分别表示用户级模式和内核级模式.

记录类型record用于构造包含多个成员的复合类型, 例如, 对于消息类型在Isabelle/HOL中可以定义为:

record message=sender::pid

      receiver::pid

      content::data

新类型message包含3个成员:发送者标识sender和接收者标识receiver, 类型为pid; 以及消息内容content, 类型为data.而类型pid和data可以是新的自定义类型.对于record类型的更新操作, 例如, 假设message类型的一个实例为msg, 值为(|sender=p1, receiver=p2, content=msg_c1|), 对于更新操作形如msg(|content:=msg_c2|), 表示将msg的content成员更新为msg_c2, 而其他成员不变.

4.2 VSOS论域

如第3节所述, 系统对象状态以及状态转化关系可以用数学系统--论域来表示^{[35, 37]}, 记为Μ.M包含3个部分:第1部分是非空元素集合m, 它可以用来描述各个进程的工作对象的所有可能的取值的集合, 显然, $\prod\nolimits_{i = 1}^n {\prod\nolimits_{j = 1}^{{t_i}} {{V_{ij}}} } $是m的一个子集; 第2部分是m上的非空函数的集合F, 从软件的角度来看, F中的函数的语义可以表达成这个函数的工作对象集合的取值空间上的一个映射, 即, 表示一个行为体如何通过工作对象集合的初始值计算出工作对象集合结束时的值; 第3部分是关于m的非空命题的集合P, 用于描述系统的性质或者F中函数的条件, 如当前的进程的地址空间不相交等性质, 或者前置/后置条件等.

系统状态、软/硬件计算单元的操作以及以命题方式表达的系统的属性组成VSOS的论域, 记为M_Computer.相应地, 在Isabelle/HOL中, 对应的VSOS论域表示为M_Isabelle/HOL.根据VSOS的设计和实现, 我们构造论域M_Isabelle/HOL.M_Computer中的数据对象和行为操作语义与M_Isabelle/HOL中描述的对象和行为定义是一一对应的, 为此, 我们可认为M_Computer和M_Isabelle/HOL是同构的^[37], 同时, M_Computer中的命题成立当且仅当M_Isabelle/HOL中的命题成立.

如图 3所示, 我们通过构造M_Isabelle/HOL和M_Computer来建立VSOS和逻辑系统之间的联系.我们通过构造VSOS系统状态模型来设计和实现VSOS.在VSOS实现的基础上, 我们描述域M_Computer以及和M_Computer同构的M_Isabelle/HOL.因此, 对于VSOS的功能性和安全性的属性, 可以映射为M_Isabelle/HOL中的逻辑命题和公式.我们通过在Isabelle/HOL逻辑系统中以推理的方式来验证VSOS设计和实现的正确性和一致性.

4.3 在Isabelle/HOL中构建VSOS系统状态模型

VSOS系统状态模型的基本元素包括系统状态集合S和状态转化函数δ.S中的每个元素是由所有当前进程的数据对象的值构成的向量.所有事件处理函数和功能性函数构成状态转化函数δ.每个状态转化函数的语义是根据功能性语义将数据对象的初始值转化为结果值.

下面阐述在Isabelle/HOL中构建VSOS系统状态模型的方法.

我们从汇编级对VSOS系统状态模型进行描述, 根据第3.4节和第4.2节的分析, 以定义1所描述的VSOS系统状态模型为基础, 我们在Isabelle/HOL中对VSOS系统状态模型从汇编级建立抽象模型, 我们对该抽象模型定义如下:

state=(M, R, IF, ZF, SF, ring, GDT, IDT)

M={nat→mem_cell}*

mem_cell=null|SomeInt int|SomeInstr instr

R={register→int}*

register=ds|es|fs|gs|di|si|fp|st|

ax|bx|cx|dx|bp|sp|pc

ring=user_level|root_level

GDT={nat→int}*

IDT={nat→int}*

instr=instr_nop|instr_fault|instr_excp

|movrr register register|movrm register nat

|movmr nat register|movrd register int

|movar register register|movra register register

|add register register|sub register register

|jmp int|jmpPC int|branch register register int

|call int|ret|iret|cli|sti

|pushr register|pushv int

|pushra register|pop register

|swint int|hwint int

|Or register register

|And register register

…

其中, state为系统状态, 包括内存状态M、寄存器状态R、条件标志(中断允许标志IF、零标志ZF、符号标志SF)、运行级别ring、全局描述符表状态GDT和中断描述符表状态IDT.指令类型instr包括对Intel X86架构下的常用指令的描述以及空指令(instr_nop)、指令错误(instr_fault)和指令异常(instr_excp)等.

类型instr中, 各个指令的操作语义见表 1, 其中, [M(n)]表示内存单元M(n)中的数据.

对于表 1中各个指令的操作语义, 在Isabelle/HOL中定义如下:

fun NextS::“state⇒instr⇒state” where

“NextS s(movrr y x)=PCinc(s(|R:=((R s)(x:=((R s) y)))|))”|

…

其中, 函数PCinc表示对PC寄存器进行递增操作, 定义如下:

fun PCinc::“state⇒state” where

“PCinc s=s(|R:=((R s)(pc:=((R s) pc)+1))|)”

函数NextS的语义是对指令的单步执行操作, 对于指令序列的操作, 可以递归地调用NextS来实现.对于空指令(instr_nop), 函数NextS将修改PC寄存器(递增); 对于指令错误(instr_fault)和指令异常(instr_excp)等情况, 函数NextS分别转入指令出错处理和指令异常处理过程.

5 系统初始化过程汇编级验证

限于篇幅, 在这一节中, 以中断描述符表IDT为例, 阐述对系统初始化过程汇编级验证的方法.

在VSOS中, 建立IDT如下:

struct GateDescriptor {

  uint_32 offset_15_0: 16;

  uint_32 segment: 16;

  uint_32 pad0: 8;

  uint_32 type: 4;

  uint_32 system: 1;

  uint_32 privilege_level: 2;

  uint_32 present: 1;

  uint_32 offset_31_16: 16;

};

struct GateDescriptor idt[];

VSOS使用init_segment()函数以及set_segment()函数来初始化全局描述符表GDT, 并使用init_idt(), set_trap()和set_intr()来初始化IDT.在初始化后, IDTR寄存器指向IDT表对象.在系统镜像刚加载到内存后, IDT表刚被定义并且尚未被赋予正确的值, 这时, 由初始化的模块对IDT表进行赋值.

IDT表的初始化代码(C语言、汇编语言部分)如下所示:

void set_trap (

  struct GateDescriptor *ptr,

  uint_32 selector,

  uint_32 offset, uint_32 dpl)

{

  ptr→offset_15_0=offset;

  ptr→segment=selector;

  ptr→pad0=0;

  ptr→type=TRAP_GATE_32;

  ptr→system=FALSE;

  ptr→privilege_level=dpl;

  ptr→present=TRUE;

  ptr→offset_31_16=

    (offset > > 16) & 0xFFFF;

}

push %ebp

mov %esp, %ebp

…

mov 0x10(%ebp), %eax

mov %eax, %edx

mov 0x8(%ebp), %eax

mov %eax, %edx

…

在汇编级抽象模型的基础上, IDT表的初始化过程对应的Isabelle/HOL定义如下:

definition set_trap::“Code” where

  “set_trap==

  pushr ebp;

  movrr esp ebp;

…

  movirr 4 ebp eax;

  movrr eax edx;

  movirr 2 ebp eax;

  movrir edx;

…”

在上述对IDT表的初始化过程的定义中, 指令movirr n reg1 reg2的语义是将内存地址reg1+n处的值赋给寄存器reg2.在set_trap的定义中, ebp+4指向参数的偏移地址.因此, movirr 4 ebp eax将参数的偏移地址赋给eax寄存器, 在执行完set_trap后, 其语义为对IDT表进行了预期的赋值.

在完成对系统初始化过程的功能语义的定义后, 为了验证这些功能语义的正确性, 我们需要在Isabelle/ HOL中给出这些正确性的命题公式, 以此作为验证的目标.针对IDT初始化过程的正确性命题公式是:

…

s.M(idt_base+offset_low)=addr_low

s.M(idt_base+idt_segment)=segment

…

s.M(idt_base+idt_flag)=flag

s.M(idt_base+offset_high)=addr_high

…

其中, s为状态对象, s.M表示内存状态, s.M(idt_base+offset_low)表示内存位置idt_base+offset_low处的值.公式s.M(idt_base+offset_low)=addr_low说明在内存位置idt_base+offset_low处被正确地赋值了addr_low.

6 系统功能模块的汇编级验证

限于篇幅, 本节以VSOS微内核消息处理为例, 阐述在Isabelle/HOL中如何在第4.3节中阐述的汇编级抽象模型的基础上对VSOS的功能模块在汇编级进行验证的方法.

现以VSOS微内核消息处理模块的发送消息函数sys_send在汇编级的正确性证明为例, 阐述对VSOS的功能模块在汇编级进行验证的方法.sys_send功能函数的工作对象集合主要包括发送进程和接收进程的进程控制块(process control block, 简称PCB).

sys_send的C代码和汇编代码:

int sys_send (

  struct proc *caller_ptr,

  int dst, message *m_ptr,

  unsigned flags)

{ struct proc*dst_ptr=

     get_proc_from_pid(dst);

…

copy_mess(m_ptr,

dst_ptr→p_messbuf, sizeof(message));

…}

‹sys_send›:

 push %ebp

 movl %esp, %ebp

 subl $0x28, %esp

 movl 0xc (%ebp), %eax

 movl %eax, (%esp)

 call c0101128

…

movl %eax, 0x4(%esp)

movl 0x10(%ebp), %eax

movl%eax, (%esp)

callc010116d ‹copy_mess›

…

在第4.3节汇编级抽象模型的基础上, sys_send功能函数的功效在Isabelle/HOL中定义如下:

definition sys_send::“Code” where

“sys_send==

pushr ebp;

movrr esp ebp;

subir10esp;

movirr3ebp eax;

movrir eax0esp;

call get_proc_from_pid;

…

movrir eax1esp;

movirr4ebp eax;

movrir eax0esp;

call copy_mess;

…”

在对sys_send语义定义的基础上, 下面从汇编级对其正确性命题进行分析.

我们尝试从汇编级对系统功能模块的语义正确性进行验证, 定义的正确性命题需要保证在任何可信状态下, 功能模块运行的语义都能满足这些正确性命题.对于sys_send功能语义的正确性命题可以定义如下:

$ \forall s, Q\left( s \right) \wedge s' = NextnS\left( {sys\_send, \mathit{s}} \right) \to P\left( {s, s'} \right) $

(3)

其中, NextnS(sys_send, s)表示在执行完sys_send的功能语义后的状态, 即, 多步执行后的效果(状态).为此, 上述公式表示当开始状态s满足条件谓词Q时, sys_send能正确地将消息发送给目标进程, 即, 开始状态s和结束状态s'满足条件谓词P(s, s').值得一提的是, 并不是所有的状态都可以满足谓词Q, 对于不满足Q的状态可以不做考虑.在公式(3)中, 条件谓词P可以作为函数sys_send的功能语义表述, 而Q作为初始条件.为此, 针对sys_send, 谓词Q定义如下:

$ Q(s) \equiv (s.regs.sp + 1 = caller\_ptr) \wedge (s.regs.sp + 2 = dst) \wedge (s.regs.sp + 3 = m\_ptr) $

(4)

公式(4)表明, sys_send函数所需的参数存放在栈中合适的位置, 并且拥有正确的值.

当发送进程将消息发给接收进程, 并且接收进程也在等待发送进程时, sys_send将发送进程消息缓冲区中预期长度的字节数复制到接收进程的缓冲区中.因此, sys_send的正确性条件是这两个内存区间的值应该相同, 也就是说, 这两个消息缓冲区中的消息体相同.该正确性条件的描述如下:

$ \begin{array}{l} P\left( {s, s'} \right) \equiv CmpM\left( {s', s.M\left( {s.regs.sp + 3} \right), } \right.\\ s'.M\left( {proc + sizeof\_proc*s.M\left( {s.regs.sp + 2} \right) + p\_messbuf} \right)\\ \left. {, sizeof\_msg} \right) \end{array} $

(5)

其中, 辅助函数CmpM的定义如下:

$ CmpM\left( {s, p, q, n} \right) \equiv \left( {i \ge 0 \wedge i \le \left( {n-1} \right)} \right) \to \left( {s.M\left( {p + i} \right) = s.M\left( {q + i} \right)} \right) $

(6)

对于上述公式(3)的证明, 我们通过展开NextnS(sys_send, s)操作, 即多步执行后的效果, 并根据第4.3节所描述的指令的操作语义, 从而验证执行完sys_send之后的状态是否满足后置条件P.

VSOS验证环境配置见表 2.VSOS汇编级的Isabelle/HOL验证工程量见表 3, 完整的验证耗时18min左右.

VSOS的完整性证明包括验证在系统运行过程中保持系统代码完整性和数据完整性以及系统功效的完整性.系统代码完整性和数据完整性是指代码和数据不可被恶意地修改, 这些可以通过访问控制策略实现.系统功效的完整性是指系统的功能行为始终能完成系统设计所期望的效果.VSOS微内核的可靠性证明是指验证微内核在运行过程中, 不存在非预期的行为和恶意行为, 即, 系统行为导致的系统安全状态可达性问题.VSOS的验证结果如图 4所示, No subgoals表明通过交互式的验证策略证明了命题目标.

7 结论

本文提出了一种OS系统状态模型, 作为VSOS汇编语言层设计和验证的纽带, 通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域, 并以此来描述VSOS汇编层的论域.在此基础上, 通过给出汇编层的功能模块的正确性命题并借助Isabelle/HOL定理证明器来验证汇编层的功能模块的正确性, 以此保证VSOS汇编语言层模块功效的正确性.

对于VSOS的完整验证, 从系统实现的代码量和验证的代码量的比例的标准来看, 我们达到了平均情况下1:10的量, 可以认为我们的方法是可行和高效的.不可否认的是, 整个验证过程共耗费了18人年的工作量, 这是一项非常耗时的研究工作.为此, 如何高效地采用模块化的验证策略, 以及验证的复用问题, 是我们接下来工作的主要方向.

值得一提的是, 我们通过构造论域M_Isabelle/HOL和M_Computer来建立VSOS和逻辑系统之间的联系.M_Isabelle/HOL是完全形式化的模型, 而M_Computer是半形式化的模型, 例如对于硬件和客观环境等信息的描述是非形式化的, 从严格意义上来讲, M_Isabelle/HOL和M_Computer之间的同构性问题是需要经过严格的形式化验证的, 我们计划从模型论(model theory)和类型论(type theory)的角度来严格地形式化描述和验证M_Isabelle/HOL和M_Computer之间的同构性问题, 这也是我们未来工作的重点.

致谢 本文作者感谢所有匿名审稿者, 感谢您们对本文提出宝贵的意见.