Review of Formal Specification and Verification for Operating Systems

doi:10.19678/j.issn.1000-3428.0069799

Abstract

Abstract: Operating Systems (OSs), which form a critical infrastructure in the information age, are widely used in core fields such as medical care, industries, and the military. Their reliability and security directly determine the operational stability of these key fields, while vulnerabilities can lead to serious consequences, including system crashes and data leakage. Hence, the construction of a systematic security assurance system would be of great theoretical and engineering value. This paper systematically reviews the research achievements in this field over the past decade based on the framework of ″formal specification—formal verification—engineering implementation″ and analyzes technical paths and practical applications. With regard to formal specification level, it clarifies the differences between model specifications that describe system functions based on mathematical structures, such as transition systems, and property specifications that define safety and liveness requirements based on Linear Temporal Logic (LTL). This analysis focuses on two key aspects: functional correctness and security attributes. Functional correctness covers task management scheduling, memory allocation and recycling, exception interrupt handling, inter-task communication, and file system read—write consistency, while security attributes focus on the BLP and BIBA models for access control, multidomain isolation in separation kernels, and noninterference and nonleakage theories of information flow. For formal verification, three core methods are considered: deductive proof, which verifies program consistency by relying on Hoare's logic; model checking, which verifies temporal properties based on LTL and Computation Tree Logic (CTL); and standardized process of property verification. Taking the seL4 microkernel, which is the first to achieve functional correctness and information flow non-interference through machine proof, as a case study, this discussion reveals the transformation from theory to engineering. With regard to engineering applications, the achievements in Controller Area Network (CAN) bus communication verification within the automotive field and robustness detection of intercomponent communication in the Android system of smartphones are summarized. This systematic review aims to establish a foundation for future research in related fields, provide dataset support for large language models, and provide a reference for the engineering implementation of these technologies.

Key words: Operating System (OS), formal method, formal specification, formal verification, system security

摘要： 操作系统(OS)作为信息时代关键基础设施,广泛应用于军事、工业、医疗等核心领域。其可靠性与安全性直接决定关键领域运行稳定,漏洞易致系统崩溃、数据泄露等严重后果,因此构建系统化安全保障体系具有重要理论与工程价值。以"形式规约-形式验证-工程落地"为框架,梳理近十年该领域研究成果,剖析技术路径与实践应用。在形式规约层面,明确基于迁移系统等数学结构描述系统功能的模型规约与基于线性时序逻辑(LTL)定义安全、活性需求的性质规约的差异,从功能正确性和安全属性两个方面进行阐述,其中,功能正确性涵盖任务管理调度、内存分配回收、异常中断处理、任务间通信与文件系统读写一致性,安全属性聚焦访问控制的BLP模型与BIBA模型、分离内核多域隔离、信息流无干扰与无泄漏理论。在形式验证层面,阐述依托霍尔逻辑验证程序一致性的推理证明、基于LTL与计算树逻辑(CTL)验证时序属性的模型检测、属性验证标准化流程3类核心方法,并以首个通过机器证明实现功能正确与信息流无干扰的seL4微内核为案例,揭示理论到工程的转化路径。在工程应用上,总结汽车领域控制器局域网(CAN)总线通信验证、智能手机Android系统组件间通信鲁棒性检测的成果。本文的系统性梳理旨在为相关领域的研究奠定基础,为大语言模型提供数据集支持,并为最终的技术工程落地提供参考。

关键词: 操作系统, 形式化方法, 形式规约, 形式验证, 系统安全

CLC Number:

TP311

WANG Zi, WANG Hongqiang, YANG Xiaoyi, LAN Yuqing. Review of Formal Specification and Verification for Operating Systems[J]. Computer Engineering, 2026, 52(2): 24-45.

王梓, 王洪强, 杨晓艺, 兰雨晴. 操作系统形式规约与验证综述[J]. 计算机工程, 2026, 52(2): 24-45.

/ Recommend / Download Citations

URL: https://www.ecice06.com/EN/10.19678/j.issn.1000-3428.0069799

https://www.ecice06.com/EN/Y2026/V52/I2/24

References

