I am new to the Formal Methods arena, but I feel I have an educated grasp on its applications. However, I only seem to encounter formal methods as applied to the development process, as the software is created.

I'd like to be able to apply formal methods on existing software to test whether it adheres to role based access controls (RBAC) and separation of sensitive information following the Bell-LaPadula (BLP) method.

What methods and tools do you know of that offer an automated solution for RBAC and BLP-like verification of existing software/source code?

  • I have yet to see a practical use case where BLP has any direct application... but in any case if you want to know whether (1) a tool exists or (2) creating that tool is possible, we need a better definition of the problem you want to solve. The architecture of the software you want to verify, and the programming language's primitives, matter. – Steve Dodier-Lazaro Jun 14 '15 at 22:15
  • @SteveDL I'm looking to test software written in C for potential security flaws before introducing the software into a test bed. Both to provide security for the test bed and identifty flaws in the software early on. – Methmal Forods Jun 14 '15 at 23:01
  • Ok, and what formal properties do you want to verify? There are gazillions of analysis tools for C code, and theoretical foundations that explain what you can and cannot test. Are you familiar with language-based security? – Steve Dodier-Lazaro Jun 14 '15 at 23:25
  • I'm not familiar with language based security. I'm looking to verify data access and roles. – Methmal Forods Jun 14 '15 at 23:41
  • 1
    What you're missing is the following: you must find the problem before you find a tool for it. You need to understand how to formalise the things you want to verify in your specific software in terms of information flows, and then you can find a tool that implements the type of information flow control you need, or write one yourself. Usually you need to understand the problem to understand which tool to use. – Steve Dodier-Lazaro Jun 15 '15 at 0:36

Wrote about formal methods and security many years ago here -- http://www.tssci-security.com/archives/2007/11/23/formal-methods-and-security/ -- the basics of which is how to apply old-school Orange Book standards to modern software.

If I had to rewrite that blog post in 2015, some of the updates I'd add are that SMT-based model checkers have become a lot more diverse, integrated, and advanced than the simple ones I outlined (SPIN and JPF). These pages should lead you towards some of these advancements -- http://kind2-mc.github.io/kind2/ -- http://smtlib.cs.uiowa.edu -- http://www.persistencelabs.com/research/

DARPA is working on a Crowd-Sourced Formal Verification (CSFV) project here -- http://www.darpa.mil/program/crowd-sourced-formal-verification

While I'm all for automation, it would be interesting to hear more about the problem domain to make secondary recommendations around manual testing. Is this for e-commerce web and mobile based authorization problems? Which domain(s) are involved?

| improve this answer | |
  • Come on, the start of your answer is a third-party link. :-) Could you please summarise the article, or if it is a well-referenced one, add its title and author name for future readers to find? – Steve Dodier-Lazaro Jun 14 '15 at 22:13
  • @atdre First link is a great read. Other links will prove useful too. Not looking to verify e-commerce. Mobile applications, web-based interfaces, and embedded systems. – Methmal Forods Jun 14 '15 at 23:29
  • @ Steve DL: added clarity, thank you for the feedback – atdre Jun 15 '15 at 0:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.