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.