Lightweight Analysis of Access-Control Policies

Abstract

Access-control policies play a central role in controlling the dissemination of sensitive data in domains ranging from library services to healthcare. They represent an important, but not isolated, example of policies that govern the behavior of programs. Developers increasingly express such policies in domain-specific, declarative policy languages that sit in separate modules from the rest of a program. Given that policies are both hard to get right and isolated from the rest of the program, they seem a natural candidate for formal verification. Traditional forms of verification, however, aren't necessarily appropriate or useful. This talk discusses these issues, as well as concrete results and tools we have produced for analyzing policies.

The talk is self-contained, including a brief tutorial on access-control.

Joint work with Shriram Krishnamurthi (Brown) and Dan Dougherty (WPI).