The objective of the research is a soundly based approach to Secure Software Engineering. This is motivated by the observation that the current state of security engineering in practice is far from satisfactory. The goal is thus to start with the actual industrial engineering methods of security-critical software-based systems, to identify problems which are practically amenable to tool-supported, formally sound analysis methods, and to try to solve these problems using these methods. An important objective is to ensure that these analysis methods can actually be used in practice by keeping the additional overhead in using them bounded: Firstly, they take as input artifacts which are already available in current industrial software development (such as UML models and program source code) and do not have to be constructed just to perform the analysis. Secondly, the tools should be reasonably easy to use and have a strong emphasis on automation.
An important missing link in the construction of secure systems is finding a practical way to establish a correspondence between a software design and its implementation. The research performed during this visit addresses this problem for the case of crypto-based implementations in Java (such as crypto protocols). The approach developed during the visit proceeds as follows: Given a textual specification of a crypto-based system and its implementation, we construct a compact and precise representation of the specification using the UML security extension UMLsec. This model can be verified against the security goals which are included in the UMLsec models using automated theorem provers for first order logic with equality. One can then make sure that the implementation correctly implements the specification by making use of software assurance techniques such as run-time verification and security testing. We validated the approach at the open-source Java implementation Jessie of the SSL protocol, where we found a significant security weakness which could be fixed using our approach. We also showed how this assurance approach can be supported in a way that makes the program understanding reusable by establishing traceability through refactoring scripts. We have then demonstrated reusability of the refactoring scripts and security aspects resulting from the Jessie implementation at the case of the Java Secure Socket Extension (JSSE) library recently made open-source by Sun. The approach for establishing traceability through refactoring scripts is new and can be applied generally when refactoring software (not just crypto-protocols). We also developed tools to support the approach at both the model and the code level. The routines verifying the UML models are implemented within a framework that supports implementing verification routines, based on XMI output of the diagrams from UML CASE tools. Advanced users can use this open-source framework to implement verification routines for the constraints of self-defined security requirements. On the code level, the approach is supported by tools that (1) establish traceability through refactoring scripts and (2) modularize security hardening advices through aspect-oriented programming.
Projects organized on the basis of the visit include a follow-on IJP (Aug. 2007 - July 2009) involving the Open University and TU Munich and funded by the Royal Society, which aims to apply the techniques developed during the past visit at a larger implementation, and a PhD scholarship on Verifying C Implementations of Crypto-Protocols funded by Microsoft Research (Cambridge).
Despite the importance of cryptographic protocols for IT security and today`s interconnected IT networks, there is so far little work towards analyzing existing implementations of cryptographic protocols to determine whether they in fact enforce the security properties they are designed to enforce. Since it is well-known that it is very difficult to design and implement such protocols correctly and securely, we can therefore not be sure whether the crypto protocol implementations used today are in fact secure. The work undertaken during this visit contributed to a better understanding of the security of existing crypto protocol implementations.
We considered a concrete example of such an implementation, namely the open-source Java implementation Jessie, which provides an open implementation of one of the main security library for the popular Java programming language (the Java Secure Sockets Extension, JSSE). We analyzed this implementation using our methods and tools and in fact found a significant security weakness in that implementation. We also showed how that weakness can be fixed.
The methods and tools developed for this application are more generally applicable, and we have already demonstrated for part of the approach that the results that were obtained can be efficiently transferred to another implementation of the JSSE, namely the one that is the official library for Java, which was made open-source by Sun only a few months ago. We are continuing to investigate this official library now, since it is in wide-spread use and any results obtained regarding it will be of high significance for many software developers, and even more computer users making use of their software.
Benefits to me personally include not only the opportunity to obtain the above-mentioned, very promising results, but also the opportunity to collaborate with a number of people in Munich and at the OU in the context of this visit, on a number of topics related to the main theme of the visit. Together, we have already produced a very satisfying number of papers most of which have already been published by now.
Benefits to UK science