Even with protections like array-bounds checking in place, C programs remain vulnerable to errors in untrusted third-party libraries. Yarra is a new extension to C that uses a combination of static and dynamic techniques to protect the integrity of critical data structures in a C program from corruption by buggy libraries. We have used Yarra to harden applications ranging from SSH, FTP, and HTTP servers to memory allocators like BGET from non-control data attacks in third party code.
Modern applications contain libraries and components written by different people at different times in different languages, often including unsafe languages like C or C++. As a result, one bug, such as a buffer overflow, in any component, can compromise the security and reliability of every other component. To help mitigate these problems, we introduce Yarra, a conservative extension to C with mechanisms for enforcing data integrity and partial safety, even when code is linked against unknown C libraries or binaries. 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 to show that Yarra's semantics are strong enough to support sound local reasoning and the use of a frame rule, even across calls to unknown, unverified code. We also demonstrate that Yarra's semantics can be implemented in several different ways, with different performance and pragmatic tradeoffs. In one implementation, we perform a source-to-source program transformation to ensure correct execution. In a second implementation, we do not rely upon having access to the entire source code, but instead use conventional hardware permissions to protect data. We evaluate our implementations using SPEC benchmarks to understand their performance. Additionally, we apply Yarra to four common applications with known non-control data vulnerabilities. We are able to use Yarra to defend against these attacks while sustaining a negligible impact on their end-to-end performance.
Cole Schlesinger (Princeton University)
|Karthik Pattabiraman (University of British Columbia)|
|Nikhil Swamy (Microsoft Research)|
|David Walker (Princeton University)|
|Ben Zorn (Microsoft Research)|
Modular Protections against Non-control Data Attacks; C. Schlesinger, K. Pattabiraman, N. Swamy, D. Walker, B. Zorn; In proceedings of the IEEE Symposium on Computer Security Foundations (CSF); June 2011
Yarra: An Extension to C for Data Integrity and Partial Safety; C. Schlesinger, K. Pattabiraman, N. Swamy, D. Walker, B. Zorn; Microsoft Research Technical Report (MSR-TR-2010-158); Novemeber 2010