Commit 617591b3 authored by Michael Sammler's avatar Michael Sammler

Added documentation of fileSP

parent 6b43b5a5
......@@ -3,8 +3,13 @@ From sandbox.lang.lib Require Import file assert sealing product.
Definition seal_name : namespace := nroot .@ "file".
Section sealing.
(** sandboxG collects the necessary type classes to work with the
ghost state we need. fileG contains the type classes for the file
ghost state. inSP Σ fileSPG states that the system call policy
fileSPG is part of the global system call policy. *)
Context `{sandboxG Σ} `{fileG Σ} `{inSP Σ fileSPG}.
(** Since [sealed s ty] is equivalent to [ty] we can directly use [type_do_open]. *)
Lemma type_do_open_sealed : do_open fn High [# int] (sealed seal_name file).
Proof. iApply type_do_open. Qed.
Lemma type_do_read_sealed : do_read fn High [# (sealed seal_name file)] (product [sealed seal_name file; any]).
......@@ -12,16 +17,17 @@ Section sealing.
Lemma type_do_close_sealed : do_close fn High [# (sealed seal_name file)] any.
Proof. iApply type_do_close. Qed.
(** This defines the wrapped version of the file functions. *)
Definition do_open_export : val := wrap_export do_open [# int] (sealed seal_name file).
Definition do_read_export : val := wrap_export do_read [# (sealed seal_name file)] (product [sealed seal_name file; any]).
Definition do_close_export : val := wrap_export do_close [# (sealed seal_name file)] any.
(* we now have the wrapped functions but we cannot use them directly
in expose_file_safe as they depend on sandboxG, which is not
available where we want to use these functions in expose_file_safe.
So we need this hack of defining do_open_export_val which is the
same as do_open_export as do_open_export_val_eq shows, but it does
not depend on sandboxG. *)
(** We now have the wrapped functions but we cannot use them
directly in expose_file_safe as they depend on sandboxG, which is
not available where we want to use these functions in
expose_file_safe. So we need this hack of defining
do_open_export_val which is the same as do_open_export as
do_open_export_val_eq shows, but it does not depend on sandboxG. *)
Local Transparent wrap_import wrap_export import_const_int import_int export_lowptr export_int import_any export_product import_product export_any export_sealed import_sealed.
Definition do_open_export_val : val.
Proof using.
......@@ -48,6 +54,8 @@ Section sealing.
Proof. by apply: recv_f_equal. Qed.
End sealing.
(** The interface contains the untrusted code [u] in the Low interface
and the wrapped file functions in the High interface. *)
Definition interface (u : interface_map) := λ p, match p with
| Low => u
| High =>
......@@ -56,10 +64,17 @@ Definition interface (u : interface_map) := λ p, match p with
<[ nroot.@ "close" := do_close_export_val]>
end.
Lemma expose_file_safe u t2 σ2 :
(** The main theorem of this example, which shows that it is safe to
expose the wrapped file functions to arbitrary untrusted code. *)
Theorem expose_file_safe u t2 σ2 :
(** We assume the kernel respects file_axioms. *)
let _ := SyscallG file_axioms in
(** For all untrusted code, represented as arbitrary surface values, *)
map_Forall (λ _ v, surface_val v) u
(** Each state [σ2] which is reachable from the heap with the global
variable [seal_name] initialized to an empty map and the interface [interface u]*)
rtc erased_step ([(untrusted_main_val [] at High)%E], initial_state (<[seal_name := cmap_global_init ]> ) (interface u)) (t2, σ2)
(** fulfills the fileSP system call policy. *)
is_good fileSP σ2.
Proof.
set Σ : gFunctors := #[sandboxΣ; fileΣ]. move=>??.
......
......@@ -6,18 +6,28 @@ From sandbox.lang Require Import heap proofmode type.
From sandbox.lang.lib Require Import product.
(* Set Default Proof Using "Type". *)
(** This is the fileSP system call policy, which enforces that only
open file handles can be read or closed. *)
Definition fileSP : syscall_policy := {|
(** The state of this syscall policy is the set of open file handles. *)
sp_state := gset Z;
(** In the beginning, all file handles are closed. *)
sp_initial_state := ;
sp_transitions :=
(** open adds the file handle to the set of open file handles. *)
<["open" := λ v r s, t lit_to_Z r; Some ({[ t ]} s) ]> $
(** read checks that the file is currently open and leaves the
file handle in the set of open file handles. *)
<["read" := λ v' r s, v lit_to_Z v';
if bool_decide (v s) then Some s else None ]> $
(** close checks that the file is currently open and removes the
file handle from the set of open file handles. *)
<["close" := λ v' r s, v lit_to_Z v';
if bool_decide (v s) then Some (s {[ v ]} ) else None ]>
|}.
(** Registering the necessary ghost state. *)
Class fileG Σ := FileG {
file_inG :> inG Σ (authR (gset_disjUR Z));
}.
......@@ -26,17 +36,42 @@ Definition fileΣ : gFunctors :=
Instance subG_fileG {Σ} : subG fileΣ Σ fileG Σ.
Proof. solve_inG. Qed.
(** These are the axioms which the kernel is assumed to fulfill when
working with files (A_file from the paper). *)
Definition file_axioms (π : list observation) : Prop :=
(** open only returns integers. Remember that π consists of
observations, which are tuples of the form (system call name (here
"open"), argument to the system call (here [f]), return value of the
system call (here [r])). *)
( i f r, π !! i = Some ("open", f, r) is_Some (lit_to_Z r))
(** Two distinct calls to open (distinct means different indicies
in the trace) return different file handles. *)
( i1 i2 f1 f2 r1 r2, π !! i1 = Some ("open", f1, r1) π !! i2 = Some ("open", f2, r2)
i1 i2 r1 r2).
(** fileSPG is the file system call policy extended with the necessary
invariant for working with it in the logic. *)
Program Definition fileSPG `{sandboxSPPreG Σ} `{fileG Σ} : syscall_policyG Σ := {|
(** fileSPG extends fileSP *)
spg_SP := fileSP;
(** fileSPG needs a gname for the file token ghost state. *)
spg_name := gname;
spg_prop := λ γ sps, (own γ ( GSet sps) idxs,
([ list] iidxs, o, in_trace i o)
([ set] tsps, i v, iidxs in_trace i ("open", v, LitInt t)))%I;
(** invariant of fileSPG *)
spg_prop := λ γ sps,
(** Link the state of the system call policy to the ghost state
available in the logic via the authorative construction. *)
(own γ ( GSet sps)
(** There exists a set of indices *)
idxs,
(** which all have occured in the trace (this is necessary
to show that a new observation will have a greater index
than all indices in idxs). *)
([ list] iidxs, o, in_trace i o)
(** and all currently open file handles have been opened at
an index in idxs. Together with file_axioms this allows to
see that a file handle returned by open is not in sps. *)
([ set] tsps, i v, iidxs in_trace i ("open", v, LitInt t)))%I;
(** fileSPG uses the file_axioms *)
spg_axioms := file_axioms;
|}.
Next Obligation.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment