Kit: a study in operating system verification. The author reviews Kit, a small multitasking operating system kernel written in the machine language of a uniprocessor von Neumann computer. The kernel is proved to implement on this shared computer a fixed number of conceptually distributed communicating processes. In addition to implementing processes, the kernel provides the following verified services: process scheduling, error handling, message passing, and an interface to asynchronous devices. As a by-product of the correctness proof, security-related results such as the protection of the kernel from tasks and the inability of tasks to enter supervisor mode are proved. The problem is stated in the Boyer-Moore logic, and the proof is mechanically checked with the Boyer-Moore theorem prover.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Grip, N.; Pfander, G. E.: Efficient analysis of OFDM channels (2017)
- Feng, Xinyu; Shao, Zhong; Guo, Yu; Dong, Yuan: Certifying low-level programs with hardware interrupts and preemptive threads (2009)
- Klein, Gerwin: Operating system verification---an overview (2009)
- Tews, Hendrik; Völp, Marcus; Weber, Tjark: Formal memory models for the verification of low-level operating-system code (2009)
- Cock, David; Klein, Gerwin; Sewell, Thomas: Secure microkernels, state monads and scalable refinement (2008)
- Weber-Wulff, Debora: Proof movie -- a proof with the Boyer-Moore prover (1993)
- Bevier, W. R.: Kit: A Study in Operating System Verification (1989) ioport