@inproceedings{32cff2e2ce5f46c38564be10b913d179,
title = "A Comprehensive Specification and Verification of the L4 Microkernel API",
abstract = "The L4 API (Application Programming Interface) is a core component of the operating system, which serves as the interface between user-level processes and the microkernel, facilitating communication and interaction. It is crucial to ensure the correctness and reliability of the API. This paper proposes a comprehensive formal specification and verification for the L4 microkernel API. The specification is reusable for all implementations on architectures supported by the microkernel. To further improve reusability (e.g., for the L4 family), a parameterized model is abstracted, which mainly includes variables related to L4 components and safety properties built on them. The desired properties are composed of 350 functional correctness and 39 safety properties, where the safety properties cover existing invariants of the microkernel. Several rewriting rules and reasoning steps are proposed for verification to improve proof efficiency. The proofs of the specification w.r.t these properties are accomplished in the theorem prover Isabelle/HOL, and the results show that all definitions, lemmas, and proofs pass the prover{\textquoteright}s check. During modeling and verification, 10 bugs in the source code are found, all of which are fixed in this paper.",
keywords = "Correctness, Formal Specification, Isabelle/HOL, L4 API, Refinement, Safety, Theorem Proving",
author = "Leping Zhang and Yongwang Zhao and Jianxin Li",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.; 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 ; Conference date: 06-04-2024 Through 11-04-2024",
year = "2024",
doi = "10.1007/978-3-031-57249-4\_11",
language = "英语",
isbn = "9783031572487",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "217--234",
editor = "Bernd Finkbeiner and Laura Kov{\'a}cs",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings",
address = "德国",
}