A language for access control

We present a language for access control. The language is organized around the notion of execution on behalf of a principal. This is characterized using an indexed lax modality. Central to the language is the idea of manifest security – accessing a resource requires presenting a proof of accessibility to the resource monitor. Proofs are generated at runtime by actions such as typing in password, looking up an access-control list or by composing other proofs etc. In the present work, we consider a simplified setting in which the access-control theory is static. In such a case proofs can be regarded as static entities. Proof generation can be hoisted away from resource access since proofs become permanent. Also, the actual proofs are irrelevant. The results of runtime checks can therefore be reflected as types and the program can be verified statically to ensure that relevant runtime checks would be passed before accessing any resource. We prove a theorem stating that the language is safe in terms of how all a principal can get to access a resource.