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

doi:10.3969/j.issn.1000-5641.2024.04.001

摘要/Abstract

摘要：

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

关键词: 嵌入式操作系统, 形式化验证, VCC, CBMC, PAT

Abstract:

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.

Key words: embedded operating system, formal verification, VCC, CBMC, PAT

中图分类号:

TP316

王阳, 方竟成, 蔡雄, 张志鹏, 蔡喁, 缪炜恺. 一种面向嵌入式操作系统的形式化验证方法[J]. 华东师范大学学报（自然科学版）, 2024, 2024(4): 1-17.

Yang WANG, Jingcheng FANG, Xiong CAI, Zhipeng ZHANG, Yong CAI, Weikai MIAO. A formal verification method for embedded operating systems[J]. Journal of East China Normal University(Natural Science), 2024, 2024(4): 1-17.

图/表 10

图1

图2

图3

图4

图5

图6

图7

图8

图9

图10

参考文献 42

1	KLEIN G.. Operating system verification: An overview. Sadhana, 2009, 34, 27- 69.
2	KLEIN G, ELPHINSTONE K, HEISER G, et al.. SeL4: Formal verification of an OS kernel. ACM Symposium on Operating Systems Principles, 2009, 27 (1): 207- 220.
3	WOODCOCK J, LARSEN P G, BICARREGUI J, et al.. Formal methods: Practice and experience. ACM Computing Surveys, 2009, 41 (4): 1729- 1739.
4	STAMPOULIS A, ZHONG S.. Static and user-extensible proof checking. ACM SIGPLAN Notices, 2012, 47 (1): 273- 284.
5	ALKASSR E, COHEN E, HILLEBRAND M, et al. Verifying shadow page table algorithms [C]// Formal Methods in Computer Aided Design. 2010: 267-270.
6	COHEN E, DAHLWEID M, HILLEBRAND M, et al. VCC: A practical system for verifying concurrent C [C]// Theorem Proving in Higher Order Logics. 2009: 23-42.
7	DAHLWEID M, MOSKAL M, SANTEN T, et al. VCC: Contract-based modular verification of concurrent C [C]// 2009 31st International Conference on Software Engineering-Companion Volume. 2009: 429-430.
8	CLARKE E, KROENING D, LERDA F. A tool for checking ANSI-C programs [C]// Tools and Algorithms for the Construction and Analysis of Systems. 2004: 168-176.
9	SUN J, LIU Y, LIU J. Process analysis toolkit: A tool for unifying process analysis techniques [C]// International Conference on Formal Methods and Software Engineering. 2018: 409-414.
10	LIU Y, SUN J, DONG J S. An analyzer for extended compositional process algebras [C]// Companion of the 30th International Conference on Software Engineering. 2008: 919-920.
11	WALKER B J, KEMMERER R A, POPEK G J.. Specification and verification of the UCLA Unix security kernel. Communications of the ACM, 1980, 23 (2): 118- 131.
12	WIRTH N. Program Development by Stepwise Refinement [M]. Berlin: Springer, 2001.
13	XU F W, FU M, FENG X Y, et al. A practical verification framework for preemptive OS kernels [C]// International Conference on Computer Aided Verification. 2016: 59-79.
14	FEIERTAG R J, NEUMANN P G. The foundations of a provably secure operating system (PSOS) [C]// IEEE International Workshop on Managing Requirements Knowledge. 1979: 329-334.
15	NEUMANN P G, BOYER R S, FEIERTAG R J, et al. A Provably Secure Operating System: The System, its Applications, and Proofs [M]. San Francisco: Stanford Research Institute, 1977.
16	GOGEUN J A, MESEGUER J. Security policies and security models [C]// IEEE Symposium on Security and Privacy. 1982: 11-20.
17	BEVIER W R. Kit: A study in operating system verification [J]. IEEE Transactions on Software Engineering, 1989, 15(11): 1382-1396.
18	BEVIER W R. A verified operating system kernel [D]. Austin: University of Texas at Austin, 1987.
19	BEVIER W R. Kit and the short stack [J]. Journal of Automated Reasoning, 1989, 5(4): 519-530.
20	HOHMUTH M, TEWS H, STEPHENS S G. Applying source-code verification to a microkernel: The VFiasco project [C]// Proceedings of the 10th Workshop on ACM SIGOPS European Workshop. 2002: 165-169.
21	ALKASSAR E, HILLEBRAND M A, LEINENBACH D, et al. The Verisoft approach to systems verification [C]// Working Conference on Verified Software: Theories, Tools, and Experiments, Heidelberg. 2008: 209-224.
22	GU R H, KOENIG J, RAMANANANDRO T, et al. Deep specifications and certified abstraction layers [C]// Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2015: 595–608.
23	YANG Z, LEI H, QIAN W.. A hybrid formal verification system in Coq for ensuring the reliability and security of ethereum-based service smart contracts. IEEE Access, 2020, (8): 21411- 21436.
24	ROBINSON A, VORONKOV A. Handbook of Automated Reasoning [M]. Amsterdam, Holland: Elsevier, 1999.
25	XU F, FU M, FENG X, et al. A practical verification framework for preemptive OS kernels [C]// Computer Aided Verification. 2016: 59-79.
26	CAO J Y, FU M, FENG X Y. Practical tactics for verifying C programs in Coq [C]// Proceedings of the 2015 Conference on Certified Programs and Proofs. 2015: 97-108.
27	FOSTER S, HUR C K, WOODCOCK J. Formally verified simulations of state-rich processes using Interaction Trees in Isabelle/HOL [EB/OL]. (2021-05-11)[2023-02-11]. https://arxiv.org/pdf/2105.05133.pdf.
28	钱振江. 安全操作系统形式化设计与验证方法研究[D]. 南京: 南京大学, 2013.
29	QIANZ J, ZHONG S, SUN G F, et al. A formal approach to design and security verification of operating systems for intelligent transportation systems based on object model [J]. IEEE Transactions on Intelligent Transportation Systems, 2022, 24(12): 15459-15467.
	QIANZ J, ZHONG S, SUN G F, et al. A formal approach to design and security verification of operating systems for intelligent transportation systems based on object model [J]. IEEE Transactions on Intelligent Transportation Systems, 2022, 24(12): 15459-15467.
