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]	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.
[3]	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.
[4]	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.
[5]	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.
[6]	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.
[7]	Tingyu ZHANG, Lin YUAN, Chao ZHANG, Yang LI, Zhiyuan ZHAO, Yuxiao SHI, Liquan ZHANG, Jinghua GU. Effects of coastal engineering and biological invasion on changes in the coastal pattern of Nanhui Dongtan, Shanghai [J]. Journal of East China Normal University(Natural Science), 2023, 2023(3): 167-180.
[8]	Xiaoting WANG, Hualong LUAN, Weiguo ZHANG, Nina Siu-Ngan LAM. Assessment of land use exposure to coastal erosion in the delta region and its implications on spatial planning: An example from the Pudong New Area of Shanghai [J]. Journal of East China Normal University(Natural Science), 2023, 2023(3): 181-193.
[9]	Zhaoyang WU, Jiali MAO. Research on travel time prediction based on neural network [J]. Journal of East China Normal University(Natural Science), 2023, 2023(2): 106-118.
[10]	Yang ZHANG, Yejing LAI, Dingjiang HUANG. Device component state recognition method of power distribution cabinet based on a residual networks [J]. Journal of East China Normal University(Natural Science), 2023, 2023(2): 132-142.
[11]	Zhuqing HE, Xinyi LIAO, Nuo DING. Spatial and temporal distribution of Tettigonioidea and Grylloidea at different altitudes of Tianmu Mountain [J]. Journal of East China Normal University(Natural Science), 2022, 2022(6): 123-129.
[12]	Mengnan LIU, Jianqiu XU. Two-level trajectory data partition algorithm based on query cost [J]. Journal of East China Normal University(Natural Science), 2022, 2022(5): 184-194.
[13]	Tao ZOU, Rongtao QIAN, Jiali MAO. Indexing and query technology for steel logistic data [J]. Journal of East China Normal University(Natural Science), 2022, 2022(5): 195-207.
[14]	Xin MENG, Valentin IVANNIKOV, Tim BYRNES. Bell correlation of separated two-mode squeezed Bose-Einstein condensates [J]. Journal of East China Normal University(Natural Science), 2022, 2022(4): 131-138.
[15]	Xiaozhen ZHAO, Weiqing TONG, Yongmei LIU. A graph convolutional neural network for garment pattern classification [J]. Journal of East China Normal University(Natural Science), 2022, 2022(4): 56-66.