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 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.