验证面向服务架构中授权策略与工作流的相互作用（完整版）
密码学与安全
2009-06-26 v1 计算机科学中的逻辑
摘要
在基于面向服务范式的分布式应用（如Web服务）中，一种广泛采用的设计方法是将授权策略的实施与应用程序的工作流明确分离，从而抽象掉策略层与工作流层之间的相互作用。尽管这种方法因其简单性且允许对策略的关键属性进行推理而具有吸引力，但它并未提供适当的抽象级别来指定和推理工作流如何干扰策略，反之亦然。例如，作为工作流操作副作用的证书创建可能触发策略规则并授予对特定资源的访问权限；若不执行该操作，策略规则应保持非激活状态。类似地，策略查询可用作工作流转换的守卫。在本文中，我们提出了一个两级形式化验证框架来克服这些问题，并对面向服务架构中授权策略与工作流的相互作用进行形式化推理。这使我们能够定义并研究面向服务应用的一些验证问题，并给出其可判定性的充分条件。
引用
@article{arxiv.0906.4570,
title = {Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures (Full version)},
author = {Michele Barletta and Silvio Ranise and Luca Viganò},
journal= {arXiv preprint arXiv:0906.4570},
year = {2009}
}
备注
16 pages, 4 figures, full version of paper at Symposium on Secure Computing (SecureCom09)