Library ProofOS.AbsInt.Bounded

Proving abstract machine safety by model checking

Require Import List TheoryList.

Require Import Asm.Util.Specif.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.ListUtil.
Require Import Asm.Util.Monad.

Require Import Asm.Bitvector.Bitvector.

Require Import ProofOS.Trusted.Safety.
Require Import ProofOS.Trusted.Machine.

Set Implicit Arguments.

Auxiliary definitions

When one abstract state subsumes another (i.e., describes at least as many concrete states)
Section subsumes.
   Variables mstate mastate mcontext : Set.
   Variable mconc : mcontext -> mstate -> mastate -> Prop.

  Definition subsumes ctx abs ctx' abs' :=
    forall st, mconc ctx st abs -> mconc ctx' st abs'.
End subsumes.

An abstraction of a concrete machine

  Declare Module Mac : MACHINE.
Concrete machine

  Parameter mastate : Set.
  Parameter print_mastate : mastate -> unit.
Abstract verification-time state

  Parameter mcontext : Set.
Additional abstract state used in proofs only

  Parameter mconc : mcontext -> Mac.mstate -> mastate -> Prop.
Relate abstract and concrete states

  Parameter maget_instr : forall (abs : mastate),
    sig_option (fun insPc : Mac.minstr * int32 =>
      forall st ctx, mconc ctx st abs
        -> insPc = Mac.mget_instr st).
Decode the instruction to be executed from a given state

  Parameter minit : {init : list (list mastate * mastate)
    | forall st, Mac.minitState st -> exists ctx, exists abs,
      In (nil, abs) init /\ mconc ctx st abs}.
A proposed fixed point, listing states with their assumed-safe first-order continuations. Every concrete initial state has an abstract counterpart.

  Definition progress (insPc : Mac.minstr * int32) (st : Mac.mstate) :=
    exists st' : Mac.mstate,
      Mac.mexec insPc st st'.
Making at least one safe step

  Definition localStep (hyps abss : list mastate)
    (ctx : mcontext) (st' : Mac.mstate) (abs' : mastate) :=
    ((In abs' abss \/ In abs' hyps) /\ mconc ctx st' abs').
