Events

28 April 2011

Bât. I. 1st floor
Microsoft Research - Inria Joint Centre
Parc Orsay Université

Yarra: Modular Protections against Non-control Data Attacks
Nikhil Swamy
MSR Redmond

A non-control data attack occurs when security-critical data allocated on the heap is unexpectedly modified, e.g., by third-party libraries that violate memory safety.

This paper introduces Yarra, a conservative extension to C to protect applications from non-control data attacks. Yarra programmers specify their data integrity requirements by declaring critical data types and ascribing these critical types to important data structures. Yarra guarantees that such critical data is only written through pointers with the given static type. Any attempt to write to critical data through a pointer with an invalid type (perhaps because of a buffer overrun) is detected dynamically.

We formalize Yarra’s semantics and prove the soundness of a program logic designed for use with the language. A key contribution is a novel type-based frame rule in Yarra’s logic: this rule makes the logic strong enough to support sound local reasoning even across calls to unknown, unverified code that may have arbitrary effects on the heap.

We evaluate a prototype implementation of a compiler and runtime system for Yarra by using it to harden four common server applications against known non-control data vulnerabilities. We show that Yarra defends against these attacks with only a negligible impact on their end-to-end performance.

Joint work with:
Cole Schlesinger (Princeton),
Karthik Pattabiraman (U. Brit. Columbia),
David Walker (Princeton),
and Ben Zorn (MSR Redmond)