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

提供有限和安全的资源访问是一个具有挑战性和重大社会意义的问题。安全分析可帮助组织在提供访问权限的同时，对其控制资源的能力建立信心，并帮助他们制定和维护策略。迫切需要分析工具来帮助管理员在进行管理更改以反映策略更改时确保安全性。对于管理员来说，访问控制的安全分析不是微不足道的，因为与诱人的数量的未来可能场景进行推理是很复杂的。访问控制中的安全分析技术还处于初级阶段。该项目的目标是通过最常用的基于角色的访问控制(RBAC)模型或其时空扩展来部署访问控制，从而超越可决策性/不可决策性问题，构建可扩展和可用的安全分析工具和技术。该项目的主要主题是在访问控制模型中发现安全漏洞非常类似于发现程序中的错误。一些创新的预期成果包括：将访问控制中策略的安全问题准确地映射为过渡系统中的可达性问题，包括具有时空约束的简洁离散系统和自动机；通过利用程序验证界开发的模型检查技术来搜索安全漏洞的可扩展技术；管理员表达策略和自动发现安全策略漏洞的有用工具。该项目有助于在出入控制安全和核查正式方法之间建立技术桥梁，预计将引发一系列研究，可能会统一这两个领域的问题，并以新的想法相互启动。可扩展和可用的安全分析还将满足许多环境中的需求，包括紧急情况、灾难管理和国土安全应用程序。这些工具将作为模块包括在远程医疗系统和应急管理系统中。将该项目产生的想法、技术和工具整合到教育课程中，将对准备迎接安全挑战的新培训劳动力的素质产生积极影响，使他们意识到访问控制中的安全问题，并教育他们有关检查安全漏洞的实际方法。

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.