Modeling and Verifying Information Systems with I-MAKS


Information systems that process confidential data require special care
to ensure that they don't leak confidential information. I-MAKS is a 
tool that supports the certification of information-flow security based
on the Modular Assembly Kit for Security in the automated theorem prover
Isabelle/HOL. Security certification with I-MAKS happens at the level of
event-based specifications such that it is applicable to many settings,
e.g. to software design, communication protocols, and distributed systems.

In this talk, we will give an overview of I-MAKS and its features.
Moreover, we will have a closer look into the application of I-MAKS to 
certify a confidentiality requirement on a communication platform.