A Type System for Data-Flow Integrity on Windows Vista

Avik Chaudhuri, Prasad Naldurg, and Sriram Rajamani

Abstract
Microsoft's Windows Vista operating system implements an interesting model of multi-level integrity. We observe that in this model, trusted code must participate in any information-flow attack. Thus, it is possible to eliminate such attacks by statically restricting trusted code. We formalize this model by presenting 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.

PDF

BibTeX
@inproceedings{tsdfiwv-CNR08,
    author = {Avik Chaudhuri and Prasad Naldurg and Sriram Rajamani},
    title = {A type system for data-flow integrity on {W}indows {V}ista},
    booktitle = {Proceedings of the 3rd ACM SIGPLAN Workshop on
                 Programming Languages and Analysis for Security (PLAS'08)},
    year = {2008},
    pages = {89--100},
    publisher = {ACM}
}

A longer version of this paper, containing proof details and a typechecking algorithm, appears as Microsoft Research Technical Report 2007-86, and is available as an arXiv e-print.