ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 11:00 - 11:30 at SUN II - Security and Incremental Computation Chair(s): Zhong Shao

Software Fault Isolation is a security-enhancing program transformation for instrumenting an untrusted binary module so that it runs inside a dedicated isolated address space, called a sandbox. To ensure that the untrusted module cannot escape its sandbox, existing approaches such as Google’s Native Client relies on a binary verifier to check that all memory accesses are within the sandbox. Instead of relying on a posteriori verification, Portable Software Fault Isolation proposes to insert a program instrumentation phase as part of a certified compiler, and leverage the soundness proof of this compiler to enforce a sandboxing security property. This eliminates the need for a binary verifier. In this paper, we describe the design, implementation and proof of an efficient, machine-checked \compcert implementation of Portable Software Fault Isolation. We propose a novel sandboxing transformation that has a well-defined C semantics and which supports arbitrary function pointers. Experiments show that our formally verified technique is a competitive way of implementing Software Fault Isolation.

Wed 10 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30: Security and Incremental ComputationESOP at SUN II
Chair(s): Zhong ShaoYale University
10:30 - 11:00
Talk
ESOP
Marco PatrignaniStanford University & CISPA Helmholtz Center for Information Security, Deepak GargMax Planck Institute for Software Systems
Link to publication
11:00 - 11:30
Talk
ESOP
Frédéric Besson, Sandrine BlazyUniv Rennes- IRISA, Alexandre Dang, Thomas P. JensenINRIA Rennes, Pierre WilkeYale University
Link to publication
11:30 - 12:00
Talk
ESOP
Ismail KuruDrexel University, Colin GordonDrexel University
Link to publication
12:00 - 12:30
Talk
ESOP
Paolo G. GiarrussoTU Delft, The Netherlands, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Philipp SchusterUniversity of Tübingen, Germany
Link to publication