一种面向嵌入式操作系统的形式化验证方法

A formal verification method for embedded operating systems

操作系统是整个计算机系统的核心与基石,其可靠性与安全性至关重要.操作系统的故障或漏洞可能会导致系统崩溃、数据丢失、隐私泄露和安全攻击等问题,特别是在安全攸关系统中,一旦操作系统发生错误,就可能会造成重大人员伤亡或财产损失.一直以来,如何保障操作系统的安全性和可靠性对学术界和工业界都是一个重大挑战.目前验证操作系统安全性的方法有软件测试、程序静态分析、形式化方法等.其中,形式化方法是最有潜力确保操作系统安全可信的方法,通过使用形式化方法,建立数学模型并进行系统的形式化分析和验证,从而发现潜在的错误和漏洞.在操作系统中,形式化方法可以用于验证操作系统的功能正确性、完整性以及系统安全性等.在已有的针对操作系统形式化验证的成果基础上,提出了一个面向嵌入式操作系统的形式化验证方案,采用VCC(verified C compiler)、CBMC(C bounded model checker)以及PAT(process analysis toolkit)工具分别对操作系统单元层面、模块层面和系统层面进行验证.该方法已成功应用到某操作系统的任务调度架构案例中,对于嵌入式操作系统的分析验证具有一定的通用性。

The operating system is the core and foundation of the entire computer system.Its reliability and safety are vital because faults or vulnerabilities in the operating system can lead to system crashes,data loss,privacy breaches,and security attacks.In safety-critical systems,any errors in the operating system can result in significant loss of life and property.Ensuring the safety and reliability of the operating system has always been a major challenge in industry and academia.Currently,methods for verifying the operating system’s safety include software testing,static analysis,and formal methods.Formal methods are the most promising in ensuring the operating system’s safety and trustworthiness.Mathematical models can be established using formal methods,and the system can be formally analyzed and verified to discover potential errors and vulnerabilities.In the operating system,formal methods can be used to verify the correctness and completeness of the operating system’s functions and system safety.A formal scheme for embedded operating systems is proposed herein on the basis of existing formal verification achievements for operating systems.This scheme uses VCC(verified C compiler),CBMC(C bounded model checker),and PAT(process analysis toolkit)tools to verify the operating system at the unit,module,and system levels,respectively.The schema,upon being successfully applied to a task scheduling architecture case of a certain operating system,exhibits a certain universality for analyzing and verifying embedded operating systems.