Winter 2005: CSE 291 - Static Analysis of Systems Code
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
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
Monday and Wednesday at 3:30 - 4:50 pm, in HSS 1138
Upto 4 small homework assignments covering the papers read (20 %)
Class participation and paper reviews (20%)
Scribe Notes (one lecture per student) (20%)
Your project can take one of two forms:
A survey of a particular area related to the course, together with how
the techniques surveyed may be used to verify or find errors in a
particular system of your choice. For this you need to pick the
area, the system and the property you wish to analyze the system
for, and write a 6-10 page report describing in detail how the techniques
surveyed can be used to perform the analysis. Bonus points if you can
actually use the tools that implement the technique to successfully
analyze your system.
A proposal for new research related to the course. You will need to
identify a topic, propose a set of 3-4 papers as background, and write a
6-10 page report describing and justifying the problem that you are proposing,
and describing your proposed solution.
The proposal could, for example, be a new analysis method, algorithmic
improvements in existing methods that make them more precise or scalable,
or extensions to existing methods that make them applicable in novel