| 摘要: |
| 相较于初代微内核, 第2代微内核L4在性能和灵活性方面显著提升, 并在众多领域获得广泛应用. 操作系统内核的正确性与可靠性对系统稳定运行起着决定性作用. 聚焦于L4微内核的关键机制——线程管理, 对其展开形式规约与验证. 首先构建安全规约以描述安全性质, 复用标准的 L4 API 功能规约明确功能正确性, 同时自动生成基于C++源代码的实现规约. 为缓和功能规约与实现规约间的巨大差异, 引入中间规约. 其中, 前两种规约采用 Isabelle/HOL 形式化语言编写, 后两种则以 Python 语言表达. 通过解释(interpretation)、建立正向模拟(forward simulation)等方法, 精化证明各规约间的一致性. 在证明过程中, 将交互式验证与Auto-active验证方法相结合, 提升验证自动化能力的同时, 减少人工证明工作量. 最终发现源代码中存在3个违反正确性和安全性的问题, 并针对这些问题提出解决方案. |
| 关键词: 形式规约 自动生成 精化验证 交互式 Auto-active L4 线程管理 |
| DOI：10.13328/j.cnki.jos.007609 |
| 分类号:TP311 |
| 基金项目:国家自然科学基金“叶企孙”科学基金(U2341212); 国家自然科学基金重点项目(62132014); 浙江省自然科学基金重点项目(LD24F020006) |
|
| Formal Verification of L4 Thread Management Based on Auto-active and Interactive Integration |
|
ZHANG Le-Ping1, ZHAO Yong-Wang2,3, WANG Bu-Yang4, LI Jian-Xin1
|
|
1.School of Computer Science and Engineering, Beihang University, Beijing 100191, China;2.College of Computer Science and Technology/School of Cyber Science and Technology, Zhejiang University, Hangzhou 310007, China;3.State Key Laboratory of Blockchain and Data Security (Zhejiang University), Hangzhou 310007, China;4.Zhejiang Wonsec Technology Co. Ltd., Hangzhou 311100, China
|
| Abstract: |
| Compared with original microkernels, L4 greatly improves performance and flexibility and is widely used in various fields. The correctness and reliability of the operating system kernel play a decisive role in the stable operation of the system. This study presents formal specifications and verification for thread management, a key mechanism of L4. First, a safety specification is developed to describe safety properties, a standard L4 API specification is reused to define functional correctness, and an implementation specification based on the C++ source code is automatically generated. To alleviate the significant differences between the requirement specification and the implementation specification, an intermediate specification is introduced. The first two specifications are formalized in Isabelle/HOL, and the latter two are expressed in Python. The consistency among these specifications is guaranteed through refinement proofs, such as interpretation and the establishment of forward simulation. During the proofs, interactive verification and Auto-active verification are integrated, which improves the level of automation while reducing manual proof obligations. Eventually, three issues that violate correctness and safety properties are identified in the source code, and solutions are proposed for these issues. |
| Key words: formal specification automatic generation refinement verification interactive Auto-active L4 thread management |
