Model Checking Security Vulnerabilities in Software Design

Software faults in the design are frequent sources of security vulnerabilities. Mode checking shows the great promise in detecting and eradicating security vulnerabilities in the programs. The wide use of the system modeling language UML with precise syntax and semantics enables software engineers to analyze the design in details. We present a method of integrating the two techniques to detect design faults which may become security vulnerabilities in the software. Given a software design in UML and security policy, our method extracts the security properties and formally expresses them in temporal logic language. Combining with the security properties, we convert the UML models into PROMELA models, which are input of the model checker SPIN. The method either statically proves that the model satisfies the security property, or provides an execution path that exhibits a violation of the property. A case study shows the feasibility of the method.