ForTIA Industry Day 2006
Formal Methods for Security and Trust in Industrial Applications
August 23rd, 2006
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.
Invited talk (jointly with Technical Symposium)
Session Chair: Tobias Nipkow
Embedded Systems Design Challenge.
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 Chair: Marcel Verhoef
Werner Stephan, DFKI, Germany
Formal Methods for Security: Lightweight Plug-in or New Engineering Discipline
Jan Juerjens, TU Munich, Germany
Model-based Security Engineering for Real
Michael Waidner, IBM Research, US
Cryptography and Tool-Supported Proofs
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)
Invited talk (jointly with Technical Symposium)
MDCL 1105 Session Chair:
Validating the Microsoft Hypervisor
- 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.
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
Randy Johnson, NSA, US
Cost Effective Software Engineering for Security
Dusko Pavlovic, Kestrel Institute, US
Connector-Based Software Development: Deriving Secure Protocols
- Volkmar Lotz (SAP Research, ForTIA chairman, France)
- Asuman Suenbuel (SAP Research, USA)
- 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)
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.