论文部分内容阅读
摘要：随着工业上广泛采用基于模型的开发(model-based development.MBD)的工具，这正在改变工业上因为采用形式化方法所带来的花费和效益的平衡。形式化方法例如模型检测融合到软件开发环境中能降低费用和使复杂的检测能自动和严密的进行。该文主要用一个实际应用来说明软件安全性重要性和模型检测怎样降低其费用。
关键词：MBD；模型检测；NuSMV；规约
中图分类号：TP368.6文献标识码：A文章编号：1009-3044(2011)09-2028-02
无论从哪个方面来看，近年来已大量的用于商用和军用对安全性要求极高的密码协议软件，其大小和复杂性呈指数级增长。当前的验证方法已经不能有效的应对下一代密码协议软件。一些新的验证过程被发展增加分析技巧的测试，例如形式化方法。这些方法将帮助密码协议软件以一个合理的花费来验证从而达到要求的安全级别。
在过去形式化的方法没有广泛的使用主要有以下几个障碍：
1）构造单独分析模型的费用。
2）所构建模型和所设计的软件保持一致性的困难。
3）建模和分析使用一些不为大家所熟悉的符号。
4）没有足够的工具来应对工业化的问题
广泛传播和使用的MBD工具正在扫除前三个障碍。MBD倾向于使用占统治地位的描述（经常用图型）建模语言，这就使得实际的系统被构建之前可以在仿真的环境下执行。使用这样的建模语言允许工程师创造一个系统模型，在他们自己的桌上执行。更进一步工具现在发展到可以把设计模型翻译成分析模型从而可以被形式化的方法工具所检验，结果会返回到原始的模型等号中。这个过程支持原来的建模成果并且允许工程师在他们的领域用他们所熟悉的符号。
快速提高分析算法和由摩尔法则所预言的CPU性能稳定提升而价格下降正在消除第四个障碍。更快的算法和更便宜的硬件意味着在十年前不能分析完成的任务现在只是一秒钟的事情。
1 模型检测
模型检测机有着高度的自动化，要求很少或不要求使用者的交互。一个模型检测机将考虑每个可能的状态和输入的组合来决定是否满足系统所要求的一系列的属性。如果其中有某一个不满足，模型检测机将会给出一个反例来显示那个属性是怎么样违反的。
这里有许多类型的模型检测机，每一个都有自己的长处和短处。我们有以BBDs为基础的模型檢测器NuSMV可以分析超过10的120次方空间。以可满足性数模理论（Satisfiability modulo theoryies SMT）为基础的模型检测器例如SAL和Prover使用一种归纳的形式能自动的证明模型所持属性。这允许检测器可以处理很大级别的模型，甚至包括无限状态空间模型。暗示的状态模型检测器例如二分图（Binary Decision Diagrams BDDs）存取每一个经历的状态的代表符号。这样暗示模型检测器可以允许处理比明示模型检测器要大得多的状态空间。明示的状态模型检测器例如SPIN直接执行形式化模型并且存储每一个经历的状态。在一些情况下这使得以SMT为基础的模型检测器比明示或暗示状态空间模型检测器更难使用。
发展更有效率且更强算法的模型检测是当前研究的一个热点。在过去的十年我们已经取提了很大的提高，分析模型所要时间我们已经减少了几个数量级，且大大提高了可以分析模型的尺寸和复杂度。摩尔法则更进一步提高CPU的频率且价格更低使我们桌面电脑有更强的能力。所在这些都意味着更强大的模型检测工具可以为工程师所得到来分析工业级的规模的问题。
2 验证过程
在以分析为基础的验证过程，我们一般认为对于一个特定的子系统有功能相关的要求。环境假定和约束限定了执行的环境。属性限定了子系统的行为（输出值或状态变量），该行为必须保证在指定的假定环境中所在的系统状态可以达到。属性其实就是一个简单且精确的反映其我们将要分析的系统需求的规约。
在需求被详细说明成待检验的属性，模型已经被构建来执行需求，这时形式化的分析可以开始了。模型被翻译成模型检测工具所认识的语言然后检验其属性。模型检测器然后执行其分析得出结果，要么报告属性是正确的，或提供一个反例来说明违反了其属性。
使用模型检测器的一个优点就是如果违反了属性可以产生一个反例，该反例可以确切的显示属性是怎么样违反的。这就给开发者提供了一个指导，即什么错了怎么样去改正它。仅仅通过模型检测器的输出对于一个大的系统是非常困难且很需要时间去判定错误的根本原因，但仿真的MBD工具这时就可以来重放其反例。
当一个反例被发现的时候，要采取正确行动来改正它。产生反例的原因可能是下面当中的其一：
1）需求错误
2）模型错误
3）属性形式化错误
4）不正确或丢失子系统的不变量
在实际中模型检测器从一组违反属性中可能产生一个在真实环境中没有意义的一个反例，即产生的反例在真实环境中不可能发生的。为了去掉这些在真实系统中不可能的反例，有时需要一些环境的约束。这些约束作为一个精确的环境假设的描述.
3 NS协议实际应用
我们最初的尝试是使用该方法应用在一个实际的例子是Needham-Schroeder(NS)协议是使用密钥分发中心KDC(KeyDistribution Center)实现认证的经典协议. 对称密码体制NSSK协议按功能划分为两个部分:获取共享密钥和双方身份认证。协议分析前提:完善保密(perfect encryption)前提,即协议采用的密码算法是完善保密的;参与协议运行的主体除了诚实的合法用户外,还有不怀好意的入侵者;入侵者的知识与能力,即使不知道加密部分的内容,也可重放他所看到的任何消息。
NS协议模式逻辑非常适合使用我们的翻译框架来和形式化的模型检测器例如NuSMV来分析。我们分析其模式逻辑由五个模式转换图，总共10个模式中，51个事件，85个转换。每一个模式图中一个状态的改变会至少影响一个，经常是多个别的模式图。即便每个单个的图可以直接的理解，但能抓住图之间的交互是非常困难的。
分析其早期模式逻辑的规约我们发现了3个错误。其中3个错误中的2个我们发现如果用传统的方法如测试方法是不能发现其错误的。
用这个分析方法其中一个主要优点当需求仍然在开发阶段的时候我们在研发过程早期就可以进行分析了。
4 结束语
当前的研究主要集中进一步扩大模型检测器能有效应用检测模型的范围。我们的框架可以处理整型和定点数的类型，但新的分析方法需要要能处理更多的数据类型，如浮点数和非线性方程等。从分析算法的角度SMT模型检测器显得有非常好的前途。
随着MBD工具的越来越流行，模型检测器的功能越来越强大，使得形式化验证成为商业的实际应用。这解决了主要障碍中的一个，即在软件工程师所用的商用模型工具和已经存在的形式化验证工具架起了桥梁。这就让模型检测可以整合到开发过程从而模型可以自动分析，且不用付出很大的努力。
通过所做的一些检测案例我们感觉模型检测有很大的实际应用前途。我们可以在开发早期发现且改正设计错误，其中很多错误是通过测试是很难发现的。在研发早期消灭错误可以大大地减少整个软件开发的费用。
参考文献：
[1] Gerard Holzmann.The SPIN Model Checker: Primer and Reference Manual[J].Addison-Wesley Professional,2003(6).
[2] Edmund Clarke,Orna Grumberg,DoronPeled.Model Checking[M].The MIT Press,Cambridge,Massachusetts,2001.
关键词：MBD；模型检测；NuSMV；规约
中图分类号：TP368.6文献标识码：A文章编号：1009-3044(2011)09-2028-02
无论从哪个方面来看，近年来已大量的用于商用和军用对安全性要求极高的密码协议软件，其大小和复杂性呈指数级增长。当前的验证方法已经不能有效的应对下一代密码协议软件。一些新的验证过程被发展增加分析技巧的测试，例如形式化方法。这些方法将帮助密码协议软件以一个合理的花费来验证从而达到要求的安全级别。
在过去形式化的方法没有广泛的使用主要有以下几个障碍：
1）构造单独分析模型的费用。
2）所构建模型和所设计的软件保持一致性的困难。
3）建模和分析使用一些不为大家所熟悉的符号。
4）没有足够的工具来应对工业化的问题
广泛传播和使用的MBD工具正在扫除前三个障碍。MBD倾向于使用占统治地位的描述（经常用图型）建模语言，这就使得实际的系统被构建之前可以在仿真的环境下执行。使用这样的建模语言允许工程师创造一个系统模型，在他们自己的桌上执行。更进一步工具现在发展到可以把设计模型翻译成分析模型从而可以被形式化的方法工具所检验，结果会返回到原始的模型等号中。这个过程支持原来的建模成果并且允许工程师在他们的领域用他们所熟悉的符号。
快速提高分析算法和由摩尔法则所预言的CPU性能稳定提升而价格下降正在消除第四个障碍。更快的算法和更便宜的硬件意味着在十年前不能分析完成的任务现在只是一秒钟的事情。
1 模型检测
模型检测机有着高度的自动化，要求很少或不要求使用者的交互。一个模型检测机将考虑每个可能的状态和输入的组合来决定是否满足系统所要求的一系列的属性。如果其中有某一个不满足，模型检测机将会给出一个反例来显示那个属性是怎么样违反的。
这里有许多类型的模型检测机，每一个都有自己的长处和短处。我们有以BBDs为基础的模型檢测器NuSMV可以分析超过10的120次方空间。以可满足性数模理论（Satisfiability modulo theoryies SMT）为基础的模型检测器例如SAL和Prover使用一种归纳的形式能自动的证明模型所持属性。这允许检测器可以处理很大级别的模型，甚至包括无限状态空间模型。暗示的状态模型检测器例如二分图（Binary Decision Diagrams BDDs）存取每一个经历的状态的代表符号。这样暗示模型检测器可以允许处理比明示模型检测器要大得多的状态空间。明示的状态模型检测器例如SPIN直接执行形式化模型并且存储每一个经历的状态。在一些情况下这使得以SMT为基础的模型检测器比明示或暗示状态空间模型检测器更难使用。
发展更有效率且更强算法的模型检测是当前研究的一个热点。在过去的十年我们已经取提了很大的提高，分析模型所要时间我们已经减少了几个数量级，且大大提高了可以分析模型的尺寸和复杂度。摩尔法则更进一步提高CPU的频率且价格更低使我们桌面电脑有更强的能力。所在这些都意味着更强大的模型检测工具可以为工程师所得到来分析工业级的规模的问题。
2 验证过程
在以分析为基础的验证过程，我们一般认为对于一个特定的子系统有功能相关的要求。环境假定和约束限定了执行的环境。属性限定了子系统的行为（输出值或状态变量），该行为必须保证在指定的假定环境中所在的系统状态可以达到。属性其实就是一个简单且精确的反映其我们将要分析的系统需求的规约。
在需求被详细说明成待检验的属性，模型已经被构建来执行需求，这时形式化的分析可以开始了。模型被翻译成模型检测工具所认识的语言然后检验其属性。模型检测器然后执行其分析得出结果，要么报告属性是正确的，或提供一个反例来说明违反了其属性。
使用模型检测器的一个优点就是如果违反了属性可以产生一个反例，该反例可以确切的显示属性是怎么样违反的。这就给开发者提供了一个指导，即什么错了怎么样去改正它。仅仅通过模型检测器的输出对于一个大的系统是非常困难且很需要时间去判定错误的根本原因，但仿真的MBD工具这时就可以来重放其反例。
当一个反例被发现的时候，要采取正确行动来改正它。产生反例的原因可能是下面当中的其一：
1）需求错误
2）模型错误
3）属性形式化错误
4）不正确或丢失子系统的不变量
在实际中模型检测器从一组违反属性中可能产生一个在真实环境中没有意义的一个反例，即产生的反例在真实环境中不可能发生的。为了去掉这些在真实系统中不可能的反例，有时需要一些环境的约束。这些约束作为一个精确的环境假设的描述.
3 NS协议实际应用
我们最初的尝试是使用该方法应用在一个实际的例子是Needham-Schroeder(NS)协议是使用密钥分发中心KDC(KeyDistribution Center)实现认证的经典协议. 对称密码体制NSSK协议按功能划分为两个部分:获取共享密钥和双方身份认证。协议分析前提:完善保密(perfect encryption)前提,即协议采用的密码算法是完善保密的;参与协议运行的主体除了诚实的合法用户外,还有不怀好意的入侵者;入侵者的知识与能力,即使不知道加密部分的内容,也可重放他所看到的任何消息。
NS协议模式逻辑非常适合使用我们的翻译框架来和形式化的模型检测器例如NuSMV来分析。我们分析其模式逻辑由五个模式转换图，总共10个模式中，51个事件，85个转换。每一个模式图中一个状态的改变会至少影响一个，经常是多个别的模式图。即便每个单个的图可以直接的理解，但能抓住图之间的交互是非常困难的。
分析其早期模式逻辑的规约我们发现了3个错误。其中3个错误中的2个我们发现如果用传统的方法如测试方法是不能发现其错误的。
用这个分析方法其中一个主要优点当需求仍然在开发阶段的时候我们在研发过程早期就可以进行分析了。
4 结束语
当前的研究主要集中进一步扩大模型检测器能有效应用检测模型的范围。我们的框架可以处理整型和定点数的类型，但新的分析方法需要要能处理更多的数据类型，如浮点数和非线性方程等。从分析算法的角度SMT模型检测器显得有非常好的前途。
随着MBD工具的越来越流行，模型检测器的功能越来越强大，使得形式化验证成为商业的实际应用。这解决了主要障碍中的一个，即在软件工程师所用的商用模型工具和已经存在的形式化验证工具架起了桥梁。这就让模型检测可以整合到开发过程从而模型可以自动分析，且不用付出很大的努力。
通过所做的一些检测案例我们感觉模型检测有很大的实际应用前途。我们可以在开发早期发现且改正设计错误，其中很多错误是通过测试是很难发现的。在研发早期消灭错误可以大大地减少整个软件开发的费用。
参考文献：
[1] Gerard Holzmann.The SPIN Model Checker: Primer and Reference Manual[J].Addison-Wesley Professional,2003(6).
[2] Edmund Clarke,Orna Grumberg,DoronPeled.Model Checking[M].The MIT Press,Cambridge,Massachusetts,2001.