Modeling test cases for security protocols with SecureMDD
Introduction
Developing a complex and secure system is not only a long and complicated process, but also very prone to errors. While a malicious user often only has to find one flaw in order to exploit an application, the developer has to cover all possible intrusion points and consider all possible attacking scenarios in order to make his system secure. Testing security-critical applications during development stages is essential to the quality of the final product, thus demanding easy and intuitive testing methods. Those methods should allow the modeler or an external tester to both test the functionality of the code as well as to emulate a malicious user in order to avoid possible attacks on the implementation.
Using a model-driven approach to design complex and secure systems can simplify the development process significantly, thus explaining its popularity with developers. In this paper we introduce a method to test the functionality and security of a distributed application based on cryptographic protocols. Our approach is model-driven and allows the modeling of test cases with UML. Based on the UML model Java test code is generated fully automatically, which allows to run the tests on code level. A custom, domain-specific language tailored to designing and testing security protocols as well as intuitive modeling guidelines assist the modeler in designing test cases for complex systems. The test framework is integrated into SecureMDD [1], which is a model-driven approach to develop security-critical systems in the domain of e-Commerce and e-Government. It also supports fully automatic code generation for the modeled system and allows to verify its security properties interactively.
Section 2 introduces the SecureMDD approach. Section 3 focuses on modeling guidelines for test cases in SecureMDD using a running example application “Copycard”. Section 4 explains the process of code generation and shows the resulting test framework architecture for SecureMDD applications. Section 5 discusses some of the related work on model-driven testing, while Section 6 provides an overview over evaluation results. Section 7 concludes this paper.
Section snippets
SecureMDD approach
SecureMDD [1] offers a method to model an application in UML, supporting the design of secure cryptographic protocols between several components. Furthermore, the correctness of those protocols can be proved using formal methods. SecureMDD also considers the implementation of the system, providing a framework to generate executable and deployable code for smart cards and terminals (i.e. components that are connected to a smart card reader and communicate with smart cards) [2].
A SecureMDD model
Test case modeling guidelines
We focus on testing code generated from a platform-independent application model using the SecureMDD framework to not only find protocol logic flaws, but also bugs in the implementation. Such bugs can arise from incorrectly implemented transformation scripts (the verification of their correctness is work in progress [7]). We support functional tests to verify the functionality of modeled protocols and component behavior. We also support security test cases by modeling attack sequences to
Generating code
SecureMDD uses model-to-model and model-to-text transformations to generate platform-specific UML models as well as deployable Java and Java Card3-code.
Several platform specific UML models are generated from the input model using QVTO4 scripts: one for each component type respectively (terminal, smartcard and/or service) and one for test cases.
Code
State of the art and related work
Model-driven testing is a well-researched area with a variety of available implementations, none of which were found to be optimally compatible with SecureMDD. Bouquet et al. [9] introduce their own guidelines for modeling applications in UML and OCL, which allow test cases to be generated automatically from the application model. However, they do not consider security testing of protocols.
Sensler et al. [10] introduce an approach which focuses on designing and generating functional test cases
Evaluation
The test case modeling and generation have been successfully evaluated using several SecureMDD case studies more complex than Copycard. Functional test cases were modeled for a smart card application AgeVerification that uses public-key cryptography and certificates for age verification on the smart card. The ability of the smart card to perform the age verification correctly with different dates was successfully tested. The SecureMDD model of the real-world smart card electronic cash system
Conclusion and outlook
Defining and verifying security attributes of applications is an important part of the development process with SecureMDD, as shown in our previous work [28]. With the new modeling guidelines presented in this paper it is now easily possible to also test those attributes and to exploit found vulnerabilities by designing appropriate test cases. By testing the actual, deployable codebase we provide a testing environment close to the real world. Thus, by introducing and executing test cases in the
Kuzman Katkalov was born in Rostov-on-Don, Russia on February 22, 1986, and moved to Germany in 1996. He graduated at the University of Augsburg (Germany) in 2011, where he has been working since as a research assistant. His main research interests are in model-driven development as well as protocol and information flow security. He is now working on the project IFlow within the Reliably Secure Software Systems priority program of the German Research Foundation.
References (28)
Model-based security testing using UMLsec: a case study
Electronic Notes in Theoretical Computer Science
(2008)- N. Moebius, K. Stenzel, H. Grandy, W. Reif, SecureMDD: A model-driven development method for secure smart card...
- N. Moebius, K. Stenzel, H. Grandy, W. Reif, Model-driven code generation for secure smart card applications, in:...
- N. Moebius, Modellgetriebene Entwicklung sicherer Smart Card-Anwendungen (German), Ph.D. thesis,...
- Oracle, Java Card Platform Specification 2.2.2, 2012....
- et al.
Formal verification of application-specific security properties in a model-driven approach
- et al.
KIV 3.0 for provably correct systems
- et al.
Formal verification of QVT transformations for code generation
- et al.
On the security of public key protocols
IEEE Transactions on Information Theory
(1983) - F. Bouquet, C. Grandpierre, B. Legeard, F. Peureux, N. Vacelet, M. Utting, A subset of precise UML for model-based...
Test automation with model-driven test script development
Secure Systems Development with UML
Cited by (4)
Application-oriented Serial Interface Communication Protocols Formal Modeling Method
2021, Proceedings - 2021 21st International Conference on Software Quality, Reliability and Security Companion, QRS-C 2021An Analysis on OCL/UML Constraints in E-commerce Application
2020, Lecture Notes in Networks and SystemsSecure integration of third party components in a model-driven approach
2016, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)Integration and exchangeability of external security-critical web services in a model-driven approach
2015, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Kuzman Katkalov was born in Rostov-on-Don, Russia on February 22, 1986, and moved to Germany in 1996. He graduated at the University of Augsburg (Germany) in 2011, where he has been working since as a research assistant. His main research interests are in model-driven development as well as protocol and information flow security. He is now working on the project IFlow within the Reliably Secure Software Systems priority program of the German Research Foundation.
Nina Moebius studied Computer Science at the University of Lübeck. Since 2006 she is working as a research assistant at the department of software engineering in Augsburg. Her doctoral thesis is about the model-driven development of secure Smart Card applications. Her research interests are security engineering, verification, model-driven development, software engineering in general and information flow control.
Kurt Stenzel studied Computer Sciences in Karlsruhe, Germany, and began working as a research assistant there. After a period at the University of Ulm, Germany, he moved to Augsburg University where he received his Ph.D. in computer sciences in 2005. Since then he is working in Augsburg on formal Java verification, interactive theorem proving, model-driven development of security-critical systems, and information flow control.
Marian Borek was born in Boskovice, Czech Republic on July 06, 1986, and moved to Germany in 1990. He graduated at the University of Augsburg (Germany) in 2011, where he has been working since as a research assistant. His main research topics of interest are security-critical applications and model driven development. He is now working on the project SecureMDD that is funded by the German Research Foundation.
Wolfgang Reif is full professor for software engineering at Augsburg University, Germany. He is vice-president of the University of Augsburg, and director of the Institute for Software & Systems Engineering. He received his doctoral degree in computer science from the University of Karlsruhe, and held a professorship in software engineering at the University of Ulm from 1995 to 2000. His current research interests are software and systems engineering, safety, reliability and security, organic computing, as well as software-driven mechatronics and robotics. Wolfgang Reif is author of a large number of scientific publications, and is consultant to leading technology companies.