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

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

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.