Abstract
Dynamic separation of duties, delegation and other dynamic security constraints require the state of the security system to be managed explicitly at run-time in software. The majority of this software is still programmed directly by humans, and is thus susceptible to errors that will impact the overall functionality and security of the system. In this paper we demonstrate a technique for statically checking properties of the software that manages dynamic security policies. We base our work on Kilim, a shared-nothing, message-passing Java framework that provides a faster safer alternative to the dominant shared-memory and locking paradigm. We demonstrate that Kilim's static, compile-time verification of type linearity can also effect validation of aspects of dynamic security systems. We describe our initial steps toward the use of Kilim to support active, distributed security infrastructure.