软件学报

作者：章乐平，赵永望，王布阳，李建欣

单位：章乐平，北京航空航天大学 计算机学院, 北京 10019111,赵永望，浙江大学 计算机科学与技术学院/网络空间安全学院, 浙江 杭州 310007;区块链与数据安全全国重点实验室(浙江大学), 浙江 杭州 31000702,王布阳，浙江望安科技有限公司, 浙江 杭州 31110003,李建欣，北京航空航天大学 计算机学院, 北京 10019104

关键词：形式规约;自动生成;精化验证;交互式;Auto-active;L4 线程管理

基金：国家自然科学基金“叶企孙”科学基金(U2341212); 国家自然科学基金重点项目(62132014); 浙江省自然科学基金重点项目(LD24F020006)

相较于初代微内核, 第2代微内核L4在性能和灵活性方面显著提升, 并在众多领域获得广泛应用. 操作系统内核的正确性与可靠性对系统稳定运行起着决定性作用. 聚焦于L4微内核的关键机制——线程管理, 对其展开形式规约与验证. 首先构建安全规约以描述安全性质, 复用标准的 L4 API 功能规约明确功能正确性, 同时自动生成基于C++源代码的实现规约. 为缓和功能规约与实现规约间的巨大差异, 引入中间规约. 其中, 前两种规约采用 Isabelle/HOL 形式化语言编写, 后两种则以 Python 语言表达. 通过解释(interpretation)、建立正向模拟(forward simulation)等方法, 精化证明各规约间的一致性. 在证明过程中, 将交互式验证与Auto-active验证方法相结合, 提升验证自动化能力的同时, 减少人工证明工作量. 最终发现源代码中存在3个违反正确性和安全性的问题, 并针对这些问题提出解决方案.

来源：2026年第9期

《软件学报》期刊编辑部

查看软件学报杂志2026年第9期