Coq development for "The High-Level Benefits of Low-Level Sandboxing"
This is the Coq development accompanying "The High-Level Benefits of Low-Level Sandboxing".
Prerequisites
This version is known to compile with Coq 8.9.0 and 8.9.1 but should also work with other versions supported by Iris.
Building from source
When building from source, we recommend to use opam (1.2.2 or newer) for installing the dependencies. This requires the following two repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Once you got opam set up, run make build-dep
to install the right versions
of the dependencies.
Run make -jN
to build the full development, where N
is the number of your
CPU cores.
Structure
The proofs of the main theorems can be found in the following files:
Theorem | file | name in Coq |
---|---|---|
Theorem 2 (Soundness of the sandbox) | theories/lang/adversary.v | type_adv_expr' |
Theorem 3 (Robust Safety) | theories/lang/robust_safety.v | robust_safety |
-
The main proofs are in the folder lang.
-
lang.v: Definition of the language lambda-sandbox and its operational semantics.
-
syscall_policies.v: Definition of system call policies.
-
heap.v and lifting.v: Instantiation of Iris and lifting lemmata for working with WP.
The stronger version of P-syscall mentioned in the paper is
wp_syscall
in lifting.v. -
type.v: Definition of the semantic type system, basic types like functions and products and typing rules.
It contains the following typing rules from the paper (the first column is always the name from the paper and the second column the name in this Coq development):
Rule Definition/Lemma T-val type_val T-stuck type_stuck T-let type_let T-seq type_seq T-any any T-int int T-any-copy any_copy T-int-copy int_copy T-add type_plus T-alloc type_new T-write type_write T-read-copy type_read_copy T-read type_read T-fn-copy fn_copy T-fn type_fn T-call type_fn_call T-low-ptr lowptr T-low-copy lowptr_copy T-alloc-low type_new_low T-free-low type_delete_low T-write-low type_write_low T-read-low type_read_low Note that functions in the Coq development have a privilege parameter, which is implicitly always High in the rules presented in the paper.
-
adversary.v: Proof of Theorem 2 (Soundness of the sandbox) as
type_adv_expr'
and T-gated-call astype_gated_call
. -
robust_safety.v: Proof of Theorem 3 (Robust Safety) as
robust_safety
. It also contains a comment explaining the statement of the theorem. -
wrapper.v: Definition of import and export wrappers and implementation of the wrappers for the basic types.
Wrapper Definition any.import import_any any.export export_any int.import import_int int.export export_int LowPtr.import import_lowptr LowPtr.export export_lowptr product.import import_product product.export export_product -
interface.v: Definition of
wrap_import
andwrap_export
and corresponding typing rules.Definition/Rule Definition/Lemma wrap_import wrap_import T-wrap-import type_wrap_import wrap_export wrap_export T-wrap-export type_wrap_export main_file untrusted_main / type_untrusted_main
-
-
lib contains additional libraries.
-
file.v: Definition of the file system call policy, the file related functions and the associated typing rules.
Definition/Rule Definition/Lemma fileSP fileSP A_file file_axioms I_fileSP fileSPG T-file-open type_file_open T-file-read type_file_read T-file-close type_file_close do_open do_open / type_do_open do_read do_read / type_do_read do_close do_close / type_do_close -
sum.v: Sum types and
option
.Definition Definition/Lemma option option unwrap unwrap / type_unwrap -
mutex.v: Mutex implementation.
Definition/Rule Definition/Lemma mutex mutex mutex copy mutex_copy guard mutexguard acquire acquire / type_acquire release release / type_release -
int_map.v: Integer map and associated operations.
Definition Definition/Lemma map int_map map_put int_map_put / type_int_map_put map_take int_map_take / type_int_map_take -
sealing.v: Wrappers for dynamic sealing.
Definition/Rule Definition/Lemma T-sealed sealed sealed.import / T-sealed-import import_sealed sealed.export / T-sealed-export export_sealed
-
-
The folder examples contains examples.
-
The
unsafe_print
example can be found in unsafe_print.v.Definition/Rule Definition/Lemma printSP printSP main_sandbox main T-lessthan1000 less_than_1000 T-print type_unsafe_print print print / type_print robust safety theorem print_safe -
The file system example can be found in sealing.v.
Definition/Rule Definition/Lemma robust safety theorem expose_file_safe
-
Presentational differences to the paper
-
This Coq development does not define typing contexts explicitly, but directly works with the semantic interpretation of typing contexts. This means that
v1 ◁ int, v2 ◁ int |=_p e : bool | v1 ◁ int, v2 ◁ int
is represented as
v1 ◁ int -∗ v2 ◁ int -∗ typed_expr p bool (v1 ◁ int ∗ v2 ◁ int) e
This makes working with the typing judgment a lot more pleasant since the type assignments can be manipulated with the standard Iris tactics. This also means that the T-weaken and T-copy typing rules are not explicitly formalized in this Coq development since they are implicitly provided by Iris.
-
For presentation purposes the paper glosses over some of the details of the handling of surface values. More concretely, in the paper types are defined as a function from
SurfaceVal
toiProp
to make the definition of types cleaner and easier to follow. However, such a function is very cumbersome to use in Coq as one would always need to prove that a value is a surface value to be able to state that it is well-typed. Thus, in this formalization each type is defined via a function fromVal
toiProp
with the additional requirement that each well-typed value is actually a surface value (seetype
in type.v). This means the obligation to show thatv
inv ◁ ty
is a surface value can be handled once in the typing rules forty
instead of everytimev ◁ ty
is used.
Extensions to the paper
-
This Coq development provides a mechanism to merge different system call policies (
mergeSP
andmergeSPG
in syscall_policies.v), which allows to link functions that are verfied with regard to different system call policies as long as the system call policies talk about different system calls. Seeuse_file_assert_safe
in file.v for an example. -
This Coq development includes additional typing rules like
type_case
in type.v which are not discussed in the paper.