By Reason and Authority: A System for Authorization of Proof-Carrying Code

We present a system, BLF, that combines an authorization logic based on the Binder language with a logical framework, LF, able to express semantic properties of programs. BLF is a general system for specifying and enforcing policies that rely on both reason and trust. In particular, BLF supports extensible software systems that employ both digitally signed code and language-based security, especially proof-carrying code. We describe BLF, establish some of its fundamental properties, and explain its use.

• Type: Conference
• Year: 2004
• Where: CSFW
• Authors: Nathan Whitehead, Martín Abadi, George C. Necula
• Keywords: Authorization Logic, CSFW 2004, Extensible Software Systems, Security Privacy, Semantic Properties