When: Monday, April 23, 12:00 p.m.

Where: NULLvalue Collaborative Innovation Center

Alex Aiken, Stanford University

CyLab Seminar

Abstract:
This talk will relate our experience using static analysis technology to 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 over 6.2 million lines of code. Designing analysis algorithms that work at this scale with sufficient precision is challenging; we'll present progress made so far and what issues remain. We will also discuss some recent theoretical results and experiments suggesting how to remove one of the major remaining obstacles to complete verification.

This is joint work with Suhabe Bugrara, Isil Dillig, and Thomas Dillig.

<< Back