Towards a formally verifiable multiprocessor microkernel
Authors
NICTA
UNSW
Published:
Poster presented at the 2009<undefined>Abstract
Embedded systems in safety-critical areas require a high degree of assurance with regards to correctness and reliability. While extensive testing and using redundant subsystems can increase the degree of assurance, they can never guarantee that a system is correct and bug-free.
Microkernels are increasingly being used in today's embedded systems. They improve security and reliability by providing isolation between system components. NICTA's seL4 project adapted the L4 microkernel's API to enable fine-grained dissemination of authority via capabilities. This allows controlled communication between otherwise isolated components. In order to raise the degree of assurance, NICTA's L4.verified project aims to formally verify the isolation properties of seL4's API and the functional correctness of the complete C implementation. This will guarantee the absence of bugs and yield the highest possible degree of assurance. Guaranteed isolation is desired mainly because faults in one component of the system are guaranteed not to affect another, potentially vital component.
In order not to have to deal with concurrency in seL4's proofs, which is inherently hard, seL4 is a uniprocessor microkernel and does not allow preemption within the kernel except from a few well-defined preemption points in long-running system calls. However, with embedded applications increasing in complexity and demanding more and more computing power, embedded multiprocessor/multicore systems gain additional popularity. Thus, my work aims to provide the same guarantees for a multiprocessor version of seL4 as we already have for the uniprocessor version.
BibTeX Entry
@misc{vonTessin_09,
address = {San Diego, CA, USA},
author = {von Tessin, Michael},
howpublished = {Poster presented at the 2009},
keywords = {formal verification, multiprocessor, microkernel, sel4, isabelle/hol},
month = jun,
paperurl = {https://trustworthy.systems/publications/nicta_full_text/2092.pdf},
title = {Towards a Formally Verifiable Multiprocessor Microkernel},
year = {2009}
}
BibTeX