Proof-carrying authorization in distributed systems with Beluga: a case study

Abstract

The rising popularity of distributed systems creates a need for a secure method of message passing. One approach to access control is accomplished through proof-carrying and proof authorization. The requesting party must provide a proof of authorization of access while the serving party must verify the validity of the proof. PCML5 is a programming language which enables a programmer to encode proofs and perform proof-checking procedures more easily.

The purpose of this project is to encode PCML5 with Beluga, a new functional programming language which supports dependent types and which has built in some of the more common procedures. Such an implementation will provide formal guarantees regarding the language of PCML5 itself. Moreover, this case study will aid in the understanding of the development and implementation of software specically for programming with proofs. It will provide insight into the tools needed to allow any programmer to easily specify and verify complex behavioral properties of programs.