by Dimitris E. Simos (SBA Research)
The SPLIT project applies methods from the field of combinatorial (interaction) testing and model-based testing with the aim of providing quality assurance to software security protocols. The project thus makes a significant contribution towards protecting the information of communicating parties in a digitally connected society.
Security protocols are communication protocols that guarantee the security properties (authentication or confidentiality) by defined rules and cryptography methods. The mathematics community tried to suppress revelations that the NSA BULLRUN and PRISM projects eavesdropped on user communications as well as planting backdoors in cryptographic systems that protect our data [1]. Computer scientists may need to re-verify the popular cryptography methods and protocol designs for secure communication (e.g., TLS/SSL, SSH) in order to win back public trust in security mechanisms and products. Even when the security protocols are designed perfectly, backdoors may also be proposed during the implementation of the protocols and pave the way for breaches of security by potential attackers. The SPLIT project addresses this important security problem and proposes different models and algorithms to verify the security of the related protocol implementations automatically and reveal the infused backdoors.
In particular, the security aspects of protocol implementations have so far not been thoroughly tested and potential security vulnerabilities can have a severe impact on their intended functionality. Part of the reason for this is that security testing still lacks automation and thus requires a lot of resources.
SPLIT [L1] faces the challenges of developing automated security testing methods that can analyse security protocols and prove that they have been implemented securely, and of bringing security testing into the software development life cycle early on as part of an ICT process. We have three specific goals:
1. Methodology for security protocol interaction testing: We aim to create new models and establish algorithmic foundations for model-based testing [2] and combinatorial testing [3], respectively, so that a wide range of security protocols and their respective implementations can be evaluated for detecting vulnerabilities with guaranteed levels of trustworthiness in security testing results. A framework for detection of flaws in protocol specification will be provided, which checks whether an implementation is vulnerable to different types of attacks.
2. Improving automation for security testing: We aim to ensure and improve automation during the security testing process by combining the aforementioned testing methodologies. In particular, even in the early phases of software development, the availability of a testing framework for security can significantly improve the likelihood of detecting security related faults early, thereby contributing to the overall quality of the generated software.
3. Provide quality assurance: We aim to provide quality assurance of implementations of security protocols and to prove that they have been implemented securely. We will do so on two levels: One will be to examine the order of execution of events of the protocol at a macro level, the other will be to examine each major step atomically and take a detailed look at error handling at each step. This way we also attempt to show the correctness of the protocol itself.
Figure 1: Methodology of the SPLIT project.
The SPLIT project has been running since February 2016 and is funded by the BRIDGE Early Stage Program (a funding scheme of the FFG, the Austrian Research Promotion Agency). The project is led by SBA Research in collaboration with Graz University of Technology and OBJENTIS Software Integration, all located in Austria. University of Texas at Arlington and the National Institute of Standards and Technology (NIST), both based in USA, serve in the project’s advisory board.
Currently, a group of ten researchers – mathematicians, software engineers and security specialists – is working in this project towards an automated testing framework based on combinatorial methods that can be used for X.509 certificate testing. Work on model-based testing approaches for the description of attacks that can occur in the TLS protocol and combinatorial coverage measurements for TLS cipher suites recommendations is also in progress.
Link:
[L1] https://www.sba-research.org/split/
References:
[1] A. Odlyzko: “The Mathematical Community and the National Security Agency”, in Notices of the American Mathematical Society, Volume 61, Number 6.
[2] I. Schieferdecker, J. Grossmann, M. Schneider: “Model-based security testing”, in Proc. of the Model-Based Testing Workshop at ETAPS 2012, p. 1–12, 2012.
[3] D. Kuhn, R. Kacker, Y. Lei: “Practical combinatorial testing”, NIST Special Publication 800-142, 2010.
Please contact:
Dimitris E. Simos, SBA Research, Vienna, Austria
