On Secure Distributed Implementations of Dynamic Access Control

TL;DR

This paper analyzes the security of distributed access control implementations, revealing subtle flaws in standard protocols and proposing refined specifications and formal methods to ensure security in distributed systems.

Contribution

It identifies security issues in capability-based protocols and introduces a refined specification with formal proofs for secure distributed access control.

Findings

Standard protocols can have security flaws under simple specifications.

Refined specifications enable secure distributed access control implementations.

Formal models and proofs validate the proposed security refinements.

Abstract

Distributed implementations of access control abound in distributed storage protocols. While such implementations are often accompanied by informal justifications of their correctness, our formal analysis reveals that their correctness can be tricky. In particular, we discover several subtleties in a standard protocol based on capabilities, that can break security under a simple specification of access control. At the same time, we show a sensible refinement of the specification for which a secure implementation of access control is possible. Our models and proofs are formalized in the applied pi calculus, following some new techniques that may be of independent interest. Finally, we indicate how our principles can be applied to securely distribute other state machines.