A formal verification method for embedded operating systems

doi:10.3969/j.issn.1000-5641.2024.04.001

Abstract

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

CLC Number:

TP316

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.

Figures/Tables 10

Fig.1

Fig.2

Fig.3

Fig.4

Fig.5

Fig.6

Fig.7

Fig.8

Fig.9

Fig.10

References 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.

[1]	GAO Qin-qin， ZHU Jian-rong， DUAN Yi-hong， SUN Ming-hua. Impacts of the symmetrical and unsymmetrical typhoons on the storm surge simulation in the East China and the South China Seas [J]. Journal of East China Normal University(Natural Sc, 20120, 2012(6): 57-72.
[2]	Ying LI, Ye HUANG, Ye LI, Min LIU. Spatiotemporal distribution characteristics and respiratory exposure risk of PCDD/Fs in Shanghai, China [J]. Journal of East China Normal University(Natural Science), 2024, 2024(6): 124-135.
[3]	Yuyi WANG, Ye HUANG, Jing YANG, Fangfang DING, Tianhao HE, Yushan LI, Lin HUANG, Ye LI, Min LIU. Spatiotemporal differential distribution characteristics and ecological risk assessment of antibiotics in the Yangtze River Estuary and offshore areas [J]. Journal of East China Normal University(Natural Science), 2024, 2024(6): 136-150.
[4]	Dingye YANG, Jing YANG, Ruihe JIN, Fangfang DING, Yuxin ZHANG, Min LIU. Occurrence characteristics and risk assessment of halogenated flame retardants in soils of Hefei City [J]. Journal of East China Normal University(Natural Science), 2024, 2024(6): 161-177.
[5]	Jing YANG, Yan WU, Yue LI, Xia LIU, Dingye YANG, Yuanyuan CHEN, Ruihe JIN, Ye LI, Min LIU. Occurrence characteristics and healthy risk assessment of hexabromocyclododecane in agricultural soils in Shanghai [J]. Journal of East China Normal University(Natural Science), 2024, 2024(6): 178-187.
[6]	Ruihe JIN, Yuyun YANG, Yan WU, Jing YANG, Min LIU. Regional-specific distribution of organophosphate esters in road dust from multiple land types [J]. Journal of East China Normal University(Natural Science), 2024, 2024(6): 62-73.
[7]	Bao LI, Ruihe JIN, Yuxin ZHANG, Manjing RUAN, Yan WU, Jing YANG, Min LIU. Multi-media distribution and partitioning behavior of organophosphate esters in the Yangtze River Estuary [J]. Journal of East China Normal University(Natural Science), 2024, 2024(6): 99-113.
[8]	Hao CUI, Wenyao ZHENG, Xing ZHANG, Cheng JIANG, Xiaoliang MAO, Lianjun SHENG, Fan BAI, Dingjiang HUANG. Design and implementation of an intelligent patrol system based on microservices [J]. Journal of East China Normal University(Natural Science), 2024, 2024(5): 183-192.
[9]	Linding XIE, Yuan ZHANG, Yihong CAI. Bioinformatics-based construction of immune prognostic gene model for hepatocellular carcinoma and preliminary model validation [J]. Journal of East China Normal University(Natural Science), 2024, 2024(4): 100-110.
[10]	Yufei LIN, Wei XIE. High-fidelity transmission of optical polarization based on beam splitters [J]. Journal of East China Normal University(Natural Science), 2024, 2024(4): 47-56.
[11]	Xiang’en CHEN, Jing CAO. ${\rm{E}} $ -total coloring of cycles and paths which are vertex-distinguished by multiple sets [J]. Journal of East China Normal University(Natural Science), 2024, 2024(2): 14-22.
[12]	Yan TIAN, Yang JIAO, Haoran YU. Several classes of sign pattern matrices that allow algebraic positivity [J]. Journal of East China Normal University(Natural Science), 2024, 2024(2): 23-29.
[13]	Man PENG, Yiping SHAO, Bei PEI, Mengjie YANG, Gen LI, Wanruo WEN, Kai YANG. Spatial-temporal pattern and regional regulation of supply and demand of ecosystem services in the Yangtze River Delta integration demonstration zone [J]. Journal of East China Normal University(Natural Science), 2023, 2023(6): 145-157.
[14]	Lulu JIANG, Siqi SUN, Haidong ZOU, Lina LU, Rui FENG. Diabetic retinopathy grading based on dual-view image feature fusion [J]. Journal of East China Normal University(Natural Science), 2023, 2023(6): 39-48.
[15]	Lianjun SHENG, Zhixuan TANG, Xiaoliang MAO, Fan BAI, Dingjiang HUANG. Smoke detection based on spatial and frequency domain methods [J]. Journal of East China Normal University(Natural Science), 2023, 2023(5): 147-163.