[talks] C Schlesinger general exam

[Melissa Lawson]

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.
---------------------------------

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 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.


Reading list:

Textbooks:

- 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.

Systems papers:

- 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,
2009.
- 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.