具有类独立约束的工作流可满足性问题
密码学与安全
2015-09-15 v2 数据结构与算法
摘要
工作流规范定义了步骤集和用户集。授权策略为每个用户确定其被允许执行的步骤子集。其他安全需求，如职责分离，对哪些用户子集可以执行某些步骤子集施加约束。工作流可满足性问题（WSP）是确定是否存在满足所有此类授权和约束的用户到工作流步骤的分配的问题。求解 WSP 的算法很重要，既作为工作流规范的静态分析工具，也用于工作流管理系统的运行时参考监控。考虑到 WSP 的计算难度，特别是对于第二个应用，此类算法应尽可能高效。我们引入了类独立约束，使我们能够建模用户集被划分为组且用户组的身份对约束满足无关的场景。我们证明对于此类约束求解 WSP 是固定参数可追踪（FPT）的，并开发了一个在实际中有用的 FPT 算法。在计算实验中，我们将 FPT 算法的性能与 SAT4J（一个伪布尔 SAT 求解器）进行了比较，结果表明我们的算法在许多 WSP 实例上显著优于 SAT4J。用户独立约束是类独立约束的一个大类，包含许多实际约束，对于该类约束 WSP 已被证明是 FPT 的（Cohen 等，J. Artif. Intel. Res. 2014）。因此我们的结果显著扩展了我们对 WSP 固定参数可追踪性的认识。
引用
@article{arxiv.1504.03561,
title = {On the Workflow Satisfiability Problem with Class-Independent Constraints},
author = {Jason Crampton and Andrei Gagarin and Gregory Gutin and Mark Jones and Magnus Wahlstrom},
journal= {arXiv preprint arXiv:1504.03561},
year = {2015}
}