30	郭建, 丁继政, 朱晓冉.. 嵌入式实时操作系统内核混合代码的自动化验证框架. 软件学报, 2020, 31 (5): 1353- 1373.
31	关钰千. 嵌入式操作系统内核服务的形式化验证与设计开发[D]. 上海: 华东师范大学, 2021.
32	朱晓冉. 基于重写逻辑的嵌入式操作系统建模与验证技术研究[D]. 上海: 华东师范大学, 2019.
33	GUAN Y Q, GUO J, LI Q.. Formal verification of a hybrid IoT operating system model. IEEE Access, 2021, (9): 59171- 59183.
34	史建琦. 面向目标代码的实时操作系统形式化验证方法研究[D]. 上海: 华东师范大学, 2012.
35	彭云辉. 基于AUTOSAR 的汽车电子操作系统及其应用的建模与分析[D]. 上海: 华东师范大学, 2014.
36	ANTHONY C J F, GARETH S, SHALE X, et al. A verification methodology for the Arm^® confidential computing architecture: From a secure specification to safe implementations [C]// Proceedings of the ACM on Programming Languages. 2023: 376-405.
37	HUANG Y H, ZHAO Y X, ZHU L F, et al. Modeling and verifying the code-level OSEK/VDX operating system with CSP [C]// 2011 Fifth International Conference on Theoretical Aspects of Software Engineering. 2011: 142-149.
38	SUN HY, LEI Y.. A design and verification methodology for a TrustZone trusted execution environment. IEEE Access, 2020, (8): 33870- 33883.
39	SUN H Y, LEI H.. Formal verification of a task scheduler for embedded operating systems. Journal of Intelligent & Fuzzy Systems, 2020, 38 (2): 1391- 1399.
40	FENG Z, ZHAO Y W. Fine-grained formal specification and analysis of buddy memory allocation in zephyr RTOS [C]// Proceedings of the 2019 IEEE 22nd International Symposium on Real-Time Distributed Computing. 2019: 10-17.
41	姜菁菁, 乔磊, 杨孟飞, 等.. 基于Coq的操作系统任务管理需求层建模及验证. 软件学报, 2020, 31 (8): 2375- 2387.
42	张啸然.. 实时操作系统中有限优先级反转的验证. 小型微型计算机系统, 2021, 42 (1): 1- 8.