[1] 兰雨晴. 操作系统——信息时代的关键基础设施[N], 人民日报, 2023-05-30(20). LAN Y Q. Operating system—key infrastructure in the information age[N]. People’s Daily, 2023-05-30(20).(in Chinese)
[2] 詹乃军, 王戟. 复杂系统规约、分析与验证发展现状与展望[J]. 前瞻科技, 2023, 2(1): 7-22. ZHAN N J, WANG J. Challenges and trends for specification, analysis, and verification of complex systems[J]. Science and Technology Foresight, 2023, 2(1): 7-22. (in Chinese)
[3] 王戟, 詹乃军, 冯新宇, 等. 形式化方法概貌[J]. 软件学报, 2018, 30(1): 33-61. WANG J, ZHAN N J, FENG X Y, et al. Overview of formal methods[J]. Journal of Software, 2018, 30(1): 33-61. (in Chinese)
[4] LAMPORT L. Proving the correctness of multiprocess programs[J]. IEEE Transactions on Software Engineering, 1977, 3(2): 125-143.
[5] ALPERN B, SCHNEIDER F B. Recognizing safety and liveness[J]. Distributed Computing, 1987, 2(3): 117-126.
[6] 姜菁菁, 乔磊, 杨孟飞, 等. 基于Coq的操作系统任务管理需求层建模及验证[J]. 软件学报, 2020, 31(8): 2375-2387. JIANG J J, QIAO L, YANG M F, et al. Operating system task management requirements layer modeling and verification based on Coq[J]. Journal of Software, 2020, 31(8): 2375-2387. (in Chinese)
[7] 谭彦亮, 杨桦, 乔磊. 基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证[J]. 空间控制技术与应用, 2014, 40(4): 57-62. TAN Y L, YANG H, QIAO L. Formal modeling and verification of task-management requirement for SpaceOS2 based on Event-B[J]. Aerospace Control and Application, 2014, 40(4): 57-62. (in Chinese)
[8] 顾海博, 付明, 乔磊, 等. SpaceOS中若干全局性质的形式化描述和验证[J]. 小型微型计算机系统, 2019, 40(1): 141-148. GU H B, FU M, QIAO L, et al. Formalization and verification of several global properties of SpaceOS[J]. Journal of Chinese Computer Systems, 2019, 40(1): 141-148. (in Chinese)
[9] 张林雁, 李希萌, 施智平, 等. 微内核操作系统互斥量模块功能正确性的形式化验证[J]. 软件学报, 2024, 35(9): 4179-4192. ZHANG L Y, LI X M, SHI Z P, et al. Formal verification of functional correctness for mutexes in microkernel[J]. Journal of Software, 2024, 35(9): 4179-4192. (in Chinese)[10] 王若川,  杨孟飞, 乔磊. 基于时间自动机的操作系统中断管理建模与验证[J]. 空间控制技术与应用, 2014, 40(4): 52-56. WANG R C, YANG M F, QIAO L. Modeling and verification of operating system interrupt management based on timed automata[J]. Aerospace Control and Application, 2014, 40(4): 52-56. (in Chinese)[11] 李佳洁,  陈哲, 陈龙腾. 一种基于无锁队列的运行时多线程并行验证方法[J]. 小型微型计算机系统, 2024, 45(5): 1249-1256. LI J J, CHEN Z, CHEN L T. Runtime multi-thread parallel verification method based on lock-free queues[J]. Journal of Chinese Computer Systems, 2024, 45(5): 1249-1256. (in Chinese)[12] LI  P, RAVINDRAN B, SUHAIB S, et al. A formally verified application-level framework for real-time scheduling on POSIX real-time operating systems[J]. IEEE Transactions on Software Engineering, 2004, 30(9): 613-629.[13] XU  F W, FU M, FENG X Y, et al. A practical verification framework for preemptive OS kernels[M]. Berlin, Germany: Springer International Publishing, 2016.[14] 乔磊,  杨孟飞, 谭彦亮, 等. 基于Event-B的航天器内存管理系统形式化验证[J]. 软件学报, 2017, 28(5): 1204-1220. QIAO L, YANG M F, TAN Y L, et al. Formal verification of memory management system in spacecraft using Event-B[J]. Journal of Software, 2017, 28(5): 1204-1220. (in Chinese)[15] 李少峰,  乔磊, 杨孟飞, 等. 面向安全关键内存管理系统分层验证方法[J]. 软件学报, 2022, 33(6): 2312-2330. LI S F, QIAO L, YANG M F, et al. Verification method of hierarchical for safety-critical memory management systems[J]. Journal of Software, 2022, 33(6): 2312-2330. (in Chinese)[16] 钱振江,  刘永俊, 姚宇峰, 等. 微内核架构内存管理的形式化设计和验证方法研究[J]. 电子学报, 2017, 45(1): 251-256. QIAN Z J, LIU Y J, YAO Y F, et al. Research on method of formal design and verification of memory management based on microkernel architecture[J]. Acta Electronica Sinica, 2017, 45(1): 251-256. (in Chinese)[17] 章乐平,  赵永望, 王布阳, 等. L4虚拟内存子系统的形式化验证[J]. 软件学报, 2023, 34(8): 3527-3548. ZHANG L P, ZHAO Y W, WANG B Y, et al. Formal verification of virtual memory subsystem in L4[J]. Journal of Software, 2023, 34(8): 3527-3548. (in Chinese)[18] 李薛剑,  王俊宜. 基于类C语言内存模型的复杂数据结构验证方法[J]. 计算机技术与发展, 2024, 34(8): 57-66. LI X J, WANG J Y. C-like memory model based verification method for complex data structures[J]. Computer Technology and Development, 2024, 34(8): 57-66. (in Chinese)[19] CUI  J, DUAN Z H, TIAN C, et al. Modeling and verification of an interrupt system in μC/OS-III with TMSVL[C]//Proceedings of International Workshop on Structured Object-Oriented Formal Language and Method. Berlin, Germany: Springer International Publishing, 2016: 15-28.[20] 马智,  乔磊, 杨孟飞, 等. 面向SPARC处理器架构的操作系统异常管理验证[J]. 软件学报, 2021, 32(6): 1631-1646. MA Z, QIAO L, YANG M F, et al. Verification of operating system exception management for SPARC processor architecture[J]. Journal of Software, 2021, 32(6): 1631-1646. (in Chinese)[21] CARBONNEAUX  Q, ZILBERSTEIN N, KLEE C, et al. Applying formal verification to microkernel IPC at meta[C]//Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York, USA: ACM Press, 2022: 116-129.[22] 姜玉蓉.  LINUX进程间通信的模型检测[J]. 计算机科学, 2008, 35(10):295-299. JIANG Y R. Model checking for LINUX interprocess communication[J]. Computer Science, 2008, 35(10):295-299. (in Chinese)[23] 祁方民,  鱼滨, 牟力科, 等. 基于CCS的信号量形式化建模与验证[J]. 计算机应用与软件, 2011, 28(8): 230-233. QI F M, YU B, MOU L K, et al. Formal modeling and validation of semaphore based on CCS[J]. Computer Applications and Software, 2011, 28(8): 230-233. (in Chinese)[24] 王亚,  王瑞, 关永, 等. RGMP-ROS混合机器人操作系统节点间通信的形式化验证[J]. 小型微型计算机系统, 2015, 36(10): 2379-2383. WANG Y, WANG R, GUAN Y, et al. Formal verification of node communications in the hybrid robot operating system RGMP-ROS[J]. Journal of Chinese Computer Systems, 2015, 36(10): 2379-2383. (in Chinese)[25] 钱振江,  唐洪英, 李康杰, 等. 微内核架构文件系统的形式化设计与验证方法研究[J]. 小型微型计算机系统, 2013, 34(10): 2261-2266. QIAN Z J, TANG H Y, LI K J, et al. Research on methodology of formal design and verification for file system based on microkernel architecture[J]. Journal of Chinese Computer Systems, 2013, 34(10): 2261-2266. (in Chinese)[26] SIGURBJARNARSON  H, BORNHOLT J, TORLAK E, et al. Push-button verification of file systems via crash refinement[C]//Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation. New York, USA: ACM Press, 2016: 1-16.[27] ILERI  A, CHAJED T, CHLIPALA A, et al. Proving confidentiality in a file system using DiskSec[C]//Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation. New York, USA: ACM Press, 2018: 323-338.[28] DENNIS  J B, VAN HORN E C. Programming semantics for multiprogrammed computations[J]. Communications of the ACM, 1966, 9(3): 143-155.[29] BELL  D E, LAPADULA L J. Secure computer systems: mathematical foundations[M].[S. l.]: National Technical Information Service, 1989.[30] BIBA  K J. Integrity considerations for secure computer systems[EB/OL].[2024-03-11]. https://www.researchgate.net/publication/235043659_Integrity_Considerations_for_Secure_Computer_Systems.[31] SANDHU  R S. Role-based access control[M]. Amsterdam, Holland: Elsevier, 1998.[32] FERRAIOLO  D F, BARKLEY J F, KUHN D R. A role-based access control model and reference implementation within a corporate Intranet[J]. ACM Transactions on Information and System Security, 1999, 2(1): 34-64.[33] COULOURIS  G, DOLLIMORE J, ROBERTS M. Role and task-based access control in the PerDiS groupware platform[C]//Proceedings of the 3rd ACM Workshop on Role-Based Access Control. New York, USA: ACM Press, 1998: 115-121.[34] OH  S, PARK S. Task-role-based access control model[J]. Information Systems, 2003, 28(6): 533-562.[35] YAO  L, KONG X W, XU Z C. A task-role based access control model with multi-constraints[C]//Proceedings of the 4th International Conference on Networked Computing and Advanced Information Management. Washington D.C., USA: IEEE Press, 2008: 137-143.[36] CAI  F B, ZHU N F, HE J S, et al. Survey of access control models and technologies for cloud computing[J]. Cluster Computing, 2019, 22(3): 6111-6122.[37] 李凤华,  苏铓, 史国振, 等. 访问控制模型研究进展及发展趋势[J]. 电子学报, 2012, 40(4): 805-813. LI F H, SU M, SHI G Z, et al. Research status and development trends of access control model[J]. Acta Electronica Sinica, 2012, 40(4): 805-813. (in Chinese)[38] 李晓峰,  冯登国, 陈朝武, 等. 基于属性的访问控制模型[J]. 通信学报, 2008, 29(4): 90-98. LI X F, FENG D G, CHEN Z W, et al. Model for attribute based access control[J]. Journal on Communications, 2008, 29(4): 90-98. (in Chinese)[39] COETZEE  M, ELOFF J H P. Towards Web service access control[J]. Computers & Security, 2004, 23(7): 559-570.[40] ANGGOROJATI  B, MAHALLE P, PRASAD N, et al. Capability-based access control delegation model on the federated IoT network[C]//Proceedings of the 15th International Symposium on Wireless Personal Multimedia Communications. Washington D.C., USA: IEEE Press, 2012: 604-608.[41] 李凤华,  王巍, 马建峰, 等. 基于行为的访问控制模型及其行为管理[J]. 电子学报, 2008, 36(10): 1881-1890. LI F H, WANG W, MA J F, et al. Action-based access control model and administration of actions[J]. Acta Electronica Sinica, 2008, 36(10): 1881-1890. (in Chinese)[42] LI  F, SHI G, ZHANG J, et al. An action-based access control model implementation for MLS information systems[C]//Proceedings of the 2012 International Conference on Computer Application and System Modeling.[S. l.]: Atlantis Press, 2012: 1080-1083.[43] RAY  I, KUMAR M. Towards a location-based mandatory access control model[J]. Computers & Security, 2006, 25(1): 36-44.[44] ARDAGNA  C A, CREMONINI M, DAMIANI E, et al. Supporting location-based conditions in access control policies[C]//Proceedings of the 2006 ACM Symposium on Information, Computer and Communications Security. New York, USA: ACM Press, 2006: 212-222.[45] DAMIANI  M L, BERTINO E, PERLASCA P. Data security in location-aware applications: an approach based on RBAC[J]. International Journal of Information and Computer Security, 2007(1/2): 5.[46] BERTINO  E, BONATTI P A, FERRARI E. TRBAC: a temporal role-based access control model[C]//Proceedings of the 5th ACM Workshop on Role-Based Access Control. New York, USA: ACM Press, 2000: 21-30.[47] JOSHI  J B D, BERTINO E, LATIF U, et al. A generalized temporal role-based access control model[J]. IEEE Transactions on Knowledge and Data Engineering, 2005, 17(1): 4-23.[48] SHAFIQ  B, JOSHI J B D, BERTINO E, et al. Secure interoperation in a multidomain environment employing RBAC policies[J]. IEEE Transactions on Knowledge and Data Engineering, 2005, 17(11): 1557-1577.[49] GHAZAL  R, MALIK A, RAZA B, et al. Agent-based semantic role mining for intelligent access control in multi-domain collaborative applications of smart cities[J]. Sensors, 2021, 21(13): 4253.[50] YANG  B Y, HU H S. Secure conflicts avoidance in multidomain environments: a distributed approach[J]. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 2021, 51(9): 5478-5489.[51] RUSHBY  J M. Design and verification of secure systems[J]. ACM SIGOPS Operating Systems Review, 1981, 15(5): 12-21.[52] RUSHBY  J M. Proof of separability A verification technique for a class of security kernels[M]. Berlin, Germany: Springer, 1982.[53] FOSS  J A, OMAN P W, TAYLOR C, et al. The MILS architecture for high-assurance embedded systems[J]. International Journal of Embedded Systems, 2006, 2(3/4): 239.[54] VANFLEET  W M, LUKE J A, BECKWITH R W, et al. MILS: architecture for high-assurance embedded computing[J]. CrossTalk, 2005, 18(8): 12-16.[55] PARKINSON  P. Safety, security and multicore[C]//Proceedings of the 19th Safety-Critical Systems Symposium. Berlin, Germany: Springer, 2010: 215-232.[56] ZHAO  Y W, YANG Z B, MA D F. A survey on formal specification and verification of separation kernels[J]. Frontiers of Computer Science, 2017, 11(4): 585-607.[57] ZHAO  Y W, SANÁN D, ZHANG F Y, et al. Refinement-based specification and security analysis of separation kernels[J]. IEEE Transactions on Dependable and Secure Computing, 2019, 16(1): 127-141.[58] ZHAO  Y, SANAN D, ZHANG F, et al. Reasoning about information flow security of separation kernels with channel-based communication[C]//Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Germany: Springer, 2016: 791-810.[59] ZHAO  Y W, SANAN D, ZHANG F Y, et al. Formal specification and analysis of partitioning operating systems by integrating ontology and refinement[J]. IEEE Transactions on Industrial Informatics, 2016, 12(4): 1321-1331.[60] NELSON  L, BORNHOLT J, KRISHNAMURTHY A, et al. Noninterference specifications for secure systems[J]. ACM SIGOPS Operating Systems Review, 2020, 54(1): 31-39.[61] GOGUEN  J A, MESEGUER J. Security policies and security models[C]//Proceedings of the IEEE Symposium on Security and Privacy. Washington D.C., USA: IEEE Press, 1982: 1-11.[62] HAIGH  J T, YOUNG W D. Extending the noninterference version of MLS for SAT[J]. IEEE Transactions on Software Engineering, 1987, 13(2): 141-150.[63] LI  P, ZDANCEWIC S. Downgrading policies and relaxed noninterference[C]//Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, USA: ACM Press, 2005: 158-170.[64] VON  OHEIMB D. Information flow control revisited: noninfluence = noninterference + nonleakage[C]//Proceedings of ESORICS’04. Berlin, Germany: Springer, 2004: 225-243.[65] RUSHBY  J. Noninterference, transitivity, and channel-control security policies[M]. Menlo Park, USA: SRI International Computer Science Laboratory, 1992.[66] SIGURBJARNARSON  H, NELSON L, CASTRO-KARNEY B, et al. Nickel: a framework for design and verification of information flow control systems[C]//Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation. New York, USA: ACM Press, 2018: 1-9.[67] 孙海泳,  杨霞, 雷航, 等. 基于TrustZone的TEE设计与信息流形式化验证[J]. 电子科技大学学报, 2019, 48(2): 259-263. SUN H Y, YANG X, LEI H, et al. The design of TEE based on TrustZone and formal verification of information flow[J]. Journal of University of Electronic Science and Technology of China, 2019, 48(2): 259-263. (in Chinese)[68] ZDANCEWIC  S. Challenges for information-flow security[C]//Proceedings of the 1st International Workshop on the Programming Language Interference and Dependence. New York, USA: ACM Press, 2004, 6-15.[69] MURRAY  T, MATICHUK D, BRASSIL M, et al. seL4: from general purpose to a proof of information flow enforcement[C]//Proceedings of the IEEE Symposium on Security and Privacy. Washington D.C., USA: IEEE Press, 2013: 415-429.[70] MURRAY  T, MATICHUK D, BRASSIL M, et al. Noninterference for operating system kernels[C]//Proceedings of the 2nd International Conference on Certified Programs and Proofs. Berlin, Germany: Springer, 2012: 126-142.[71] LEROY  X. A formally verified compiler back-end[J]. Journal of Automated Reasoning, 2009, 43(4): 363-446.[72] HOARE  C A R. An axiomatic basis for computer programming[J]. Communications of the ACM, 1969, 12(10): 576-580.[73] FLOYD  R W. Assigning meanings to programs[M]. Berlin, Germany: Springer, 1993.[74] DE  BOER F S, HIEP H A. Completeness and complexity of reasoning about call-by-value in Hoare logic[J]. ACM Transactions on Programming Languages and Systems, 2021, 43(4): 1-35.[75] OWICKI  S, GRIES D. An axiomatic proof technique for parallel programs I[J]. Acta Informatica, 1976, 6(4): 319-340.[76] JONES  C B. Tentative steps toward a development method for interfering programs[J]. ACM Transactions on Programming Languages and Systems, 1983, 5(4): 596-619.[77] OWICKI  S, GRIES D. Verifying properties of parallel programs[J]. Communications of the ACM, 1976, 19(5): 279-285.[78] O’HEARN  P W. Resources, concurrency, and local reasoning[J]. Theoretical Computer Science, 2007, 375(1/2/3): 271-307.[79] UTIYAMA  R. Invariant theoretical interpretation of interaction[J]. Physical Review, 1956, 101(5): 1597-1607.[80] NOETHER  E. Invariant variation problems[J]. Transport Theory and Statistical Physics, 1971, 1(3): 186-207.[81] HARRISON  M A. Introduction to formal language theory[M].[S. l.]: Addison-Wesley Longman Publishing Co., Inc., 1978.[82] KELLER  R M. Formal verification of parallel programs[J]. Communications of the ACM, 1976, 19(7): 371-384.[83] 葛宁,  贺俞凯, 翟树茂, 等. 共识协议的形式化验证研究现状与展望[J]. 软件学报, 2023, 34(11): 4989-5007. GE N, HE Y K, ZHAI S M, et al. Formal verification of consensus protocols: survey and perspective[J]. Journal of Software, 2023, 34(11): 4989-5007. (in Chinese)[84] 陈锦富,  冯乔伟, 蔡赛华, 等. 基于形式化方法的区块链系统漏洞检测模型[J]. 软件学报, 2024, 35(9): 4193-4217. CHEN J F, FENG Q W, CAI S H, et al. Vulnerability detection model for blockchain systems based on formal method[J]. Journal of Software, 2024, 35(9): 4193-4217. (in Chinese)[85] GEATTI  L, GIANOLA A, GIGANTE N. Linear temporal logic modulo theories over finite traces[C]//Proceedings of IJCAI’22. New York, USA: ACM Press, 2022: 2641-2647.[86] YE  X, SHI J Q, HUANG Y H, et al. Parallel computational tree logic model-checking on pushdown systems[J]. Concurrency and Computation: Practice and Experience, 2022, 34(23): 7173.[87] PNUELI  A. The temporal logic of programs[C]//Proceedings of the 18th Annual Symposium on Foundations of Computer Science. Washington D.C., USA: IEEE Press, 1977: 46-57.[88] ANEVLAVIS  T, PHILIPPE M, NEIDER D, et al. Being correct is not enough: efficient verification using robust linear temporal logic[J]. ACM Transactions on Computational Logic, 2022, 23(2): 1-39.[89] CLARKE  E M, EMERSON E A. Design and synthesis of synchronization skeletons using branching time temporal logic[C]//Proceedings of Workshop on Logic of Programs. Berlin, Germany: Springer, 2005: 52-71.[90] 骆翔宇,  黄欣玥, 古天龙, 等. 基于时态测试器的实时分支时态逻辑模型检测[J]. 软件学报, 2022, 33(8): 2930-2946. LUO X Y, HUANG X Y, GU T L, et al. Model checking for real-time branching-time temporal logic based on temporal testers[J]. Journal of Software, 2022, 33(8): 2930-2946. (in Chinese)[91] 张华强,  李凯航, 王继刚. 基于线性时态逻辑的物联网操作系统安全性设计[J]. 电子技术应用, 2020, 46(2): 92-97, 102. ZHANG H Q, LI K H, WANG J G. Safety design of IoT operating system based on linear temporal logic[J]. Application of Electronic Technique, 2020, 46(2): 92-97, 102. (in Chinese)[92] SUN  J W, LONG X, ZHAO Y W. A verified capability-based model for information flow security with dynamic policies[J]. IEEE Access, 2018, 6: 16395-16407.[93] ELKADUWE  D, KLEIN G, ELPHINSTONE K. Verified protection model of the seL4 microkernel[C]//Proceedings of the 2nd International Conference Verified Software: Theories, Tools, Experiments. Berlin, Germany: Springer Berlin Heidelberg, 2008: 99-114.[94] KLEIN  G, ELPHINSTONE K, HEISER G, et al. seL4: formal verification of an OS kernel[C]//Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. New York, USA: ACM Press, 2009: 207-220.[95] KLEIN  G, ANDRONICK J, ELPHINSTONE K, et al. Comprehensive formal verification of an OS microkernel[J]. ACM Transactions on Computer Systems, 2014, 32(1): 1-70.[96] BRUN  M, ACHERMANN R, CHAJED T, et al. Beyond isolation: OS verification as a foundation for correct applications[C]//Proceedings of the 19th Workshop on Hot Topics in Operating Systems. New York, USA: ACM Press, 2023: 158-165.[97] MILLWOOD  J, VANVOSSEN R, ELLIOTT L. Performance impacts from the seL4 hypervisor[C]//Proceedings of the SAE Technical Paper Series. Novi, USA: National Defense Industrial Association, 2020: 13-15.[98] DORAN  M A, KANDALAFT N. Embedded virtualization on RISC-V with seL4[C]//Proceedings of the IEEE 14th Annual Ubiquitous Computing, Electronics & Mobile Communication Conference (UEMCON). Washington D.C., USA: IEEE Press, 2023: 736-740.[99] DE  MATOS E, LENNON C, VIEGAS E K, et al. Integrating VirtIO and QEMU on seL4 for enhanced devices virtualization support[C]//Proceedings of the IEEE 22nd International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom). Washington D.C., USA: IEEE Press, 2023: 1076-1085.
[100] SEWELL T, WINWOOD S, GAMMIE P, et al. seL4 enforces integrity[C]//Proceedings of International Conference on Interactive Theorem Proving. Berlin, Germany: Springer, 2011: 325-340.
[101] DE OLIVEIRA NUNES I, HWANG S, JAKKAMSETTI S, et al. mathcal ARseL: towards a verified root-of-trust over seL4[C]//Proceedings of the IEEE/ACM International Conference on Computer Aided Design (ICCAD). Washington D.C., USA: IEEE Press, 2023: 1-9.
[102] NICOLAE A, IROFTI P, LEUSTEAN I. OpenBSD formal driver verification with seL4[C]//Proceedings of the International Conference on Information Technology and Communications Security. Berlin, Germany: Springer, 2024: 144-156.
[103] LESLIE B, HEISER G. The seL4 core platform[EB/OL].[2024-03-11]. https://github.com/Kswin01/sel4cp.
[104] PATUREL M, SUBASINGHE I, HEISER G. First steps in verifying the seL4 core platform[C]//Proceedings of the 14th ACM SIGOPS Asia-Pacific Workshop on Systems. Seoul Republic of Korea. New York, USA: ACM Press, 2023: 9-15.
[105] HEISER G, KLEIN G, ANDRONICK J. seL4 in Australia[J]. Communications of the ACM, 2020, 63(4): 72-75
[106] 张芮, 王瑞, 楚敏. 智能汽车CAN总线通信系统的建模与验证[J]. 计算机应用与软件, 2020, 37(7): 1-8, 42. ZHANG R, WANG R, CHU M. Modeling and verification of CAN bus communication system in intelligent vehicle[J]. Computer Applications and Software, 2020, 37(7): 1-8, 42. (in Chinese)
[107] 李青, 朱晓冉, 郭建. AUTOSAR OS存储保护机制的形式化验证框架[J]. 计算机工程, 2017, 43(1): 79-85. LI Q, ZHU X R, GUO J. Formal verification framework for AUTOSAR OS storage protection mechanism[J]. Computer Engineering, 2017, 43(1): 79-85. (in Chinese)
[108] 夏春艳, 黄松, 郑长友, 等. 自动驾驶交叉路口测试场景建模及验证方法[J]. 软件学报, 2023, 34(7): 3002-3021. XIA C Y, HUANG S, ZHENG C Y, et al. Modeling and verification method of intersection test scenario for automated driving[J]. Journal of Software, 2023, 34(7): 3002-3021(in Chinese).
[109] MAJI A K, ARSHAD F A, BAGCHI S, et al. An empirical study of the robustness of inter-component communication in Android[C]//Proceedings of the IEEE/IFIP International Conference on Dependable Systems and Networks. Washington D.C., USA: IEEE Press, 2012: 1-12.
[110] JHA A K, LEE S, LEE W J. Modeling and test case generation of inter-component communication in Android[C]//Proceedings of the 2nd ACM International Conference on Mobile Software Engineering and Systems. New York, USA: ACM Press, 2015: 113-116.
[111] LI L, BARTEL A, BISSYANDÉ T F, et al. IccTA: detecting inter-component privacy leaks in Android Apps[C]//Proceedings of the IEEE/ACM 37th IEEE International Conference on Software Engineering. New York, USA: ACM Press, 2015: 280-291.
[112] SUN Q, CHEN Z, XU F, et al. A survey of neural code intelligence: paradigms, advances and beyond[EB/OL].[2024-03-11]. https://arxiv.org/abs/2403.14734.
[113] POLU S, SUTSKEVER I. Generative language modeling for automated theorem proving[EB/OL].[2024-03-11]. https://arxiv.org/abs/2009.03393.
[114] POLU S, HAN J M, ZHENG K, et al. Formal mathematics statement curriculum learning[EB/OL].[2024-03-11]. https://arxiv.org/abs/2202.01344.
[115] LAMPLE G, LACROIX T, LACHAUX M A, et al. Hypertree proof search for neural theorem proving[J]. Advances in Neural Information Processing Systems, 2022, 35: 26337-26349.
[116] WANG H M, YUAN Y, LIU Z Y, et al. DT-Solver: automated theorem proving with dynamic-tree sampling guided by proof-level value function[C]//Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). Stroudsburg, USA: ACL, 2023: 12632-12646.
[117] JIANG A Q, LI W, TWORKOWSKI S, et al. Thor: wielding hammers to integrate language models and automated theorem provers[J]. Advances in Neural Information Processing Systems, 2022, 35: 8360-8373.
[118] MIKUA M, ANTONIAK S, TWORKOWSKI S, et al. Magnushammer: a Transformer-based approach to premise selection[EB/OL].[2024-03-11]. https://arxiv.org/abs/2303.04488.
[119] WU Y, JIANG A Q, LI W, et al. Autoformalization with large language models[J]. Advances in Neural Information Processing Systems, 2022, 35: 32353-32368.
[120] JIANG A Q, WELLECK S, ZHOU J P, et al. Draft, sketch, and prove: guiding formal theorem provers with informal proofs[EB/OL].[2024-03-11]. https://arxiv.org/abs/2210.12283.
[121] FIRST E, RABE M N, RINGER T, et al. Baldur: whole-proof generation and repair with large language models[C]//Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. New York, USA: ACM Press, 2023: 1229-1241.
[122] ZHAO X, LI W, KONG L. Decomposing the enigma: subgoal-based demonstration learning for formal theorem proving[EB/OL].[2024-03-11]. https://arxiv.org/abs/2305.16366.
[123] WANG H, XIN H, ZHENG C, et al. Lego-prover: neural theorem proving with growing libraries[EB/OL].[2024-03-11]. https://arxiv.org/abs/2310.00656.

