header {* \isaheader{A Defensive JVM} *}
theory JVMDefensive
imports JVMExec "../Common/Conform"
begin
text {*
Extend the state space by one element indicating a type error (or
other abnormal termination) *}
datatype 'a type_error = TypeError | Normal 'a
consts is_Addr :: "val => bool"
recdef is_Addr "{}"
"is_Addr (Addr a) = True"
"is_Addr v = False"
consts is_Intg :: "val => bool"
recdef is_Intg "{}"
"is_Intg (Intg i) = True"
"is_Intg v = False"
consts is_Bool :: "val => bool"
recdef is_Bool "{}"
"is_Bool (Bool b) = True"
"is_Bool v = False"
constdefs
is_Ref :: "val => bool"
"is_Ref v ≡ v = Null ∨ is_Addr v"
consts
check_instr :: "[instr, jvm_prog, heap, val list, val list,
cname, mname, pc, frame list] => bool"
primrec
check_instr_Load:
"check_instr (Load n) P h stk loc C M0 pc frs =
(n < length loc)"
check_instr_Store:
"check_instr (Store n) P h stk loc C0 M0 pc frs =
(0 < length stk ∧ n < length loc)"
check_instr_Push:
"check_instr (Push v) P h stk loc C0 M0 pc frs =
(¬is_Addr v)"
check_instr_New:
"check_instr (New C) P h stk loc C0 M0 pc frs =
is_class P C"
check_instr_Getfield:
"check_instr (Getfield F C) P h stk loc C0 M0 pc frs =
(0 < length stk ∧ (∃C' T. P \<turnstile> C sees F:T in C') ∧
(let (C', T) = field P C F; ref = hd stk in
C' = C ∧ is_Ref ref ∧ (ref ≠ Null -->
h (the_Addr ref) ≠ None ∧
(let (D,vs) = the (h (the_Addr ref)) in
P \<turnstile> D \<preceq>* C ∧ vs (F,C) ≠ None ∧ P,h \<turnstile> the (vs (F,C)) :≤ T))))"
check_instr_Putfield:
"check_instr (Putfield F C) P h stk loc C0 M0 pc frs =
(1 < length stk ∧ (∃C' T. P \<turnstile> C sees F:T in C') ∧
(let (C', T) = field P C F; v = hd stk; ref = hd (tl stk) in
C' = C ∧ is_Ref ref ∧ (ref ≠ Null -->
h (the_Addr ref) ≠ None ∧
(let D = fst (the (h (the_Addr ref))) in
P \<turnstile> D \<preceq>* C ∧ P,h \<turnstile> v :≤ T))))"
check_instr_Checkcast:
"check_instr (Checkcast C) P h stk loc C0 M0 pc frs =
(0 < length stk ∧ is_class P C ∧ is_Ref (hd stk))"
check_instr_Invoke:
"check_instr (Invoke M n) P h stk loc C0 M0 pc frs =
(n < length stk ∧ is_Ref (stk!n) ∧
(stk!n ≠ Null -->
(let a = the_Addr (stk!n);
C = cname_of h a;
Ts = fst (snd (method P C M))
in h a ≠ None ∧ P \<turnstile> C has M ∧
P,h \<turnstile> rev (take n stk) [:≤] Ts)))"
check_instr_Return:
"check_instr Return P h stk loc C0 M0 pc frs =
(0 < length stk ∧ ((0 < length frs) -->
(P \<turnstile> C0 has M0) ∧
(let v = hd stk;
T = fst (snd (snd (method P C0 M0)))
in P,h \<turnstile> v :≤ T)))"
check_instr_Pop:
"check_instr Pop P h stk loc C0 M0 pc frs =
(0 < length stk)"
check_instr_IAdd:
"check_instr IAdd P h stk loc C0 M0 pc frs =
(1 < length stk ∧ is_Intg (hd stk) ∧ is_Intg (hd (tl stk)))"
check_instr_IfFalse:
"check_instr (IfFalse b) P h stk loc C0 M0 pc frs =
(0 < length stk ∧ is_Bool (hd stk) ∧ 0 ≤ int pc+b)"
check_instr_CmpEq:
"check_instr CmpEq P h stk loc C0 M0 pc frs =
(1 < length stk)"
check_instr_Goto:
"check_instr (Goto b) P h stk loc C0 M0 pc frs =
(0 ≤ int pc+b)"
check_instr_Throw:
"check_instr Throw P h stk loc C0 M0 pc frs =
(0 < length stk ∧ is_Ref (hd stk))"
constdefs
check :: "jvm_prog => jvm_state => bool"
"check P σ ≡ let (xcpt, h, frs) = σ in
(case frs of [] => True | (stk,loc,C,M,pc)#frs' =>
P \<turnstile> C has M ∧
(let (C',Ts,T,mxs,mxl0,ins,xt) = method P C M; i = ins!pc in
pc < size ins ∧ size stk ≤ mxs ∧
check_instr i P h stk loc C M pc frs'))"
exec_d :: "jvm_prog => jvm_state => jvm_state option type_error"
"exec_d P σ ≡ if check P σ then Normal (exec (P, σ)) else TypeError"
inductive_set
exec_1_d :: "jvm_prog => (jvm_state type_error × jvm_state type_error) set"
and exec_1_d' :: "jvm_prog => jvm_state type_error => jvm_state type_error => bool"
("_ \<turnstile> _ -jvmd->1 _" [61,61,61]60)
for P :: jvm_prog
where
"P \<turnstile> σ -jvmd->1 σ' ≡ (σ,σ') ∈ exec_1_d P"
| exec_1_d_ErrorI: "exec_d P σ = TypeError ==> P \<turnstile> Normal σ -jvmd->1 TypeError"
| exec_1_d_NormalI: "exec_d P σ = Normal (Some σ') ==> P \<turnstile> Normal σ -jvmd->1 Normal σ'"
-- "reflexive transitive closure:"
consts
"exec_all_d" :: "jvm_prog => jvm_state type_error => jvm_state type_error => bool"
("_ |- _ -jvmd-> _" [61,61,61]60)
syntax (xsymbols)
"exec_all_d" :: "jvm_prog => jvm_state type_error => jvm_state type_error => bool"
("_ \<turnstile> _ -jvmd-> _" [61,61,61]60)
defs
exec_all_d_def1: "P \<turnstile> σ -jvmd-> σ' ≡ (σ,σ') ∈ (exec_1_d P)*"
lemma exec_1_d_eq:
"exec_1_d P = {(s,t). ∃σ. s = Normal σ ∧ t = TypeError ∧ exec_d P σ = TypeError} ∪
{(s,t). ∃σ σ'. s = Normal σ ∧ t = Normal σ' ∧ exec_d P σ = Normal (Some σ')}"
by (auto elim!: exec_1_d.cases intro!: exec_1_d.intros)
declare split_paired_All [simp del]
declare split_paired_Ex [simp del]
lemma if_neq [dest!]:
"(if P then A else B) ≠ B ==> P"
by (cases P, auto)
lemma exec_d_no_errorI [intro]:
"check P σ ==> exec_d P σ ≠ TypeError"
by (unfold exec_d_def) simp
theorem no_type_error_commutes:
"exec_d P σ ≠ TypeError ==> exec_d P σ = Normal (exec (P, σ))"
by (unfold exec_d_def, auto)
lemma defensive_imp_aggressive:
"P \<turnstile> (Normal σ) -jvmd-> (Normal σ') ==> P \<turnstile> σ -jvm-> σ'"
proof -
have "!!x y. P \<turnstile> x -jvmd-> y ==> ∀σ σ'. x = Normal σ --> y = Normal σ' --> P \<turnstile> σ -jvm-> σ'"
apply (unfold exec_all_d_def1)
apply (erule rtrancl_induct)
apply (simp add: exec_all_def)
apply (fold exec_all_d_def1)
apply simp
apply (intro allI impI)
apply (erule exec_1_d.cases, simp)
apply (simp add: exec_all_def exec_d_def split: type_error.splits split_if_asm)
apply (rule rtrancl_trans, assumption)
apply blast
done
moreover
assume "P \<turnstile> (Normal σ) -jvmd-> (Normal σ')"
ultimately
show "P \<turnstile> σ -jvm-> σ'" by blast
qed
end