2026年6月6日上午，由best365官网计算机与控制工程学院主办的“两校名师讲座”在承先图书馆承先厅举行。本次讲座特邀北京大学计算机学院博雅特聘教授、国家杰出青年科学基金获得者詹乃军教授作为主讲嘉宾，作了题为“国产多核实时操作系统微内核形式验证”的学术报告。学院相关领域师生近百人参加了此次活动。

一、报告核心内容

詹乃军教授的报告系统梳理了其项目组近年来完成的一项重大工程——某国产多核实时操作系统微内核的形式验证工作。该项目面向我国重点领域对高安全、高可靠操作系统的迫切需求，以形式化方法对操作系统内核进行了全面、严格的数学验证。

本次验证工作覆盖了操作系统的七个核心功能模块：任务管理与调度、中断和异常处理、任务同步与通信、核间通信与动态重构、时钟管理、权能访问控制，以及分区配置和分区通信。被验证内核代码总计约两万五千行，规模可观，验证难度极大。

为完成这一艰巨任务，项目组自主发展了两套验证框架：一是基于CSL-R（并发分离逻辑-扩展）的操作系统功能性验证框架，用于保证内核功能行为的正确性；二是基于信息流分析的信息安全性验证框架，用于确保系统不出现信息泄露等安全漏洞。此外，项目组还首次提出了面向DSP（数字信号处理器）的最坏情况执行时间（WCET）分析技术，并实现了相应的自动化分析工具，填补了该领域的技术空白。

CSL-R（并发分离逻辑-扩展）方法的核心优势在于，它能够精确刻画多核环境下线程间的资源竞争与协作关系，借助分离逻辑的框架将共享状态与私有状态严格隔离，从而将全局验证问题分解为若干局部可解的子问题。信息流分析框架则从保密性与完整性双重视角出发，通过严格的数学推导确保系统在任意执行路径上均不会发生非授权的信息传递，有效杜绝侧信道攻击等隐蔽安全威胁。两套框架互为补充，构成了功能正确性与信息安全性并重的立体验证体系。

整个验证工作体量庞大，仅Coq形式化验证代码就编写了约四十五万行。在验证过程中，项目组发现并纠正了二十多类、累计数百个隐藏于代码中的缺陷，有力保障了内核质量。正是得益于这一严谨的形式验证工作，该款操作系统最终顺利通过了国际上安全性要求最为严苛的CC EAL5+认证，为我国关键基础设施领域的自主可控提供坚实的技术支撑。

值得强调的是，CC EAL5+（信息技术安全评估通用准则评估保证级5+级）是目前国际公认的操作系统安全认证最高级别之一，要求开发者对系统的安全策略、功能规范、高层设计与实现进行半形式化乃至形式化的验证。该国产操作系统的成功获证，不仅标志着我国在基础软件形式验证能力上达到了国际先进水平，更意味着我国在关键基础设施软件的安全保障方面实现了从依赖测试到数学证明的范式跃迁，具有里程碑式的意义。

图1. 詹乃军教授做报告

在报告最后，詹教授介绍了其团队在基础软件验证方法论层面的最新进展。他们提出了面向操作系统等基础软件的全新验证框架，该框架有望大幅提升验证效率与自动化水平，从根本上降低形式验证的人力成本，推动形式化方法从“高端定制”走向“规模化应用”。

据悉，该新框架的核心理念是将领域知识驱动的推理策略与机器学习技术深度融合，实现验证目标的自动分解与证明脚本的智能合成。若能成功落地，有望将形式验证的工程成本降低一个数量级，使形式化方法从少数高端项目的专属配置转变为基础软件的常规开发实践，这对于推动我国自主基础软件生态的高质量发展意义深远。

二、主讲人简介

詹乃军教授1971年5月出生，是我国形式化方法领域的领军学者。他本科与硕士均就读于南京大学（数学系与计算机系），博士毕业于中国科学院软件研究所。现任北京大学计算机学院博雅特聘教授、国家杰出青年科学基金获得者，此前长期担任中科院软件所研究员、计算机科学国家重点实验室执行主任、中国科学院大学岗位教授。

詹教授长期深耕形式化方法、实时与嵌入式系统、混成系统及程序验证等研究方向，在CAV、RTSS、HSCC、ICCP、EMSOFT等国际著名会议和期刊发表论文一百五十余篇，出版专著两部、编著四部。他担任《Journal of Automated Reasoning》《Formal Aspects of Computing》《软件学报》《计算机研究与发展》等多家重要学术期刊的编委，是形式化方法旗舰会议FM 2021和验证领域顶级会议TACAS 2027的程序委员会共同主席，现任CCF形式化方法专委主任，在国内外形式化方法学术界享有盛誉。

三、讲座意义与反响

本次讲座既是学术前沿的分享，也是家国情怀的传递。詹教授及其团队以四十五万行Coq代码铸就国产操作系统的安全基石，让在场师生深刻感受到基础软件自主创新的艰辛与荣光。形式验证技术作为保障系统安全性和可靠性的”终极防线”，在航空、航天、核电、轨道交通等关键领域具有不可替代的战略价值。

在交流环节，师生们围绕形式验证的可扩展性、Coq验证与工业级开发的衔接、国内形式化方法学科的人才培养等话题踊跃提问，詹教授一一耐心解答，现场气氛热烈。他勉励青年学子和科研工作者沉心静气、精益求精，在基础理论与关键技术层面做出真正有影响力的原创成果。

此次”两校名师讲座”的成功举办，进一步加强了best365官网与北京大学在计算机科学领域的学术交流，为学院师生提供了与国内顶尖学者面对面学习的机会，开阔了学术视野，激发了科研热情。

图2. 詹乃军教授回答学生提问

与会教师还就形式化方法在工业界的推广瓶颈、国产工具链生态建设等现实问题与詹教授进行了深入交流。詹教授指出，我国在形式化方法理论研究方面已与国际同步，下一步的关键在于培养大批兼具理论功底与工程实践能力的复合型人才，构建产学研协同创新生态，将形式验证技术从学术前沿成果高效转化为推动产业升级的核心驱动力。

best365官网计算机与控制工程学院

2026年6月15日