On the Significance of Formal Methods in the Development of High-Assurance Secure Systems
Sp-117, 30 July 2003, 1400-1450
Download Presentation Part A
Download Presentation Part B

We discuss the use of formal methods, especially rewriting logic and its supporting tools, in several recent projects: (1) Operational semantics of PLAN, a programming language for active networks. (2) Design and analysis of Sectrace, a new protocol to set up security associations and security policies in IPSec networks. (3) Formal specification of Spread, a group communication middleware that is available for various operating systems. As it can be seen from these applications, formal methods can be beneficial in different phases of the development process. Furthermore, rewriting logic together with its central notion of executable specifications, can serve as a basis for an entire spectrum, ranging from lightweight to heavyweight formal methods. In this talk we argue that formal methods can not only increase the quality of the resulting product, but they can also shorten the overall development process by using executable formal prototypes and suitable tools for their analysis.

About Dr. Mark-Oliver Stehr
After graduating from University of Hamburg in 1996, Mark-Oliver was employed as research assistant in the theoretical foundations of computer science group at the same university. His research and teaching was concerned with distributed systems, especially with the work of Prof. h.c. C.A. Petri, and with the theory and application of logic and type theory. His employment at the university of was interrupted by several research visits to the US. For about three years between 1998 and 2001 Mark-Oliver was International Fellow at SRI International and part of the time Visiting Scholar at Stanford University. During this period Mark-Oliver completed his thesis "Programming, Specification, and Interactive Theorem Proving - Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory", which was supported via several projects by DARPA, NSF, ONR, and NASA, and defended at the University of Hamburg in 2002. Currently, Mark-Oliver is employed as postdoctoral research associate at the University of Illinois at Urbana-Champain, further advancing the practical use of formal methods in real world applications involving protocols and security aspects.