Bugs in security-critical software are common and costly. I propose a lightweight approach both for finding these bugs and for verifying their absence in large software programs. In this approach, I identify rules of safe programming practice, encode them as safety properties, and verify whether programs satisfy these properties. Since manually verifying properties is expensive, I have developed a model checking tool, MOPS, for automating this process.

To achieve my goal of making model checking for security practical, I must solve three research challenges: making MOPS scale to large programs, helping the MOPS user specify complex but structured properties, and allowing the user to apply MOPS conveniently and comprehend its error reports easily. I will describe my new algorithms and approaches for solving these challenges.

Using MOPS, I checked over one million lines of mature, widely deployed application programs and discovered more than a dozen security vulnerabilities and weaknesses. I checked a security API on several Unix systems and found portability pitfalls, documentation errors, and an implementation bug. I also verified several invariants in the EROS kernel.

Hao Chen is a faculty candidate.

Tuesday, April 20 at 4:00 p.m. in DH 1070
Reception precedes the presentation at 3:30 p.m. in the atrium by the third floor printer room.

Copyright 2000 Rice University
site problems: www@cs.rice.edu

--- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- ---