|
|
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+.
|