峰会回顾第20期 | 操作系统形式验证与安全认证

演讲嘉宾 | 赵永望

回顾整理 | 廖 涛

排版校对 | 李萍萍

嘉宾简介

赵永望，浙江大学教授/博士生导师。担任移动终端安全技术浙江省工程研究中心主任、ARINC653国际操作系统标准委员会委员（国内唯一委员）、国际信息技术安全评估标准(Common Criteria,CC)操作系统内核技术委员会委员、中国计算机学会(CCF)高级会员、CCF系统软件专委会和形式化方法专委会委员。任国际标准化组织 ISO/IEC JTC1 SOA研究组组长、国家信标委分委会委员，起草4项ISO国际标准、12项国家标准。曾任新加坡南洋理工大学高级研究员。主要研究方向包括操作系统安全、形式验证、编程语言原理等。主持和参与国家自然基金、核高基重大专项、重点研发计划、载人航天工程重点项目、工信部物联网创新项目等10余项，2011和2017年分别获得中国电子学会和山东省科技进步一等奖。相关研究成果得到美国波音、法国空客和国际知名实时操作系统厂商的认可，被纳入国际标准，并在开源实时操作系统社区产生影响力。

内容来源

第一届开放原子开源基金会OpenHarmony技术峰会——OpenHarmony高校技术俱乐部分论坛

正 文 内 容

形式验证根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性，对保障操作系统安全起到重要作用。OpenHarmony形式验证与安全认证面临哪些挑战，又有哪些技术方法和思路呢？浙江大学教授、移动终端安全技术浙江省工程研究中心主任赵永望在第一届OpenHarmony技术峰会上分享了精彩观点。

01►

为什么需要形式验证与安全认证？

随着计算机技术创新与行业发展，操作系统与软件层出不穷，在航空航天、手机、车机、物联网、医疗以及金融等领域应用广泛。在各行各业综合化、网络化、智能化以及软件化转型的关键阶段，操作系统安全的重要性日益凸显，同时面临新的安全挑战。操作系统形式验证与安全认证，是保障操作系统安全的关键手段之一。

目前，操作系统仍潜在较多安全风险。例如，VxWorks 6.5版本被发现存在11个漏洞，影响2亿台关键设备；seL4的8900行C代码中，通过形式验证发现了160多个新问题；Zephyr RTOS中也存在多个内存管理错误。其中，seL4作为演变了多年的成熟开源微内核，仍存在较多代码层的安全漏洞和问题。OpenHarmony作为一个开源社区，包含了几千万甚至上亿行代码，潜在的风险和问题不容忽视。

为什么操作系统会潜在如此多的问题呢？客观上，现在的软件越来越复杂，很难摸透运行规律和质量特征。主观上，开源社区、互联网公司等大都采用敏捷式开发或者瀑布式开发，这种主流软件开发方法难以满足高安全可靠要求。

操作系统安全问题

安全认证通过严格的过程和证据解决软件的安全问题，对证据链的要求很高。其证据链由非形式化、半形式化以及形式化的数据组成，包括文档、数据、模型等。目前，证据链在很多场合通过文档和人工评审的方式来形成，但对于安全等级非常高的场景仍难以满足相关要求。因此，在该场景下可通过形式化方法，完成准确且完备的软件建模和认证。

形式化方法

形式化方法基于严格数学基础对计算机软硬件系统进行描述、开发和验证的技术，具有精确、严格以及完备的特点。在高级别安全认证中，强烈推荐或强制使用形式化方法。目前，与国外相比，国内开源操作系统在关键的DO-178 A和CC EAL 6/7等高安全等级的形式验证与安全认证方法相关研究基本处于空白状态。

安全认证及相关标准

02►

如何实现操作系统形式验证？

浙江大学提出的操作系统形式验证框架涉及操作系统各个不同层面，兼顾功能安全和信息安全，符合EAL7/SIL4等安全级别和ARINC653等工业标准，且支持多核/可抢占并发内核，覆盖需求到C代码的形式验证，并具有统一的开发与验证环境。

浙江大学操作系统形式验证的理论与技术框架

在该框架中，操作系统领域知识层面包括信息流安全/功能安全、ARINC 653标准、操作系统设计以及操作系统C代码等；操作系统模型与证明层面包括安全需求、功能规约、高层设计规约、低层设计规约以及实现模型等。此外，还包含形式规约语言及编译器、规约求精框架、并发验证方法、安全性验证方法、系统级执行模型、自动化验证方法、源代码形式语义以及逻辑证明内核等形式语义和支撑工具。此外，赵永望所在团队基于Isabelle定理证明器自研了操作系统形式验证工具：Isabelle/Cloud云平台，通过云化和开源的方式，让社区的开发者和高校师生都能够在该平台上做相应的验证和建模等工作。

该框架具有以下特征：（1）采用逐步求精方法，覆盖安全、需求、设计、源码全部层面；（2）提供完整的形式化模型；（3）提供完整的自顶向下证据链，最终保障内核代码的安全性和正确性；（4）模型和验证可扩展；（5）采用自研工具；（6）整体框架和采用的技术符合CC最高安全级EAL7。目前，该框架在某国产安全微内核操作系统的形式验证中，获得了国内评测机构颁发的首个软件领域的EAL5+的证书，且正在实施国内最早的一批软件EAL5+形式验证与评估项目。

03►

未来挑战与建议

操作系统形式验证与安全认证技术在进一步的发展中仍在面临诸多挑战和困难。在技术方面，需要考虑多核并发、执行抢占、C语言自身复杂性、ISA耦合、操作系统数据结构与算法复杂以及代码规模大等因素；在工程方面，存在领域知识专业门槛高、没有针对性的验证工具、模型编写难、验证难度高、工作量大、代码规模大以及操作系统版本迭代等问题。其中，针对操作系统资料/文档的形式化建模效率低、源码验证代码规模大、结构复杂、语言类型多、验证难度大以及成本高等问题，可以考虑自动形式模型生成和源码自动形式验证等方法。

操作系统形式验证部分痛点

OpenHarmony是一个面向全场景智能终端的开源操作系统，覆盖全场景应用，同时也支持多样性设备。对于OpenHarmony来说，形式验证与安全认证有以下5个关键点：（1）重要性：OpenHarmony作为信息基础设施底座，如果缺少形式验证与安全认证，潜在风险程度很高；（2）必要性：OpenHarmony赋能千行百业，其中囊括了许多安全关键产业，形式验证与安全认证是安全关键行业所必须的。此外，一个安全可靠的操作系统将具有更高数量级的产业价值；（3）OpenHarmony这样大规模操作系统的形式验证与安全认证技术国产化的成功，符合目前操作系统国产化替代和发展的策略；（4）挑战性：OpenHarmony这样大规模软件系统的自动化形式验证难度较高，高效率安全认证面临挑战；（5）可行性：目前，国内已积累一定的形式验证与安全认证基础，且国内外形式化技术快速发展，OpenHarmony开源社区同样发展迅速，能够提供助力，进一步发展OpenHarmony形式验证与安全认证具备可行性。

形式验证与安全认证是保障OpenHarmony操作系统安全的重要一环，期待后续能够有更多的开发者与高校师生加入到相关领域的研究中来，共同促进OpenHarmony开源社区繁荣发展。

E N D

审核编辑 黄宇