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.