Secure Programming as a Parity Game

Abstract

Traditionally, reference monitors have been used both to specify a policy of secure behaviors of an application, and to ensure that an application satisfies its specification. However, for recently proposed privilege-aware systems, applications satisfy a policy defined over a set of security-sensitive events by invoking explicitly a separate set of primitive operations provided by the system. To date, a programmer who writes an application for such a system both defines and implements a policy using the low-level primitives. While the programmer may have a high-level policy in mind, it is difficult for him to ensure that the application calls the primitives in such a way that it satisfies the policy. It is also difficult for him to ensure that he does not call the primitives in such a way that it cripples the program's original functionality.

In this paper, we formalize the problem of writing programs for privilege-aware systems, and make significant steps toward solving the problem, using an automata-theoretic approach. First, we distinguish between the high-level policies supported by a privilege-aware system and the low-level primitives provided to enforce policies. Second, we define the policy-weaving problem, which is to take as input (1) a declarative description of a privilege-aware system, (2) a program that makes no use of the primitives provided by the system, and (3) a high-level policy that describes the program's security and functionality requirements, and produce as output a program that uses the primitives of the privilege-aware system to satisfy the high-level policy. We reduce important subclasses of the weaving problem to finding strategies to parity games. Finally, we formalize the Capsicum capability system, demonstrating that the problem of writing secure programs for a practical privilege-aware system can be described as a policy-weaving problem.