PartialMAX-SAT求解法在RBAC授权查询中的应用

摘要信息: 本文提出了一种基于局部最大可满足性问题（Partial MAX-SAT）求解器的RBAC（基于角色的访问控制）授权查询方法。该方法旨在保证系统的安全性，同时实现最小权限分配，以提高授权的有效性。通过将静态授权逻辑和动态互斥角色约束转化为严格子句，并应用子句更新算法处理满足不同匹配请求的权限，转化为松弛子句。通过子句编码和递归算法寻找真值指派，以满足所有严格子句和尽可能多的松弛子句。实验结果显示，这种方法在确保系统安全性的前提下，实现了最小权限的分配，并且在处理最大匹配和精确匹配的请求时，其查询效率优于传统的MAX-SAT求解方法。该研究受到多项科研项目的资助，并由三位作者共同完成，他们在访问控制、模型检测、软件工程等领域有深入研究。 关键词: 基于角色的访问控制, 部分最大可满足性问题, 用户授权查询问题, 严格子句, 松弛子句 文章详细内容: 随着信息技术的发展，基于角色的访问控制（Role-Based Access Control，RBAC）已经成为现代系统中管理用户权限和访问控制的主要机制。然而，如何高效准确地进行授权查询，尤其是在考虑安全性、互斥角色和最小权限原则时，成为一个挑战。局部最大可满足性问题（Partial MAX-SAT）是一种优化的布尔 satisfiability problem (SAT) 解决方法，它寻找满足大部分子句的布尔公式解，适用于解决复杂的优化问题。 孙伟、李艳灵和鲁骏三位作者提出了将Partial MAX-SAT技术应用于RBAC授权查询的新方法。他们首先定义了RBAC模型中的授权逻辑，包括角色分配、权限分配以及角色间的互斥关系。接着，他们设计了一套转换规则，将这些逻辑和约束转化为 Partial MAX-SAT 的形式，即严格子句和松弛子句。严格子句代表必须满足的授权条件，而松弛子句则表示可以放宽的部分。 在查询过程中，该方法使用子句更新算法来处理不同用户的权限请求。当一个请求与当前角色集合不匹配时，算法会将不匹配的部分转化为松弛子句，然后通过子句编码和递归算法寻找一个满足所有严格子句并尽可能多的松弛子句的解。这种方法的关键在于找到一个既满足安全策略又尽量减少角色数量的授权方案。 实验结果表明，基于Partial MAX-SAT的授权查询方法在保持系统安全性的前提下，有效地解决了最小权限分配问题。与传统的基于MAX-SAT的方法相比，该方法在处理最大匹配和精确匹配的查询时，表现出更高的效率，这意味着它能更快地为用户提供合适的访问权限。 该研究不仅为RBAC系统提供了新的授权查询策略，还为解决类似优化问题提供了一种新的视角。通过结合 Partial MAX-SAT 求解器，这种方法有望在实际应用中提升系统的安全性和效率，为未来RBAC系统的优化设计提供了理论基础和技术支持。