Typed Static Analysis for Concurrent, Policy-Based, Resource Access Control
Nicholas Nguyen, Julian Rathke · 2006
Abstract. We present a type and effect system for statically determin-ing whether concurrent programs in a simple functional language adhere to a strict access control policy. Policy states are represented by automata states and are tracked, statically, by the type and effect system. We en-sure that, per thread, all function calls are, independently, in accordance with policy with respect to the current state. To verify that several con-current threads jointly satisfy a policy we are required to explore the state space of an interleaving of the several threads ’ effects. However, we observe that by furnishing our language with monitor synchronisation primitives we can reduce our state space search by abstracting away be-haviours inside atomic sections. The type and effect system is proved to satisfy Subject Reduction and a Safety theorem which guarantees that well-typed programs never violate policy. 1