Ulrich Stern
Home
Contact
Resume
Research
Publications
Software
Consulting
 

Java model checking

I will provide a summary about this project shortly. [workshop paper]

Protocol verification

The Murphi Verifier developed in David Dill's research group has been successfully used to find errors in several industrial protocols. One example would be the verification of the typical set cache coherence protocol of the IEEE/ANSI Standard for Scalable Coherent Interface (SCI). During a four-month project, I was able to find several errors in the C-code that defines this protocol, although it had previously been extensively discussed, simulated and even implemented.

The memory requirements of the Murphi Verifier, which employs explicit state enumeration, however, are a bottleneck when verifying the increasingly complex industrial protocols. Thus, I have been working on probabilistic verification algorithms that strongly reduce the memory requirements at the cost of a small probability that protocol errors might go undetected during verification. Even if an error is very unlikely in normal operation of a protocol, the probabilistic verification algorithm will find this error with high, say 99.9%, probability.

When combining state and memory reduction techniques for explicit state enumeration, a shift from memory to run-time as the new major limiting factor in verification can be observed. Thus, I developed a parallel version of the Murphi system on the Berkeley NOW (Network of Workstations) using Active Messages. Later I was hired (for two weeks) by IBM Watson to port parallel Murphi to IBM's SP2s. For several large protocols, close to linear speedups were achieved. I plan to port parallel Murphi to MPI soon to make it more widely usable.

I also worked on an algorithm that allows using magnetic disk instead of main memory for storing almost all of the state table maintained in explicit state enumeration. In experiments with three complex protocols and a table on disk that is one or two orders of magnitude larger than the table in main memory, the runtime overhead is typically only around 15% in comparison to a conventional algorithm working in main memory only.


Security

I recently started working on problems in computer security. I used the Murphi Verifier to model the Needham-Schroeder protocol and was able to detect a flaw first discovered by Gavin Lowe. The Murphi source files of the original and the fixed versions of the protocol are available. The second protocol I modeled was the Kerberos Protocol Version 5. Murphi discovered a bug in a documented version of this protocol. The bug, however, does not occur when implementing the protocol according to the RFC-1510 defining Kerberos.

I am currently working with John Mitchell, Mark Mitchell, and Vitaly Shmatikov on verifying further protocols (including, e.g., SSL 3.0) and on automatically generating the intruder parts of the models of cryptographic protocols. We are also looking into modeling cryptographic functions at a lower level of detail. On example is cipher block chaining in the IP Encapsulating Security Payload (ESP) protocol. The Murphi source file is available.

For more information, please also visit John's page describing the project.


Queueing theory

For my Diplom thesis, I worked on an analytical performance model - based on queueing theory - for computer systems based on the IEEE Standard for Futurebus+.