Providing restrictive and secure access to resources is a challenging and socially important problem. Security analysis helps organizations gain confidence on the control they have on resources while providing access, and helps them devise and maintain policies. There is a dire need for analysis tools to help administrators ensure security as they make administrative changes to reflect changes in policy. Security analysis of access control is non-trivial for an administrator due to the complexity of reasoning with the beguiling number of possible future scenarios. Techniques for the analysis of security in access control is in its infancy. The goal of this project is to go beyond decidability/undecidability issues, and go forth to build scalable and usable security analysis tools and techniques when access control is deployed via the most commonly used role-based access control (RBAC) models or its spatiotemporal extensions.
The main thesis of this project is that finding breaches of security in an access control model is very similar to finding errors in a program. Some of the innovative expected results include: accurate mapping of the security problem for policies in access control as reachability problems in transition systems, including succinct discrete systems and automata with spatio-temporal constraints; scalable techniques to search for security breaches by exploiting the model-checking techniques developed by the program verification community; usable and useful tools for administrators to express policies and automatically find breaches of their security policies. The project helps in building technical bridges between the communities of access control security and formal methods in verification, which is expected to trigger a flurry of research, possibly unifying problems in the two fields, and initiating each other with new ideas. Scalable and usable security analysis will also serve needs in many settings including emergency, disaster management and homeland security applications. The tools will be included as modules in a tele-medicine system and an emergency management system. The integration of the ideas, techniques, and tools resulting from this project into the education curriculum will positively impact the quality of a newly trained workforce that is prepared to meet security challenges, making them aware of security issues in access control, and educating them on practical ways to check for breaches in security.
Resources, both digital and otherwise, are protected using access control rules that determine the permissions subjects have on these resources. Furthermore, administration of access control itself is delegated to certain subjects, who can confer or revoke permissions to other subjects. However, the policies put into place may not satisfy the broader security goals, and hence may allow for breaches, causing misuse of resources and loss of data and privacy. The project herein has built foundational techniques that allows people to determine the effect of role-based access control policy with administrative rules. The techniques we develop allow us to determine whether a set of untrusted users can misuse their priveleges, granting permissions to others, perhaps colluding in groups, to create a breach in security. The primary techniques we develop stem from the observation that security analysis of access control polciies can be determined using techniques for program analysis and verification. Just like a program can execute and cause its state to evolve, the access permissions for users can also evolve, and hence can be analyzed using similar techniques. We developed, over the course of this period, techniques based on abstraction and model-checking, to both find security breaches and to prove the lack of security breaches in an access control policy. Our techniques have for the first time led to tools that can effectively handle this problem for large access control policies, including temporal and spatial policies that allow access permissions to depend on the time and place the subjects are at. The broader impact of our work is in building techniques that protect resources protected by complex access control policies, allowing the designer to check whether it meets the broader security goals. Access control is used everywhere--- in businesses, in guarding national resources, in protecting privacy in healthcare domains, etc., and our work builds foundational techniques that can ensure their correctness. The work here has been disseminated to researchers in academia and industry through publications in premier conferences, and our tools have been made available both to researchers and the general public for their use. Furthermore, the grant has also helped train two graduate students and a postdoctoral researcher, helping them to be trained in solving important problems involving security of access control. The PI has also taught several formal methods courses at the University of Illinois where applications to security have been incorporated.
