I-MAKS - A tool for the specification and verification of secure information systems
The security of information systems can be certified with a high degree of trust using formal methods. One approach to such certifications is to formally model the system's behavior, specify the desired security requirements, and finally prove that the system model fulfills these requirements. I-MAKS is a tool for the specification and security verification of information systems that supports all these tasks and integrates methodology for each of them into an extensible architecture.
I-MAKS supports all features of the Modular Assembly Kit for Security (MAKS), a theoretical framework of specification formalisms and verification techniques for a wide range of possibilistic security properties. I-MAKS uses Isabelle/HOL as verification engine, which helps users in modeling and verifying secure systems by the flexibility and the reliability of a general purpose theorem prover. Extensions of I-MAKS, such as a library of traditional security properties like noninterference, further improve its usability for specific application domains.
In this talk, we give an overview of I-MAKS, how it is used and how it can be extended. I-MAKS is joint work by Richard Gay, Sylvia Grewe, Steffen Lortz, Heiko Mantel and Henning Sudbrock.