FLoC '02 - VERIFY Friday July 26th

VERIFY on Friday

Detailed program
Friday July 26th, 2002
See also the unified by-slot program

All sessions take place in auditorium 6.

Session 5: FCS Invited talk

Joint with FCS
Chair: Iliano Cervesato

09:00-

10:30

Dieter Gollmann, Microsoft Research Cambridge, UK
Invited talk: Defining security is difficult and error prone
It is often claimed that the design of security protocols is difficult and error prone, with formal verification suggested as the recommended remedy. Verification requires a formal statement of the desired security properties and, maybe surprisingly, many protocols are broken simply by varying the assumptions on goals and intended environment. To defend my claim that defining security is difficult and error prone (and the really interesting challenge in formal verification) I will discuss some old and new examples of security protocols and their formal analysis.

Session 6: Specification and Verification

11:00-

11:30

Amy L. Herzog, MITRE, USA
Joshua Guttman, MITRE, USA
Eager formal methods for security management
Controlling complexity is a core problem in information security. Achieving a security goal in a networked system requires the cooperation of many devices, such as routers, firewalls, virtual private network gateways, and individual host operating systems. Different devices may require different configurations, depending on their purposes and network locations. Many information security problems may be solved given models of these devices and their interactions. We have focused for several years on these problems, using eager formal methods as our approach.
Eager formal methods front-loads the contribution of formal methods to problem-solving. The focus is on modeling devices, their behavior as a function of configurations, and the consequences of their interactions. A class of practically important security goals must also be expressible in terms of these models.
In eager formal methods, the models suggest algorithms taking as input information about system configuration, and returning the security goals satisfied in that system. In some cases, we can also derive algorithms to generate configurations to satisfy given security goals. The formal models provide a rigorous justification of soundness. By contrast, algorithms are implemented as ordinary computer programs requiring no logical expertise to use. Resolving practical problems then requires little time, and no formal methods specialists.
We have applied this approach to several problems. In this extended abstract, we briefly describe two problems and the modeling frameworks that lead to solutions. The first is the distributed packet filtering problem, in which filtering routers or firewalls are located at various points in a network with complex topology. The problem is to constrain the flow of different types of packets through the network. The second problem concerns configuring gateways for the IP security protocols (IPsec); the problem is to ensure that authentication and confidentiality goals are achieved for specific types of packets traversing particular paths through the network. Solutions to these problems have been published and implemented. We also describe how to unify the two solutions, so that packet filtering goals and IPsec authentication and confidentiality are jointly enforced on a network.

11:30-

12:00

Alessandro Armando, U Genova, Italy
Maria Paola Bonacina, U Iowa, USA
Silvio Ranise, LORIA Nancy, France
Michaël Rusinowitch, LORIA Nancy, France
Aditya Kumar Sehgal, U Iowa, USA
High-performance deduction for verification: a case study in the theory of arrays
We outline an approach to use ordering-based theorem-proving strategies as satisfiability procedures for certain decidable theories. We report on experiments with synthetic benchmarks in the theories of arrays with extensionality, showing that a theorem prover - the E system - compares favorably with the state-of-the-art validity checker CVC.

12:00-

12:30

Bernhard Beckert, Karlsruhe U, Germany
Uwe Keller, Karlsruhe U, Germany
Peter H. Schmitt, Karlsruhe U, Germany
Translating the object constraint language into first-order predicate logic
In this paper we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models, realized by an interactive theorem prover. We put an emphasis on usability of the formulas resulting from the translation, and we have developed optimisations and heuristics to enhance the efficiency of the theorem proving process.
The translation has been implemented as part of the KeY system, but our implementation can also be used stand-alone.

Session 7

Joint with FCS
Chair: Serge Autexier, Iliano Cervesato, Heiko Mantel

14:00-

15:30

Ernie Cohen, Microsoft Research Cambridge, UK
Alan Jeffrey, DePaul U, USA
Fabio Martinelli, CNR Pisa, Italy
Fabio Massacci, U Trento, Italy
Catherine Meadows, Naval Research Laboratory, USA
David Basin, U Freiburg, Germany
Panel: The future of protocol verification
This panel is aimed at assessing the state of the art and exploring trends and emerging issues in computer security in general and protocol verification in particular. It brings together experts from both the security community and the verification area. Some of questions over which they will be invited to discuss their views, and maybe even to answer, include: What is already solved? What still needs improvement? What are the challenging open problems? What is the role of automated theorem proving in protocol verification? What else is there in computer security besides protocol verification? A format for this panel has been chosen as to achieve an interesting, vibrant, and productive discussion.

15:30-

15:40

Closing Remarks