论文部分内容阅读
软硬件在关键领域越来越广泛的应用也对其自身的正确性提出了更高的要求。目前，保证正确性有两个办法：工程的方法和数学的方法。第一个办法是建立在经验的累计上，第二个办法是建立在严谨的数学理论上的。在安全攸关的领域中，现在更倾向于在应用工程的办法中加入数学的方法进行保证，这种数学的方法称之为形式化方法。操作系统作为管理、使用计算机资源的一个系统软件，它的正确性和安全性关系到在其上应用的软件，所以在研发的过程中必须用更严谨的办法来保障它的正确以及一些需要具备的性质。文中提出了形式化工具PVS结合自动机模型描述操作系统的方法以及在功能设计阶段数据驱动的描述与验证的方法，并给出相应的例子。
PVS在形式化方法中是一个重要的工具，也越来越被广泛应用，它是基于高阶逻辑的强类型的语言与证明集于一身的工具。这使得描述与验证有了一个统一的环境，不需要分开进行，有时为了进行验证还得对描述进行一些转换。同时，由于操作系统的状态复杂，状态空间的巨大使得模型检验的办法难以实施，这也是选择PVS的一个原因。
确定了工具后就要找办法对系统进行描述和验证。直接从功能出发进行验证的方法有些盲目，从需要验证的性质的角度，比如说隔离机制、完整性，这都可以看成是对对象的保护，也就是在系统的约束下数据的活动范围以及轨迹的限定。那么要实现以及验证这些性质，我们可以从对象(数据)出发，先找到我们需要保护或者约束起范围和轨迹的关键数据，而后从设计中找到对应的访问该对象的所有功能，并通过这些功能检验该对象是否满足要求。从以上考虑的出发，区别于传统的对单个功能或者模块的描述，提出了一种称为“对象驱动的描述”。该方法起于对关键数据的寻找，然后找出跟这些关键数据对应的功能以及安全服务器的约束作为一个整体进行描述以及性质的验证。前期的工作主要是对功能进行验证，下一步是希望利用这些功能的性质得到隔离机制、机密性、完整性等的系统性质。
以上是一个整体思路，具体到如何对某个功能、模块等进行描述的时候采用的是文中提出的PVS结合自动机描述的方法，该方法对系统进行分块进行逐步细化的描述，每一块进行独立的描述并给出记号，最后用递归函数的方法把他们整合在一个函数里。