The objective of our research is a soundly based approach to Secure Software Engineering. More specifically, one main current focus is the automated, formally based analysis of software artefacts against security requirements. 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: First, they take as input artefacts 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. Second, the tools should be reasonably easy to use and have a strong emphasis on automation.
So far, part of our research has focused on the specification level. There, starting from the practical software security point-of-view and based on experiences from industrial application projects, an extension of the industrial specification notation UML (Unified Modeling Language) has been defined which is used to include static and behavioural security requirements into models of software systems . To facilitate the treatment of complex security concepts, an aspect-oriented approach to modeling security requirements in this context is investigated .
Depending on the security problems to be addressed, different automated, formally-based tools are used to establish practical security requirements. More concretely, this includes automated theorem provers for first-order logic (such as SPASS and Setheo ), evaluation using Prolog , and model-checking using Spin and SMV . This work is based on a formal execution semantics for UML diagrams (including Statecharts and Sequence Diagrams ). The verification tools are integrated into a modular, extensible UML verification tool framework available as open-source . In particular, reasoning techniques for security requirements have been examined, such as refinement ( proposing a solution for the "refinement paradox" well-known in the formal methods for security community), protocol layering , and composability issues .
More recently, we have applied automated verification for security requirements to the source code level . This has been supported by a PhD scholarship on Verifying Implementations of Security Protocols in C funded by Microsoft Research (Cambridge), co-supervised by Andrew D. Gordon (MSRC). To support the source code analysis, we have also been interested in the topic of program comprehension .
A link between formal and industrial verification techniques is made with work on automated model-based test-sequence generation for security-critical systems against security requirements using constraint-solving techniques . An empirical study on different code analysis and testing tools was published .
A lot of our work has been done in cooperation with industrial partners including BMW, HypoVereinsbank, O2 (Germany), Infineon, Deutsche Telekom, Munich Re, IBMRational, Deutsche Bank, Allianz, and others . Experiences from a collaboration with O2 (Germany) on applying model-based security engineering techniques to mobile communication systems were published . An application of model-based security engineering to an intranet information system at BMW was published . As an application of our research, in the context of the Verisoft-project funded by the German Ministry of Education and Research (BMBF), a practical, formally based security engineering approach was developed and applied at the hand of a biometric authentication system developed by Deutsche Telekom . Of particular interest are also the application domains of smart-card based systems and electronic payment systems .
The second main difficulty with security-critical software in practice, besides a correct enforcement of security requirements during development, is the correct configuration of security-critical applications. For example, security permissions in the financial sector (such as the permission for an employee to grant a credit) have to obey general security policy rules, such as the "four-eye-principle" (i.e., large credits have to be confirmed by two employees). With large permission sets (60,000 in the case of the bank that motivated this particular research, the HypoVereinsbank), dynamic changes (for example, vacancy substitutions), and complicated permissions (such as delegation of rights), a continuous manual inspection is infeasible. This motivates our work on developing a logic-based analysis method for security-critical permission configuration, and the associated tool-support in Prolog .
Another difficulty with security-critical systems is that adversaries will generally try to attack the weakest link in the system, and in particular exploit any mismatches between security requirements and guarantees on different conceptual or physical levels of a system. Therefore, the approach taken has to be as seamless as possible, which is another focus of research. As one example, in joint work with Martin Abadi, it is shown that, under suitable assumptions, the usual abstract approach to security analysis using formal methods is faithful with respect to the more fine-grained complexity-theoretical security models for cryptography .
In other strands of research, the methods and insights gained in the security engineering field are being transferred to other application domains with sophisticated non-functional requirements, such as dependable, safety-critical, real-time, or performance-sensitive systems .
Long-standing research interests are logical versus algebraic definability results (such as a result solving an open problem from a standard book on categorical model theory (Gabriel, Ulmer 1971), and refuting a theorem from another standard book in this area from 1994) .