近日，区块链与数据安全全国重点实验室赵永望教授团队的论文《Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-B》，被ACM Formal Aspects of Computing(FAC)期刊遴选为2023年度 Featured Article。FAC期刊创刊于1989年，是形式化方法领域的国际顶级期刊。
该论文使用Event-B方法对最新版的ARINC653多核操作系统标准进行了严格的形式化建模与自动化验证。论文提出了一种多核操作系统的细粒度行为分解方法，从而使用经典的状态机模型（Event-B抽象机）来刻画复杂的并发行为，采用层次化的规约精化方式，开发了ARINC653标准完整、精确、分层的形式化模型，最终在Event-B工具中实现自动的形式化验证，并发现了多核ARINC653标准中的多个错误。
ARINC653标准是国际航空工业界实时操作系统的事实性标准，已有20年历史，被航空航天领域绝大多数实时操作系统所遵循，已应用到空客A380、波音787、F22、NASA猎户座飞船等。近年来，随着硬件能力和系统功能复杂性的大幅提高，ARINC 653标准也逐渐应用到汽车、工业控制等领域。ARINC653标准委员会成员来自波音、空客、洛克希德马丁、GE航空、霍尼韦尔、以及国际实时操作系统主要厂商。赵永望教授多年来一直是ARINC653标准委员会的成员，参与标准的研制工作，其形式化模型及其相关成果也被纳入ARINC653标准的最新版本中。
形式化方法已被学术界和产业界认为是安全保障的重要方法，2024年2月，美国白宫发布一份题为《Back to The Building Blocks: A Path Toward Secure and Measurable Software》的报告，呼吁使用内存安全的硬件与编程语言，强调形式化方法在软硬件安全领域的重要性，建议将形式化方法应用于软硬件开发的全过程，并在软件供应链中采用经过形式化验证的基础组件。形式化方法作为一种严谨、精确的验证技术，通过与大模型等新兴技术的结合，将在未来软硬件和网络安全方面发挥关键作用。
区块链与数据安全全国重点实验室聚焦区块链与数据安全科技前沿，建设国家战略科技力量，构筑国家技术竞争新优势，实现我国区块链与数据安全技术高水平自立自强。实验室已在形式化方法进行了重点布局，主要围绕区块链底层基础设施、密码、共识协议、智能合约等层面开展形式化验证的前沿研究。赵永望教授团队多年来始终围绕基础软硬件开展形式化方法研究工作，提出了操作系统形式化验证的系统性理论和方法、面向高安全系统的形式化开发语言及验证理论、多核并发系统的组合验证逻辑与多语言集成方法等，研发了新型程序设计语言自动化验证工具、符合信息安全认证标准的形式化建模验证工具，全面开展国产操作系统的形式化验证，包括华为、小米、军事科学院、中国信科、航天五院、中航工业、中兴通讯等，获得国内第一个、第二个最高等级的软件EAL5+证书，自研的形式化验证技术与工具成为小米澎湃OS全域安全的技术底座。
