A Type System for Data-Flow Integrity on Windows Vista

TL;DR

This paper introduces a formal type system to enforce data-flow integrity on Windows Vista, ensuring trusted objects remain untainted by untrusted code and optimizing runtime checks.

Contribution

It formalizes Vista's integrity model with a type system that guarantees data integrity and identifies redundant runtime checks for potential optimization.

Findings

Type system guarantees trusted objects are untainted

Some runtime checks are redundant and can be optimized

Formal model aligns with Vista's integrity guarantees

Abstract

The Windows Vista operating system implements an interesting model of multi-level integrity. We observe that in this model, trusted code can be blamed for any information-flow attack; thus, it is possible to eliminate such attacks by static analysis of trusted code. We formalize this model by designing a type system that can efficiently enforce data-flow integrity on Windows 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 Windows Vista's runtime access checks are necessary for soundness; others are redundant and can be optimized away.