A Certified Distributed Security Logic For Authorizing Code

In previous work we have proposed a distributed security logic for authorizing code. To gain assurance about the correctness of the implementation of our system, we now present a series of security logics of increasing expressive power leading up to our logic. We encode each logic in Coq, develop an algorithm for deciding queries, and prove properties about the algorithm in Coq. By using Coq's automatic extraction mechanism, we are able to gain a high assurance about the resulting reference monitor implementations. Following this strategy yields reference monitors fully certified at the source code level for Datalog, Binder, Binder with a general extension mechanism, and a logic that combines Binder and the calculus of co-inductive constructions.