Collaborative End-to-end Enforcement of Security Policies in Distributed Systems

Whether due to economic incentives, legislation, or political realities, large organizations, often with competing interests, must share sensitive information across administrative boundaries in order to carry out their daily operations. For example, in the aerospace industry, military contracts are often shared between rival manufacturers requiring organizations to share critical elements of designs across administrative domains, while still protecting their trade secrets [46]. Similar situations arise in the management of medical records [33], in e-commerce, in the outsourcing of software development, and in military coalitions [18,11]. While protecting their own information assets from improper use is the primary goal, principals are also expected to respect the security policies of their partners, e.g., a partnership may be bound by legal contracts that place restrictions on how shared data is to be used. Failure to properly carry out their contractual obligations (e.g., due to faults in the software that manipulates shared data) can have practical consequences, such as costly legal action. As such, organizations require assurance that their software correctly enforces both their own security policies as well as those of their partners. Towards this end, we advocate a program of research with the aim of formally verifying that security-critical software, potentially assembled from components authored by multiple principals, is in compliance with a security policy.