Open Collections

The design of a verifiable operating system kernel

University of British Columbia

The design and implementation of an operating system kernel is described and justified. The kernel implements processes and primitive operations on processes. A variety of operating systems can be implemented by processes executing in the environment the kernel provides. Processes communicate via messages. Several facilities found in other kernels, such as memory management and device handling, are not included. Instead, the kernel provides operations that allow these services to be implemented by processes. The ease of reasoning about (i.e. the verifiability of) both the kernel and the systems it supports is of primary concern. The kernel's verifiability is enhanced because: it has been kept as small as reasonable; all kernel operations are indivisible; the semantics of the kernel operations are simple; and, the kernel does not depend upon any processes for its correct operation. The verifiability of systems the kernel supports is enhanced because they can be modularized such that each module can be verified individually. This is possible because the kernel eliminates many process interdependencies. An implementation of the kernel that supports a multi-process test system lends empirical support to the design. Although a complete operating system has not yet been constructed or verified, the results to date are promising.

Text

2010-03-19

For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.

http://hdl.handle.net/2429/22157

Computer Science

University of British Columbia

Graduate