A Security Analysis of a Biometric Authentication System using UMLsec and the Java Modeling Language

Lloyd, J. G. (2007). A Security Analysis of a Biometric Authentication System using UMLsec and the Java Modeling Language. Student dissertation for The Open University module M801 MSc in Software Development Research Dissertation.

Please note that this student dissertation is made available in the format that it was submitted for examination, thus the author has not been able to correct errors and/or departures from academic standards in areas such as referencing.

DOI: https://doi.org/10.21954/ou.ro.0001605a

Abstract

The UMLsec approach is intended to be a simpler way for software designers to specify system security requirements and to verify their correctness. UMLsec is a set of Unified Modeling Language (UML) stereotypes with associated tags and constraints that can be added to UML diagrams to specify security requirements such as secrecy, integrity and authenticity. The approach includes the description of protocol security requirements using a cryptographic protocol notation. The UML diagrams can then be analysed by a set of tools to automatically verify these requirements for correctness. However, even if the specification is provably correct, security flaws might be introduced during the design, implementation and subsequent maintenance of the system through errors and omissions. The UMLsec approach includes a set of techniques and tools that seek to automatically verify that implemented code does not contain security flaws, but these techniques and tools do not yet relate back to the specified security requirements in UMLsec so ways are needed to verify that the implemented system is correct in relation to this specification. This research dissertation designed a prototypical biometric authentication system using UMLsec to evaluate how easy UMLsec is to use in this context and to investigate how easy it is to implement a system in Java from this design. It then examined the use of the Java Modeling Language (JML) to relate the code back to its specification to verify that the implementation was secure. The UMLsec approach was effective in specifying security requirements succinctly and sufficiently precisely to avoid significant change during coding, although the capabilities of the implementation language need to be taken into account to avoid redundancy in the specification. The threat model was particularly useful in clarifying the extent of an adversary’s access to the system. However UMLsec is not a design or implementation approach and so does not assist with issues such as selecting the type or strength of security algorithms. The approach should contribute to reducing the high training and usage costs of formal methods but it will need training, simpler documentation and CASE tool support to appeal to industry. The UMLsec specification would also need to be maintained throughout the life of a system so that all changes made could be verified, which would increase maintenance effort and cost. JML was applied to parts of the prototype code and helped to verify it by focusing attention on the consistency of the code with its UMLsec specification, which revealed a number of security flaws and weaknesses. However a subsequent manual check revealed more flaws, design weaknesses and inconsistencies in the UMLsec specification, some of which would not have been revealed by JML even if it had been fully applied. The jmlc and ESC/Java 2 tools were used to compile and statically check JML against the Java code. However there is no tool support for verifying the JML against a UML specification so the Java code could not be verified against its UMLsec specification via JML. The JML specifications might therefore not completely reflect the UMLsec specification. The value of JML was limited because it was applied after code development to a software design that was not entirely suitable; it would have been more useful to have used it to specify methods during design and made less use of the Object Constraint Language (OCL) to specify class operations. JML was also sometimes cumbersome to use in verifying security requirements. Any organisation adopting JML would therefore need to develop a design style guide and security patterns, and provide adequate training for designers and developers. Using JML does not eliminate security flaws since they could be contained in products, design features not implemented in code, infrastructure, and associated business and operational processes. Future research should develop a tool to generate draft JML specifications from UMLsec sequence diagrams to improve JML coding efficiency and reduce the risk of omissions. Other research might map UMLsec to features of implementation language frameworks, develop UMLsec and JML security patterns, evaluate other JML tools in a security requirements context and integrate these techniques within a coherent security systems development method.