Name
Abstract | ||
|---|---|---|
Software Fault Isolation (SFI) 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 rely on a binary verifier to check that all memory accesses are within the sandbox. Instead of relying on a posteriori verification, we design, implement and prove correct a program instrumentation phase as part of the formally verified compiler CompCert that enforces a sandboxing security property a priori. This eliminates the need for a binary verifier and, instead, leverages the soundness proof of the compiler to prove the security of the sandboxing transformation. The technical contributions are a novel sandboxing transformation that has a well-defined C semantics and which supports arbitrary function pointers, and a formally verified C compiler that implements SFI. Experiments show that our formally verified technique is a competitive way of implementing SFI. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1007/978-3-030-17184-1_18 | ESOP |
Field | DocType | Citations |
Address space,Sandbox (computer security),Function pointer,Programming language,Program transformation,Computer science,A priori and a posteriori,Compiler,Soundness,Semantics | Conference | 1 |
PageRank | References | Authors |
0.35 | 0 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frédéric Besson | 1 | 213 | 16.86 |
| S. Blazy | 2 | 36 | 6.66 |
| Alexandre Dang | 3 | 1 | 0.69 |
| Thomas P. Jensen | 4 | 632 | 68.50 |
| Pierre Wilke | 5 | 10 | 2.61 |