| 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 |
Module Type ABSTRACTION.
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 |
End ABSTRACTION.
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).
End CHECKER.
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
often
|
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 impliessafety 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
end.
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)
end.
Hint Extern 2 (relatively_safe _) => use_AllS.
Ltac use_AllS_In :=
match goal with
| [ H1 : AllS _ _, H2 : In _ _ |- _ ] =>
generalize (AllS_In H1 _ H2)
end.
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
end.
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)
end.
Hint Extern 2 (step_safe _) => use_preservation.
Ltac inject_pair :=
match goal with
| [ H : (_, _) = (_, _) |- _ ] =>
injection H; intros; subst; clear H
end.
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.