Run-time monitors are a common and pervasive mechanism for ensuring that software and systems adhere to security policies. Anti-virus and anti-spyware programs, personal firewalls, intrusion-detection tools, Java's stack inspection, and even mechanisms that trap operatingsystem exceptions in order to show a ?blue screen of death? can all be thought of as run-time monitors. Although they differ greatly in their complexity and scope of policies that they can enforce, these mechanisms all observe the behavior of a running system and detect and react to potentially dangerous events. Despite the pervasiveness and real-world importance of runtime monitors, their use has far outpaced theoretical work that makes it possible to rigorously reason about monitors and the policies that they enforce, particularly in distributed settings. This project develops models, tools, and mechanisms for reasoning about and implementing distributed, concurrently executing run-time monitors. The research adopts a holistic, four-prong approach that spans the breadth of the space between theoretical models and practical systems for enforcing run-time policies. Specifically, this project (1) creates a framework for reasoning about enforcement that permits the possibilities of concurrent, distributed computations; (2) develops a type-safe policy-specification language that ensures that specified policies compile into well-behaved monitoring mechanisms; (3) designs trustworthy algorithms for automatically translating a desired overall policy into node-specific policies that can be distributed and enforced throughout a network; and (4) designs, implements, and tests a prototype system for specifying and enforcing run-time policies with support for concurrently executing computations. Taken together, these research tasks enable formal modeling and automatic enforcement of run-time security policies in concurrent and distributed settings.
