# 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](theories/lang).
- [lang.v](theories/lang/lang.v): Definition of the language
lambda-sandbox and its operational semantics.
- [syscall_policies.v](theories/lang/syscall_policies.v): Definition
of system call policies.
- [heap.v](theories/lang/heap.v) and
[lifting.v](theories/lang/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](theories/lang/lifting.v).
- [type.v](theories/lang/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](theories/lang/adversary.v): Proof of Theorem 2
(Soundness of the sandbox) as `type_adv_expr'` and T-gated-call
as `type_gated_call`.
- [robust_safety.v](theories/lang/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](theories/lang/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](theories/lang/interface.v): Definition of
`wrap_import` and `wrap_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](theories/lang/lib) contains additional libraries.
- [file.v](theories/lang/lib/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](theories/lang/lib/sum.v): Sum types and `option`.
| Definition | Definition/Lemma |
|-----------------|----------------------|
| option | option |
| unwrap | unwrap / type_unwrap |
- [mutex.v](theories/lang/lib/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](theories/lang/lib/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](theories/lang/lib/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](theories/examples) contains examples.
- The `unsafe_print` example can be found in [unsafe_print.v](theories/examples/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](theories/examples/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` to `iProp` 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 from `Val` to `iProp` with the additional requirement
that each well-typed value is actually a surface value (see `type`
in [type.v](theories/lang/type.v)). This means the obligation to
show that `v` in `v ◁ ty` is a surface value can be handled once in
the typing rules for `ty` instead of everytime `v ◁ ty` is
used.
## Extensions to the paper
- This Coq development provides a mechanism to merge different system
call policies (`mergeSP` and `mergeSPG` in
[syscall_policies.v](theories/lang/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. See `use_file_assert_safe` in
[file.v](theories/examples/file.v) for an example.
- This Coq development includes additional typing rules like
`type_case` in [type.v](theories/lang/type.v) which are not
discussed in the paper.