Skip to content
Snippets Groups Projects

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 as type_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 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 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 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). 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), 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 for an example.

  • This Coq development includes additional typing rules like type_case in type.v which are not discussed in the paper.