赵翔鹏的Blog Xiangpeng's Thinkpad

RBAC的形式化验证……

RBAC也算是个研究了很久了的东西了，有很多实际应用。但是角色一多，管理就会成问题，随之就可能带来一些安全漏洞。实验室的师兄做了一个描述逻辑的框架来形式化RBAC，提出了一组公理和推理规则，然后可以用一个叫Racer的工具来判定是否存在collision。

感想：

1. 基于描述逻辑(description logic)和constraint
solving的验证方法会求出所有的解，因此效率必然会成问题。基于时态逻辑(temporal
logic)和model-checking的验证方法只求出一个解（反例），所以效率应该高一点（虽然我也遇到了状态爆炸的问题）。

2. RBAC在不同的系统上的实施可能是很不同的。比如针对工作流上的RBAC和针对文件管理的RBAC，一个可能是动态的，一个只有静态的。因此一个通用的框架未必好用。比如在工作流的访问控制上也有人提出了Transaction logic。

3. 今天师兄也提到WS-Policy比较弱，说XACML比较适合。不知道XACML是否可以理解为RBAC的XML描述。如果是的话，那么BPEL能否跟XACML结合在一起，从而实现访问控制和流程控制的分离？就这一点，还需要了解一下工业实践的具体做法。