Making a step within the current function

  Definition callStep (hyps abss : list mastate) (ctx : mcontext)
    (st' : Mac.mstate)
    (abs' : mastate) (ctx' : mcontext) (hyps' : list mastate) :=
    In (hyps', abs') (proj1_sig minit)
    /\ AllS (fun need => exists have,
      (In have abss \/ In have hyps)
      /\ subsumes mconc ctx' need ctx have) hyps'
    /\ mconc ctx' st' abs'.
Making a function call step

  Definition preservation (hyps : list mastate) (abs : mastate)
    (insPc : Mac.minstr * int32) (abss : list mastate)
    (st : Mac.mstate) (ctx : mcontext) :=
    forall (st' : Mac.mstate) (Hexec : Mac.mexec insPc st st'),
      exists abs', localStep hyps abss ctx st' abs'
        \/ exists ctx', exists hyps', callStep hyps abss ctx st' abs' ctx' hyps'.
Every step corresponds to accurate abstract state information

  Parameter mstep : forall hyps abs insPc, sig_option (fun abss : list mastate =>
    forall st ctx, mconc ctx st abs
      -> progress insPc st
      /\ preservation hyps abs insPc abss st ctx).
A transition function for testing the fixed point

The signature of a bounded model checker

Module Type CHECKER.
  Declare Module Mac : MACHINE.

  Parameter verify : nat ->
    pred_option (forall st, Mac.minitState st
      -> safe (cstep Mac.mexec Mac.mget_instr) st).

A functor for building a model checker from an abstraction

Module Checker (_Abs : ABSTRACTION) : CHECKER with Module Mac := _Abs.Mac.
  Import _Abs.
  Module S := Safety(_Abs.Mac).
  Import S.

  Import _Abs.Mac.

A conservative kind of safety based on returning to minit infinitely

  Inductive relatively_safe : mstate -> Prop :=
    | rsafe_step : forall st st',
      cstep st st'
      -> (forall st'', cstep st st'' -> step_safe st'')
      -> relatively_safe st

  with step_safe : mstate -> Prop :=
A local step
    | step_rel : forall st,
      relatively_safe st
      -> step_safe st
A function return or other continuation call step
    | step_fp : forall st hyps abs ctx,
      In (hyps, abs) (proj1_sig minit)
      -> mconc ctx st abs
      -> (forall hyp, In hyp hyps -> forall st', mconc ctx st' hyp -> relatively_safe st')
      -> step_safe st.

   Hint Constructors relatively_safe step_safe.

The "relativity" theorem, which says that relative safety implies

safety as long as we model-check every root state.
   Section Relativity.
     Hypothesis init_safe : forall hyps abs,
      In (hyps, abs) (proj1_sig minit)
      -> forall ctx, AllS (fun hyp => forall st, mconc ctx st hyp -> relatively_safe st) hyps
        -> forall st, mconc ctx st abs
          -> relatively_safe st.

    Theorem relativity : forall st, relatively_safe st -> safe st.
Unfortunately, I couldn't use much automation for this proof, since auto and friends don't take care to respect validity constraints on co-inductive arguments.
   End Relativity.

  Definition asafe ctx abs := forall st, mconc ctx st abs -> relatively_safe st.
Safety of an abstract state: all related concrete states are safe

Proof automation support

   Hint Unfold cstep Safety.cstep asafe.

Make use of the knowledge that the instruction decoded from the abstract state matches the instruction decoded from any related concrete state.
   Ltac rewrite_maget_instr' :=
    match goal with
      | [ ctx : mcontext,
        H : forall (st : mstate) (ctx : mcontext),
          mconc ctx st ?abs -> ?insPc = mget_instr st
          |- context[mget_instr ?mySt] ] => rewrite <- (H mySt ctx); trivial
      | [ ctx : mcontext,
        H : forall (st : mstate) (ctx : mcontext),
          mconc ctx st ?abs -> ?insPc = mget_instr st,
          H' : context[mget_instr ?mySt] |- _ ] => rewrite <- (H mySt ctx) in H'; trivial
   Ltac rewrite_maget_instr := rewrite_maget_instr'; repeat rewrite_maget_instr'.

   Hint Extern 2 (mexec _ _ _) => rewrite_maget_instr.
   Hint Extern 2 (step_safe _) => rewrite_maget_instr.

  Lemma use_asafe : forall ctx abs,
    asafe ctx abs
    -> forall st : mstate, mconc ctx st abs -> relatively_safe st.

   Hint Resolve use_asafe.

   Ltac use_AllS :=
    match goal with
      | [ H : popt_to_bool _ = true |- relatively_safe _ ] =>
        generalize (popt_to_bool_true _ H)

   Hint Extern 2 (relatively_safe _) => use_AllS.

   Ltac use_AllS_In :=
    match goal with
      | [ H1 : AllS _ _, H2 : In _ _ |- _ ] =>
        generalize (AllS_In H1 _ H2)

   Hint Extern 2 (asafe _ _) => use_AllS_In.
   Hint Extern 2 (relatively_safe _) => use_AllS_In.

   Ltac instantiate_exists :=
    match goal with
      | [ H : ex _ |- _ ] => destruct H

   Ltac intu' := intuition; repeat instantiate_exists; try use_AllS_In; try use_AllS;
    intuition (eauto 8).
   Ltac intu := do 2 intu'.

   Ltac use_preservation :=
    match goal with
      | [ H : preservation _ _ _ _ _ _, st : mstate |- _ ] =>
        generalize (H st)

   Hint Extern 2 (step_safe _) => use_preservation.

   Ltac inject_pair :=
    match goal with
      | [ H : (_, _) = (_, _) |- _ ] =>
        injection H; intros; subst; clear H

   Hint Extern 1 (asafe _ _) => inject_pair; eauto.

Model checking code

The main model checking function, following all paths up to a fixed length from an abstract state, failing if some path goes that long without returning to minit
  Definition bounded_verify : nat -> forall hyps abs,
    pred_option (forall ctx, AllS (asafe ctx) hyps -> asafe ctx abs).

Verify that every abstract state in a list is safe
  Definition verify_list : nat -> forall abss,
    pred_option (forall hyps abs, In (hyps, abs) abss
        -> forall ctx, AllS (asafe ctx) hyps
        -> asafe ctx abs).

Verify that the concrete machine is safe
  Definition verify : nat ->
    pred_option (forall st, Mac.minitState st
      -> safe st).

  Module Mac := _Abs.Mac.
End Checker.

This page has been generated by coqdoc