| Building abstractions from word-level type systems |
Require Import Arith List TheoryList.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.ListUtil.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Monad.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.X86.
Require Import ProofOS.Trusted.Safety.
Require Import ProofOS.Trusted.Machine.
Require Import ProofOS.Trusted.Arches.
Require Import ProofOS.AbsInt.Bounded.
Require Import ProofOS.AbsInt.Sal.
Require Import ProofOS.AbsInt.FixedCode.
Set Implicit Arguments.
Inductive apc : Set :=
| ApcConst : int32 -> apc
| ApcUnknown.
Section stateDescription.
Variables ty mastate mcontext : Set.
Variable hasTy : mcontext -> int32 -> ty -> Prop.
Variable mconc : mcontext -> salState -> mastate -> Prop.
Record stateDescription : Set := {
sdPc : apc;
sdRegs : SalRegMap.t ty;
sdCust : mastate
}.
Parameter print_stateDescription : (ty -> unit) -> (mastate -> unit)
-> apc -> ty -> ((salReg * ty -> unit) -> unit) -> mastate -> unit.
Definition pcOk pc st :=
match pc with
| ApcUnknown => True
| ApcConst pc => pc = SstPc st
end.
Record typeMconc (ctx : mcontext) (st : salState) (abs : stateDescription) : Prop := {
mcPc : pcOk (sdPc abs) st;
mcRegs : forall r, hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs abs));
mcCust : mconc ctx st (sdCust abs)
}.
End stateDescription.
Module Make (Param : M86_PARAM_FIXED_CODE).
Module Fixed := FixedCode.Make(Param).
Import Fixed.
Import MySal.
Section viewShift.
Variables ty mastate : Set.
| Describe how to change perspective at a jump |
Record viewShift : Set := {
vsSuccs : list (stateDescription ty mastate);
| Additional states to queue for visitation |
vsHyps : list (stateDescription ty mastate);
| Continuation hypotheses known to be covered by the successors and the current hypotheses together |
vsAbs : stateDescription ty mastate
| Main abstract state to switch to |
}.
End viewShift.
Definition of a type system |
Module Type TYPE_SYSTEM.
Parameter ty : Set.
Parameter print_ty : ty -> unit.
| A language of types describing machine words |
Parameter mastate : Set.
Parameter print_mastate : mastate -> unit.
| Custom abstract state information |
Parameter mcontext : Set.
| A summary of aspects of a machine state that don't need to be represented explicitly at verification time, but are important in soundness proofs |
Parameter mconc : mcontext -> M.mstate -> mastate -> Prop.
| Concretization relation |
Parameter subMastate : forall (abs1 abs2 : mastate),
pred_option (forall ctx st,
mconc ctx st abs1 -> mconc ctx st abs2).
| A way to check compatibility of abstract states |
Parameter hasTy : mcontext -> int32 -> ty -> Prop.
| What it means for a word to be of a type |
Parameter tyTop : ty.
Axiom tyTopSound : forall ctx v, hasTy ctx v tyTop.
Parameter tyConst : int32 -> ty.
Axiom tyConstSound1 : forall ctx v, hasTy ctx v (tyConst v).
Axiom tyConstSound2 : forall ctx v1 v2, hasTy ctx v1 (tyConst v2) -> v1 = v2.
Parameter isTyConst : forall (t : ty), sig_option (fun n => t = tyConst n).
Parameter subTy : forall (t1 t2 : ty),
pred_option (forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2).
| A way to check compatibility of types |
Parameter typeof : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
{t : ty
| forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> hasTy ctx (evalExp st e) t}.
| A type inference procedure for SAL expressions |
Parameter typeofLoad : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
{t : ty
| forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> hasTy ctx (get_mem32 st (evalExp st e)) t}.
| Type inference for memory loads |
Parameter checkStore : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
pred_option (forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> apartFromCode (evalExp st e)
/\ not_too_high (evalExp st e)).
| Type inference for memory loads |
Parameter effectOfCmd : forall (abs : mastate) (rs : SalRegMap.t ty) (cmd : salCmd),
sig_option (fun abs' => forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> mconc ctx (salExecCmd st cmd) abs').
| Update the custom state to reflect the result of a command. |
Parameter effectOfJump : forall (abs : mastate) (rs : SalRegMap.t ty)
(jmp : salJump) (nextPc : int32),
sig_option (fun abs' => forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> match salExecJmp jmp nextPc st with
| None => False
| Some st' => mconc ctx st' abs'
end).
| Update the custom state to reflect the result of a jump. |
Parameter effectOfConditionalJump : forall (abs : stateDescription ty mastate)
(co : cc) (pc nextPc : int32) (b : bool),
sig_option (fun abs' => forall ctx st,
typeMconc hasTy mconc ctx st abs
-> check_cc st co = b
-> match salExecJmp (SConditionalJump co pc) nextPc st with
| None => False
| Some st' => typeMconc hasTy mconc ctx st' abs'
end).
Specialized version of effectOfJump that allows different states in
different cases of a conditional jump test
|
Parameter viewShiftOfJump : forall (hyps : list (stateDescription ty mastate))
(abs : stateDescription ty mastate)
(jmp : salJump) (nextPc : int32),
sig_option (fun vs => forall ctx st,
typeMconc hasTy mconc ctx st abs
-> exists ctx', typeMconc hasTy mconc ctx' st (vsAbs vs)
/\ AllS (fun need => exists have, (In have (vsSuccs vs) \/ In have hyps)
/\ subsumes (typeMconc hasTy mconc) ctx' need ctx have) (vsHyps vs)).
| Massage the form of an abstract state to match what a jump target expects; for instance, at a function call. |
End TYPE_SYSTEM.
Instantiation of a type system to a particular verification problem |
Module Type USE_TYPE_SYSTEM.
Declare Module Sys : TYPE_SYSTEM.
Parameter minit : {init : list (list (stateDescription Sys.ty Sys.mastate)
* stateDescription Sys.ty Sys.mastate)
| (AllS (fun sd => match sdPc (snd sd) with
| ApcUnknown => False
| ApcConst pc => validPc pc
end) init)
/\ forall st, M.minitState st -> exists ctx, exists sd,
In (nil, sd) init
/\ ApcConst (SstPc st) = sdPc sd
/\ (forall r, Sys.hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs sd)))
/\ Sys.mconc ctx st (sdCust sd)}.
| An initial set of states, given by program counter and register types |
End USE_TYPE_SYSTEM.
Module Abstraction (Use : USE_TYPE_SYSTEM) : FIXED_CODE_ABSTRACTION with Module Mac := M.
Import Use.
Module Mac := M.
Import Sys.
Definition mastate := stateDescription ty mastate.
Definition print_mastate abs :=
let (default, elems) := SalRegMap.elements (sdRegs abs) in
print_stateDescription print_ty print_mastate
(sdPc abs)
default
(fun f => iter f elems)
(sdCust abs).
Definition mcontext := mcontext.
Definition mconc := typeMconc hasTy mconc.
Hint Unfold mconc.
Hint Constructors typeMconc.
Hint Unfold pcOk.
Definition apc_eq_dec : forall (pc1 pc2 : apc), {pc1 = pc2} + {pc1 <> pc2}.
Definition subMastate : forall (abs1 abs2 : mastate),
pred_option (forall ctx st,
mconc ctx st abs1 -> mconc ctx st abs2).
Definition maPc' : forall (abs : mastate), sig_option (fun pc =>
sdPc abs = ApcConst pc /\ forall ctx st, mconc ctx st abs -> SstPc st = pc).
Definition maPc : forall (abs : mastate), sig_option (fun pc =>
forall ctx st, mconc ctx st abs -> SstPc st = pc).
Definition absValidPc' (abs : mastate) :=
match maPc' abs with
| SNone => True
| SSome pc _ => validPc pc
end.
Definition absValidPc abs :=
match maPc abs with
| SNone => True
| SSome pc _ => validPc pc
end.
Lemma absValidPc_imp : forall abs, absValidPc' abs -> absValidPc abs.
Definition minit : {init : list (list mastate * mastate)
| (forall abs hyps, In (hyps, abs) init -> absValidPc abs)
/\ forall st, Mac.minitState st -> exists ctx, exists abs,
In (nil, abs) init /\ mconc ctx st abs}.
We build up a fast look-up structure to find preconditions of codeaddresses represented inminit.
|
Definition pcToAbs_map' (states : list (list mastate * mastate)) m :=
fold_left (fun m abs =>
match sdPc (snd abs) with
| ApcUnknown => m
| ApcConst pc => Int32Map.set pc (Some abs) m
end) states m.
Definition pcToAbs_map := pcToAbs_map' (proj1_sig minit) (Int32Map.init None).
Lemma pcToAbs_map'_sound : forall init states m,
incl states init
-> (forall r ha, Int32Map.get r m = Some ha -> In ha init)
-> (forall r ha, Int32Map.get r (pcToAbs_map' states m) = Some ha -> In ha init).
Definition pcToAbs : forall (pc : int32), sig_option (fun hypsAbs =>
In hypsAbs (proj1_sig minit)).
Definition progress (insPc : Mac.minstr * int32) (st : Mac.mstate) :=
instructionOk st (fst insPc)
/\ exists st' : Mac.mstate,
Mac.mexec insPc st st'.
Definition localStep (hyps abss : list mastate)
(ctx : mcontext) (st' : Mac.mstate) (abs' : mastate) :=
((In abs' abss \/ In abs' hyps) /\ mconc ctx st' abs').
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'.
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'.
Lemma execCmd_pc : forall st cmd,
SstPc (salExecCmd st cmd) = SstPc st.
Hint Rewrite SalRegMap.gss : Maps.
Hint Rewrite SalRegMap.gso using (trivial; fail) : Maps.
Definition checkCmd : forall abs cmd, sig_option (fun abs' =>
forall ctx st, mconc ctx st abs
-> mconc ctx (salExecCmd st cmd) abs'
/\ cmdOk st cmd).
Definition checkCmds : forall abs cmds, sig_option (fun abs' =>
forall ctx st, mconc ctx st abs
-> mconc ctx (fold_left salExecCmd cmds st) abs'
/\ cmdsOk st cmds).
Definition hypCovered : forall (hyp : mastate) (hyps : list mastate),
pred_option (exists have, In have hyps
/\ forall st ctx, mconc ctx st hyp
-> mconc ctx st have).
Definition subHyps : forall (hyps1 hyps2 : list mastate),
pred_option (AllS (fun need => exists have, In have hyps1
/\ forall st ctx, mconc ctx st need
-> mconc ctx st have) hyps2).
Definition checkJump : forall hyps abs (jmp : salJump) (nextPc : int32),
sig_option (fun succs =>
(exists abs', (In abs' hyps /\ forall ctx st, mconc ctx st abs -> mconc ctx st abs')
\/ exists hyps', In (hyps', abs') (proj1_sig minit)
/\ forall ctx st, mconc ctx st abs
-> exists ctx', mconc ctx' st abs'
/\ AllS (fun need => exists have,
(In have succs \/ In have hyps)
/\ subsumes mconc ctx' need ctx have) hyps')).
Lemma progress_fallthru : forall x86 cmds nextPc st ctx abs abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> mconc ctx st abs
-> progress (x86, (cmds, SFallthru), nextPc) st.
Hint Resolve progress_fallthru.
Lemma preservation_fallthru_covered : forall ctx st abs succs x86 cmds nextPc hyps cust abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> (exists abs'0 : mastate,
(In abs'0 hyps /\ forall ctx st, mconc ctx st
(Build_stateDescription (ApcConst nextPc) (sdRegs abs') cust)
-> mconc ctx st abs'0)
\/ (exists hyps' : list mastate,
In (hyps', abs'0) (proj1_sig minit) /\
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st
(Build_stateDescription (ApcConst nextPc) (sdRegs abs') cust) ->
exists ctx' : mcontext,
mconc ctx' st abs'0 /\
AllS
(fun need : mastate =>
exists have : mastate,
(In have succs \/ In have hyps) /\
subsumes mconc ctx' need ctx have) hyps')))
-> (forall (ctx : Sys.mcontext) (st : Mac.mstate),
Sys.mconc ctx st (sdCust abs') ->
(forall r : SalRegIndexed.t,
hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs abs'))) ->
Sys.mconc ctx (set_pc st nextPc) cust)
-> mconc ctx st abs
-> preservation hyps abs (x86, (cmds, SFallthru), nextPc) succs st ctx.
Hint Resolve preservation_fallthru_covered.
Lemma preservation_fallthru : forall ctx st cust abs' nextPc x86 cmds abs hyps,
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> (forall (ctx : Sys.mcontext) (st : Mac.mstate),
Sys.mconc ctx st (sdCust abs') ->
(forall r : SalRegIndexed.t,
hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs abs'))) ->
Sys.mconc ctx (set_pc st nextPc) cust)
-> mconc ctx st abs
-> preservation hyps abs (x86, (cmds, SFallthru), nextPc)
(cons (Build_stateDescription (ApcConst nextPc) (sdRegs abs') cust) nil) st ctx.
Hint Resolve preservation_fallthru.
Lemma progress_jump : forall x86 cmds nextPc st ctx abs pc abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> mconc ctx st abs
-> progress (x86, (cmds, SJump pc), nextPc) st.
Hint Resolve progress_jump.
Lemma preservation_jump_covered : forall pc ctx st abs succs x86 cmds nextPc hyps cust abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> (exists abs'0 : mastate,
(In abs'0 hyps /\ forall ctx st, mconc ctx st
(Build_stateDescription (ApcConst pc) (sdRegs abs') cust)
-> mconc ctx st abs'0)
\/ (exists hyps' : list mastate,
In (hyps', abs'0) (proj1_sig minit) /\
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st
(Build_stateDescription (ApcConst pc) (sdRegs abs') cust) ->
exists ctx' : mcontext,
mconc ctx' st abs'0 /\
AllS
(fun need : mastate =>
exists have : mastate,
(In have succs \/ In have hyps) /\
subsumes mconc ctx' need ctx have) hyps')))
-> (forall (ctx : Sys.mcontext) (st : Mac.mstate),
Sys.mconc ctx st (sdCust abs') ->
(forall r : SalRegIndexed.t,
hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs abs'))) ->
Sys.mconc ctx (set_pc st pc) cust)
-> mconc ctx st abs
-> preservation hyps abs (x86, (cmds, SJump pc), nextPc) succs st ctx.
Hint Resolve preservation_jump_covered.
Lemma progress_call : forall x86 cmds nextPc st ctx abs pc abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> mconc ctx st abs
-> progress (x86, (cmds, SIndirectJump SCall (SConst pc)), nextPc) st.
Hint Resolve progress_call.
Lemma preservation_call_covered : forall pc ctx st abs succs x86 cmds nextPc hyps cust abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> (exists abs'0 : mastate,
(In abs'0 hyps /\ forall ctx st, mconc ctx st
(Build_stateDescription (ApcConst pc) (sdRegs abs') cust)
-> mconc ctx st abs'0)
\/ (exists hyps' : list mastate,
In (hyps', abs'0) (proj1_sig minit) /\
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st
(Build_stateDescription (ApcConst pc) (sdRegs abs') cust) ->
exists ctx' : mcontext,
mconc ctx' st abs'0 /\
AllS
(fun need : mastate =>
exists have : mastate,
(In have succs \/ In have hyps) /\
subsumes mconc ctx' need ctx have) hyps')))
-> (forall (ctx : Sys.mcontext) (st : Mac.mstate),
Sys.mconc ctx st (sdCust abs') ->
(forall r : SalRegIndexed.t,
hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs abs'))) ->
Sys.mconc ctx (set_pc st pc) cust)
-> mconc ctx st abs
-> preservation hyps abs (x86, (cmds, SIndirectJump SCall (SConst pc)), nextPc) succs st ctx.
Hint Resolve preservation_call_covered.
Lemma progress_ret : forall x86 cmds nextPc st ctx abs e abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> mconc ctx st abs
-> progress (x86, (cmds, SIndirectJump SRet e), nextPc) st.
Hint Resolve progress_ret.
Lemma preservation_ret_covered : forall e ctx st abs succs x86 cmds nextPc hyps cust abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> (exists abs'0 : mastate,
(In abs'0 hyps /\ forall ctx st, mconc ctx st
(Build_stateDescription ApcUnknown (sdRegs abs') cust)
-> mconc ctx st abs'0)
\/ (exists hyps' : list mastate,
In (hyps', abs'0) (proj1_sig minit) /\
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st
(Build_stateDescription ApcUnknown (sdRegs abs') cust) ->
exists ctx' : mcontext,
mconc ctx' st abs'0 /\
AllS
(fun need : mastate =>
exists have : mastate,
(In have succs \/ In have hyps) /\
subsumes mconc ctx' need ctx have) hyps')))
-> (forall (ctx : Sys.mcontext) (st : Mac.mstate),
Sys.mconc ctx st (sdCust abs') ->
(forall r : SalRegIndexed.t,
hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs abs'))) ->
Sys.mconc ctx (set_pc st (evalExp st e)) cust)
-> mconc ctx st abs
-> preservation hyps abs (x86, (cmds, SIndirectJump SRet e), nextPc) succs st ctx.
Hint Resolve preservation_ret_covered.
Lemma progress_conditional : forall co pc x86 cmds nextPc st ctx abs abs',
(forall (ctx : mcontext) (st : Mac.mstate),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> mconc ctx st abs
-> progress (x86, (cmds, SConditionalJump co pc), nextPc) st.
Hint Resolve progress_conditional.
Lemma preservation_conditional_covered : forall ctx st custFalse custTrue succs abs' pc co
x86 cmds nextPc abs hyps,
(forall (ctx : Sys.mcontext) (st : salState),
mconc ctx st abs ->
mconc ctx (fold_left salExecCmd cmds st) abs' /\ cmdsOk st cmds)
-> (forall (ctx : Sys.mcontext) (st : Mac.mstate),
typeMconc hasTy Sys.mconc ctx st abs' ->
check_cc st co = true ->
typeMconc hasTy Sys.mconc ctx
(if check_cc st co then set_pc st pc else set_pc st nextPc)
custTrue)
-> (forall (ctx : Sys.mcontext) (st : Mac.mstate),
typeMconc hasTy Sys.mconc ctx st abs' ->
check_cc st co = false ->
typeMconc hasTy Sys.mconc ctx
(if check_cc st co then set_pc st pc else set_pc st nextPc)
custFalse)
-> (exists abs'0 : stateDescription ty Sys.mastate,
In abs'0 hyps /\
(forall (ctx : Sys.mcontext) (st : salState),
mconc ctx st custTrue ->
mconc ctx st abs'0) \/
(exists hyps' : list mastate,
In (hyps', abs'0) (proj1_sig minit) /\
(forall (ctx : Sys.mcontext) (st : salState),
mconc ctx st
custTrue ->
exists ctx' : Sys.mcontext,
mconc ctx' st abs'0 /\
AllS
(fun need : stateDescription ty Sys.mastate =>
exists have : stateDescription ty Sys.mastate,
(In have succs \/ In have hyps) /\
subsumes mconc ctx' need ctx have) hyps')))
-> mconc ctx st abs
-> preservation hyps abs (x86, (cmds, SConditionalJump co pc), nextPc)
(cons custFalse succs)
st ctx.
Hint Resolve preservation_conditional_covered.
Definition 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).
End Abstraction.
End Make.