[talks] J Kroll general exam
mml at CS.Princeton.EDU
Fri May 6 14:38:07 EDT 2011
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.
Portable, Verifiable Low-Level Memory Safety
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
First, we present BakerSFIeld, an SFI framework [1, 2, 3] for the x64
instruction set architecture . 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 , 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
. 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.
 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.
 S. McCamant and G. Morrisett, "Evaluating SFI for a CISC
architecture", in 15th USENIX Security Symposium, 2006, pp. 209-224.
 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.
 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,
 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,
 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.
 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.
 Andrew W. Appel. Foundational proof-carrying code. In Proceedings
of the IEEE Symposium on Logic in Computer Science. IEEE Computer
 X. Leroy. A formally verified compiler back-end. Journal of
Automated Reasoning, 43(4):363-446, 2009.
 F.B. Schneider, G. Morrisett, and R. Harper. A Language-Based
Approach to Security. 2000.
 Ross Anderson. Security Engineering: A Guide to Building
Dependable Distributed Systems, Second Edition. Wiley Publishing,
 Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the talks