|
Research
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.
The publications mentioned below can be found here.
Model-based Development
So far, part of our research has focussed 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 (see the UMLsec book, the FOSAD book chapter
and the conference contributions at FASE'01 and UML'02). To facilitate the
treatment of complex security concepts, an aspect-oriented approach to
modeling security requirements in this context is investigated in the
conference paper at Models`05.
Formal Verification
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; see
the conference paper at ICSE'05 and the FMCO'05 book chapter),
evaluation using Prolog (see the HASE'04 conference paper), and
model-checking using Spin and SMV (see the STTT'07 journal paper and
the conference contributions at UML'04 and FASE'05). This work is
based on a formal execution semantics for UML diagrams (including
Statecharts and Sequence Diagrams; see the UMLsec book and the
conference papers at FMOODS'02). The verification tools are integrated
into a modular, extensible UML verification tool framework available
as open-source (see the UMLsec tools and the ICSE'06 conference
paper). In particular, reasoning techniques for security requirements
have been examined, such as refinement (see the FME'01 conference paper
proposing a solution for the "refinement paradox" well-known
in the formal methods for security community), protocol layering (see
the SAFECOMP'03 conference paper), and composability issues (see the
Concur'01 conference paper).
Source Code Analysis
More recently, I have applied automated verification for security
requirements also to the source code level (see the conference papers
at ASE'07, ASE'06, ASE'05, ACSAC'05). This has recently become 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, I have recently
also become interested in the topic of program comprehension (see the
conference papers at ICSM'05, CSMR'07, and CSMR'08).
Testing
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 (see the
conference papers at ASE'01 and ICFEM'02). An empirical study on different
code analysis and testing tools is presented in the TestCom'05 conference
paper.
Industrial Applications
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
(see the invited conference paper at the FM'06 industry day for an
overview). Experiences from a collaboration with O2 (Germany) on
applying model-based security engineering techniques to mobile
communication systems are presented in the ICSE'08 paper. An
application of model-based security engineering to an intranet
information system at BMW is presented in the ICSE'07 paper. 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 (see the conference paper at ACSAC'05 and
the ICSE'07 tutorial paper). Of
particular interest are also the application domains of smart-card
based systems and electronic payment systems (see e.g. the ASE'01 conference
paper), as well as service-oriented systems (see the ICSOC'04 paper).
Security Configurations
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 (see e.g. the
conference contribution at FASE'08).
Complexity-theoretical Soundness of Symbolic Analysis
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 (see the
conference contribution at TACS'01).
Dependability
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 (see the forthcoming journal paper at the Journal of
Software and Systems, the book chapter [Bc4] and the
conference papers at EDCC-5, UML'03, Dependable Computing'03, and
ACSD'01).
Foundations
Long-standing research interests are logical versus algebraic
definability results (see the journal article in the Journal for Pure
and Applied Algebra for 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),
as well as programming language semantics (see the Elsevier "Synthese"
journal article for a survey on research in that area which has
inspired much of my research in one way or another).
|