Tools for model-based security engineering

We present tool-support for checking UML models and C code against security requirements. A framework supports implementing verification routines, based on XMI output of the diagrams from UML CASE tools, and on control flow generated from the C code. The tool also supports weav-ing security aspects into the code generated from the mod-els. Advanced users can use this open-source framework to implement verification routines for the constraints of self-defined security requirements. We focus on a verification routine that automatically verifies crypto-based software for security requirements by using automated theorem provers