Towards Secure Distributed Choreographies

Choreographic programming is an emerging paradigm for message-passing concurrency. A choreographic program (or "choreography") describes the computation of an entire system; this ensures deadlock-freedom without requiring the extraneous checks that other solutions like session types require. Choreographies seem perfect for designing distributed systems, since they allow deadlock freedom with arbitrary communication patterns for codesigned nodes. This talk looks at two challenges involved in using choreographies this way: information security and the closed-world assumption. In both cases, I will discuss what makes these problems challenging, and report on current work meant to address them.