物联网操作系统: 形式验证与安全认证
IoT operating systems – formal verification and safety/security certification
赵永望 北京航空航天大学 计算机学院
2018年8月
摘要：本文是2018年中国网络安全年会(CNCERT 2018)上的演讲报告。主要讨论(1)物联网操作系统(OS)为何要做形式验证和安全认证，(2)国外关键领域物联网OS形式验证和安全认证的现状，(3)物联网OS形式验证的技术挑战和我们的总体技术框架，(4)我们取得的系列成果及国内外影响。希望为我国自主可控、安全可靠的物联网操作系统发展提供一种思路。
目 录
1. 物联网操作系统
2. 软件很重要，但也很脆弱
3. 软件定义一切的时代，软件由什么定义？
4. 物联网OS为什么要做形式验证和安全认证
5. 形式化验证的效果和成本怎么样
6. 国外物联网OS形式验证/安全认证的现状
7. 物联网OS形式验证的挑战和技术框架
8. 已取得的部分研发成果
- 成果1(需求层): ARINC 653操作系统标准的形式化验证
- 成果2(设计层): 物联网OS的安全与形式化开发
- 成果3(源码层): 并发物联网OS的C代码形式验证
- 成果4(二进制层): 指令集ISA的形式模型
9. 成果的国际影响力和工业应用
- ARINC653标准委员会
- CC国际信息安全评估
- 操作系统开源社区
- 成果的工业应用
10. 结论
1. 物联网操作系统
物联网的概念及其重要性，已经众所周知，本文不做详细讨论。本文讨论的物联网比传统物联网的概念更宽泛一些，也包括工业物联网、车联网、天空地一体化网络等，网络设备除了传感器等小型设备，我们把航天器、航空器、无人汽车、工业控制设施等都看作物联网的节点，因为这些设备正逐渐融入到网络环境中。
物联网环境下，万物互联、软件定义一切(SDX)是系统的重要特征，这就决定了平台/软件逐渐呈现多样化、网络化、规模化。在物联网环境下，可以把基础设施分为端设备、边缘设备和云平台设备等三大类，本文主要讨论端设备和边缘设备上的OS，云平台的OS不在本文范围。这样的物联网OS，必须满足新的要求，包括多架构、模块化、连接性、低功耗等等。
针对不同的设备，操作系统内核也呈现多种架构，包括极小设备上的纳微内核nanokernel、小型设备上的微内核microkernel和一些富资源设备上的分区内核partition kernel。同时，物联网OS的关键特性将逐渐融合功能安全safety、信息安全security和时间确定性realtime等。这些都是新一代操作系统需满足的安全要求，目前从国外物联网OS的发展趋势来看，也有这样一种走势，包括PikeOS、VxWorks等。而操作系统是现代计算系统/电子系统上软件栈的最底层，它的Bug容易导致系统奔溃、被攻击、不确定性，对于关键领域的应用来说后果是非常严重的。
2. 软件很重要，但也很脆弱
在物联网环境下，SDX的驱动使得软件在系统中的地位越来越重要，软件占系统功能的比重大，成为创新的主体。以汽车车载软件为例，软件规模从10万行增长到1亿行，目前，80%以上的汽车系统创新在软件领域。另外，从1960年代到最近，每个NASA的飞行软件的规模以每10年10倍的速度增长。
虽然，软件越来越重要，但是因为软件的Bug导致各领域的严重后果，却时有发生。近3年，区块链领域智能合约漏洞已导致了巨大的经济损失，例如The DAO被盗6千万美元、美链BEC价值归零、BAI和EDU任意账户转帐、以太坊Parity钱包漏洞损失1.5亿美元等。在无人车领域，Uber无人车撞死行人、特斯拉可被黑客远程控制。在无人机领域，美国RQ-170S哨兵、MQ-1C捕食者等军用无人机被劫持。在航天领域，2016 日本“瞳”卫星解体、NASA火星探测器坠毁等等。这些案例的背后，都是因为系统或软件中几行甚至一行代码存在Bug而导致的重大事故。
为什么软件会有这么多问题？从客观分析，软件太复杂，很难摸透运行规律和质量特征。因此，与其他工程学科相比，软件项目一直难以有效得到控制。从主观分析，现在主流软件开发方法难以满足高安全可靠的要求。现在很多互联网/物联网系统开发中，需求描述不精确、设计模型与需求不一致、代码实现的测试不完备，这是难以满足关键领域物联网系统/软件的安全可靠性的。最终，这些问题导致代码中带入很多Bug，这些Bug在运行环境中一旦触发，可能导致系统的崩溃/时间的不确定，或者被黑客恶意利用，从而受到攻击或关键信息泄漏。
3. 软件定义一切的时代，软件由什么定义？
回过头来，我们来回答一个问题：软件定义一切的时代，软件本身该由什么来定义？我们的初步结论是软件可以由形式逻辑(Formal Logics)来定义。我们知道，人工智能现在这么火，但是它仍然没有一个可被证明的理论作为基础（见丘成桐CNCC 2017演讲），所以现在人工智能的可解释性、确定性和安全可靠性等仍然是问题。幸运的是，对于软件来说，不存在类似的问题，几十年来计算机科学家已经为软件打下了扎实的逻辑基础，图灵奖50多年来，许多获奖工作都与此相关。我们需要做的是如何开发好用的工具，来解决工业界真实软件的安全可靠性问题。
例来说，对于计算机程序，如何定义一个程序？通常程序员只是用命令式或函数式语言写出程序，但这只是定义了程序的HOW（程序怎么做，它的开发实现），如下所示的二分法搜索程序。而现在工业界的软件开发中，往往缺乏对程序应该做什么WHAT（它的规约specification）和程序为什么做得对WHY（它的证据proof）的定义。这就导致程序的正确性缺乏依据和证据，软件中存在诸多Bug也就不足为奇。
采用逻辑方法进行软硬件规约、开发和验证的方法，称为形式化方法(Formal methods)。形式验证和软件测试、代码静态分析做简单对比：
- (1)软件测试是跑测试用例，来看用例执行结果是否满足预期。那么测试用例是否完备、是否能有效执行就是核心问题。对于操作系统来说，由于抢占、中断和内核并发等因素，测试用例往往较难构造；而内核测试环境的构造也比较困难。
- (2)代码静态分析是根据某种代码模式，从源代码中去发现这种模式，从而发现代码的错误或漏洞。静态分析主要关注语言相关的漏洞，比如指针越界访问等，而对于代码的功能，难以做有效的分析。而且，静态分析的误报率很高，与业内顶级研究者讨论，准确性能达到30%就算比较好了。
- (3)形式验证是使用逻辑分析的方法，对软硬件系统的所有可能执行情况进行分析，从而能挖掘出基本的功能Bug、程序语言相关的漏洞以及并发等深层Bug。但是自动化形式验证（如model checking）由于状态空间爆炸，对于复杂系统/代码无法有效应对；交互式证明的形式验证，不存在类似问题，但是对于人员的要求较高，成本也较高。
这三种方法都是打击Bug的武器，我们可以把“测试”看成“步枪/机关枪”，把“静态分析”看成“自动火炮”，而“形式验证”是现代化的精确打击武器。对于一般应用软件，以测试/静态分析为主，而对于高安全等级软件，形式验证是必备技。
4. 物联网OS为什么要做形式验证和安全认证
首先，我们来说说安全认证。为了确保系统和软件的安全可靠性，不同领域对它们的开发管理过程和输出物进行了严格的规定。
IEC 61508是国际电工委员会发布的《电气/电子/可编程电子安全系统的功能安全》标准，该标准已被采纳到不同的领域，形成领域特定的安全标准，如民机机载软件的DO-178B/C、铁路轨道交通的EN 50126/8/9、汽车的ISO 26262等。这些标准已被领域广泛接受，例如DO-178B/C标准是国内外民用大飞机适航，发动机控制系统、航电系统等必须符合的安全标准。
这些标准都非常重视形式化方法，并对其做了具体的规定。IEC61508对认证系统的安全等级进行了划分，分为SIL 1-4四个级别，其中SIL 4安全等级最高。下图中，可以看作随着认证系统的安全等级逐渐提高，形式化方法应用的要求也逐步提升。SIL 4强烈推荐在系统和软件的各阶段都采用形式化方法来进行开发和验证。虽然是强烈推荐，但不采用形式化方法，其实很难过SIL 4级认证。同样，2012年颁布的DO-178C标准，增加了DO-333 “形式化方法”附件，对系统研发过程中的形式化方法应用提出具体要求。
另外，在信息安全领域，国际信息技术安全评估标准CommonCriteria(CC)是被广泛认可的安全评估标准之一。如下图所示，工业发达国家，如法国、德国、加拿大、美国等已经有很多产品经过了CC的高级别安全认证。而且近十年，每年都有上百项产品经过CC高级别安全认证(EAL 5级以上)。
CC对形式化方法做了强制性的使用要求，EAL 5级以上，在开发过程各阶段都不同程度地要求使用形式化方法来进行开发和验证，如下所示。
从这些行业的安全认证标准中，对于系统实现代码层面，并不要求做代码级的形式化验证。最近，澳大利亚seL4操作系统内核和美国CertiKOS操作系统内核的形式验证，已经能覆盖到源代码和二进制代码的层面，做到了从需求、设计到代码的完全形式验证(fully formal verification)。经过完全形式验证，可以做到操作系统的零Bug，它的安全等级实际上比EAL7/SIL 4等更高。
5. 形式化验证的效果和成本怎么样
形式化验证的效果怎么样？人力/时间成本如何？这是行业采用形式化方法最为关心的问题。关于形式化验证的效果，举4个例子。
seL4 (https://sel4.systems/)是一个经过源代码完全形式验证的OS内核，包括8700行C代码和几百行汇编代码。形式验证包括需求、设计和源码3个层面，验证了整个OS内核的访问控制、信息隔离、功能正确性和代码的空指针/越界访问等，验证中发现了C代码中160多个Bug，很多Bug超乎内核开发人员的想象。而对同样版本的L4内核进行再次测试，只发现了16个新Bug。
CompCert (http://compcert.inria.fr/)是完全采用形式化方法开发与验证的C语言编译器，其编译能力与GCC相当，性能比GCC低10%左右。美国有一个项目，专门各类编译器进行暴力分析和测试，以发现其中的Bug。但是，至今CompCert中经过验证的部分，没有发现任何Bug，而GCC和LLVM等编译器中，发现了几百个漏洞。编译器的重要性在于，带Bug的编译器对完全正确的源代码进行编译，可能在二进制代码中引入新的Bug。
美国DARPA 高可信网络军事系统HACMS计划(http://smaccmpilot.org)，对一个四旋翼无人机进行了完整的形式验证。整个项目分为3个阶段，其中第1阶段为期16个月，并雇佣一批顶级黑客对无人机进行攻击。起初，直接采用现有软硬件直接搭建这架无人机，黑客很快攻入UAV，截获控制权，并借此攻破UAV操作员的电脑。16个月后，采用经过形式验证的操作系统、控制软件来重新部署UAV，并且将系统源码和文档都给黑客，他们攻击了6个星期未能攻破系统。
最后一个案例是亚马逊AWS云平台的形式验证。从2011年开始亚马逊AWS团队就开始使用形式化验证工具来发现和排除系统中潜藏的错误。截止目前，亚马逊已经在AWS Simple Storage Service（S3）对象存储系统、DynamoDB NoSQL数据库服务、Elastic Block Store弹性块存储（EBS）服务等系统上使用了形式化验证，合计发现了10多个错误，如下图所示。而且通过这些方法的应用，使得工程师对于系统的理解得到了本质上的提高，并以此为基础进行系统优化，提升了AWS的性能。现在，在亚马逊总共有7个开发团队在用形式化方法来提高软硬件系统的安全可靠性。
形式化验证的成本方面，国内学术界/工业界都有一个误区，通常认为形式化验证只能应对小程序/小系统，形式化验证难度大、工具差、成本高、工业不可用。我们认为形式化验证近10年取得了巨大的进步，上面的几个案例，已经说明形式化方法可以应对整个OS内核、整个编译器等中大型软件，当然对于Linux等上千万行代码的规模，现在仍然难以应对。关于这一点请进一步参考《形式化方法对软件开发的挑战：历史与发展》。
其次，认为形式化验证难度大、工具差、成本高、工业不可用，其实主要是人的问题。人的问题是说，要做形式化验证一定要有这方面的基础和积累，我们不能去希望没有这方面经验的人，能马上去看懂或上手做形式化的开发和验证。就像只掌握基本C语言的学生，很难开发出一个优秀的操作系统一样，这需要经过多年不断的学习、实践和积累。一旦具备了这样的积累，做形式化开发和验证项目，时间和成本就可得到有效的控制，下表展示了国际上一些基础软件形式化验证的规模和人力成本，其中LoC是代码行数，LoP是证据行数，PY是人年。总体来说，投入产出比约1万行/1人年，而且随着验证框架和工具的成熟，成本会更低。我们实验室近年做了不少形式化验证的项目，培养的硕士生/博士生都可以上手来做，时间/人力成本基本和下表相当。
6. 国外物联网OS形式验证/安全认证的现状
物联网操作系统是软件系统中最核心的软件，在关键应用领域它的安全等级要求是非常高的。因此，国外工业界的操作系统产品和学术界的操作系统，不少通过了高级别的安全认证和完全形式验证。总体情况，如下图所示。这里面，有些工业产品只是提供了可认证的证据包，并没有真正去做安全认证。
美国风河的VxWorks系列、绿山的INTEGRITY系列、LynxSecure的LnynxOS、德国SYSGO的PikeOS、QNX等工业产品，都能提供不同安全认证标准要求的高等级认证证据包，有些已经随着大系统的安全认证，通过了高安全认证。这里DO-178 Level A是最高级别，CC EAL 7是最高级别，IEC 61508 SIL 4是最高级别，ISO 26262 ASIL D是最高级别。
开源的物联网操作系统，uC/OS II随大系统的安全认证，已通过DO-178 A级认证，FreeRTOS的安全版本SafeRTOS也通过了61508和26262的安全认证。Linux基金会下的Zephyr物联网操作系统也计划对其LTS版本开展一系列安全认证。
学术界则更多关注到操作系统的完全形式验证，如seL4和CertiKOS操作系统，经过了需求到代码的形式验证。目前，seL4已经应用到美国DARPA等军事系统、CertiKOS也在一系列军用无人车上应用。
虽然，物联网操作系统的形式验证和安全认证在国外已取得了良好的效果，但是从技术上来说，多核操作系统安全认证、源码级形式验证仍然是挑战。另外，对于我们国家来说，国内还没有符合高级别安全认证的操作系统，这是我国物联网领域自主可控、安全可靠必须解决的问题。
7. 物联网OS形式验证的挑战和技术框架
要做一个操作系统已经是比较难的一件事情了，而要从逻辑上来验证一个操作系统更是难上加难，因此技术挑战还是有很多的。主要从C代码、OS机制和安全认证三个方面来讨论。
（1）从C代码的角度看：现在的物联网OS主要使用C语言开发，C语言非常灵活复杂，包含多维指针/函数指针/复杂数据结构/位运算。同时，OS的C代码中与处理器ISA耦合，许多地方C代码的执行方式是依赖于硬件的，比如中断控制的语句、线程切换的语句等。下图是一些物联网OS中典型的C代码。
这样，对物联网OS的C代码形式验证，在C代码通过手工/自动化转化为等价的形式化模型时，存在很大的难度。
（2）从物联网OS的机制看：由于多核处理器的广泛使用，物联网OS上层多样化的硬件驱动，以及物联网OS的实时性要求，物联网OS内核一般是并发、可中断、可抢占的内核。在多核处理器上，多个内核实例在每个核上并发执行，但内存是共享的，因此内核代码中存在很大共享资源访问的地方。内核一般使用细粒度锁，来实现多个上层任务/线程的共享资源访问、通信等。可中断/可抢占意味着在内核态，程序执行到某条语句，都有可能被其他中断程序打断，具体如下图所示。
这样，在物联网OS的内核态，不同线程的系统调用执行是并发的。由于使用细粒度锁，这些syscall的多数代码行在执行时，是互相穿插的(Interleaved)的，如下图所示。
OS内核的这些并发执行给物联网OS的形式验证带来了巨大的挑战。虽然，CertiKOS做了部分多核并发内核的形式验证，在国内外，对并发OS内核的形式验证，尤其是源代码级的，仍然是一个难题。
（3）从安全认证要求的角度看：各行业的安全认证都非常强调不同开发阶段产出物之间的一致性/符合性/可追溯/可验证。以DO-178B/C安全认证为例，其要求如下图所示。形式化开发/验证要符合安全认证标准，必须提供多个层次的模型、它们之间的这些特性要求，给开发/验证方法和工具支持都带来很大的挑战。
针对物联网OS的特征、形式验证/安全认证的需求及其技术挑战，我们提出了物联网OS形式验证的技术方案。这个技术方案的特征包括：
- 支持功能安全和信息安全
- 符合EAL7/SIL4等最高安全级别认证的要求
- 符合ARINC653等操作系统的工业标准
- 支持多核/可抢占/可中断等形态的并发内核
- 覆盖安全模型、需求、设计到源码的形式验证
- 可集成所有模型和证据的统一开发与验证环境
我们已经在Isabelle/HOL中实现了整个技术框架，包括操作系统的安全模型、操作系统通用的执行模型、一系列形式化规约语言、各种验证方法、C语言完整的形式语义和验证方法等等，形成了10多万行的框架代码，可有效支持物联网OS的形式化开发和验证，达到符合高级别安全认证的要求和OS源码的完全正确性。
8. 已取得的部分研发成果
围绕上述技术方案和工具实现，我们在各个层面都开展了一系列研发工作。这里主要介绍典型的4个成果，覆盖需求、设计、源码和二进制代码层。
成果1（需求层）：ARINC 653操作系统标准的形式化验证
这项成果的详细信息，见之前的微信公众号文章《ARINC 653实时操作系统标准、应用及分析验证》。这里只做简单介绍。
ARINC 653是航空航天领域实时操作系统的事实性标准，几乎所有商业RTOS遵循ARINC 653，如VxWorks、INTEGRITY-178B、LynxOS、DDC-I、PikeOS等，并应用到波音/空客新型客机、洛马隐身战机、美国NASA猎户座飞船、火星探测器等。目前，汽车电子系统AUTOSAR的OS也逐步采用ARINC 653的分区架构。
这项成果中，我们对ARINC 653标准定义的6大类功能、57个系统调用，进行了完整的形式化建模，模型覆盖所有功能点、所有数据结构和所有系统调用接口的每行伪代码。根据ARINC653标准以及分区操作系统的领域知识定义了90多条安全不变式，完成了1600多个定理的证明，其中99%实现了自动化。通过形式验证发现了ARINC653 P1-3标准的6个功能安全问题。
成果2（设计层）：物联网OS的安全与形式化开发
成果1可以看作是操作系统需求层面和部分功能规约层面的形式化模型与验证。依据安全认证的要求，高层设计、低层设计都需要形式化地开发和验证，并且保持与需求、功能规约的一致性、符合性和可追溯性等。因此，本项成果中，我们以Common Criteria EAL7级为目标，提供了物联网OS从安全模型、需求、功能规约、高层设计到低层设计的逐步求精式开发框架。
我们在Isabelle/HOL中完整实现了物联网OS的安全模型和形式开发框架，包括16000行形式规约与证明，并对ARINC 653标准和一些操作系统源码进行验证分析，发现其中10个Security缺陷，包括VxWorks 653工业OS、XtratuM和POK开源OS，具体如下表所示。这些缺陷的后果是，高安全级别的分区/进程内的信息可能泄漏到低安全区域。黑客可以通过网络攻击入侵联网的低安全分区，然后通过这些漏洞，偷取高安全分区内的信息或影响高安全分区内应用的执行行为。
成果3（源码层）: 并发物联网OS的C代码形式验证
这是我们在2018年上半年刚刚完成的一项成果，具体信息会在后续的公众号文章中详细介绍。本项成果是全球第一个对OS并发内存管理算法和C代码的形式化验证工作。
成果2中，我们已经实现了物联网OS低层设计的形式验证，再往下就是源代码层面。如前所述，OS源码的形式验证，尤其对于并发OS来说，是非常难的。目前，国际上的成果也很少。
本项成果验证对象是Zephyr物联网OS内存管理模块。Zephyr是Linux基金会下唯一的开源物联网OS，主要由Intel贡献，是其收购风河公司后，根据VxWorks相关成果重新开发的一个RTOS。目前，Zephyr已支持ARM、X86、RISC-V等指令集架构和80多种板卡，已应用到智能手表、智能鞋等产品中。
Zephyr是一个精简、高效、实时的物联网OS，其内核使用开关中断实现细粒度的共享资源访问锁。Zephyr内存管理模块，使用伙伴系统(buddy system)的内存管理算法，支持多任务并发的动态内存分配和回收。
Zephyr内存管理模块的数据结构和内存管理算法非常复杂。数据结构包括物理内存块、四叉树的内存块信息维护、多级空闲内存块双向链表、多级空闲标志位表bitmap等。内存分配时，会根据用户请求块的大小，逐层裂解大的内存块，一直到合适的大小，再分配给用户。内存回收时，也会将逐层空闲块进行合并。如下图所示。
最复杂的是，内存管理模块支持多线程并发访问，即多个线程可以同时对一个内存池进行内存分配和回收操作。而多个线程的分配/回收两个系统调用，在内核态是细粒度锁的并发。下图展示了内存管理的部分C代码，这段代码中，只有所示alloc_block函数内部的部分语句，通过关中断得到共享资源锁，在其他任何代码处，都是可被抢占、可被中断的。另外，Zephyr的内存管理模块C代码中，也存在重调度，当请求内存块无法被满足时，内核会挂起当前线程并主动调度给其他线程去执行。
为了实现并发OS内存C代码的形式验证，我们在Isabelle/HOL中开发了并发C代码形式语言及验证方法，并对Zephyr内存管理模块的C代码都做了形式化建模，最后进行组合验证。开发了约15000行形式规约和证明，实现了并发OS验证框架，支持调度、抢占、中断、锁机制。又开发了10000行内存管理C代码的形式模型和证明，覆盖Zephyr内存管理模块每行C代码。
内存管理的形式化验证主要性质包括功能正确性、安全不变式、可终止性等，最终从Zephyr的内存管理C代码中发现3个严重Bug，包括并发Bug、系统调用返回值逻辑不正确、系统调用死循环。
这些Bug的后果非常严重，一旦Bug被触发，整个OS管理的内存全部紊乱。或被黑客利用，通过恶意进程影响OS其他进程的正常执行。而这些Bug隐藏较深，通过软件测试的方式是很难发现的，我们也尝试用最先进的代码分析工具去跑，也扫不出这些Bug。
成果4（二进制层）: 指令集ISA的形式模型
处理器的指令集架构ISA是物联网OS验证的基础，OS的C代码中与硬件相关部分都嵌入汇编指令来实现，OS二进制代码则都是对ISA的调用。因此，无论是C代码从还是二进制代码层的形式化验证，都离不开ISA的形式模型。
本成果构造了ISA2形式模型(ISA in ISABELLE)，包括ISA形式模型基本框架、SPARC v8和RISC-V等ISA形式模型，覆盖物联网OS内核所需的所有指令。在Isabelle中开发了15000行的模型和证明。
ISA2是可执行的模型，C代码编译得到的二进制程序在该模型上可以执行。另外，如下图所示，通过与Xilinx开发板的执行结果进行比对，对ISA2模型进行了正确性测试。最后，对ISA2模型的安全性进行了安全性证明，包括正确状态连续一致性、数据隔离安全性、用户态/内核态权限安全性等。
9. 成果的国际影响力和工业应用
(1) ARINC653标准委员会
这一条参见之前的微信公众号文章《ARINC 653实时操作系统标准、应用及分析验证》。
(2) Common Criteria(CC)国际信息安全评估
我们开发的“符合安全认证的形式开发框架”以及对工业、开源OS进行形式验证的成果，得到国际上认可，包括：欧盟EURO-MILS重大项目、德国SYSGO公司(PikeOS研发商)和美国风河(Intel收购)等。2018年，我们受邀加入CC的操作系统内核工作组，参与起草操作系统内核的security protection profile。该工作组主要成员来自：美国国家安全部、新加坡网络空间安全署、美国风河、德国大陆汽车电子、美国雷神等。
随着物联网、工业互联网等的快速发展，CC在工业各领域发挥越来越重要的作用。德国、法国、美国、加拿大等工业发达国家，每年都有许多产品通过EAL 5 以上的高级别安全认证，包括安全设备、工业控制系统、安全操作系统、数据库等。工业知名的操作系统，如绿山INTEGRITY-178、风河VxWorks Cert等，均符合CC EAL 6安全级别。EAL 5级以上，要求采用形式化方法进行产品开发，这正是我们目前重点研究方向之一。我国由于种种原因尚没有工业产品，过CC高级别安全认证。
(3) 操作系统开源社区
我们在操作系统形式验证方面的多篇综述/研究论文，已被POK开源操作系统列为该领域重要参考文献，我们的研究成果初步得到开源界的认可。POK是仅有的2个符合ARINC653标准的开源操作系统之一，目前已商业化应用到俄罗斯民航飞机，计划于2019年完成POK的DO-178BLevel A安全认证。
(4) 成果的工业应用
目前，我们已完成/正在开展我国多个物联网领域国产操作系统的形式验证，覆盖需求/设计/源代码等多个层面，发现了许多设计和代码中的Bug。同时，我们正在为我国载人航天工程核心软件、某国产无人驾驶车的控制系统等，开展形式化验证和安全认证的研发工作。形式化验证技术已落地到梆梆安全，形成形式化代码审计服务能力，支撑梆梆安全在物联网、区块链、安全关键领域的业务应用。
10. 结论
近年来，物联网OS群雄逐鹿，谷歌、英特尔(风河)、微软、ARM等都推出各自的物联网OS。国产OS厂商也纷纷跟进，如AliOSThing、Huawei LiteOS、SylixOS、RT-Thread、SZOS、SpaceOS、GEOS、AcoreOS等。物联网可以看作国产OS崛起的一个历史机遇。
国际上，系统级形式化验证技术逐步成熟，美国、欧盟、英国、澳大利亚等都开展了包括OS、编译器、计算机系统、嵌入式系统等完整的形式化验证，形成了一系列的方法技术和工具环境。
对我们国家来说，国产物联网OS的安全可靠性保障、A级/EAL 7高级别安全认证亟待突破，这是我国“自主可控、安全可靠”必须要迈过去的一个门槛。北航已经在这方面积累了丰富的经验，期待为我国物联网OS的发展，做一点点贡献。
作者：赵永望，北京航空航天大学 计算机学院，主要从事形式化方法、实时操作系统、安全可靠软件等研究。
