A Type System for Data-Flow Integrity on Windows Vista

The 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 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. Categories and Subject Descriptors D.4.6 [Operating Systems]: Security and Protection--Access controls, Information flow controls, Verification; D.2.4 [Software Engineering]: Program Verification--Correctness proofs; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs-Sp...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Avik Chaudhuri, Prasad Naldurg, Sriram K. Rajamani
• Keywords: CORR 2008, Data-flow Integrity, Education, Windows Vista, Windows Vista Operating System