嵌入式操作系统的形式化验证方法

《嵌入式操作系统的形式化验证方法》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、第４５卷第２期航空计算技术Ｖｏｌ．４５Ｎｏ．２２０１５年３月ＡｅｒｏｎａｕｔｉｃａｌＣｏｍｐｕｔｉｎｇＴｅｃｈｎｉｑｕｅＭａｒ．２０１５嵌入式操作系统的形式化验证方法胡宁，叶宏（中航工业西安航空计算技术研究所，陕西西安７１００６８）摘要：对嵌入式操作系统类安全关键软件，测试、模拟、分析等传统软件验证方法不能保证其正确性，需要使用形式化方法。综述了主流商用嵌入式操作系统所采用的形式化验证方法，分析了操作系统内核不同特性的形式化验证思路。通常对空间隔离、信息流控制、系统调用、进程间通信等的证明采用定理证明方

2、式，而对时间隔离的证明则采用模型检测方式。ｓｅＬ４的通用抽象和逐层精化方法、模型检测和定理证明的混合方法在工程使用中都有前途。关键词：操作系统；形式化验证；定理证明；模型检测；嵌入式软件中图分类号：ＴＰ３１６文献标识码：Ａ文章编号：１６７１-６５４Ｘ（２０１５）０２-００９６-０５FormalVerificationofEmbeddedOperatingSystemsＨＵＮｉｎｇ，ＹＥＨｏｎｇ（Xi′anAeronauticsComputingTechniqueResearchInstitute，AVI

3、C，Xi′an７１００６８，China）Abstract：Ｔｈｅｆｏｒｍａｌｍｅｔｈｏｄｉｓａｂｅｔｔｅｒｔｈａｎｔｈｅｔｒａｄｉｔｉｏｎａｌｓｏｆｔｗａｒｅ-ｅｎｇｉｎｅｅｒｉｎｇａｐｐｒｏａｃｈｅｓ，ｓｕｃｈａｓｔｅｓ－ｔｉｎｇ，ｓｉｍｕｌａｔｉｎｇａｎｄａｎａｌｙｓｉｓ，ｔｏｐｒｏｖｅｔｈｅｃｏｒｒｅｃｔｎｅｓｓｏｆｔｈｅｓａｆｅｔｙｃｒｉｔｉｃａｌｅｍｂｅｄｄｅｄｏｐｅｒａｔｉｎｇｓｙｓｔｅｍ．Ｔｈｉｓｐａｐｅｒｓｕｍｍａｒｉｚｅｓｔｈｅｆｏｒｍａｌｖｅｒｉｆｉｃａｔｉｏｎｍｅｔｈｏｄｕｓｅｄｉ

4、ｎｔｈｅｌｅａｄｉｎｇｃｏｍｍｅｒｃｉａｌｅｍｂｅｄｄｅｄｏｐｅｒａｔｉｎｇｓｙｓｔｅｍ，ａｎｄａｎａｌｙｚｅｓｔｈｅｆｏｒｍａｌｖｅｒｉｆｉｃａｔｉｏｎｉｄｅａｓｏｆｅａｃｈｅｍｂｅｄｄｅｄｏｐｅｒａｔｉｎｇｓｙｓｔｅｍ．Ｗｅｆｏｕｎｄｔｈａｔｍｏｓｔｏｆｔｈｅｖｅｒｉｆｉｃａｔｉｏｎｗｏｒｋｓｏｎｓｐａｔｉａｌｓｅｐａｒａｔｉｏｎ，ｉｎｆｏｒｍａｔｉｏｎｆｌｏｗｃｏｎｔｒｏｌ，ｓｙｓｔｅｍｃａｌｌ，ａｎｄｉｎｔｅｒ-ｐｒｏｃｅｓｓｃｏｍｍｕｎｉｃａｔｉｏｎ（ＩＰＣ）ｕｓｅｔｈｅｔｈｅｏｒｅｍｐｒｏｖ

5、ｉｎｇａｐｐｒｏａｃｈ．Ｔｈｅｖｅｒｉｆｙｉｎｇｔｈｅｔｅｍｐｏｒａｌｓｅｐａｒａｔｉｏｎｕｓｕａｌｌｙｕ－ｓｅｓｔｈｅｍｏｄｅｌｃｈｅｃｋｉｎｇａｐｐｒｏａｃｈ．ＴｈｅｇｅｎｅｒａｌａｂｓｔｒａｃｔａｎｄｒｅｆｉｎｅｍｅｎｔｕｓｅｄｉｎｓｅＬ４ａｎｄｔｈｅｍｉｘｅｄｍｅｔｈｏｄｗｈｉｃｈｉｎｃｌｕｄｅｓｍｏｄｅｌｃｈｅｃｋｉｎｇａｎｄｔｈｅｏｒｅｍｐｒｏｖｉｎｇｉｓｂｅｔｔｅｒｍｅｔｈｏｄｉｎｐｒａｃｔｉｃｅ．Keywords：ｅｍｂｅｄｄｅｄｏｐｅｒａｔｉｎｇｓｙｓｔｅｍｓ；ｆｏｒｍａｌｖｅｒｉｆｉ

6、ｃａｔｉｏｎ；ｔｈｅｏｒｅｍｐｒｏｖｉｎｇ；ｍｏｄｅｌｃｈｅｃｋｉｎｇ；ｅｍｂｅｄｄｅｄｓｏｆｔｗａｒｅ引言式操作系统的安全性成为关注的焦点，用形式化的方法证明嵌入式操作系统的正确性已成为当前工业界和软件规模与复杂性的增大需要新的验证手段。传学术界的热点。业内主流嵌入式操作系统厂商发布的统的软件验证方法（如测试、模拟、分析等）只能尽可安全关键嵌入式操作系统产品，如ＩＮＴＥＧＲＩＴＹ－能发现缺陷，不能保证没有缺陷，而机载等安全关键领１７８Ｂ、ＶｘＷｏｒｋｓＭＩＬＳ２、ＰｉｋｅＯＳ等均开始引入形式化的域的软

7、件规模和复杂性显著提升，质量隐患增大，使传方法，而作为形式化验证最为全面和成功的产品之一统的软件开发和验证方法力不从心。软件形式化验证的ｓｅＬ４，也开始从学术界向工业界推广。方法则可以证明软件特定剖面的一致性或特定属性的本文在概述软件形式化方法的基础上，讨论了国正确性，从而提升软件质量。外知名嵌入式操作系统所使用的形式化方法。本文所网络化作战和无人装备的大量使用使得信息安全选择的都是商业上获得成功的嵌入式操作系统，由于问题成为重点关注的问题，而形式化验证已成为构建领域认证需要或自身安全能力提升需要，开展

8、了针对高安全等级信息安全软件的必要条件。对于需要达到特定属性的形式化验证；而选择ｓｅＬ４是由于其在操作ＩＳＯ／ＩＥＣ１５４０８ＥＡＬ６级或７级认证要求的软件，软件系统的形式化验证方面独树一帜。开发中必须使用形式化的方法。作为安全关键嵌入式系统的核心基础软件，嵌入收稿日期：２０１５－０２－１３修订日期：２０１５－０３－０４基金项目：国家“９７３”计划项目资助（２０１４ＣＢ７４４９００）；民用飞机专项科研项目资助（ＭＪ－Ｓ－２０１２－０５）作者