Changes to the compartment model

[jeremyThibault]

The goal of this PR is to restore the ability to compile programs all the way from C to RISC-V assembly, which had been broken since the removal of the default compartment. Additionally, this PR removes the notion of "cross-compartment external call" entirely. This means that after merging this, every call to an external function is treated as a call within the calling compartment.

The PR achieve these goals in the following manner:

• we introduce a more general compartment model;
• we remove the compartment argument of externals and builtins;
• we modify the checks done at each level, by adding a new component to the call-states that records the calling compartment.

The new compartment model

We adopt a new generic lattice-based compartment model, and we instantiate it appropriately. The COMPTYPE module type in common/AST.v gives the interface of our compartment model:

Module Type COMPTYPE.

Parameter compartment: Type.
Parameters top bottom: compartment.
Parameter flowsto: compartment -> compartment -> Prop.
Notation "c '⊆' c'" := (flowsto c c') (no associativity, at level 95).
Notation "c '⊈' c'" := (not (flowsto c c')) (no associativity, at level 95).
Axiom flowsto_dec: forall cp cp', {cp ⊆ cp'} + {cp ⊈ cp'}.
Axiom flowsto_refl: forall cp, cp ⊆ cp.
Axiom flowsto_antisym: forall cp cp', cp ⊆ cp' -> cp' ⊆ cp -> cp = cp'.
Axiom flowsto_trans: forall cp cp' cp'', cp ⊆ cp' -> cp' ⊆ cp'' -> cp ⊆ cp''.

Lemma cp_eq_dec: forall (cp cp': compartment), {cp = cp'} + {cp <> cp'}.
  intros cp cp'.
  destruct (flowsto_dec cp cp') as [f1 | n1]; destruct (flowsto_dec cp' cp) as [f2 | n2].
  - left; eapply flowsto_antisym; eauto.
  - right; intros ?; subst cp'; contradiction.
  - right; intros ?; subst cp'; contradiction.
  - right; intros ?; subst cp'; apply n1; now eapply flowsto_refl.
Qed.

Parameter comp_to_pos: compartment -> positive.
Axiom comp_to_pos_inj: forall x y: compartment, comp_to_pos x = comp_to_pos y -> x = y.

Module COMPARTMENT_INDEXED_TYPE <: INDEXED_TYPE.
  Definition t := compartment.
  Definition index := comp_to_pos.
  Definition index_inj := comp_to_pos_inj.
  Definition eq := cp_eq_dec.
End COMPARTMENT_INDEXED_TYPE.

Module CompTree := ITree (COMPARTMENT_INDEXED_TYPE).

Axiom bottom_flowsto: forall cp, bottom ⊆ cp.
Axiom flowsto_top: forall cp, cp ⊆ top.

End COMPTYPE.

and it is instantiated in the COMP module in common/AST.v. We use the following definitions for the compartment type and the flowsto property:

Variant compartment' :=
    | bottom': compartment'
    | top': compartment'
    | Comp: ident -> compartment'
  .

  Definition compartment := compartment'.
  Definition bottom := bottom'.
  Definition top := top'.

  Variant flowsto': compartment -> compartment -> Prop :=
    | bottom_flowsto': forall cp, flowsto' bottom cp
    | flowsto_top': forall cp, flowsto' cp top
    | flowsto_refl': forall cp, flowsto' cp cp.

  Definition flowsto := flowsto'.

The intuition behind the lattice is the following: the higher in the lattice, the more privileged the compartment is. Given two compartments cp and cp', if cp ⊆ cp', then cp' has access to at least everything cp has access to. This is done by replacing most of the checks of compartment equality (in memory operations or within-compartment calls, for instance) by checks of compartment flow.

Compiler passes usually preserve compartments across languages. (i.e. they use compartment equality, not flow).

Changes to external calls

The changes to the semantics of all level w.r.t. external calls is best exemplified with Cminor.
First, callstates now record an additional element, the calling compartment:

  | Callstate:                  (**r Invocation of a function *)
      forall (f: fundef)                (**r function to invoke *)
             (args: list val)           (**r arguments provided by caller *)
             (k: cont)                  (**r what to do next  *)
             (m: mem)                   (**r memory state *)
             (cp: compartment),   (**r the compartment that lead to this [Callstate]. /!\ This is not necessary [call_comp k] *)
                                  (* this is because of tailcalls: after a tailcall, we are calling from the current comp,
                                     but [call_comp k] return the previous caller's compartment (which might be different )*)

This is because the calling compartment is not necessarily the one recorded in the continuation (for instance, in the case of tailcalls)

The relevant rules for steps of execution:

  | step_call: forall f optid sig a bl k sp e m vf vargs fd t,
      eval_expr sp e m (comp_of f) a vf ->
      eval_exprlist sp e m (comp_of f) bl vargs ->
      Genv.find_funct ge vf = Some fd ->
      funsig fd = sig ->
      (* Check that the call to the function pointer is allowed *)
      forall (ALLOWED: Genv.allowed_call ge (comp_of f) vf),
      forall (NO_CROSS_PTR: Genv.type_of_call (comp_of f) (comp_of fd) = Genv.CrossCompartmentCall -> Forall not_ptr vargs),
      forall (EV: call_trace ge (comp_of f) (comp_of fd) vf vargs (sig_args sig) t),
      step (State f (Scall optid sig a bl) k sp e m)
        t (Callstate fd vargs (Kcall optid f sp e k) m (comp_of f))

  | step_tailcall: forall f sig a bl k sp e m vf vargs fd m',
      eval_expr (Vptr sp Ptrofs.zero) e m (comp_of f) a vf ->
      eval_exprlist (Vptr sp Ptrofs.zero) e m (comp_of f) bl vargs ->
      Genv.find_funct ge vf = Some fd ->
      funsig fd = sig ->
      forall (COMP: comp_of fd = comp_of f),
      forall (SIG: sig_res (fn_sig f) = sig_res sig),
      Mem.free m sp 0 f.(fn_stackspace) (comp_of f) = Some m' ->
      step (State f (Stailcall sig a bl) k (Vptr sp Ptrofs.zero) e m)
        E0 (Callstate fd vargs (call_cont k) m' (comp_of f))

  | step_builtin: forall f optid ef bl k sp e m vargs t vres m',
      eval_exprlist sp e m (comp_of f) bl vargs ->
      external_call ef ge (comp_of f) vargs m t vres m' ->
      step (State f (Sbuiltin optid ef bl) k sp e m)
         t (State f Sskip k sp (set_optvar optid vres e) m')

…


  | step_internal_function: forall f vargs k m cp m' sp e,
      Mem.alloc m (comp_of f) 0 f.(fn_stackspace) = (m', sp) ->
      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
      step (Callstate (Internal f) vargs k m cp)
        E0 (State f f.(fn_body) k (Vptr sp Ptrofs.zero) e m')
  | step_external_function: forall ef vargs k m cp t vres m',
      external_call ef ge cp vargs m t vres m' ->
      step (Callstate (External ef) vargs k m cp)
         t (Returnstate vres k m' (sig_res (ef_sig ef)) bottom)

External functions have compartment bottom, so they are always allowed. When actually executing step, they are temporarily granted the calling compartment's privilege (this is useful to state the properties of external functions).

[jeremyThibault]

It would be great if someone was willing to look at it quickly and check that everything makes sense!