Logic is emerging as an important tool in the design and implementation of secure systems. It can be used not only to reason about correctness of system components and protocols, but also to directly enforce integrity and confidentiality in both code and data. This talk presents two applications of logic, one in each of these two areas.

First, the talk describes the architecture and implementation of a file system that uses proof-carrying authorization (PCA) to protect the integrity and confidentiality of stored data. PCA allows rigorous and administratively lightweight enforcement of complex access policies using logic. However, it is challenging to make PCA efficient enough for practical use in a low-level system. It is argued and demonstrated here that PCA can be combined with conditional capabilities to obtain sufficient efficiency, without losing any of its benefits. The talk also covers a tool for proof search in an expressive authorization logic, which helps make the implementation practical for end users.

Second, the talk presents a logic-based framework for modeling and proving properties of secure systems at a high level of abstraction. The framework is intended to help system builders rule out errors at the design level. It includes a formal language to model system components, and a Hoare-style logic to prove their safety properties in the face of arbitrary adversaries. Drawing upon ideas from work in security protocol analysis, the framework combines symbolic reasoning about cryptographic primitives, network communication, shared memory, access control, and dynamically loaded code in a novel and technically challenging manner.