TC: Small: Collaborative Research: Formal Security Analysis of Access Control Models and Extensions

点击翻译按钮获取中文摘要

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 tohelp 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 andautomatically 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 eachother 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 beincluded 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.