<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 12 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
        {font-family:"Cambria Math";
        panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
        {font-family:"Arial Unicode MS";
        panose-1:2 11 6 4 2 2 2 2 2 4;}
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
        {font-family:"\@Arial Unicode MS";
        panose-1:2 11 6 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0in;
        margin-bottom:.0001pt;
        font-size:11.0pt;
        font-family:"Calibri","sans-serif";}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:purple;
        text-decoration:underline;}
p.MsoPlainText, li.MsoPlainText, div.MsoPlainText
        {mso-style-priority:99;
        mso-style-link:"Plain Text Char";
        margin:0in;
        margin-bottom:.0001pt;
        font-size:9.0pt;
        font-family:"Arial","sans-serif";}
span.PlainTextChar
        {mso-style-name:"Plain Text Char";
        mso-style-priority:99;
        mso-style-link:"Plain Text";
        font-family:"Arial","sans-serif";}
.MsoChpDefault
        {mso-style-type:export-only;}
@page WordSection1
        {size:8.5in 11.0in;
        margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
        {page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=EN-US link=blue vlink=purple><div class=WordSection1><p class=MsoPlainText>Joshua Kroll will present his research seminar/general exam on Friday May 13 <o:p></o:p></p><p class=MsoPlainText>at 10 AM in Room 302 (note room!).  The members of his committee are:  Ed <o:p></o:p></p><p class=MsoPlainText>Felten 9advisor), Andrew Appel, and Mike Freedman.  Everyone is welcome to <o:p></o:p></p><p class=MsoPlainText>attend his talk, and those faculty wishing to remain for the oral exam following <o:p></o:p></p><p class=MsoPlainText>are welcome to do so.  His abstract and reading list follow below.<o:p></o:p></p><p class=MsoPlainText>--------------------------------------<o:p></o:p></p><p class=MsoPlainText><o:p> </o:p></p><p class=MsoPlainText>Title:<o:p></o:p></p><p class=MsoPlainText>Portable, Verifiable Low-Level Memory Safety<o:p></o:p></p><p class=MsoPlainText><o:p> </o:p></p><p class=MsoPlainText>Abstract<o:p></o:p></p><p class=MsoPlainText>Operating systems can provide isolation between different programs<o:p></o:p></p><p class=MsoPlainText>running on the same computer. How- ever, this protection is too coarse<o:p></o:p></p><p class=MsoPlainText>or too slow for large applications with extensible functionality, such<o:p></o:p></p><p class=MsoPlainText>as browsers, database and web servers, device drivers, and document<o:p></o:p></p><p class=MsoPlainText>editors. It is thus necessary to have ro- bust, trustworthy<o:p></o:p></p><p class=MsoPlainText>protections that are valid below the process abstraction provided by<o:p></o:p></p><p class=MsoPlainText>the operating system. Here, we present two results in the area of<o:p></o:p></p><p class=MsoPlainText>Software Fault Isolation (SFI), a mechanism for just this sort of<o:p></o:p></p><p class=MsoPlainText>protection.<o:p></o:p></p><p class=MsoPlainText>First, we present BakerSFIeld, an SFI framework [1, 2, 3] for the x64<o:p></o:p></p><p class=MsoPlainText>instruction set architecture [4]. SFI is an increasingly widely-used<o:p></o:p></p><p class=MsoPlainText>sub-process sandboxing technique in which applications are rewritten<o:p></o:p></p><p class=MsoPlainText>using special code-generation tools and augmented with dynamic guards<o:p></o:p></p><p class=MsoPlainText>that ensure policy compliance with minimal overhead. BakerSFIeld is<o:p></o:p></p><p class=MsoPlainText>derived from PittSFIeld [2], and retains the assembly language<o:p></o:p></p><p class=MsoPlainText>rewriting style of its predecessor. We measure the performance of<o:p></o:p></p><p class=MsoPlainText>BakerSFIeld on a modern 64-bit desktop machine and determine that it<o:p></o:p></p><p class=MsoPlainText>has significantly lower overhead than its 32-bit cousin.<o:p></o:p></p><p class=MsoPlainText>But such a scheme is not useful for security unless we are sure that<o:p></o:p></p><p class=MsoPlainText>its implementation can be trusted. Thus, we present a novel formally<o:p></o:p></p><p class=MsoPlainText>verified sandboxing solution built on top of the CompCert C compiler<o:p></o:p></p><p class=MsoPlainText>[9]. This tool generates sandboxed code by rewriting abstract syntax<o:p></o:p></p><p class=MsoPlainText>inside CompCert to ensure that all generated code complies with the<o:p></o:p></p><p class=MsoPlainText>sandboxing policy. Through a combination of static analysis and<o:p></o:p></p><p class=MsoPlainText>dynamic checking, we provide code which is provably policy-compliant<o:p></o:p></p><p class=MsoPlainText>at runtime but remains true to the SFI philosophy of<o:p></o:p></p><p class=MsoPlainText>ensure-don't-check. As traditional SFI makes use of very concrete<o:p></o:p></p><p class=MsoPlainText>aspects of a system's address structure for security, our most<o:p></o:p></p><p class=MsoPlainText>surprising result is that an SFI system can also be implemented in<o:p></o:p></p><p class=MsoPlainText>CompCert's more abstract setting.<o:p></o:p></p><p class=MsoPlainText><o:p> </o:p></p><p class=MsoPlainText>Reading List<span style='font-family:"Arial Unicode MS","sans-serif"'>-</span>Papers<o:p></o:p></p><p class=MsoPlainText>[1] R. Wahbe, S. Lucco, T. Anderson, and S. Graham, <span style='font-family:"Arial Unicode MS","sans-serif"'>"</span>Efficient<o:p></o:p></p><p class=MsoPlainText>software-based fault isolation", in Proceedings of the Fourteenth<o:p></o:p></p><p class=MsoPlainText>ACM symposium on Operating systems principles.        ACM, 1994, p. 216.<o:p></o:p></p><p class=MsoPlainText>[2] S. McCamant and G. Morrisett, <span style='font-family:"Arial Unicode MS","sans-serif"'>"</span>Evaluating SFI for a CISC<o:p></o:p></p><p class=MsoPlainText>architecture", in 15th USENIX Security Symposium, 2006, pp. 209<span style='font-family:"Arial Unicode MS","sans-serif"'>-</span>224.<o:p></o:p></p><p class=MsoPlainText>[3] B. Yee, D. Sehr, G. Dardyk, J. Chen, R. Muth, T. Ormandy, S.<o:p></o:p></p><p class=MsoPlainText>Okasaka, N. Narula, and N. Fullagar, <span style='font-family:"Arial Unicode MS","sans-serif"'>"</span>Native client: A sandbox for<o:p></o:p></p><p class=MsoPlainText>portable, untrusted x86 native code", in Proceedings of the IEEE<o:p></o:p></p><p class=MsoPlainText>Symposium on Security and Privacy, 2009.<o:p></o:p></p><p class=MsoPlainText>[4] D. Sehr, R. Muth, C. Biffle, V. Khimenko, E. Pasko, K. Schimpf, B.<o:p></o:p></p><p class=MsoPlainText>Yee, and B. Chen. Adapting software fault isolation to contemporary<o:p></o:p></p><p class=MsoPlainText>CPU architectures. In Proceedings of USENIX Security, pages 1<span style='font-family:"Arial Unicode MS","sans-serif"'>-</span>11,<o:p></o:p></p><p class=MsoPlainText>2010.<o:p></o:p></p><p class=MsoPlainText>[5] J.R. Douceur, J. Elson, J. Howell, and J.R. Lorch. Leveraging<o:p></o:p></p><p class=MsoPlainText>legacy code to deploy desktop applications on the web. In Proceedings<o:p></o:p></p><p class=MsoPlainText>of the 2008 Symposium on Operating System Design and Implementation,<o:p></o:p></p><p class=MsoPlainText>December 2008.<o:p></o:p></p><p class=MsoPlainText>[6] B.N. Bershad, S. Savage, P. Pardyak, E.G. Sirer, M.E. Fiuczynski,<o:p></o:p></p><p class=MsoPlainText>D. Becker, C. Chambers, and S. Eggers. Extensibility safety and<o:p></o:p></p><p class=MsoPlainText>performance in the SPIN operating system. In ACM SIGOPS Operating<o:p></o:p></p><p class=MsoPlainText>Systems Review, volume 29, pages 267<span style='font-family:"Arial Unicode MS","sans-serif"'>-</span>283. ACM, 1995.<o:p></o:p></p><p class=MsoPlainText>[7] G.C. Necula and P. Lee. Safe kernel extensions without run-time<o:p></o:p></p><p class=MsoPlainText>checking. In Proceedings of the Second Symposium on Operating Systems<o:p></o:p></p><p class=MsoPlainText>Design and Implementation. USENIX, 1996.<o:p></o:p></p><p class=MsoPlainText>[8] Andrew W. Appel. Foundational proof-carrying code. In Proceedings<o:p></o:p></p><p class=MsoPlainText>of the IEEE Symposium on Logic in Computer Science. IEEE Computer<o:p></o:p></p><p class=MsoPlainText>Society, 2001.<o:p></o:p></p><p class=MsoPlainText>[9] X. Leroy. A formally verified compiler back-end. Journal of<o:p></o:p></p><p class=MsoPlainText>Automated Reasoning, 43(4):363<span style='font-family:"Arial Unicode MS","sans-serif"'>-</span>446, 2009.<o:p></o:p></p><p class=MsoPlainText>[10] F.B. Schneider, G. Morrisett, and R. Harper. A Language-Based<o:p></o:p></p><p class=MsoPlainText>Approach to Security. 2000.<o:p></o:p></p><p class=MsoPlainText><o:p> </o:p></p><p class=MsoPlainText>Reading List<span style='font-family:"Arial Unicode MS","sans-serif"'>-</span>Textbooks<o:p></o:p></p><p class=MsoPlainText>[1] Ross Anderson. Security Engineering: A Guide to Building<o:p></o:p></p><p class=MsoPlainText>Dependable Distributed Systems, Second Edition. Wiley Publishing,<o:p></o:p></p><p class=MsoPlainText>Inc., 2008.<o:p></o:p></p><p class=MsoPlainText>[2] Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.<o:p></o:p></p></div></body></html>