Confidence in Confinement: An Axiom-free, Mechanized Verification of Confinement in Capability-based Systems

Operating Systems;Confinement;Capabilities;Capability-based;Capability-based Systems;Coq;Verification;Automated Verification;Coyotos;EROS;KeyKOS;Security;Safety;Constructor;Computer Science

Doerrie, Michael ScottShapiro, Jonathan S. ;

Johns Hopkins University

关键词: Operating Systems;    Confinement;    Capabilities;    Capability-based;    Capability-based Systems;    Coq;    Verification;    Automated Verification;    Coyotos;    EROS;    KeyKOS;    Security;    Safety;    Constructor;    Computer Science;   

Others  :  https://jscholarship.library.jhu.edu/bitstream/handle/1774.2/39567/DOERRIE-DISSERTATION-2015.pdf?sequence=1&isAllowed=y

瑞士|英语

来源: JOHNS HOPKINS DSpace Repository

【 摘 要 】

Confinement is a security policy that restricts the outward communication of a subsystem to authorized channels. It stands at the border of mandatory and discretionary policies and can be used to implement either. In contrast to most security policies, confinement is composable. In capability-based systems, confinement is validated by a simple decision procedure on newly minted subsystems. However, there is a long-standing debate in the literature as to whether confinement is enforceable in capability-based systems. All previous attempts to demonstrate confinement have arrived at negative results, either due to flawed system models or to proof errors that have not survived inspection.This dissertation presents SDM: a formal, general, and extensible system model for a broad class of capability-based systems. SDM includes: 1) a mechanical formalization for reasoning about capability-based systems that produces a machine-checked proof of the safety problem, 2) the construction of a system-lifetime upper-bound on potential information flow based on the safety property, and 3) an embedding of the confinement test for capability-based systems and the first mechanically verified proof that such systems support confinement. All proofs in SDM are constructed using the Coq proof assistant without using or declaring axioms that are not part of the core logic. In consequence, there is no portion of the specification which relies on an uninstantiable assertions. SDM further distinguishes itself from other efforts by enabling the formal specifications of security-enforcing applications to be embedded without being injected into the system semantics.