| Using both reason and authority as strategies for code authorization is desirable, possible, and practical. We present BCIC, a system that combines an authorization logic based on the Binder language with CIC, a logical framework able to express semantic properties of programs. BCIC is a general system for specifying and enforcing policies that rely on both reason and authority. In particular, BCIC supports extensible software systems that employ both digitally signed code and language-based security, including proof-carrying code.; We describe BCIC, establish some of its fundamental properties, and explain its use. We develop a series of examples at varying levels of detail to demonstrate our system in action and explain what types of benefits it provides. We include an example for auditing system calls, an example that includes a type system for tracking trust in the lambda-calculus, and an example showing a limited form of control-flow integrity for x86 machine code.; To allow policy writers to extend the language of BCIC we also explain how proof-by-computation works in BCIC, and demonstrate how decision procedures for predicates can be embedded in policies. Such decision procedures work with utilitarian data structures and can also be used to perform automatic static analysis of programs within the policy.; To obtain high assurance that our reference monitor is correct, we have created a certified implementation of BCIC using program extraction from our Coq proofs of decidability of BCIC. Along the way we also extract certified implementations for Datalog and Binder, useful in their own right. |
