在现有软件中应用正式方法验证安全策略的自动化工具

Question

我刚接触过正式的方法领域，但我觉得我对它的应用有了一定的了解。然而，当软件被创建时，我似乎只遇到了应用于开发过程的正式方法。

我希望能够在现有软件上应用正式的方法来测试它是否遵循基于角色的访问控制(RBAC)和按照Bell-LaPadula (BLP)方法分离敏感信息。

您知道哪些方法和工具为RBAC和BLP样的现有软件/源代码验证提供了自动化解决方案？

Answer 1

许多年前在这里写过关于正式方法和安全性的文章-- http://www.tssci-security.com/archives/2007/11/23/formal-methods-and-security/ --它的基础是如何将古老的橙书标准应用到现代软件中。

如果我必须在2015年重写那篇博客文章，我要补充的一些更新是，基于SMT的模型检查器已经比我描述的简单的模型检查器(SPIN和JPF)更多样化、更完整、更先进。这些页面应该会带你走向这些进步-- http://kind2-mc.github.io/kind2/ -- http://smtlib.cs.uiowa.edu -- http://www.persistencelabs.com/research/

DARPA正在这里从事一个来自人群的正式验证(CSFV)项目-- http://www.darpa.mil/program/crowd-sourced-formal-verification。

虽然我完全支持自动化，但更多地了解问题领域，以便就手动测试提出次要建议会很有趣。这是针对电子商务、网络和基于移动的授权问题吗？涉及哪个领域(S)？