Hao Chen
UC Davis
Thursday, November 4, 2004
1131 Kemper Hall
3 :10-4:00 p.m.
Bugs in security-critical software are common and costly.
We propose a lightweight approach both for finding these bugs and for
verifying their absence in large software programs. In this approach,
we identify rules of safe programming practice, encode them as safety
properties, and verify whether programs satisfy these properties. Since
manually verifying properties is expensive, we have developed a model
checking tool MOPS for automating this process.
Using MOPS, we checked over one million lines of mature, widely deployed
application programs and discovered more than a dozen security vulnerabilities
and weaknesses. Recently, we checked the entire RedHat Linux distribution
containing more than 60 million lines of code and found lots of vulnerabilities.
I will describe the lessons learned from these experiences and directions
for future work.