操作系统安全【四】：形式化规范与验证

     形式化规范这部分对于自己来说太抽象了，全部是理论，还有数学公式之类的罗列，这里不再详细的笔记了，只是说说自己的理解和一些感觉重要的地方吧！
     我们设计安全操作系统当然希望它可以达到一定的安全级别，但是我们无法形式地规定对于一个系统而言什么是“安全“，我们需要借助科学的语言——数学来进行描述和证明——一是说明我们的系统没有目前任何可以想到的”缺陷“，二是说明我们的系统满足所有安全要求的属性。这样的过程就是形式化技术。所以说形式化程序规范和验证技术是研制高安全等级安全操作系统的一个必要的保障手段。
     形式化验证的目的在于提供一种允许在一个计算机系统的功能规范生成、开发过程和验证过程中使用一种严格的数学注释，从而使得对一个系统的一致性、完备性和正确性可以用一种系统的方式来获得。形式化验证技术相关的两种最主要的方法是证明检查器和模型检查器，形式验证技术的主要目的是提高系统的可信度。
     为了有效降低安全操作系统设计中形式化验证工作的复杂程度，在验证过程中常采用层次分解技术，而层次分解技术主要有数据结构精化、算法精化和过程抽象等。一个典型的形式化安全验证系统至少要由规范语言处理器、验证条件生成器和定理证明器等构成。
      定理证明器：处理由一个规范处理器或者一个验证条件生成器所产生的公式。
     规范语言处理器是指从数学、逻辑和程序设计中派生出的形式化注释，它们的目的是用一种简捷的详细方式精确地陈述由一个给定程序系统所提供的功能；一个功能规范就是对一个系统的输出时如何和它的输入最恰当的描述。
     验证条件生成器：把一个程序和有关这个程序的一些断言作为输入，生成用一宣城这两者是一致的公式；通过把有关程序变量值的断言插入到不同点的方式，一个程序就被准备为一个验证条件生成器的输入。