This thesis studies an emerging class of software bugs called unstable
code: code that is unexpectedly discarded by compiler optimizations
due to undefined behavior in the program. Unstable code is present in
many systems, including the Linux kernel and the Postgres database.
The consequences of unstable code range from incorrect functionality
to missing security checks.
To reason about unstable code, this thesis proposes a formal and
practical approach, which views unstable code in terms of
optimizations that leverage undefined behavior. Using this approach,
we introduce a new static checker called Stack that precisely
identifies unstable code. Applying Stack to widely used systems has
uncovered 160 new bugs that have been confirmed and fixed by
Thesis Supervisors: Frans Kaashoek and Nickolai Zeldovich