类无关约束下的工作流可满足性问题研究
On the Workflow Satisfiability Problem with Class-Independent Constraints
摘要：
工作流规范定义步骤集和用户集。授权策略为每个用户确定允许该用户执行的步骤的子集。其他安全要求，例如职责分离，对哪些用户子集可以执行某些步骤子集施加约束。\emph{workflow satisfiability problem}（WSP）是确定是否存在满足所有此类授权和约束的用户到工作流步骤的分配的问题。一个算法来解决WSP是重要的，无论是作为一个静态分析工具的工作流规范，并为工作流管理系统的运行时参考监视器的建设。考虑到WSP的计算难度，重要的是，特别是对于第二种应用，这样的算法尽可能有效。我们引入类独立的约束，使我们能够建模的情况下，一组用户划分成组，和用户组的身份是无关的约束的满意度。我们证明了解决WSP是固定参数易处理（FPT）的这类约束，并开发了FPT算法，是有用的，在实践中。在计算实验中，我们将FPT算法与SAT 4J（一种伪布尔SAT求解器）的性能进行了比较，结果表明，在WSP问题的许多实例中，FPT算法的性能明显优于SAT 4J。用户无关约束是一个包含许多实际约束的大类约束，它是类无关约束的一个特例，WSP被证明是FPT（Cohen { \em et al.}，J. Artif.英特尔Res. 2014）。因此，我们的研究结果大大扩展了我们的知识固定参数易处理的WSP。
英文摘要：
A workflow specification defines sets of steps and users. An authorization policy determines for each user a subset of steps the user is allowed to perform. Other security requirements, such as separation-of-duty, impose constraints on which subsets of users may perform certain subsets of steps. The \emph{workflow satisfiability problem} (WSP) is the problem of determining whether there exists an assignment of users to workflow steps that satisfies all such authorizations and constraints. An algorithm for solving WSP is important, both as a static analysis tool for workflow specifications, and for the construction of run-time reference monitors for workflow management systems. Given the computational difficulty of WSP, it is important, particularly for the second application, that such algorithms are as efficient as possible. We introduce class-independent constraints, enabling us to model scenarios where the set of users is partitioned into groups, and the identities of the user groups are irrelevant to the satisfaction of the constraint. We prove that solving WSP is fixed-parameter tractable (FPT) for this class of constraints and develop an FPT algorithm that is useful in practice. We compare the performance of the FPT algorithm with that of SAT4J (a pseudo-Boolean SAT solver) in computational experiments, which show that our algorithm significantly outperforms SAT4J for many instances of WSP. User-independent constraints, a large class of constraints including many practical ones, are a special case of class-independent constraints for which WSP was proved to be FPT (Cohen {\em et al.}, J. Artif. Intel. Res. 2014). Thus our results considerably extend our knowledge of the fixed-parameter tractability of WSP.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
