Joshua Kroll will present his research seminar/general exam on Friday May 13 at 10 AM in Room 302 (note room!). The members of his committee are: Ed Felten 9advisor), Andrew Appel, and Mike Freedman. Everyone is welcome 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. -------------------------------------- Title: Portable, Verifiable Low-Level Memory Safety Abstract Operating systems can provide isolation between different programs running on the same computer. How- ever, this protection is too coarse or too slow for large applications with extensible functionality, such as browsers, database and web servers, device drivers, and document editors. It is thus necessary to have ro- bust, trustworthy protections that are valid below the process abstraction provided by the operating system. Here, we present two results in the area of Software Fault Isolation (SFI), a mechanism for just this sort of protection. First, we present BakerSFIeld, an SFI framework [1, 2, 3] for the x64 instruction set architecture [4]. SFI is an increasingly widely-used sub-process sandboxing technique in which applications are rewritten using special code-generation tools and augmented with dynamic guards that ensure policy compliance with minimal overhead. BakerSFIeld is derived from PittSFIeld [2], and retains the assembly language rewriting style of its predecessor. We measure the performance of BakerSFIeld on a modern 64-bit desktop machine and determine that it has significantly lower overhead than its 32-bit cousin. But such a scheme is not useful for security unless we are sure that its implementation can be trusted. Thus, we present a novel formally verified sandboxing solution built on top of the CompCert C compiler [9]. This tool generates sandboxed code by rewriting abstract syntax inside CompCert to ensure that all generated code complies with the sandboxing policy. Through a combination of static analysis and dynamic checking, we provide code which is provably policy-compliant at runtime but remains true to the SFI philosophy of ensure-don't-check. As traditional SFI makes use of very concrete aspects of a system's address structure for security, our most surprising result is that an SFI system can also be implemented in CompCert's more abstract setting. Reading List-Papers [1] R. Wahbe, S. Lucco, T. Anderson, and S. Graham, "Efficient software-based fault isolation", in Proceedings of the Fourteenth ACM symposium on Operating systems principles. ACM, 1994, p. 216. [2] S. McCamant and G. Morrisett, "Evaluating SFI for a CISC architecture", in 15th USENIX Security Symposium, 2006, pp. 209-224. [3] B. Yee, D. Sehr, G. Dardyk, J. Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar, "Native client: A sandbox for portable, untrusted x86 native code", in Proceedings of the IEEE Symposium on Security and Privacy, 2009. [4] D. Sehr, R. Muth, C. Biffle, V. Khimenko, E. Pasko, K. Schimpf, B. Yee, and B. Chen. Adapting software fault isolation to contemporary CPU architectures. In Proceedings of USENIX Security, pages 1-11, 2010. [5] J.R. Douceur, J. Elson, J. Howell, and J.R. Lorch. Leveraging legacy code to deploy desktop applications on the web. In Proceedings of the 2008 Symposium on Operating System Design and Implementation, December 2008. [6] B.N. Bershad, S. Savage, P. Pardyak, E.G. Sirer, M.E. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility safety and performance in the SPIN operating system. In ACM SIGOPS Operating Systems Review, volume 29, pages 267-283. ACM, 1995. [7] G.C. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proceedings of the Second Symposium on Operating Systems Design and Implementation. USENIX, 1996. [8] Andrew W. Appel. Foundational proof-carrying code. In Proceedings of the IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 2001. [9] X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363-446, 2009. [10] F.B. Schneider, G. Morrisett, and R. Harper. A Language-Based Approach to Security. 2000. Reading List-Textbooks [1] Ross Anderson. Security Engineering: A Guide to Building Dependable Distributed Systems, Second Edition. Wiley Publishing, Inc., 2008. [2] Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.