01/01/2008 09:00 AM
Computer Science
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 state-of-the-art implementation based on capabilities, that can undermine correctness under a simple specification of access control. We consider both safety and security for correctness; loosely, safety requires that an implementation does not introduce unspecified behaviors, and security requires that an implementation preserves the specified behavioral equivalences. We show that a secure implementation of a static access policy already requires some care in order to prevent unspecified leaks of information about the access policy. A dynamic access policy causes further problems. For instance, if accesses can be dynamically granted then the implementation does not remain secure---it leaks information about the access policy. If accesses can be dynamically revoked then the implementation does not even remain safe. We show that a safe implementation is possible if a clock is introduced in the implementation. A secure implementation is possible if the specification is accordingly generalized. Our analysis shows how a distributed implementation can be systematically designed from a specification, guided by precise formal goals. While our results are based on formal criteria, we show how violations of each of those criteria can lead to real attacks. We distill the key ideas behind those attacks and propose corrections in terms of useful design principles. We show that other stateful computations can be distributed just as well using those principles.
