我是形式方法领域的新手，但我觉得我对它的应用有一定的了解。但是，我似乎只遇到了应用于开发过程的正式方法，因为软件是创建的。
我希望能够在现有软件上应用形式化方法来测试它是否遵循基于角色的访问控制 (RBAC) 和遵循Bell-LaPadula (BLP) 方法的敏感信息分离。
您知道哪些方法和工具可以为现有软件/源代码的 RBAC 和 BLP 类验证提供自动化解决方案？
干杯，
M·福兹
问问题
103 次
1 回答
0
RBAC 有几个正式的工具。
有些基于模型检查（nuSMV），值得注意的是 Karthick Jayaraman 等人的 Mohawk：http: //people.csail.mit.edu/rinard/paper/tissec13.pdf
还有一些工具使用基于 SMT 的模型检查：Anna Lisa Ferrara、P. Madhusudan、Truc L. Nguyen 和 Gennaro Parlato VAC - Verifier of Administrative Role-based Access Control Policies
于 2015-06-21T19:46:27.557 回答