| ||||
| ||||
![]() Title:Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base Conference:AVOCS 2018 Tags:Coq, formal proof, memory isolation and protokernel Abstract: The development of provably secure OS kernels represents a fundamental step in the creation of safe and secure systems. To this aim, we propose the notion of protokernel and an implementation --- the Pip protokernel --- as a separation kernel whose trusted computing base is reduced to its bare bones, essentially providing separation of tasks in memory, on top of which non-influence can be proved. This proof-oriented design allows us to formally prove separation properties on a concrete executable model very close to its automatically extracted C implementation. Our design is shown to be realistic as it can execute isolated instances of a real-time embedded system that has moreover been modified to isolate its own processes through the Pip services. Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base ![]() Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base | ||||
Copyright © 2002 – 2025 EasyChair |