Winter 2005: CSE 291 - Static Analysis of Systems Code

Course Description

The success that researchers have had in improving the performance of computer systems has led to heavy dependance upon computing machinery. Prudence dictates that we depend only upon systems that are reliable, as the cost of bugs leading to loss of throughput, exploitable vulnerabilities, or crashes, is millions of dollars as well as human life. Unfortunately, the ever increasing size and complexity of such systems makes traditional quality assurance methods like code inspection and testing insufficient as both methods are swamped by the proliferation of ``corner cases". An alternative approach is to harness the computing horsepower now available to automatically and rigorously analyze programs to prove that they have desirable safety properties, or, if not, to find unsafe executions. This class will be a survey of research into methods for rigorously and statically (i.e. at compile time) analyzing systems programs for a variety of safety properties. We will study the classical methods on which most recent techniques are based, namely Type Systems, Data-flow Analysis, Deductive Methods, and Model Checking, as well as recently proposed analyses, including methods for checking for buffer overrun exploits, correct use of root privileges, data races and deadlocks in multithreaded programs, safe OS Kernel Extensions, floating-point errors in real-time embedded systems, and the correct usage of Kernel APIs by device drivers.

Prerequisites

The class will be mainly self-contained. Familiarity with undergrad level Data Structures, Algorithms, Computability, Programming Languages, Compilers and Operating Systems helps, but is not essential.

Lecture Times and Location

Instructor

Class Schedule: Lectures, Readings

Topics, Reading List

Requirements and Grading

Projects

Your project can take one of two forms: