Authors
Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone
Publication date
2008
Conference
Verified Software: Theories, Tools, Experiments: Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings 2
Pages
99-114
Publisher
Springer Berlin Heidelberg
Description
This paper presents a machine-checked high-level security analysis of seL4—an evolution of the L4 kernel series targeted to secure, embedded devices. We provide an abstract specification of the seL4 access control system together with a formal proof that shows how confined subsystems can be enforced. All proofs and specifications in this paper are developed in the interactive theorem prover Isabelle/HOL.
Total citations
Scholar articles
D Elkaduwe, G Klein, K Elphinstone - … Conference, VSTTE 2008, Toronto, Canada, October 6 …, 2008