文章基本信息

标题：Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
本地全文：下载
作者：Narjes Jomaa ; Paolo Torrini ; David Nowak 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2019
卷号：76
页码：1-21
DOI：10.14279/tuj.eceasst.76.1080
出版社：European Association of Software Science and Technology (EASST)
摘要：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.
关键词：protokernel; memory isolation; formal proof; Coq