Tools for model-based security engineering

ABSTRACT

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 weaving security aspects into the code generated from the models. 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.

REFERENCES

• 1: AbsInt. aicall. http://www.aicall.de/, 2004.
• 2: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Roby, Bandera: a source-level interface for model checking Java programs, Proceedings of the 22nd international conference on Software engineering, p.762-765, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337625]
• 3: J. Jürjens. Secure Systems Development with UML Springer, 2004.
• 4: Jan Jurjens, Code Security Analysis of a Biometric Authentication System Using Automated Theorem Provers, Proceedings of the 21st Annual Computer Security Applications Conference, p.138-149, December 05-09, 2005 [doi>10.1109/CSAC.2005.15]
• 5: Jan Jürjens, Sound methods and effective tools for model-based security engineering with UML, Proceedings of the 27th international conference on Software engineering, p.322-331, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062519]
• 6: J. Jürjens and S. H. Houmb. Dynamic secure aspect modeling with UML: From models to code. In ACM / IEEE 8th International Conference on Model Driven Engineering Languages and Systems (MoDELS / UML 2005),LNCS. Springer,2005.
• 7: T. Margaria, R. Nagel, and B. Steffen. jETI: Atoolforremote tool integration. In N. Halbwachs and L. D. Zuck, editors, 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), volume 3440 of LNCS pages 557--562. Springer, 2005.
• 8: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 9: Johann Schumann, Automatic Verification of Cryptographic Protocols with SETHEO, Proceedings of the 14th International Conference on Automated Deduction, p.87-100, July 13-17, 1997
• 10: UMLsec tool, 2004. http://www4.in.tum.de/csduml/interface

INDEX TERMS

Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Security

Keywords:
UML, code analysis, model-based software engineering, security, verification framework