Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker and Benjamin Zorn, Proceedings of the Computer Security Foundations Symposium (CSF), 2011. [ PDF | Talk ]
You can find the technical report version here.
Abstract: 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 critical 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.