Towards Proving Security in the Presence of Large Untrusted Components.
International Conference on Systems(2010)
摘要
This paper proposes a generalized framework to build large, complex systems where security guarantees can be given for the overall system's implementation. The work builds on the formally proven correct seL4 micro-kernel and on its fine-grained access control. This access control mechanism allows large untrusted components to be isolated in a way that prevents them from violating a defined security property, leaving only the trusted components to be formally verified. The first steps of the approach are illustrated by the formalisation of a multi-level secure access device and a proof in Isabelle/HOL that information cannot flow from one back-end network to another.
更多查看译文
关键词
access control mechanism,fine-grained access control,multi-level secure access device,large untrusted component,security guarantee,security property,back-end network,complex system,generalized framework,overall system
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络