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?
Cheers,
M. Forods
There are several formal tools for RBAC.
Some are based on model checking (nuSMV), noteworthy Mohawk by Karthick Jayaraman et.al.: http://people.csail.mit.edu/rinard/paper/tissec13.pdf
There are also tools using SMT based model checking: Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen and Gennaro Parlato VAC - Verifier of Administrative Role-based Access Control Policies