微内核操作系统互斥量模块功能正确性的形式化验证  

Formal Verification of Functional Correctness for Mutexes in Microkernel

作　　者：张林雁 李希萌 施智平[1,2] 关永[1,3] 曹钦翔 张倩颖[1,3] ZHANG Lin-Yan;LI Xi-Meng;SHI Zhi-Ping;GUAN Yong;CAO Qin-Xiang;ZHANG Qian-Ying(Information Engineering College,Capital Normal University,Beijing 100048,China;Beijing Key Laboratory of Electronic System Reliability Technology(Capital Normal University),Beijing 100048,China;Beijing Advanced Innovation Center for Imaging Theory and Technology(Capital Normal University),Beijing 100048,China;John Hopcroft Center for Computer Science,Shanghai Jiao Tong University,Shanghai 200030,China)

机构地区：[1]首都师范大学信息工程学院,北京100048 [2]电子系统可靠性技术北京市重点实验室(首都师范大学),北京100048 [3]北京成像理论与技术高精尖创新中心(首都师范大学),北京100048 [4]上海交通大学约翰霍普克罗夫特计算机科学中心,上海200030

出　　处：《软件学报》2024年第9期4179-4192,共14页Journal of Software

基　　金：国家自然科学基金(62002246,62272322,62272323,62372311,62372312,61902240)。

摘　　要：操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.Operating systems are the key foundational components of the software stacks employed in many safety-critical scenarios.A tiny error or loophole in the operating system may cause major failures of the overall software system,resulting in huge economic losses or endangering human lives.Thus,the correctness of the operating system should be verified to reduce the number of such accidents.Traditional testing methods cannot guarantee the exhaustive detection of potential errors in the target system.Therefore,it is necessary to adopt formal methods based on strict mathematical theories for verifying operating systems.In an operating system,mutexes are utilized to coordinate the access of shared resources by tasks and they are a typical means of task synchronization.The functional correctness of mutexes is the key to the correct functioning of multi-task applications.Based on the theorem proof method,this study conducts formal verification on the code of the mutex module of a preemptive microkernel in an interactive theorem prover Coq,gives the formal specifications of the interface functions of this module,and formally proves the functional correctness of these interface functions.

关 键 词：互斥量 功能正确性 形式化验证 定理证明 Coq定理证明器 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]