符合工业标准的多核隔离内核形式规约与安全验证技术

With the application of multicore platform and development of internet, security and safety integrated multicore separation kernel is one of trends in OS kernels of safety-critical system. Formal verification of information-flow security on multicore separation kernels is the necessary way for high-level security and certification. However, the state of the art on this topic was focused on monocore kernels. Moreover, there is no industrial standards compliant formal specification for multicore separation kernels. High-level security and certification cannot be archived in such situation. To address the above problem and challenges, this project aims at ARINC 653 compliant separation kernels and focuses on formal specification and information-flow security verification which are compliant with highest evaluation level of Common Criteria certification. The project will address key techniques, such as information-flow security definition of multicore separation kernels, compositional verification of them, security-preservation refinement of formal specifications. The project will build a set of levels of formal specification for ARINC 653 multicore separation kernels, and formally verify the source code of open-source kernels as practice. The outcomes of the project could provide reusable approach and formal models for design/verification and security certification of Chinese multicore operating systems.

随着多核计算平台的逐步应用和互联网的纵深发展，综合Security和Safety特性的多核隔离内核是安全攸关领域操作系统内核的发展趋势。多核隔离内核的信息流安全验证，是提升内核安全性、开展工业安全认证的必要途径。而国际上对内核的信息流安全验证主要集中在单核处理器，没有符合主要工业标准的多核隔离内核形式规约，严重制约多核操作系统的安全性确保和认证。本项目以遵循ARINC 653标准的多核隔离内核为研究对象，开展符合Common Criteria高安全等级认证的形式规约以及信息流安全验证技术研究，突破多核内核信息流安全表征、多核内核安全性质的组合验证、安全保持的规约求精等关键技术，构造ARINC 653多核隔离内核形式规约，并以开源内核为案例开展源代码的形式验证实践。本项目研究方法和成果也可为后续国产多核操作系统的设计/验证、安全认证等提供可复用的技术方法和形式模型。

随着多核计算平台的逐步应用和互联网的纵深发展，综合Security和Safety特性的多核隔离内核是安全攸关领域操作系统内核的发展趋势。多核隔离内核的信息流安全验证，是提升内核安全性、开展工业安全认证的必要途径。而国际上对内核的信息流安全验证主要集中在单核处理器，没有符合主要工业标准的多核隔离内核形式规约，严重制约多核操作系统的安全性确保和认证。本项目以遵循ARINC 653标准的多核隔离内核为研究对象，开展符合CC认证要求的形式规约以及信息流安全验证技术研究，包括事件驱动的多核内核规约语言(PiCore)及组合推理技术、多核隔离内核的信息流安全模型、多核隔离内核的规约求精方法、符合CC EAL7的ARINC 653多核隔离内核形式规约及应用。突破了多核内核信息流安全表征、多核内核形式规约及安全性质的组合验证、安全保持的多核内核规约求精等关键技术，研发了并发系统形式化验证工具PiCore、符合CC信息安全认证的形式化框架CCCert、并发操作系统形式化规约求精工具CSim2等，构造了多核隔离内核信息流安全模型、ARINC 653标准的多核隔离内核功能规约和设计规约，共计Isabelle代码37000多行。相关成果已在多个国产操作系统的形式化建模验证以及CC安全认证中得到实际应用，包括元心科技SyberX形式化建模验证、军事科学院无人机智能操作系统xROS形式化建模与验证、大唐数据所微内核形式化建模与验证、华为海思THEE形式化验证、小米MiTEE形式化验证、航天502所多核操作系统形式化验证等。其中，元心SyberX获得国家级评估机构颁发的首个软件EAL5+评测证书，为国内最高EAL等级软件。