[1]	PENG Chengwei, YANG Jinji, YANG Guang. Formal Verification and Improvement of SAP-AKA Secondary Authentication Protocol [J]. Computer Engineering, 2025, 51(6): 204-211.
[2]	WANG Zhan, ZHANG Pengcheng, JIN Huiying, JI Shunhui. Future Attribute Verification of Service Composition in Cloud-Network Integration Environment [J]. Computer Engineering, 2025, 51(3): 310-319.
[3]	PENG Long, GAO Yuanjun, LIU Xiaodong, YU Jie. Survey of Communication and Programming Frameworks for Multi-Robot Systems [J]. Computer Engineering, 2025, 51(10): 37-52.
[4]	WANG Wenbin, QIAN Zhenjiang, JIN Yong, SUN Gaofei, XING Xiaoshuang, SU Chao, SUN Tianqi. Formal Design and Verification of File System Based on Isabelle/HOL [J]. Computer Engineering, 2024, 50(4): 277-285.
[5]	ZHAO Dadi, WANG Keming. Safety-Critical System Development Method Based on Translating State Chart to B Formal Model [J]. Computer Engineering, 2024, 50(11): 173-186.
[6]	YU Xinsheng, ZHU Danjiang, LUO Lunhan. System Security Analysis Method Based on CLPN [J]. Computer Engineering, 2024, 50(10): 255-265.
[7]	YAN Qianqian, MIAO Weikai. Scenario-based Requirement Analysis Method for Railway Control Software [J]. Computer Engineering, 2021, 47(8): 284-293,300.
[8]	YANG Jinxiang, XIONG Yan, HUANG Wenchao. Research on Optimization of Security Protocol Formal Verification Based on Reinforcement Learning [J]. Computer Engineering, 2021, 47(12): 141-146.
[9]	XIA Rui, QIAN Zhenjiang, LIU Wei. A Verification Method of Security Communication Protocol Based on Isabelle/HOL [J]. Computer Engineering, 2021, 47(1): 146-153.
[10]	OUYANG Hengyi, XIONG Yan, HUANG Wenchao. A Formal Modeling and Verification Method for Token Smart Contract [J]. Computer Engineering, 2020, 46(10): 41-45,51.
[11]	CHEN Jinxin,SU Wen. Research on automated module composition method based on Event-B [J]. Computer Engineering, 2019, 45(5): 298-307,314.
[12]	LIN Rongfeng, SHI Jian, ZHU Yanqing, SHEN Yiwei, ZHOU Yu. Formal Verification Framework of SCADE Model Based on STP Method [J]. Computer Engineering, 2019, 45(10): 70-77.
[13]	QI Longyun, Lü Xiaoliang, LU Hong, HUANG Hao. Automatic Formal Specification and Its Verification of Assembly-Level Sequential Statement Blocks [J]. Computer Engineering, 2019, 45(10): 64-69,77.
[14]	LI Kun,ZHANG Xuesong. Design and Formal Verification of Safety Communication Protocol in STP [J]. Computer Engineering, 2018, 44(12): 120-128.
[15]	LI Qing,ZHU Xiaoran,GUO Jian. Formal Verification Framework for AUTOSAR OS Storage Protection Mechanism [J]. Computer Engineering, 2017, 43(1): 79-85.

Please choose a citation manager

Content to export