Combining Reason and Authority for Authorization of Proof-Carrying Code

In this doctoral dissertation I show that using both reason and authority as strategies for code authorization is desirable, possible, and practical. I 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.