Alex Aiken
Computer Science Department
Stanford University
" Verifying a Security Property of an Operating System "
Abstract
This talk will relate our experience using static analysis technologyto try to verify a security property of an entire operating system. The Linux kernel in the "full" configuration has more than 90,000 functions and about 6.2 million lines of code. Designing analysis algorithms that work at this scale with sufficient precision is challenging. This talk will discuss both the theoretical and practical issues that we encountered in this project and describe how far we got, or, depending on your point of view, how far we have yet to go. The talk will conclude with what we believe is a complete list of remaining open problems to be solved before we can claim to have completely verified a non-trivial property of a full operating system.
This is joint work with Suhabe Bugrara, Isil Dillig, Thomas Dillig,Brian Hackett and Peter Hawkins.
Bio:
Alex Aiken received his Bachelors degree in Computer Science and Music from Bowling Green State University in 1983 and his Ph.D. from Cornell University in 1988. Alex was a Research Staff Member at the IBM Almaden Research Center (1988-1993) and a Professor in the EECS department at UC Berkeley (1993-2003) before joining the Stanford faculty in 2003.
URL:http://theory.stanford.edu/~aiken/
Thursday, October 16,2008
3:00 - 4:15
Wu & Chen
101 Levine Hall