[talks] C Schlesinger general exam
mml at CS.Princeton.EDU
Thu Apr 28 11:29:50 EDT 2011
Cole Schlesinger will present his research seminar/general exam on Wednesday
May 4 at 10AM in Room 402. The members of his committee are: David
Walker (advisor), David August, and Andrew Appel. Everyone is invited to attend
his talk and those faculty wishing to remain for the oral exam following are
welcome to do so. His abstract and reading list follow below.
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
extension to C with mechanisms for enforcing data integrity and partial
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
the given static type. Any attempt to write to critical data through a
with an invalid type (perhaps because of a buffer overrun) is detected
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
semantics are strong enough to support sound local reasoning and the use
frame rule, even across calls to unknown, unverified code. We evaluate a
prototype implementation of a compiler and runtime system for Yarra by
to harden four common server applications against known non-control data
vulnerabilities. We show that Yarra defends against these attacks with
negligible impact on their end-to-end performance.
- Pierce, Benjamin. Types and Programming Languages.
- Winskel, Glynn. The Formal Semantics of Programming Langauges.
(Chapters 1 - 6).
Formal methods papers:
- S. Ishtiaq, P. O'Hearn. BI as an Assertion Language for Mutable Data
Structures. In POPL, 2001.
- P. O'Hearn, H. Yang, J. Reynolds. Separation and Information Hiding.
In POPL, 2004.
- S. K. Lahiri, S. Qadeer, D. Walker. Linear Maps. In PLPV, 2011.
- G. Tan. JNI Light: An Operational Model for the Core JNI. In APLAS, 2010.
- G. C. Necula, S. McPeak, and W. Weimer. CCured: Type-Safe Retrofitting of
Legacy Code. In POPL, 2002.
- S. Chen, J. Xu, E. C. Sezer, P. Gauriar, and R. K. Iyer. Noncontrol-data
attacks are realistic threats. In Usenix Security (SSYM), 2005.
- R. W. M. Jones and P. H. J. Kelly. Backwards-compatible bounds checking
for arrays and pointers in C programs. In AADEBUG, 1997.
- S. Nagarakatte, J. Zhao, M. M. K. Martin, and S. Zdancewic. SoftBound:
Highly compatible and complete spatial memory safety for C. In PLDI,
- E. D. Berger, T. Yang, and G. Novark. Grace: Safe multithreaded
programming for C/C++. In OOPSLA, 2009.
- R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient
software-based fault isolation. In SOSP, pages 203 - 216, 1993.
More information about the talks