 |
ForTIA Industry Day 2006 |
 |
Formal Methods for Security and Trust in Industrial Applications
August 23rd, 2006
Preliminary announcement
Scope and Purpose
The purpose of the Industry day is to focus on the perceived pro's and con's of formal methods by end-users, not necessarily the proposition(s) that were made by the technology providers. The aim is really to understand how formal techniques can be introduced successfully in an industrial setting and how common pitfalls can be prevented. Pitfalls, that might not necessarily have anything to do with the formal technique itself. We believe that this information is in particularly valuable for managers, project leaders, system engineers and architects from industry.
Program
Invited talk (jointly with Technical Symposium)
9:00-10:00
MDCL 1105
Session Chair: Tobias Nipkow
Tom Henzinger.
Embedded Systems Design Challenge.
Abstract - We summarize some current trends in embedded systems design and point out some of their characteristics, such as the chasm between analytical and computational models, and the gap between safety-critical and best-effort engineering practices. We call for a coherent scientific foundation for embedded systems design, and we discuss a few key demands on such a foundation: the need for encompassing several manifestations of heterogeneity, and the need for constructivity in design. We believe that the development of a satisfactory Embedded Systems Design Science provides a timely challenge and opportunity for reinvigorating computer science.
Supported in part by the ARTIST2 European Network of Excellence on Embedded Systems Design, by the NSF ITR Center on Hybrid and Embedded Software Systems (CHESS), and by the SNSF NCCR on Mobile Information and Communication Systems (MICS).
Joint work with Joseph Sifakis
Supported in part by the ARTIST2 European Network of Excellence on Embedded Systems Design, by the NSF ITR Center on Hybrid and Embedded Software Systems (CHESS), and by the SNSF NCCR on Mobile Information and Communication Systems (MICS).
Joint work with Joseph Sifakis
Session 1:
10:30-12:30
MDCL 1105
Session Chair: Marcel Verhoef
Werner Stephan, DFKI, Germany
Formal Methods for Security: Lightweight Plug-in or New Engineering Discipline
Abstract - 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 centered 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.
Jan Juerjens, TU Munich, Germany
Model-based Security Engineering for Real
Abstract - 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.
Michael Waidner, IBM Research, US
Cryptography and Tool-Supported Proofs
Abstract - 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.
Joint work with Michael Backes and Birgit Pfitzmann.
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.
Joint work with Michael Backes and Birgit Pfitzmann.
Jim Woodcock, University of York, UK
The Grand Challenge (working title)
Abstract - Some practitioners in industry and researchers from universities believe it’s 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.
Invited talk (jointly with Technical Symposium)
14:00-15:00
MDCL 1105 Session Chair:
Eric Hehner
Ernie Cohen.
Validating the Microsoft Hypervisor
Abstract -
Efforts to validate the Microsoft Hypervisor - a low-level program that partitions a real MP machine into a a number of virtual MP pachines - has led to some interesting formal methods developments. We'll survey some of these, including
Session 2:
15:30-17:30
MDCL 1105
Chair: Asuman Suenbuel
David v. Oheimb, Siemens, Germany
Formal methods in the security business: exotic flowers thriving in an expanding niche
Scott Lintelman, Boeing, US
Title tba.
Abstract
Randy Johnson, NSA, US
Cost Effective Software Engineering for Security
Dusko Pavlovic, Kestrel Institute, US
Connector-Based Software Development: Deriving Secure Protocols
- new algorithms for "optimal" stateless search and symbolic stateless search;
- techniques to make stateless search practical for shared memory programs, including efficient shared memory instrumentation and optimal trace replay using breakpoints;
- new techniques for model-based test generation, including the use of symbolic execution to eliminate redundancy and methods to handle invisible internal nondeterminism;
- formal models of the x86/x64 TLB and cache systems;
- verification of algorithms for efficient MP TLB virtualization, which has uncovered subtle design bugs;
- formal analyses of memory sharing between mutually distrustful partitions, which has revealed some surprising cache attacks;
- techniques for eliminating inductive constructs in first-order verification;
- techniques for specifying and reasoning about C code.
Session 2:
15:30-17:30
MDCL 1105
Chair: Asuman Suenbuel
David v. Oheimb, Siemens, Germany
Formal methods in the security business: exotic flowers thriving in an expanding niche
Abstract -
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.
Scott Lintelman, Boeing, US
Title tba.
Abstract
Randy Johnson, NSA, US
Cost Effective Software Engineering for Security
Abstract -
In this talk I will discuss our experience 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 even moderate 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.
Dusko Pavlovic, Kestrel Institute, US
Connector-Based Software Development: Deriving Secure Protocols
Abstract -
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: in general, security properties are not preserved under refinement or composition. The reason is that the nondestructive composition operations require that their static assumptions about the environment are maintained; but Security Engineering is concerned with dynamic, adversarial environments, and what happens when the assumptions fail.
Organizing Committee
- Volkmar Lotz (SAP Research, ForTIA chairman, France)
- Asuman Suenbuel (SAP Research, USA)
Advisory Board
- Emil Sekerinski (FM'06 organizing committee chair)
Board of Recommendation
- Teiichi Aruga, CSK, Japan
- Anthony Hall (United Kingdom, ForTIA chairman 2003/2004)
- David von Oheimb (Siemens Corporate Technology, Germany)
- Alexander Petrenko (ISPRAS, Russia)
- Nico Plat (West Consulting, The Netherlands, and FME secretary)
- Tiziana Margaria (University of Göttingen, Germany and EASST president)
- Denis Sabatier (ClearSy, France)
- Bernhard Schätz (TU Munich, Germany)
- Marcel Verhoef (Chess Information Technology, The Netherlands)
Past events
About FME and ForTIA
Formal Methods Europe ( www.fmeurope.org ) is an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. FME has been notably successful in bringing together innovators and practitioners in precise mathematical methods for software development, industrial users as well as researchers.
A separate subgroup of FME was recently established, called ForTIA (Formal Techniques Industrial Association, www.fortia.org), which focuses on dissemination of research results and promotion of formal techniques in industry and also to feed lessons learnt from industry back towards academia. ForTIA was founded in 2003 and is currently supported by some 30 companies. One of the key activities of ForTIA is to organize so-called Industry Days, small events targeted at industrial practitioners rather than academics. It is a forum to share experiences on the use of formal techniques in an industrial setting. We invite you to participate in this event.