2019/05/14 by Narjes Jomaa, Paolo Torrini, Jomaa, Narjes +7 · 2 citations
Computer Science · #Security and Verification in Computing #Advanced Malware Detection Techniques #Cloud Data Security Solutions
paper · pdf · doi:10.14279/tuj.eceasst.76.1080
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 realtime embedded system that has moreover been modified to isolate its own processes through the Pip services.