The Process of Model Checking Software Security in UML Models with SPIN

摘要

This paper describes a method of detecting design security vulnerability with the model checker SPIN. Known security properties are expressed in LTL formulae. Software design is converted into PROMELA. A case study shows feasibility and principles of the method. This paper focuses only on temporal security properties. Future work includes to create more LTL security patterns and to experiment them with more models of software design. Another issue is the automatic generation of PROMELA from software design concerning security requirements.