A Type System for Data-Flow Integrity on Windows Vista

Microsoft's Windows Vista operating system implements an interesting model of multi-level integrity. In this model, any information-flow attack requires the participation of a trusted process, and can therefore be eliminated by static analysis. We formalize this model by presenting a type system that can efficiently enforce data-flow integrity on Vista. Typechecking guarantees that objects whose contents are statically trusted never contain untrusted values, regardless of what untrusted code runs in the environment. Some of Vista's runtime access checks are necessary for soundness; others are redundant and can be optimized away.