ForTIA Industry Day 2006

Wednesday 23 august 2006

McMaster University, Hamilton, Ontario, Canada
one-day industry event at FM'06
Wednesday 23 august 2006

This contribution discusses two main lines of developments concerning the use of formal methods in security engineering. Fully automated and highly specialized methods that hide most of the formal theory from its users are compared to formal security models centred around explicit formal system models. It is argued that only the latter offer the perspective to comprehensively control the development process with its various security aspects and phases. In putting more emphasis on the combination of theories, fragmentation could be overcome by an integration of the specialized methods that are presently still applied in isolation.

We give an overview over a soundly based secure software engineering methodology and associated tool-support developed over the last few years under the name of Model-based Security Engineering (MBSE). We focus in particular on applications in industry.

Security-critical systems are an important application area for formal methods. However, such systems often contain cryptographic subsystems. The natural definitions of these subsystems are probabilistic and in most cases computational. Hence it is not obvious how one can treat cryptographic subsystems in a sound way within formal methods, in particular if one does not want to encumber the proof of an overall system by probabilities and computational restrictions due only to its cryptographic subsystems. We survey our progress on integrating cryptography into formal models, in particular our work on reactive simulatability (RSIM), a refinement notion suitable for cryptography. We also present the underlying system model which unifies a computational and a more abstract presentation and allows generic distributed scheduling. We show the relation of RSIM and other types of specifications, and clarify what role the classical Dolev-Yao (term algebra) abstractions from cryptography can play in the future.

Some practitioners in industry and researchers from universities believe it is now practical to use formal methods to produce software, even non-critical software, and that this will turn out to be the cheapest way to do it. Given the right computer-based tools, the use of formal methods could become widespread and transform the practice of software engineering. The computer science community recently committed itself to making this a reality within the next fifteen to twenty years. Collectively, we have a lot of experience in the successful use of formal methods in industry, and this is being strengthened by a new wave of tools shielding users from deep technical issues. The time is now right for a concerted push at software verification, and considerable activity is already under way in the Verified Software Grand Challenge and its pilot projects.

Formal methods in the industrial wild, outside the academic greenhouse, are still considered rather exotic, or even esoteric. Sometimes they are admired, more often smiled at, and most times simply ignored. There are some niches, though, where they display their abstract beauty. One of those places offering suitable environmental conditions is security. Which are the specific fertilizers there? Which particular sub-species have proven versatile and sturdy enough to survive in harsh industrial climate? Who recognizes the strong blessings of their hardly accessible blossoms? We share our grower's experience with them in the security field.

In this talk I will discuss the experience in our High Confidence Software and Systems research team with one particular development methodology for security related software. I will describe the general principles it follows, the tools used, and the resources needed. Then I will offer some opinions on why this approach is effective and practical for achieving moderate to high levels of security. When the goal is a very high level security, I will explain why I believe that at least the general principles, if not the specific details, are probably essential.

While most branches of engineering consist of methodologies for building complex systems from simple components, formulating incremental and compositional methods for Security Engineering has been a daunting task. The reason is that connecting components often introduces new information flows, and may not preserve security. The goal of our long-term effort towards Protocol Derivation System has been to capture the sound rules and methods for incremental protocol development, that have evolved in practice, to study their semantic foundations, and to provide tool support. In this talk, I shall summarize results of this effort so far, and present a case study of GDOI, the standard protocol for group communication and multicast over IPSec.