Achieving security in practical systems is a hard task. As it is the case for other critical system properties (i.e. safety), security should be a concern through all the phases of software development, starting with the very early phases of requirements and design. Although the arguments in favour of formal veri cation at the design level are many (rigour and cost-bene t being at the top of the list), answers to two relevant questions about the limitations of this approach are crucial for its success and further application in industrial contexts: Is security veri cation at the design phase scalable under continuous evolution? What are the limits of the formal security guarantees achieved at the model level when software is ultimately deployed? In this paper we report on recent results and work in progress towards a better understanding of these two fundamental questions.
In recent years, information security has gained increasing attention from the
general public and there is a consensus about its paramount importance in
society. Examples include recent scandals on users private data [
There are several reasons why security is di cult to achieve in practice. On the one hand, the complexity of modern system architectures is constantly increasing: software logic evolves, often driven by the market pressure to deliver new functionalities, and di erent operating systems and hardware con gurations ? PhD work supervised by Jan Jurjens at the Chair for Software Engineering of the
TU Dortmund and Jorge Cuellar at Siemens Corporate Research. 3 Also social aspects of security result in attacks in many cases, but those are very di cult to control by technological means and are out of the scope of this work. make each instantiation of an IT system unique. Moreover, software components from di erent producers delivered without accurate (if at all) security guarantees are used together to achieve customized solutions.
Techniques to tackle this ever `moving target' exist in di erent areas of computer science and engineering: from software and hardware formal veri cation to testing, but also at the level of business-processes modelling and risk-analysis. In fact, security plays a role at di erent levels of abstraction and at di erent phases of the development cycle, and if one wants to have a high degree of assurance about the security of a system one should consider them all.
In general, the strongest guarantees about software and hardware behaviour are delivered by formal methods, due to their rigour and precision. It is thus natural to consider formal methods to validate a system with respect to well-de ned, mathematical descriptions of security. Nevertheless, formal methods are di cult to apply in realistic software-development scenarios because they require highly specialized designers and programmers in order to carry out the formalizations and because many veri cation tools available hardly scale to realistic scenarios, in particular at the level of implementations. Additionally, the security requirements of a system are not always precise, because often they are formulated in natural language.
At the present time, the application of formal methods seems to be more reasonable to take place at the level of system design, where models are abstracted from implementation details and are more amenable to automated veri cation. Since some security problems can be detected already at the speci cation level, the cost-bene t of applying this methodology is typically better than repairing design problems at later stages of development. Since the de-facto standard for system modelling in industry is the Universal Modelling Language (UML), it is natural to perform this formal veri cation on UML models, if one aims at industry acceptance. It is however not enough to have strong security guarantees on system models to be able to judge the overall security of a deployed system, which is the ultimate goal. As argued before, it is di cult to verify the code because of its size and the huge variety of programming languages and paradigms. Moreover it can be the case that libraries or components from third parties are used whose source code is unavailable.
Unfortunately, security is a never ending open loop, since no matter how strong guarantees a given system has, new exploits appear that consider properties or interfaces that were not considered at design. This is prominently illustrated by side-channels: here the attacker exploits information such as electromagnetic radiation, timing and shared memory behaviour to gain possession of con dential data. Many of these side-channels are di cult to capture since they rely on micro-architectural con gurations such as the duration of processor instructions or the cache behaviour. Closing these interfaces is sometimes impossible or costly, because of the impact to other system requirements (i.e. e ciency).
In summary, we believe that it is unrealistic to attempt to build complex industrial systems with a 100% guarantee of security because logical or physical interfaces that are vulnerable to attacks are often only exposed after real attacks take place. To date there is also no standard single methodology, tool, or model to tackle the whole Software Development Life-Cycle. It is thus necessary to provide tools that help to cope with evolution problems at all levels of abstractions and during the whole life-cycle. It is our believe that the idea that systems are going to be secure because we commit to a single approach (for example rigorous security requirements elicitation, industrial best-practices, strict patch update policies etc.) is fallacious: we have to work on all phases and at di erent abstraction levels, sometimes using di erent models and di erent methodologies. In this work we propose a set of such tools, easy to use by end users, and addressing the aforementioned problems on Models, Implementations and Microarchitectures.
State Name
action State Models class HelloWorldApp { { public static void main(String[] args) } } System.out.println("Hello World!");
Implementations
Running system
In the following we summarize the goals of this research and the achieved results
so far. Security is typically described as the conjunction of one or more security
requirements, abstractly classi ed as Con dentiality, Availability and Integrity.
In this work we consider mainly Con dentiality and Integrity: we want to
understand how information is owing from a group of users to another. There are
basically two ways to look at the problem and our proposed solutions: a)
according to the abstraction level modelled and b) according to the security properties
considered. First, we will take the rst point of view (see Fig. 1).
Models We consider the problem of speci cation evolution for security at the
level of UML models. We extend the UMLsec [
Micro-architecture At this detailed abstraction level, we focus on cache con
gurations and how they can act as a leaking channel for di erent adversaries.
Con gurations of the CPU play a determinant role on the security of the
system with respect to side-channel attacks, and the change in con gurations is a
typical phenomenon of system's evolution. Avoiding the use of caches con icts
with e ciency requirements and is therefore not realistic for a wide range of
systems. A promising technique to achieve formal guarantees about
countermeasures striving for a trade-o between security and other con icting requirements
is quantitative information ow analysis (for example [
Notice that we do not aim at a formal integration of the security guarantees obtained at the discussed levels of abstraction: such a task, although interesting, goes outside the scope of this work. On the other hand, current industrial environments do not have a formally justi ed software development process. We consider di erent layers of abstraction mainly due to necessity: any error found in any of these layers would invalidate the over-all security of the system.
It is nevertheless interesting to informally discuss our contributions from the perspective of the security properties considered and the assumptions they rely on at di erent abstraction levels. In fact, when analysing information- ow at the model level, we are assuming perfect mechanisms for access control, and among others, perfect cryptography, which guarantees access control when information is shared through insecure networks. To gain con dence in the correctness of those mechanisms, we validate them locally using model-based testing and performing a Dolev-Yao analysis for the cryptographic protocol logic. To gain even more con dence about primitives, we consider the micro-architectural abstraction level, using quantitative information- ow related techniques. We can see this as an (informal) chain of assumptions and guarantees across abstraction levels, as depicted in Fig. 2.
guarantee Local Access Control assumes Information flow control assumes Communication channel Access Control guarantee Cryptographic protocols assume
Cryptography Non-interference Verification
Model Model
Model assurance assurance
Dolev-Yao Analysis assurance
Model assurance Model-based Testing
Quantitative information flow Analysis The assumptions and guarantees discussed here are by no means complete: for example we are not considering operating system access control mechanisms or semantic security properties of the cryptographic primitives. As already discussed we believe that a complete and formally justi ed methodology is unrealistic. It is nevertheless essential to consider di erent levels of abstraction and development phases to achieve a good degree of con dence in the system, since an error in any of them would invalidate the results at higher abstraction levels or previous phases. For example a faulty implementation of access control would invalidate a secure abstract design w.r.t non-interference, and a cryptographic implementation with side-channels would make a formally veri ed protocol against the Dolev-Yao adversary meaningless. 3
Software security is a di cult problem because it is a moving target, and it should be addressed at di erent levels of abstraction and in all phases of software development. Although a promising methodology to achieve practical security is formal veri cation at design time, to date there a number of limitations to this approach, in particular when the system undergoes continuous evolution. We have reported on results towards a scalable security veri cation at the model level, and pinned down many assumptions made at di erent levels of abstractions, that are vital for the formal model analysis to be sound. Our focus is to devise methodologies supporting intuitive tools, aiming at minding the gap between formal methods and industrial acceptance. At this point of our research, we have already achieved many of the original goals, and promising work in progress is being done on the missing items. Concretely, at this stage work in progress is being done for information ow analysis: at the model level, we are interested in the automatic and e cient veri cation of UML state-charts; at the micro-architectural level novel formal quanti cation techniques are being studied that provide strong security guarantees on realistic modern processor models for powerful attackers and multiple hardware con gurations. Submissions to international conferences in software engineering and automatic veri cation in both of these subjects are on preparation at the time of writing this manuscript. Acknowledgements This research was partially supported by the MoDelSec Project of the DFG Priority Programme 1496 \`Reliably Secure Software Systems { RS3" and the EU project NESSoS (FP7 256890).