Theory NonInterferenceInter
section ‹HRB Slicing guarantees IFC Noninterference›
theory NonInterferenceInter
imports "HRB-Slicing.FundamentalProperty"
begin
subsection ‹Assumptions of this Approach›
text ‹
Classical IFC noninterference, a special case of a noninterference
definition using partial equivalence relations (per)
\<^cite>‹"SabelfeldS:01"›, partitions the variables (i.e.\ locations) into
security levels. Usually, only levels for secret or high, written
‹H›, and public or low, written ‹L›, variables are
used. Basically, a program that is noninterferent has to fulfil one
basic property: executing the program in two different initial states
that may differ in the values of their ‹H›-variables yields two
final states that again only differ in the values of their
‹H›-variables; thus the values of the ‹H›-variables did not
influence those of the ‹L›-variables.
Every per-based approach makes certain
assumptions: (i) all \mbox{‹H›-variables} are defined at the
beginning of the program, (ii) all ‹L›-variables are observed (or
used in our terms) at the end and (iii) every variable is either
‹H› or ‹L›. This security label is fixed for a variable
and can not be altered during a program run. Thus, we have to extend
the prerequisites of the slicing framework in \<^cite>‹"Wasserrab:09"› accordingly
in a new locale:
›
locale NonInterferenceInterGraph =
SDG sourcenode targetnode kind valid_edge Entry
get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind"
and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and get_proc :: "'node ⇒ 'pname"
and get_return_edges :: "'edge ⇒ 'edge set"
and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
and Exit::"'node" ("'('_Exit'_')")
and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
and ParamDefs :: "'node ⇒ 'var list" and ParamUses :: "'node ⇒ 'var set list" +
fixes H :: "'var set"
fixes L :: "'var set"
fixes High :: "'node" ("'('_High'_')")
fixes Low :: "'node" ("'('_Low'_')")
assumes Entry_edge_Exit_or_High:
"⟦valid_edge a; sourcenode a = (_Entry_)⟧
⟹ targetnode a = (_Exit_) ∨ targetnode a = (_High_)"
and High_target_Entry_edge:
"∃a. valid_edge a ∧ sourcenode a = (_Entry_) ∧ targetnode a = (_High_) ∧
kind a = (λs. True)⇩√"
and Entry_predecessor_of_High:
"⟦valid_edge a; targetnode a = (_High_)⟧ ⟹ sourcenode a = (_Entry_)"
and Exit_edge_Entry_or_Low: "⟦valid_edge a; targetnode a = (_Exit_)⟧
⟹ sourcenode a = (_Entry_) ∨ sourcenode a = (_Low_)"
and Low_source_Exit_edge:
"∃a. valid_edge a ∧ sourcenode a = (_Low_) ∧ targetnode a = (_Exit_) ∧
kind a = (λs. True)⇩√"
and Exit_successor_of_Low:
"⟦valid_edge a; sourcenode a = (_Low_)⟧ ⟹ targetnode a = (_Exit_)"
and DefHigh: "Def (_High_) = H"
and UseHigh: "Use (_High_) = H"
and UseLow: "Use (_Low_) = L"
and HighLowDistinct: "H ∩ L = {}"
and HighLowUNIV: "H ∪ L = UNIV"
begin
lemma Low_neq_Exit: assumes "L ≠ {}" shows "(_Low_) ≠ (_Exit_)"
proof
assume "(_Low_) = (_Exit_)"
have "Use (_Exit_) = {}" by fastforce
with UseLow ‹L ≠ {}› ‹(_Low_) = (_Exit_)› show False by simp
qed
lemma valid_node_High [simp]:"valid_node (_High_)"
using High_target_Entry_edge by fastforce
lemma valid_node_Low [simp]:"valid_node (_Low_)"
using Low_source_Exit_edge by fastforce
lemma get_proc_Low:
"get_proc (_Low_) = Main"
proof -
from Low_source_Exit_edge obtain a where "valid_edge a"
and "sourcenode a = (_Low_)" and "targetnode a = (_Exit_)"
and "intra_kind (kind a)" by(fastforce simp:intra_kind_def)
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
with ‹sourcenode a = (_Low_)› ‹targetnode a = (_Exit_)› get_proc_Exit
show ?thesis by simp
qed
lemma get_proc_High:
"get_proc (_High_) = Main"
proof -
from High_target_Entry_edge obtain a where "valid_edge a"
and "sourcenode a = (_Entry_)" and "targetnode a = (_High_)"
and "intra_kind (kind a)" by(fastforce simp:intra_kind_def)
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
with ‹sourcenode a = (_Entry_)› ‹targetnode a = (_High_)› get_proc_Entry
show ?thesis by simp
qed
lemma Entry_path_High_path:
assumes "(_Entry_) -as→* n" and "inner_node n"
obtains a' as' where "as = a'#as'" and "(_High_) -as'→* n"
and "kind a' = (λs. True)⇩√"
proof(atomize_elim)
from ‹(_Entry_) -as→* n› ‹inner_node n›
show "∃a' as'. as = a'#as' ∧ (_High_) -as'→* n ∧ kind a' = (λs. True)⇩√"
proof(induct n'≡"(_Entry_)" as n rule:path.induct)
case (Cons_path n'' as n' a)
from ‹n'' -as→* n'› ‹inner_node n'› have "n'' ≠ (_Exit_)"
by(fastforce simp:inner_node_def)
with ‹valid_edge a› ‹sourcenode a = (_Entry_)› ‹targetnode a = n''›
have "n'' = (_High_)" by -(drule Entry_edge_Exit_or_High,auto)
from High_target_Entry_edge
obtain a' where "valid_edge a'" and "sourcenode a' = (_Entry_)"
and "targetnode a' = (_High_)" and "kind a' = (λs. True)⇩√"
by blast
with ‹valid_edge a› ‹sourcenode a = (_Entry_)› ‹targetnode a = n''›
‹n'' = (_High_)›
have "a = a'" by(auto dest:edge_det)
with ‹n'' -as→* n'› ‹n'' = (_High_)› ‹kind a' = (λs. True)⇩√› show ?case by blast
qed fastforce
qed
lemma Exit_path_Low_path:
assumes "n -as→* (_Exit_)" and "inner_node n"
obtains a' as' where "as = as'@[a']" and "n -as'→* (_Low_)"
and "kind a' = (λs. True)⇩√"
proof(atomize_elim)
from ‹n -as→* (_Exit_)›
show "∃as' a'. as = as'@[a'] ∧ n -as'→* (_Low_) ∧ kind a' = (λs. True)⇩√"
proof(induct as rule:rev_induct)
case Nil
with ‹inner_node n› show ?case by fastforce
next
case (snoc a' as')
from ‹n -as'@[a']→* (_Exit_)›
have "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' = (_Exit_)"
by(auto elim:path_split_snoc)
{ assume "sourcenode a' = (_Entry_)"
with ‹n -as'→* sourcenode a'› have "n = (_Entry_)"
by(blast intro!:path_Entry_target)
with ‹inner_node n› have False by(simp add:inner_node_def) }
with ‹valid_edge a'› ‹targetnode a' = (_Exit_)› have "sourcenode a' = (_Low_)"
by(blast dest!:Exit_edge_Entry_or_Low)
from Low_source_Exit_edge
obtain ax where "valid_edge ax" and "sourcenode ax = (_Low_)"
and "targetnode ax = (_Exit_)" and "kind ax = (λs. True)⇩√"
by blast
with ‹valid_edge a'› ‹targetnode a' = (_Exit_)› ‹sourcenode a' = (_Low_)›
have "a' = ax" by(fastforce intro:edge_det)
with ‹n -as'→* sourcenode a'› ‹sourcenode a' = (_Low_)› ‹kind ax = (λs. True)⇩√›
show ?case by blast
qed
qed
lemma not_Low_High: "V ∉ L ⟹ V ∈ H"
using HighLowUNIV
by fastforce
lemma not_High_Low: "V ∉ H ⟹ V ∈ L"
using HighLowUNIV
by fastforce
subsection ‹Low Equivalence›
text ‹
In classical noninterference, an external observer can only see public values,
in our case the ‹L›-variables. If two states agree in the values of all
‹L›-variables, these states are indistinguishable for him.
\emph{Low equivalence} groups those states in an equivalence class using
the relation ‹≈⇩L›:
›
definition lowEquivalence :: "('var ⇀ 'val) list ⇒ ('var ⇀ 'val) list ⇒ bool"
(infixl "≈⇩L" 50)
where "s ≈⇩L s' ≡ ∀V ∈ L. hd s V = hd s' V"
text ‹The following lemmas connect low equivalent states with
relevant variables as necessary in the correctness proof for slicing.›
lemma relevant_vars_Entry:
assumes "V ∈ rv S (CFG_node (_Entry_))" and "(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙"
shows "V ∈ L"
proof -
from ‹V ∈ rv S (CFG_node (_Entry_))› obtain as n'
where "(_Entry_) -as→⇩ι* parent_node n'"
and "n' ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ n'"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
⟶ V ∉ Def⇘SDG⇙ n''" by(fastforce elim:rvE)
from ‹(_Entry_) -as→⇩ι* parent_node n'› have "valid_node (parent_node n')"
by(fastforce intro:path_valid_node simp:intra_path_def)
thus ?thesis
proof(cases "parent_node n'" rule:valid_node_cases)
case Entry
with ‹V ∈ Use⇘SDG⇙ n'› have False
by -(drule SDG_Use_parent_Use,simp add:Entry_empty)
thus ?thesis by simp
next
case Exit
with ‹V ∈ Use⇘SDG⇙ n'› have False
by -(drule SDG_Use_parent_Use,simp add:Exit_empty)
thus ?thesis by simp
next
case inner
with ‹(_Entry_) -as→⇩ι* parent_node n'› obtain a' as' where "as = a'#as'"
and "(_High_) -as'→⇩ι* parent_node n'"
by(fastforce elim:Entry_path_High_path simp:intra_path_def)
from ‹(_Entry_) -as→⇩ι* parent_node n'› ‹as = a'#as'›
have "sourcenode a' = (_Entry_)" by(fastforce elim:path.cases simp:intra_path_def)
show ?thesis
proof(cases "as' = []")
case True
with ‹(_High_) -as'→⇩ι* parent_node n'› have "parent_node n' = (_High_)"
by(fastforce simp:intra_path_def)
with ‹n' ∈ HRB_slice S› ‹(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙›
have False
by(fastforce dest:valid_SDG_node_in_slice_parent_node_in_slice
simp:SDG_to_CFG_set_def)
thus ?thesis by simp
next
case False
with ‹(_High_) -as'→⇩ι* parent_node n'› have "hd (sourcenodes as') = (_High_)"
by(fastforce intro:path_sourcenode simp:intra_path_def)
from False have "hd (sourcenodes as') ∈ set (sourcenodes as')"
by(fastforce intro:hd_in_set simp:sourcenodes_def)
with ‹as = a'#as'› have "hd (sourcenodes as') ∈ set (sourcenodes as)"
by(simp add:sourcenodes_def)
from ‹hd (sourcenodes as') = (_High_)›
have "valid_node (hd (sourcenodes as'))" by simp
have "valid_SDG_node (CFG_node (_High_))" by simp
with ‹hd (sourcenodes as') = (_High_)›
‹hd (sourcenodes as') ∈ set (sourcenodes as)›
‹∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
⟶ V ∉ Def⇘SDG⇙ n''›
have "V ∉ Def (_High_)"
by(fastforce dest:CFG_Def_SDG_Def[OF ‹valid_node (hd (sourcenodes as'))›])
hence "V ∉ H" by(simp add:DefHigh)
thus ?thesis by(rule not_High_Low)
qed
qed
qed
lemma lowEquivalence_relevant_nodes_Entry:
assumes "s ≈⇩L s'" and "(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙"
shows "∀V ∈ rv S (CFG_node (_Entry_)). hd s V = hd s' V"
proof
fix V assume "V ∈ rv S (CFG_node (_Entry_))"
with ‹(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙› have "V ∈ L" by -(rule relevant_vars_Entry)
with ‹s ≈⇩L s'› show "hd s V = hd s' V" by(simp add:lowEquivalence_def)
qed
subsection ‹The Correctness Proofs›
text ‹
In the following, we present two correctness proofs that slicing
guarantees IFC noninterference. In both theorems, ‹CFG_node
(_High_) ∉ HRB_slice S›, where ‹CFG_node (_Low_) ∈ S›, makes
sure that no high variable (which are all defined in ‹(_High_)›)
can influence a low variable (which are all used in ‹(_Low_)›).
First, a theorem regarding ‹(_Entry_) -as→* (_Exit_)› paths in the
control flow graph (CFG), which agree to a complete program execution:›
lemma slpa_rv_Low_Use_Low:
assumes "CFG_node (_Low_) ∈ S"
shows "⟦same_level_path_aux cs as; upd_cs cs as = []; same_level_path_aux cs as';
∀c ∈ set cs. valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
∀i < length cs. ∀V ∈ rv S (CFG_node (sourcenode (cs!i))).
fst (s!Suc i) V = fst (s'!Suc i) V; ∀i < Suc (length cs). snd (s!i) = snd (s'!i);
∀V ∈ rv S (CFG_node m). state_val s V = state_val s' V;
preds (slice_kinds S as) s; preds (slice_kinds S as') s';
length s = Suc (length cs); length s' = Suc (length cs)⟧
⟹ ∀V ∈ Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
state_val (transfers(slice_kinds S as') s') V"
proof(induct arbitrary:m as' s s' rule:slpa_induct)
case (slpa_empty cs)
from ‹m -[]→* (_Low_)› have "m = (_Low_)" by fastforce
from ‹m -[]→* (_Low_)› have "valid_node m"
by(rule path_valid_node)+
{ fix V assume "V ∈ Use (_Low_)"
moreover
from ‹valid_node m› ‹m = (_Low_)› have "(_Low_) -[]→⇩ι* (_Low_)"
by(fastforce intro:empty_path simp:intra_path_def)
moreover
from ‹valid_node m› ‹m = (_Low_)› ‹CFG_node (_Low_) ∈ S›
have "CFG_node (_Low_) ∈ HRB_slice S"
by(fastforce intro:HRB_slice_refl)
ultimately have "V ∈ rv S (CFG_node m)"
using ‹m = (_Low_)›
by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def) }
hence "∀V ∈ Use (_Low_). V ∈ rv S (CFG_node m)" by simp
show ?case
proof(cases "L = {}")
case True with UseLow show ?thesis by simp
next
case False
from ‹m -as'→* (_Low_)› ‹m = (_Low_)› have "as' = []"
proof(induct m as' m'≡"(_Low_)" rule:path.induct)
case (Cons_path m'' as a m)
from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)›
have "targetnode a = (_Exit_)" by -(rule Exit_successor_of_Low,simp+)
with ‹targetnode a = m''› ‹m'' -as→* (_Low_)›
have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
with False have False by -(drule Low_neq_Exit,simp)
thus ?case by simp
qed simp
with ‹∀V ∈ Use (_Low_). V ∈ rv S (CFG_node m)›
‹∀V ∈ rv S (CFG_node m). state_val s V = state_val s' V› Nil
show ?thesis by(auto simp:slice_kinds_def)
qed
next
case (slpa_intra cs a as)
note IH = ‹⋀m as' s s'. ⟦upd_cs cs as = []; same_level_path_aux cs as';
∀a∈set cs. valid_edge a; m -as→* (_Low_); m -as'→* (_Low_);
∀i<length cs. ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
fst (s ! Suc i) V = fst (s' ! Suc i) V;
∀i<Suc (length cs). snd (s ! i) = snd (s' ! i);
∀V∈rv S (CFG_node m). state_val s V = state_val s' V;
preds (slice_kinds S as) s; preds (slice_kinds S as') s';
length s = Suc (length cs); length s' = Suc (length cs)⟧
⟹ ∀V∈Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
state_val (transfers(slice_kinds S as') s') V›
note rvs = ‹∀i<length cs. ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
fst (s ! Suc i) V = fst (s' ! Suc i) V›
from ‹m -a # as→* (_Low_)› have "sourcenode a = m" and "valid_edge a"
and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
show ?case
proof(cases "L = {}")
case True with UseLow show ?thesis by simp
next
case False
show ?thesis
proof(cases as')
case Nil
with ‹m -as'→* (_Low_)› have "m = (_Low_)" by fastforce
with ‹valid_edge a› ‹sourcenode a = m› have "targetnode a = (_Exit_)"
by -(rule Exit_successor_of_Low,simp+)
from Low_source_Exit_edge obtain a' where "valid_edge a'"
and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
and "kind a' = (λs. True)⇩√" by blast
from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)›
‹targetnode a = (_Exit_)› ‹valid_edge a'› ‹sourcenode a' = (_Low_)›
‹targetnode a' = (_Exit_)›
have "a = a'" by(fastforce dest:edge_det)
with ‹kind a' = (λs. True)⇩√› have "kind a = (λs. True)⇩√" by simp
with ‹targetnode a = (_Exit_)› ‹targetnode a -as→* (_Low_)›
have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
with False have False by -(drule Low_neq_Exit,simp)
thus ?thesis by simp
next
case (Cons ax asx)
with ‹m -as'→* (_Low_)› have "sourcenode ax = m" and "valid_edge ax"
and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
from ‹preds (slice_kinds S (a # as)) s›
obtain cf cfs where [simp]:"s = cf#cfs" by(cases s)(auto simp:slice_kinds_def)
from ‹preds (slice_kinds S as') s'› ‹as' = ax # asx›
obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
by(cases s')(auto simp:slice_kinds_def)
have "intra_kind (kind ax)"
proof(cases "kind ax" rule:edge_kind_cases)
case (Call Q r p fs)
have False
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with ‹intra_kind (kind a)› have "slice_kind S a = kind a"
by -(rule slice_intra_kind_in_slice)
from ‹valid_edge ax› ‹kind ax = Q:r↪⇘p⇙fs›
have unique:"∃!a'. valid_edge a' ∧ sourcenode a' = sourcenode ax ∧
intra_kind(kind a')" by(rule call_only_one_intra_edge)
from ‹valid_edge ax› ‹kind ax = Q:r↪⇘p⇙fs› obtain x
where "x ∈ get_return_edges ax" by(fastforce dest:get_return_edge_call)
with ‹valid_edge ax› obtain a' where "valid_edge a'"
and "sourcenode a' = sourcenode ax" and "kind a' = (λcf. False)⇩√"
by(fastforce dest:call_return_node_edge)
with ‹valid_edge a› ‹sourcenode a = m› ‹sourcenode ax = m›
‹intra_kind (kind a)› unique
have "a' = a" by(fastforce simp:intra_kind_def)
with ‹kind a' = (λcf. False)⇩√› ‹slice_kind S a = kind a›
‹preds (slice_kinds S (a#as)) s›
have False by(cases s)(auto simp:slice_kinds_def)
thus ?thesis by simp
next
case False
with ‹kind ax = Q:r↪⇘p⇙fs› ‹sourcenode a = m› ‹sourcenode ax = m›
have "slice_kind S ax = (λcf. False):r↪⇘p⇙fs"
by(fastforce intro:slice_kind_Call)
with ‹as' = ax # asx› ‹preds (slice_kinds S as') s'›
have False by(cases s')(auto simp:slice_kinds_def)
thus ?thesis by simp
qed
thus ?thesis by simp
next
case (Return Q p f)
from ‹valid_edge ax› ‹kind ax = Q↩⇘p⇙f› ‹valid_edge a› ‹intra_kind (kind a)›
‹sourcenode a = m› ‹sourcenode ax = m›
have False by -(drule return_edges_only,auto simp:intra_kind_def)
thus ?thesis by simp
qed simp
with ‹same_level_path_aux cs as'› ‹as' = ax#asx›
have "same_level_path_aux cs asx" by(fastforce simp:intra_kind_def)
show ?thesis
proof(cases "targetnode a = targetnode ax")
case True
with ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = m› ‹sourcenode ax = m›
have "a = ax" by(fastforce intro:edge_det)
with ‹valid_edge a› ‹intra_kind (kind a)› ‹sourcenode a = m›
‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
‹preds (slice_kinds S (a # as)) s›
‹preds (slice_kinds S as') s'› ‹as' = ax # asx›
have rv:"∀V∈rv S (CFG_node (targetnode a)).
state_val (transfer (slice_kind S a) s) V =
state_val (transfer (slice_kind S a) s') V"
by -(rule rv_edge_slice_kinds,auto)
from ‹upd_cs cs (a # as) = []› ‹intra_kind (kind a)›
have "upd_cs cs as = []" by(fastforce simp:intra_kind_def)
from ‹targetnode ax -asx→* (_Low_)› ‹a = ax›
have "targetnode a -asx→* (_Low_)" by simp
from ‹valid_edge a› ‹intra_kind (kind a)›
obtain cfx
where cfx:"transfer (slice_kind S a) s = cfx#cfs ∧ snd cfx = snd cf"
apply(cases cf)
apply(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙") apply auto
apply(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
apply(auto simp:intra_kind_def)
apply(drule slice_kind_Upd) apply auto
by(erule kind_Predicate_notin_slice_slice_kind_Predicate) auto
from ‹valid_edge a› ‹intra_kind (kind a)›
obtain cfx'
where cfx':"transfer (slice_kind S a) s' = cfx'#cfs' ∧ snd cfx' = snd cf'"
apply(cases cf')
apply(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙") apply auto
apply(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
apply(auto simp:intra_kind_def)
apply(drule slice_kind_Upd) apply auto
by(erule kind_Predicate_notin_slice_slice_kind_Predicate) auto
with cfx ‹∀i < Suc (length cs). snd (s!i) = snd (s'!i)›
have snds:"∀i<Suc(length cs).
snd (transfer (slice_kind S a) s ! i) =
snd (transfer (slice_kind S a) s' ! i)"
by auto(case_tac i,auto)
from rvs cfx cfx' have rvs':"∀i<length cs.
∀V∈rv S (CFG_node (sourcenode (cs ! i))).
fst (transfer (slice_kind S a) s ! Suc i) V =
fst (transfer (slice_kind S a) s' ! Suc i) V"
by fastforce
from ‹preds (slice_kinds S (a # as)) s›
have "preds (slice_kinds S as)
(transfer (slice_kind S a) s)" by(simp add:slice_kinds_def)
moreover
from ‹preds (slice_kinds S as') s'› ‹as' = ax # asx› ‹a = ax›
have "preds (slice_kinds S asx) (transfer (slice_kind S a) s')"
by(simp add:slice_kinds_def)
moreover
from ‹valid_edge a› ‹intra_kind (kind a)›
have "length (transfer (slice_kind S a) s) = length s"
by(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
(auto dest:slice_intra_kind_in_slice slice_kind_Upd
elim:kind_Predicate_notin_slice_slice_kind_Predicate simp:intra_kind_def)
with ‹length s = Suc (length cs)›
have "length (transfer (slice_kind S a) s) = Suc (length cs)"
by simp
moreover
from ‹a = ax› ‹valid_edge a› ‹intra_kind (kind a)›
have "length (transfer (slice_kind S a) s') = length s'"
by(cases "sourcenode ax ∈ ⌊HRB_slice S⌋⇘CFG⇙")
(auto dest:slice_intra_kind_in_slice slice_kind_Upd
elim:kind_Predicate_notin_slice_slice_kind_Predicate simp:intra_kind_def)
with ‹length s' = Suc (length cs)›
have "length (transfer (slice_kind S a) s') = Suc (length cs)"
by simp
moreover
from IH[OF ‹upd_cs cs as = []› ‹same_level_path_aux cs asx›
‹∀c∈set cs. valid_edge c› ‹targetnode a -as→* (_Low_)›
‹targetnode a -asx→* (_Low_)› rvs' snds rv calculation]
‹as' = ax # asx› ‹a = ax›
show ?thesis by(simp add:slice_kinds_def)
next
case False
from ‹∀i < Suc(length cs). snd (s!i) = snd (s'!i)›
have "snd (hd s) = snd (hd s')" by(erule_tac x="0" in allE) fastforce
with ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = m›
‹sourcenode ax = m› ‹as' = ax # asx› False
‹intra_kind (kind a)› ‹intra_kind (kind ax)›
‹preds (slice_kinds S (a # as)) s›
‹preds (slice_kinds S as') s'›
‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
‹length s = Suc (length cs)› ‹length s' = Suc (length cs)›
have False by(fastforce intro!:rv_branching_edges_slice_kinds_False[of a ax])
thus ?thesis by simp
qed
qed
qed
next
case (slpa_Call cs a as Q r p fs)
note IH = ‹⋀m as' s s'.
⟦upd_cs (a # cs) as = []; same_level_path_aux (a # cs) as';
∀c∈set (a # cs). valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
∀i<length (a # cs). ∀V∈rv S (CFG_node (sourcenode ((a # cs) ! i))).
fst (s ! Suc i) V = fst (s' ! Suc i) V;
∀i<Suc (length (a # cs)). snd (s ! i) = snd (s' ! i);
∀V∈rv S (CFG_node m). state_val s V = state_val s' V;
preds (slice_kinds S as) s; preds (slice_kinds S as') s';
length s = Suc (length (a # cs)); length s' = Suc (length (a # cs))⟧
⟹ ∀V∈Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
state_val (transfers(slice_kinds S as') s') V›
note rvs = ‹∀i<length cs. ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
fst (s ! Suc i) V = fst (s' ! Suc i) V›
from ‹m -a # as→* (_Low_)› have "sourcenode a = m" and "valid_edge a"
and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
from ‹∀c∈set cs. valid_edge c› ‹valid_edge a›
have "∀c∈set (a # cs). valid_edge c" by simp
show ?case
proof(cases "L = {}")
case True with UseLow show ?thesis by simp
next
case False
show ?thesis
proof(cases as')
case Nil
with ‹m -as'→* (_Low_)› have "m = (_Low_)" by fastforce
with ‹valid_edge a› ‹sourcenode a = m› have "targetnode a = (_Exit_)"
by -(rule Exit_successor_of_Low,simp+)
from Low_source_Exit_edge obtain a' where "valid_edge a'"
and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
and "kind a' = (λs. True)⇩√" by blast
from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)›
‹targetnode a = (_Exit_)› ‹valid_edge a'› ‹sourcenode a' = (_Low_)›
‹targetnode a' = (_Exit_)›
have "a = a'" by(fastforce dest:edge_det)
with ‹kind a' = (λs. True)⇩√› have "kind a = (λs. True)⇩√" by simp
with ‹targetnode a = (_Exit_)› ‹targetnode a -as→* (_Low_)›
have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
with False have False by -(drule Low_neq_Exit,simp)
thus ?thesis by simp
next
case (Cons ax asx)
with ‹m -as'→* (_Low_)› have "sourcenode ax = m" and "valid_edge ax"
and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
from ‹preds (slice_kinds S (a # as)) s›
obtain cf cfs where [simp]:"s = cf#cfs" by(cases s)(auto simp:slice_kinds_def)
from ‹preds (slice_kinds S as') s'› ‹as' = ax # asx›
obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
by(cases s')(auto simp:slice_kinds_def)
have "∃Q r p fs. kind ax = Q:r↪⇘p⇙fs"
proof(cases "kind ax" rule:edge_kind_cases)
case Intra
have False
proof(cases "sourcenode ax ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with ‹intra_kind (kind ax)›
have "slice_kind S ax = kind ax"
by -(rule slice_intra_kind_in_slice)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
have unique:"∃!a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
intra_kind(kind a')" by(rule call_only_one_intra_edge)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain x
where "x ∈ get_return_edges a" by(fastforce dest:get_return_edge_call)
with ‹valid_edge a› obtain a' where "valid_edge a'"
and "sourcenode a' = sourcenode a" and "kind a' = (λcf. False)⇩√"
by(fastforce dest:call_return_node_edge)
with ‹valid_edge ax› ‹sourcenode ax = m› ‹sourcenode a = m›
‹intra_kind (kind ax)› unique
have "a' = ax" by(fastforce simp:intra_kind_def)
with ‹kind a' = (λcf. False)⇩√›
‹slice_kind S ax = kind ax› ‹as' = ax # asx›
‹preds (slice_kinds S as') s'›
have False by(simp add:slice_kinds_def)
thus ?thesis by simp
next
case False
with ‹kind a = Q:r↪⇘p⇙fs› ‹sourcenode ax = m› ‹sourcenode a = m›
have "slice_kind S a = (λcf. False):r↪⇘p⇙fs"
by(fastforce intro:slice_kind_Call)
with ‹preds (slice_kinds S (a # as)) s›
have False by(simp add:slice_kinds_def)
thus ?thesis by simp
qed
thus ?thesis by simp
next
case (Return Q' p' f')
from ‹valid_edge ax› ‹kind ax = Q'↩⇘p'⇙f'› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
‹sourcenode a = m› ‹sourcenode ax = m›
have False by -(drule return_edges_only,auto)
thus ?thesis by simp
qed simp
have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
proof(rule ccontr)
assume "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
from this ‹kind a = Q:r↪⇘p⇙fs›
have "slice_kind S a = (λcf. False):r↪⇘p⇙fs"
by(rule slice_kind_Call)
with ‹preds (slice_kinds S (a # as)) s›
show False by(simp add:slice_kinds_def)
qed
with ‹preds (slice_kinds S (a # as)) s› ‹kind a = Q:r↪⇘p⇙fs›
have "pred (kind a) s"
by(fastforce dest:slice_kind_Call_in_slice simp:slice_kinds_def)
from ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙›
‹sourcenode a = m› ‹sourcenode ax = m›
have "sourcenode ax ∈ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with ‹as' = ax # asx› ‹preds (slice_kinds S as') s'›
‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
have "pred (kind ax) s'"
by(fastforce dest:slice_kind_Call_in_slice simp:slice_kinds_def)
{ fix V assume "V ∈ Use (sourcenode a)"
from ‹valid_edge a› have "sourcenode a -[]→⇩ι* sourcenode a"
by(fastforce intro:empty_path simp:intra_path_def)
with ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙›
‹valid_edge a› ‹V ∈ Use (sourcenode a)›
have "V ∈ rv S (CFG_node (sourcenode a))"
by(auto intro!:rvI CFG_Use_SDG_Use simp:SDG_to_CFG_set_def sourcenodes_def) }
with ‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
‹sourcenode a = m›
have Use:"∀V ∈ Use (sourcenode a). state_val s V = state_val s' V" by simp
from ‹∀i<Suc (length cs). snd (s ! i) = snd (s' ! i)›
have "snd (hd s) = snd (hd s')" by fastforce
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge ax›
‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs› ‹sourcenode a = m› ‹sourcenode ax = m›
‹pred (kind a) s› ‹pred (kind ax) s'› Use ‹length s = Suc (length cs)›
‹length s' = Suc (length cs)›
have [simp]:"ax = a" by(fastforce intro!:CFG_equal_Use_equal_call)
from ‹same_level_path_aux cs as'› ‹as' = ax#asx› ‹kind a = Q:r↪⇘p⇙fs›
‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
have "same_level_path_aux (a # cs) asx" by simp
from ‹targetnode ax -asx→* (_Low_)› have "targetnode a -asx→* (_Low_)" by simp
from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs cs (a # as) = []›
have "upd_cs (a # cs) as = []" by simp
from ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = Q:r↪⇘p⇙fs›
have slice_kind:"slice_kind S a =
Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"
by(rule slice_kind_Call_in_slice)
from ‹∀i<Suc (length cs). snd (s ! i) = snd (s' ! i)› slice_kind
have snds:"∀i<Suc (length (a # cs)).
snd (transfer (slice_kind S a) s ! i) =
snd (transfer (slice_kind S a) s' ! i)"
by auto(case_tac i,auto)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain ins outs
where "(p,ins,outs) ∈ set procs" by(fastforce dest!:callee_in_procs)
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
have "length (ParamUses (sourcenode a)) = length ins"
by(fastforce intro:ParamUses_call_source_length)
with ‹valid_edge a›
have "∀i < length ins. ∀V ∈ (ParamUses (sourcenode a))!i. V ∈ Use (sourcenode a)"
by(fastforce intro:ParamUses_in_Use)
with ‹∀V ∈ Use (sourcenode a). state_val s V = state_val s' V›
have "∀i < length ins. ∀V ∈ (ParamUses (sourcenode a))!i.
state_val s V = state_val s' V"
by fastforce
with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹(p,ins,outs) ∈ set procs›
‹pred (kind a) s› ‹pred (kind ax) s'›
have "∀i < length ins. (params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i"
by(fastforce intro!:CFG_call_edge_params)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹(p,ins,outs) ∈ set procs›
have "length fs = length ins" by(rule CFG_call_edge_length)
{ fix i assume "i < length fs"
with ‹length fs = length ins› have "i < length ins" by simp
from ‹i < length fs› have "(params fs (fst cf))!i = (fs!i) (fst cf)"
by(rule params_nth)
moreover
from ‹i < length fs› have "(params fs (fst cf'))!i = (fs!i) (fst cf')"
by(rule params_nth)
ultimately have "(fs!i) (fst (hd s)) = (fs!i) (fst (hd s'))"
using ‹i < length ins›
‹∀i < length ins. (params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i›
by simp }
hence "∀i < length fs. (fs ! i) (fst cf) = (fs ! i) (fst cf')" by simp
{ fix i assume "i < length fs"
with ‹∀i < length fs. (fs ! i) (fst cf) = (fs ! i) (fst cf')›
have "(fs ! i) (fst cf) = (fs ! i) (fst cf')" by simp
have "((csppa (targetnode a) (HRB_slice S) 0 fs)!i)(fst cf) =
((csppa (targetnode a) (HRB_slice S) 0 fs)!i)(fst cf')"
proof(cases "Formal_in(targetnode a,i + 0) ∈ HRB_slice S")
case True
with ‹i < length fs›
have "(csppa (targetnode a) (HRB_slice S) 0 fs)!i = fs!i"
by(rule csppa_Formal_in_in_slice)
with ‹(fs ! i) (fst cf) = (fs ! i) (fst cf')› show ?thesis by simp
next
case False
with ‹i < length fs›
have "(csppa (targetnode a) (HRB_slice S) 0 fs)!i = Map.empty"
by(rule csppa_Formal_in_notin_slice)
thus ?thesis by simp
qed }
hence eq:"∀i < length fs.
((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf) =
((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf')"
by(simp add:cspp_def)
{ fix i assume "i < length fs"
hence "(params (cspp (targetnode a) (HRB_slice S) fs)
(fst cf))!i =
((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf)"
by(fastforce intro:params_nth)
moreover
from ‹i < length fs›
have "(params (cspp (targetnode a) (HRB_slice S) fs)
(fst cf'))!i =
((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf')"
by(fastforce intro:params_nth)
ultimately
have "(params (cspp (targetnode a) (HRB_slice S) fs)
(fst cf))!i =
(params (cspp (targetnode a) (HRB_slice S) fs)(fst cf'))!i"
using eq ‹i < length fs› by simp }
hence "params (cspp (targetnode a) (HRB_slice S) fs)(fst cf) =
params (cspp (targetnode a) (HRB_slice S) fs)(fst cf')"
by(simp add:list_eq_iff_nth_eq)
with slice_kind ‹(p,ins,outs) ∈ set procs›
obtain cfx where [simp]:
"transfer (slice_kind S a) (cf#cfs) = cfx#cf#cfs"
"transfer (slice_kind S a) (cf'#cfs') = cfx#cf'#cfs'"
by auto
hence rv:"∀V∈rv S (CFG_node (targetnode a)).
state_val (transfer (slice_kind S a) s) V =
state_val (transfer (slice_kind S a) s') V" by simp
from rvs ‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
‹sourcenode a = m›
have rvs':"∀i<length (a # cs).
∀V∈rv S (CFG_node (sourcenode ((a # cs) ! i))).
fst ((transfer (slice_kind S a) s) ! Suc i) V =
fst ((transfer (slice_kind S a) s') ! Suc i) V"
by auto(case_tac i,auto)
from ‹preds (slice_kinds S (a # as)) s›
have "preds (slice_kinds S as)
(transfer (slice_kind S a) s)" by(simp add:slice_kinds_def)
moreover
from ‹preds (slice_kinds S as') s'› ‹as' = ax#asx›
have "preds (slice_kinds S asx)
(transfer (slice_kind S a) s')" by(simp add:slice_kinds_def)
moreover
from ‹length s = Suc (length cs)›
have "length (transfer (slice_kind S a) s) =
Suc (length (a # cs))" by simp
moreover
from ‹length s' = Suc (length cs)›
have "length (transfer (slice_kind S a) s') =
Suc (length (a # cs))" by simp
moreover
from IH[OF ‹upd_cs (a # cs) as = []› ‹same_level_path_aux (a # cs) asx›
‹∀c∈set (a # cs). valid_edge c› ‹targetnode a -as→* (_Low_)›
‹targetnode a -asx→* (_Low_)› rvs' snds rv calculation] ‹as' = ax#asx›
show ?thesis by(simp add:slice_kinds_def)
qed
qed
next
case (slpa_Return cs a as Q p f c' cs')
note IH = ‹⋀m as' s s'. ⟦upd_cs cs' as = []; same_level_path_aux cs' as';
∀c∈set cs'. valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
∀i<length cs'. ∀V∈rv S (CFG_node (sourcenode (cs' ! i))).
fst (s ! Suc i) V = fst (s' ! Suc i) V;
∀i<Suc (length cs'). snd (s ! i) = snd (s' ! i);
∀V∈rv S (CFG_node m). state_val s V = state_val s' V;
preds (slice_kinds S as) s; preds (slice_kinds S as') s';
length s = Suc (length cs'); length s' = Suc (length cs')⟧
⟹ ∀V∈Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
state_val (transfers(slice_kinds S as') s') V›
note rvs = ‹ ∀i<length cs. ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
fst (s ! Suc i) V = fst (s' ! Suc i) V›
from ‹m -a # as→* (_Low_)› have "sourcenode a = m" and "valid_edge a"
and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
from ‹∀c∈set cs. valid_edge c› ‹cs = c' # cs'›
have "valid_edge c'" and "∀c∈set cs'. valid_edge c" by simp_all
show ?case
proof(cases "L = {}")
case True with UseLow show ?thesis by simp
next
case False
show ?thesis
proof(cases as')
case Nil
with ‹m -as'→* (_Low_)› have "m = (_Low_)" by fastforce
with ‹valid_edge a› ‹sourcenode a = m› have "targetnode a = (_Exit_)"
by -(rule Exit_successor_of_Low,simp+)
from Low_source_Exit_edge obtain a' where "valid_edge a'"
and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
and "kind a' = (λs. True)⇩√" by blast
from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)›
‹targetnode a = (_Exit_)› ‹valid_edge a'› ‹sourcenode a' = (_Low_)›
‹targetnode a' = (_Exit_)›
have "a = a'" by(fastforce dest:edge_det)
with ‹kind a' = (λs. True)⇩√› have "kind a = (λs. True)⇩√" by simp
with ‹targetnode a = (_Exit_)› ‹targetnode a -as→* (_Low_)›
have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
with False have False by -(drule Low_neq_Exit,simp)
thus ?thesis by simp
next
case (Cons ax asx)
with ‹m -as'→* (_Low_)› have "sourcenode ax = m" and "valid_edge ax"
and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
from ‹valid_edge a› ‹valid_edge ax› ‹kind a = Q↩⇘p⇙f›
‹sourcenode a = m› ‹sourcenode ax = m›
have "∃Q f. kind ax = Q↩⇘p⇙f" by(auto dest:return_edges_only)
with ‹same_level_path_aux cs as'› ‹as' = ax#asx› ‹cs = c' # cs'›
have "ax ∈ get_return_edges c'" and "same_level_path_aux cs' asx" by auto
from ‹valid_edge c'› ‹ax ∈ get_return_edges c'› ‹a ∈ get_return_edges c'›
have [simp]:"ax = a" by(rule get_return_edges_unique)
from ‹targetnode ax -asx→* (_Low_)› have "targetnode a -asx→* (_Low_)" by simp
from ‹upd_cs cs (a # as) = []› ‹kind a = Q↩⇘p⇙f› ‹cs = c' # cs'›
‹a ∈ get_return_edges c'›
have "upd_cs cs' as = []" by simp
from ‹length s = Suc (length cs)› ‹cs = c' # cs'›
obtain cf cfx cfs where "s = cf#cfx#cfs"
by(cases s,auto,case_tac list,fastforce+)
from ‹length s' = Suc (length cs)› ‹cs = c' # cs'›
obtain cf' cfx' cfs' where "s' = cf'#cfx'#cfs'"
by(cases s',auto,case_tac list,fastforce+)
from rvs ‹cs = c' # cs'› ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
have rvs1:"∀i<length cs'.
∀V∈rv S (CFG_node (sourcenode (cs' ! i))).
fst ((cfx#cfs) ! Suc i) V = fst ((cfx'#cfs') ! Suc i) V"
and "∀V∈rv S (CFG_node (sourcenode c')).
(fst cfx) V = (fst cfx') V"
by auto
from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
obtain Qx rx px fsx where "kind c' = Qx:rx↪⇘px⇙fsx"
by(fastforce dest!:only_call_get_return_edges)
have "∀V ∈ rv S (CFG_node (targetnode a)).
V ∈ rv S (CFG_node (sourcenode c'))"
proof
fix V assume "V ∈ rv S (CFG_node (targetnode a))"
from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
obtain a' where edge:"valid_edge a'" "sourcenode a' = sourcenode c'"
"targetnode a' = targetnode a" "intra_kind (kind a')"
by -(drule call_return_node_edge,auto simp:intra_kind_def)
from ‹V ∈ rv S (CFG_node (targetnode a))›
obtain as n' where "targetnode a -as→⇩ι* parent_node n'"
and "n' ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ n'"
and all:"∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
⟶ V ∉ Def⇘SDG⇙ n''" by(fastforce elim:rvE)
from ‹targetnode a -as→⇩ι* parent_node n'› edge
have "sourcenode c' -a'#as→⇩ι* parent_node n'"
by(fastforce intro:Cons_path simp:intra_path_def)
from ‹valid_edge c'› ‹kind c' = Qx:rx↪⇘px⇙fsx› have "Def (sourcenode c') = {}"
by(rule call_source_Def_empty)
hence "∀n''. valid_SDG_node n'' ∧ parent_node n'' = sourcenode c'
⟶ V ∉ Def⇘SDG⇙ n''" by(fastforce dest:SDG_Def_parent_Def)
with all ‹sourcenode a' = sourcenode c'›
have "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes (a'#as))
⟶ V ∉ Def⇘SDG⇙ n''" by(fastforce simp:sourcenodes_def)
with ‹sourcenode c' -a'#as→⇩ι* parent_node n'›
‹n' ∈ HRB_slice S› ‹V ∈ Use⇘SDG⇙ n'›
show "V ∈ rv S (CFG_node (sourcenode c'))"
by(fastforce intro:rvI)
qed
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
have "get_proc (targetnode c') = get_proc (sourcenode a)"
by -(drule intra_proc_additional_edge,
auto dest:get_proc_intra simp:intra_kind_def)
moreover
from ‹valid_edge c'› ‹kind c' = Qx:rx↪⇘px⇙fsx›
have "get_proc (targetnode c') = px" by(rule get_proc_call)
moreover
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
have "get_proc (sourcenode a) = p" by(rule get_proc_return)
ultimately have [simp]:"px = p" by simp
from ‹valid_edge c'› ‹kind c' = Qx:rx↪⇘px⇙fsx›
obtain ins outs where "(p,ins,outs) ∈ set procs"
by(fastforce dest!:callee_in_procs)
with ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙›
‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
have slice_kind:"slice_kind S a =
Q↩⇘p⇙(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"
by(rule slice_kind_Return_in_slice)
with ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
have sx:"transfer (slice_kind S a) s =
(rspp (targetnode a) (HRB_slice S) outs (fst cfx) (fst cf),
snd cfx)#cfs"
and sx':"transfer (slice_kind S a) s' =
(rspp (targetnode a) (HRB_slice S) outs (fst cfx') (fst cf'),
snd cfx')#cfs'"
by simp_all
with rvs1 have rvs':"∀i<length cs'.
∀V∈rv S (CFG_node (sourcenode (cs' ! i))).
fst ((transfer (slice_kind S a) s) ! Suc i) V =
fst ((transfer (slice_kind S a) s') ! Suc i) V"
by fastforce
from slice_kind ‹∀i<Suc (length cs). snd (s ! i) = snd (s' ! i)› ‹cs = c' # cs'›
‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
have snds:"∀i<Suc (length cs').
snd (transfer (slice_kind S a) s ! i) =
snd (transfer (slice_kind S a) s' ! i)"
apply auto apply(case_tac i) apply auto
by(erule_tac x="Suc (Suc nat)" in allE) auto
have "∀V∈rv S (CFG_node (targetnode a)).
(rspp (targetnode a) (HRB_slice S) outs
(fst cfx) (fst cf)) V =
(rspp (targetnode a) (HRB_slice S) outs
(fst cfx') (fst cf')) V"
proof
fix V assume "V ∈ rv S (CFG_node (targetnode a))"
show "(rspp (targetnode a) (HRB_slice S) outs
(fst cfx) (fst cf)) V =
(rspp (targetnode a) (HRB_slice S) outs
(fst cfx') (fst cf')) V"
proof(cases "V ∈ set (ParamDefs (targetnode a))")
case True
then obtain i where "i < length (ParamDefs (targetnode a))"
and "(ParamDefs (targetnode a))!i = V"
by(fastforce simp:in_set_conv_nth)
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹(p,ins,outs) ∈ set procs›
have "length(ParamDefs (targetnode a)) = length outs"
by(fastforce intro:ParamDefs_return_target_length)
show ?thesis
proof(cases "Actual_out(targetnode a,i) ∈ HRB_slice S")
case True
with ‹i < length (ParamDefs (targetnode a))› ‹valid_edge a›
‹length(ParamDefs (targetnode a)) = length outs›
‹(ParamDefs (targetnode a))!i = V›[THEN sym]
have rspp_eq:"(rspp (targetnode a)
(HRB_slice S) outs (fst cfx) (fst cf)) V =
(fst cf)(outs!i)"
"(rspp (targetnode a)
(HRB_slice S) outs (fst cfx') (fst cf')) V =
(fst cf')(outs!i)"
by(auto intro:rspp_Actual_out_in_slice)
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹(p,ins,outs) ∈ set procs›
have "∀V ∈ set outs. V ∈ Use (sourcenode a)" by(fastforce dest:outs_in_Use)
have "∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node m)"
proof
fix V assume "V ∈ Use (sourcenode a)"
from ‹valid_edge a› ‹sourcenode a = m›
have "parent_node (CFG_node m) -[]→⇩ι* parent_node (CFG_node m)"
by(fastforce intro:empty_path simp:intra_path_def)
with ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙›
‹V ∈ Use (sourcenode a)› ‹sourcenode a = m› ‹valid_edge a›
show "V ∈ rv S (CFG_node m)"
by -(rule rvI,
auto intro!:CFG_Use_SDG_Use simp:SDG_to_CFG_set_def sourcenodes_def)
qed
with ‹∀V ∈ set outs. V ∈ Use (sourcenode a)›
have "∀V ∈ set outs. V ∈ rv S (CFG_node m)" by simp
with ‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
have "∀V ∈ set outs. (fst cf) V = (fst cf') V" by simp
with ‹i < length (ParamDefs (targetnode a))›
‹length(ParamDefs (targetnode a)) = length outs›
have "(fst cf)(outs!i) = (fst cf')(outs!i)" by fastforce
with rspp_eq show ?thesis by simp
next
case False
with ‹i < length (ParamDefs (targetnode a))› ‹valid_edge a›
‹length(ParamDefs (targetnode a)) = length outs›
‹(ParamDefs (targetnode a))!i = V›[THEN sym]
have rspp_eq:"(rspp (targetnode a)
(HRB_slice S) outs (fst cfx) (fst cf)) V =
(fst cfx)((ParamDefs (targetnode a))!i)"
"(rspp (targetnode a)
(HRB_slice S) outs (fst cfx') (fst cf')) V =
(fst cfx')((ParamDefs (targetnode a))!i)"
by(auto intro:rspp_Actual_out_notin_slice)
from ‹∀V∈rv S (CFG_node (sourcenode c')).
(fst cfx) V = (fst cfx') V›
‹V ∈ rv S (CFG_node (targetnode a))›
‹∀V ∈ rv S (CFG_node (targetnode a)).
V ∈ rv S (CFG_node (sourcenode c'))›
‹(ParamDefs (targetnode a))!i = V›[THEN sym]
have "(fst cfx) (ParamDefs (targetnode a) ! i) =
(fst cfx') (ParamDefs (targetnode a) ! i)" by fastforce
with rspp_eq show ?thesis by fastforce
qed
next
case False
with ‹∀V∈rv S (CFG_node (sourcenode c')).
(fst cfx) V = (fst cfx') V›
‹V ∈ rv S (CFG_node (targetnode a))›
‹∀V ∈ rv S (CFG_node (targetnode a)).
V ∈ rv S (CFG_node (sourcenode c'))›
show ?thesis by(fastforce simp:rspp_def map_merge_def)
qed
qed
with sx sx'
have rv':"∀V∈rv S (CFG_node (targetnode a)).
state_val (transfer (slice_kind S a) s) V =
state_val (transfer (slice_kind S a) s') V"
by fastforce
from ‹preds (slice_kinds S (a # as)) s›
have "preds (slice_kinds S as)
(transfer (slice_kind S a) s)"
by(simp add:slice_kinds_def)
moreover
from ‹preds (slice_kinds S as') s'› ‹as' = ax#asx›
have "preds (slice_kinds S asx)
(transfer (slice_kind S a) s')"
by(simp add:slice_kinds_def)
moreover
from ‹length s = Suc (length cs)› ‹cs = c' # cs'› sx
have "length (transfer (slice_kind S a) s) = Suc (length cs')"
by(simp,simp add:‹s = cf#cfx#cfs›)
moreover
from ‹length s' = Suc (length cs)› ‹cs = c' # cs'› sx'
have "length (transfer (slice_kind S a) s') = Suc (length cs')"
by(simp,simp add:‹s' = cf'#cfx'#cfs'›)
moreover
from IH[OF ‹upd_cs cs' as = []› ‹same_level_path_aux cs' asx›
‹∀c∈set cs'. valid_edge c› ‹targetnode a -as→* (_Low_)›
‹targetnode a -asx→* (_Low_)› rvs' snds rv' calculation] ‹as' = ax#asx›
show ?thesis by(simp add:slice_kinds_def)
next
case False
from this ‹kind a = Q↩⇘p⇙f›
have slice_kind:"slice_kind S a = (λcf. True)↩⇘p⇙(λcf cf'. cf')"
by(rule slice_kind_Return)
with ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
have [simp]:"transfer (slice_kind S a) s = cfx#cfs"
"transfer (slice_kind S a) s' = cfx'#cfs'" by simp_all
from slice_kind ‹∀i<Suc (length cs). snd (s ! i) = snd (s' ! i)›
‹cs = c' # cs'› ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
have snds:"∀i<Suc (length cs').
snd (transfer (slice_kind S a) s ! i) =
snd (transfer (slice_kind S a) s' ! i)" by fastforce
from rvs1 have rvs':"∀i<length cs'.
∀V∈rv S (CFG_node (sourcenode (cs' ! i))).
fst ((transfer (slice_kind S a) s) ! Suc i) V =
fst ((transfer (slice_kind S a) s') ! Suc i) V"
by fastforce
from ‹∀V ∈ rv S (CFG_node (targetnode a)).
V ∈ rv S (CFG_node (sourcenode c'))›
‹∀V∈rv S (CFG_node (sourcenode c')).
(fst cfx) V = (fst cfx') V›
have rv':"∀V∈rv S (CFG_node (targetnode a)).
state_val (transfer (slice_kind S a) s) V =
state_val (transfer (slice_kind S a) s') V" by simp
from ‹preds (slice_kinds S (a # as)) s›
have "preds (slice_kinds S as)
(transfer (slice_kind S a) s)"
by(simp add:slice_kinds_def)
moreover
from ‹preds (slice_kinds S as') s'› ‹as' = ax#asx›
have "preds (slice_kinds S asx)
(transfer (slice_kind S a) s')"
by(simp add:slice_kinds_def)
moreover
from ‹length s = Suc (length cs)› ‹cs = c' # cs'›
have "length (transfer (slice_kind S a) s) = Suc (length cs')"
by(simp,simp add:‹s = cf#cfx#cfs›)
moreover
from ‹length s' = Suc (length cs)› ‹cs = c' # cs'›
have "length (transfer (slice_kind S a) s') = Suc (length cs')"
by(simp,simp add:‹s' = cf'#cfx'#cfs'›)
moreover
from IH[OF ‹upd_cs cs' as = []› ‹same_level_path_aux cs' asx›
‹∀c∈set cs'. valid_edge c› ‹targetnode a -as→* (_Low_)›
‹targetnode a -asx→* (_Low_)› rvs' snds rv' calculation] ‹as' = ax#asx›
show ?thesis by(simp add:slice_kinds_def)
qed
qed
qed
qed
lemma rv_Low_Use_Low:
assumes "m -as→⇩√* (_Low_)" and "m -as'→⇩√* (_Low_)" and "get_proc m = Main"
and "∀V ∈ rv S (CFG_node m). cf V = cf' V"
and "preds (slice_kinds S as) [(cf,undefined)]"
and "preds (slice_kinds S as') [(cf',undefined)]"
and "CFG_node (_Low_) ∈ S"
shows "∀V ∈ Use (_Low_).
state_val (transfers(slice_kinds S as) [(cf,undefined)]) V =
state_val (transfers(slice_kinds S as') [(cf',undefined)]) V"
proof(cases as)
case Nil
with ‹m -as→⇩√* (_Low_)› have "valid_node m" and "m = (_Low_)"
by(auto intro:path_valid_node simp:vp_def)
{ fix V assume "V ∈ Use (_Low_)"
moreover
from ‹valid_node m› ‹m = (_Low_)› have "(_Low_) -[]→⇩ι* (_Low_)"
by(fastforce intro:empty_path simp:intra_path_def)
moreover
from ‹valid_node m› ‹m = (_Low_)› ‹CFG_node (_Low_) ∈ S›
have "CFG_node (_Low_) ∈ HRB_slice S"
by(fastforce intro:HRB_slice_refl)
ultimately have "V ∈ rv S (CFG_node m)" using ‹m = (_Low_)›
by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def) }
hence "∀V ∈ Use (_Low_). V ∈ rv S (CFG_node m)" by simp
show ?thesis
proof(cases "L = {}")
case True with UseLow show ?thesis by simp
next
case False
from ‹m -as'→⇩√* (_Low_)› have "m -as'→* (_Low_)" by(simp add:vp_def)
from ‹m -as'→* (_Low_)› ‹m = (_Low_)› have "as' = []"
proof(induct m as' m'≡"(_Low_)" rule:path.induct)
case (Cons_path m'' as a m)
from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)›
have "targetnode a = (_Exit_)" by -(rule Exit_successor_of_Low,simp+)
with ‹targetnode a = m''› ‹m'' -as→* (_Low_)›
have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
with False have False by -(drule Low_neq_Exit,simp)
thus ?case by simp
qed simp
with Nil ‹∀V ∈ rv S (CFG_node m). cf V = cf' V›
‹∀V ∈ Use (_Low_). V ∈ rv S (CFG_node m)›
show ?thesis by(fastforce simp:slice_kinds_def)
qed
next
case (Cons ax asx)
with ‹m -as→⇩√* (_Low_)› have "sourcenode ax = m" and "valid_edge ax"
and "targetnode ax -asx→* (_Low_)"
by(auto elim:path_split_Cons simp:vp_def)
show ?thesis
proof(cases "L = {}")
case True with UseLow show ?thesis by simp
next
case False
show ?thesis
proof(cases as')
case Nil
with ‹m -as'→⇩√* (_Low_)› have "m = (_Low_)" by(fastforce simp:vp_def)
with ‹valid_edge ax› ‹sourcenode ax = m› have "targetnode ax = (_Exit_)"
by -(rule Exit_successor_of_Low,simp+)
from Low_source_Exit_edge obtain a' where "valid_edge a'"
and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
and "kind a' = (λs. True)⇩√" by blast
from ‹valid_edge ax› ‹sourcenode ax = m› ‹m = (_Low_)›
‹targetnode ax = (_Exit_)› ‹valid_edge a'› ‹sourcenode a' = (_Low_)›
‹targetnode a' = (_Exit_)›
have "ax = a'" by(fastforce dest:edge_det)
with ‹kind a' = (λs. True)⇩√› have "kind ax = (λs. True)⇩√" by simp
with ‹targetnode ax = (_Exit_)› ‹targetnode ax -asx→* (_Low_)›
have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
with False have False by -(drule Low_neq_Exit,simp)
thus ?thesis by simp
next
case (Cons ax' asx')
from ‹m -as→⇩√* (_Low_)› have "valid_path_aux [] as" and "m -as→* (_Low_)"
by(simp_all add:vp_def valid_path_def)
from this ‹as = ax#asx› ‹get_proc m = Main›
have "same_level_path_aux [] as ∧ upd_cs [] as = []"
by -(rule vpa_Main_slpa[of _ _ m "(_Low_)"],
(fastforce intro!:get_proc_Low simp:valid_call_list_def)+)
hence "same_level_path_aux [] as" and "upd_cs [] as = []" by simp_all
from ‹m -as'→⇩√* (_Low_)› have "valid_path_aux [] as'" and "m -as'→* (_Low_)"
by(simp_all add:vp_def valid_path_def)
from this ‹as' = ax'#asx'› ‹get_proc m = Main›
have "same_level_path_aux [] as' ∧ upd_cs [] as' = []"
by -(rule vpa_Main_slpa[of _ _ m "(_Low_)"],
(fastforce intro!:get_proc_Low simp:valid_call_list_def)+)
hence "same_level_path_aux [] as'" by simp
from ‹same_level_path_aux [] as› ‹upd_cs [] as = []›
‹same_level_path_aux [] as'› ‹m -as→* (_Low_)› ‹m -as'→* (_Low_)›
‹∀V ∈ rv S (CFG_node m). cf V = cf' V› ‹CFG_node (_Low_) ∈ S›
‹preds (slice_kinds S as) [(cf,undefined)]›
‹preds (slice_kinds S as') [(cf',undefined)]›
show ?thesis by -(erule slpa_rv_Low_Use_Low,auto)
qed
qed
qed
lemma nonInterference_path_to_Low:
assumes "[cf] ≈⇩L [cf']" and "(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "CFG_node (_Low_) ∈ S"
and "(_Entry_) -as→⇩√* (_Low_)" and "preds (kinds as) [(cf,undefined)]"
and "(_Entry_) -as'→⇩√* (_Low_)" and "preds (kinds as') [(cf',undefined)]"
shows "map fst (transfers (kinds as) [(cf,undefined)]) ≈⇩L
map fst (transfers (kinds as') [(cf',undefined)])"
proof -
from ‹(_Entry_) -as→⇩√* (_Low_)› ‹preds (kinds as) [(cf,undefined)]›
‹CFG_node (_Low_) ∈ S›
obtain asx where "preds (slice_kinds S asx) [(cf,undefined)]"
and "∀V ∈ Use (_Low_).
state_val (transfers (slice_kinds S asx) [(cf,undefined)]) V =
state_val (transfers (kinds as) [(cf,undefined)]) V"
and "slice_edges S [] as = slice_edges S [] asx"
and "transfers (kinds as) [(cf,undefined)] ≠ []"
and "(_Entry_) -asx→⇩√* (_Low_)"
by(erule fundamental_property_of_static_slicing)
from ‹(_Entry_) -as'→⇩√* (_Low_)› ‹preds (kinds as') [(cf',undefined)]›
‹CFG_node (_Low_) ∈ S›
obtain asx' where "preds (slice_kinds S asx') [(cf',undefined)]"
and "∀V ∈ Use (_Low_).
state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V =
state_val (transfers(kinds as') [(cf',undefined)]) V"
and "slice_edges S [] as' =
slice_edges S [] asx'"
and "transfers (kinds as') [(cf',undefined)] ≠ []"
and "(_Entry_) -asx'→⇩√* (_Low_)"
by(erule fundamental_property_of_static_slicing)
from ‹[cf] ≈⇩L [cf']› ‹(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙›
have "∀V ∈ rv S (CFG_node (_Entry_)). cf V = cf' V"
by(fastforce dest:lowEquivalence_relevant_nodes_Entry)
with ‹(_Entry_) -asx →⇩√*(_Low_)› ‹(_Entry_) -asx'→⇩√* (_Low_)›
‹CFG_node (_Low_) ∈ S› ‹preds (slice_kinds S asx) [(cf,undefined)]›
‹preds (slice_kinds S asx') [(cf',undefined)]›
have "∀V ∈ Use (_Low_).
state_val (transfers(slice_kinds S asx) [(cf,undefined)]) V =
state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V"
by -(rule rv_Low_Use_Low,auto intro:get_proc_Entry)
with ‹∀V ∈ Use (_Low_).
state_val (transfers (slice_kinds S asx) [(cf,undefined)]) V =
state_val (transfers (kinds as) [(cf,undefined)]) V›
‹∀V ∈ Use (_Low_).
state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V =
state_val (transfers(kinds as') [(cf',undefined)]) V›
‹transfers (kinds as) [(cf,undefined)] ≠ []›
‹transfers (kinds as') [(cf',undefined)] ≠ []›
show ?thesis by(fastforce simp:lowEquivalence_def UseLow neq_Nil_conv)
qed
theorem nonInterference_path:
assumes "[cf] ≈⇩L [cf']" and "(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "CFG_node (_Low_) ∈ S"
and "(_Entry_) -as→⇩√* (_Exit_)" and "preds (kinds as) [(cf,undefined)]"
and "(_Entry_) -as'→⇩√* (_Exit_)" and "preds (kinds as') [(cf',undefined)]"
shows "map fst (transfers (kinds as) [(cf,undefined)]) ≈⇩L
map fst (transfers (kinds as') [(cf',undefined)])"
proof -
from ‹(_Entry_) -as→⇩√* (_Exit_)› obtain x xs where "as = x#xs"
and "(_Entry_) = sourcenode x" and "valid_edge x"
and "targetnode x -xs→* (_Exit_)"
apply(cases "as = []")
apply(clarsimp simp:vp_def,drule empty_path_nodes,drule Entry_noteq_Exit,simp)
by(fastforce elim:path_split_Cons simp:vp_def)
from ‹(_Entry_) -as→⇩√* (_Exit_)› have "valid_path as" by(simp add:vp_def)
from ‹valid_edge x› have "valid_node (targetnode x)" by simp
hence "inner_node (targetnode x)"
proof(cases rule:valid_node_cases)
case Entry
with ‹valid_edge x› have False by(rule Entry_target)
thus ?thesis by simp
next
case Exit
with ‹targetnode x -xs→* (_Exit_)› have "xs = []"
by -(drule path_Exit_source,auto)
from Entry_Exit_edge obtain z where "valid_edge z"
and "sourcenode z = (_Entry_)" and "targetnode z = (_Exit_)"
and "kind z = (λs. False)⇩√" by blast
from ‹valid_edge x› ‹valid_edge z› ‹(_Entry_) = sourcenode x›
‹sourcenode z = (_Entry_)› Exit ‹targetnode z = (_Exit_)›
have "x = z" by(fastforce intro:edge_det)
with ‹preds (kinds as) [(cf,undefined)]› ‹as = x#xs› ‹xs = []›
‹kind z = (λs. False)⇩√›
have False by(simp add:kinds_def)
thus ?thesis by simp
qed simp
with ‹targetnode x -xs→* (_Exit_)› obtain x' xs' where "xs = xs'@[x']"
and "targetnode x -xs'→* (_Low_)" and "kind x' = (λs. True)⇩√"
by(fastforce elim:Exit_path_Low_path)
with ‹(_Entry_) = sourcenode x› ‹valid_edge x›
have "(_Entry_) -x#xs'→* (_Low_)" by(fastforce intro:Cons_path)
from ‹valid_path as› ‹as = x#xs› ‹xs = xs'@[x']›
have "valid_path (x#xs')"
by(simp add:valid_path_def del:valid_path_aux.simps)
(rule valid_path_aux_split,simp)
with ‹(_Entry_) -x#xs'→* (_Low_)› have "(_Entry_) -x#xs'→⇩√* (_Low_)"
by(simp add:vp_def)
from ‹as = x#xs› ‹xs = xs'@[x']› have "as = (x#xs')@[x']" by simp
with ‹preds (kinds as) [(cf,undefined)]›
have "preds (kinds (x#xs')) [(cf,undefined)]"
by(simp add:kinds_def preds_split)
from ‹(_Entry_) -as'→⇩√* (_Exit_)› obtain y ys where "as' = y#ys"
and "(_Entry_) = sourcenode y" and "valid_edge y"
and "targetnode y -ys→* (_Exit_)"
apply(cases "as' = []")
apply(clarsimp simp:vp_def,drule empty_path_nodes,drule Entry_noteq_Exit,simp)
by(fastforce elim:path_split_Cons simp:vp_def)
from ‹(_Entry_) -as'→⇩√* (_Exit_)› have "valid_path as'" by(simp add:vp_def)
from ‹valid_edge y› have "valid_node (targetnode y)" by simp
hence "inner_node (targetnode y)"
proof(cases rule:valid_node_cases)
case Entry
with ‹valid_edge y› have False by(rule Entry_target)
thus ?thesis by simp
next
case Exit
with ‹targetnode y -ys→* (_Exit_)› have "ys = []"
by -(drule path_Exit_source,auto)
from Entry_Exit_edge obtain z where "valid_edge z"
and "sourcenode z = (_Entry_)" and "targetnode z = (_Exit_)"
and "kind z = (λs. False)⇩√" by blast
from ‹valid_edge y› ‹valid_edge z› ‹(_Entry_) = sourcenode y›
‹sourcenode z = (_Entry_)› Exit ‹targetnode z = (_Exit_)›
have "y = z" by(fastforce intro:edge_det)
with ‹preds (kinds as') [(cf',undefined)]› ‹as' = y#ys› ‹ys = []›
‹kind z = (λs. False)⇩√›
have False by(simp add:kinds_def)
thus ?thesis by simp
qed simp
with ‹targetnode y -ys→* (_Exit_)› obtain y' ys' where "ys = ys'@[y']"
and "targetnode y -ys'→* (_Low_)" and "kind y' = (λs. True)⇩√"
by(fastforce elim:Exit_path_Low_path)
with ‹(_Entry_) = sourcenode y› ‹valid_edge y›
have "(_Entry_) -y#ys'→* (_Low_)" by(fastforce intro:Cons_path)
from ‹valid_path as'› ‹as' = y#ys› ‹ys = ys'@[y']›
have "valid_path (y#ys')"
by(simp add:valid_path_def del:valid_path_aux.simps)
(rule valid_path_aux_split,simp)
with ‹(_Entry_) -y#ys'→* (_Low_)› have "(_Entry_) -y#ys'→⇩√* (_Low_)"
by(simp add:vp_def)
from ‹as' = y#ys› ‹ys = ys'@[y']› have "as' = (y#ys')@[y']" by simp
with ‹preds (kinds as') [(cf',undefined)]›
have "preds (kinds (y#ys')) [(cf',undefined)]"
by(simp add:kinds_def preds_split)
from ‹[cf] ≈⇩L [cf']› ‹(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹CFG_node (_Low_) ∈ S›
‹(_Entry_) -x#xs'→⇩√* (_Low_)› ‹preds (kinds (x#xs')) [(cf,undefined)]›
‹(_Entry_) -y#ys'→⇩√* (_Low_)› ‹preds (kinds (y#ys')) [(cf',undefined)]›
have "map fst (transfers (kinds (x#xs')) [(cf,undefined)]) ≈⇩L
map fst (transfers (kinds (y#ys')) [(cf',undefined)])"
by(rule nonInterference_path_to_Low)
with ‹as = x#xs› ‹xs = xs'@[x']› ‹kind x' = (λs. True)⇩√›
‹as' = y#ys› ‹ys = ys'@[y']› ‹kind y' = (λs. True)⇩√›
show ?thesis
apply(cases "transfers (map kind xs') (transfer (kind x) [(cf,undefined)])")
apply (auto simp add:kinds_def transfers_split)
by((cases "transfers (map kind ys') (transfer (kind y) [(cf',undefined)])"),
(auto simp add:kinds_def transfers_split))+
qed
end
text ‹The second theorem assumes that we have a operational semantics,
whose evaluations are written ‹⟨c,s⟩ ⇒ ⟨c',s'⟩› and which conforms
to the CFG. The correctness theorem then states that if no high variable
influenced a low variable and the initial states were low equivalent, the
reulting states are again low equivalent:›
locale NonInterferenceInter =
NonInterferenceInterGraph sourcenode targetnode kind valid_edge Entry
get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses
H L High Low +
SemanticsProperty sourcenode targetnode kind valid_edge Entry get_proc
get_return_edges procs Main Exit Def Use ParamDefs ParamUses sem identifies
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind"
and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and get_proc :: "'node ⇒ 'pname"
and get_return_edges :: "'edge ⇒ 'edge set"
and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
and Exit::"'node" ("'('_Exit'_')")
and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
and ParamDefs :: "'node ⇒ 'var list" and ParamUses :: "'node ⇒ 'var set list"
and sem :: "'com ⇒ ('var ⇀ 'val) list ⇒ 'com ⇒ ('var ⇀ 'val) list ⇒ bool"
("((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [0,0,0,0] 81)
and identifies :: "'node ⇒ 'com ⇒ bool" ("_ ≜ _" [51,0] 80)
and H :: "'var set" and L :: "'var set"
and High :: "'node" ("'('_High'_')") and Low :: "'node" ("'('_Low'_')") +
fixes final :: "'com ⇒ bool"
assumes final_edge_Low: "⟦final c; n ≜ c⟧
⟹ ∃a. valid_edge a ∧ sourcenode a = n ∧ targetnode a = (_Low_) ∧ kind a = ⇑id"
begin
text‹The following theorem needs the explicit edge from ‹(_High_)›
to ‹n›. An approach using a ‹init› predicate for initial statements,
being reachable from ‹(_High_)› via a ‹(λs. True)⇩√› edge,
does not work as the same statement could be identified by several nodes, some
initial, some not. E.g., in the program \texttt{while (True) Skip;;Skip}
two nodes identify this inital statement: the initial node and the node
within the loop (because of loop unrolling).›
theorem nonInterference:
assumes "[cf⇩1] ≈⇩L [cf⇩2]" and "(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "CFG_node (_Low_) ∈ S"
and "valid_edge a" and "sourcenode a = (_High_)" and "targetnode a = n"
and "kind a = (λs. True)⇩√" and "n ≜ c" and "final c'"
and "⟨c,[cf⇩1]⟩ ⇒ ⟨c',s⇩1⟩" and "⟨c,[cf⇩2]⟩ ⇒ ⟨c',s⇩2⟩"
shows "s⇩1 ≈⇩L s⇩2"
proof -
from High_target_Entry_edge obtain ax where "valid_edge ax"
and "sourcenode ax = (_Entry_)" and "targetnode ax = (_High_)"
and "kind ax = (λs. True)⇩√" by blast
from ‹n ≜ c› ‹⟨c,[cf⇩1]⟩ ⇒ ⟨c',s⇩1⟩›
obtain n⇩1 as⇩1 cfs⇩1 where "n -as⇩1→⇩√* n⇩1" and "n⇩1 ≜ c'"
and "preds (kinds as⇩1) [(cf⇩1,undefined)]"
and "transfers (kinds as⇩1) [(cf⇩1,undefined)] = cfs⇩1" and "map fst cfs⇩1 = s⇩1"
by(fastforce dest:fundamental_property)
from ‹n -as⇩1→⇩√* n⇩1› ‹valid_edge a› ‹sourcenode a = (_High_)› ‹targetnode a = n›
‹kind a = (λs. True)⇩√›
have "(_High_) -a#as⇩1→⇩√* n⇩1" by(fastforce intro:Cons_path simp:vp_def valid_path_def)
from ‹final c'› ‹n⇩1 ≜ c'›
obtain a⇩1 where "valid_edge a⇩1" and "sourcenode a⇩1 = n⇩1"
and "targetnode a⇩1 = (_Low_)" and "kind a⇩1 = ⇑id" by(fastforce dest:final_edge_Low)
hence "n⇩1 -[a⇩1]→* (_Low_)" by(fastforce intro:path_edge)
with ‹(_High_) -a#as⇩1→⇩√* n⇩1› have "(_High_) -(a#as⇩1)@[a⇩1]→* (_Low_)"
by(fastforce intro!:path_Append simp:vp_def)
with ‹valid_edge ax› ‹sourcenode ax = (_Entry_)› ‹targetnode ax = (_High_)›
have "(_Entry_) -ax#((a#as⇩1)@[a⇩1])→* (_Low_)" by -(rule Cons_path)
moreover
from ‹(_High_) -a#as⇩1→⇩√* n⇩1› have "valid_path_aux [] (a#as⇩1)"
by(simp add:vp_def valid_path_def)
with ‹kind a⇩1 = ⇑id› have "valid_path_aux [] ((a#as⇩1)@[a⇩1])"
by(fastforce intro:valid_path_aux_Append)
with ‹kind ax = (λs. True)⇩√› have "valid_path_aux [] (ax#((a#as⇩1)@[a⇩1]))"
by simp
ultimately have "(_Entry_) -ax#((a#as⇩1)@[a⇩1])→⇩√* (_Low_)"
by(simp add:vp_def valid_path_def)
from ‹valid_edge a› ‹kind a = (λs. True)⇩√› ‹sourcenode a = (_High_)›
‹targetnode a = n›
have "get_proc n = get_proc (_High_)"
by(fastforce dest:get_proc_intra simp:intra_kind_def)
with get_proc_High have "get_proc n = Main" by simp
from ‹valid_edge a⇩1› ‹sourcenode a⇩1 = n⇩1› ‹targetnode a⇩1 = (_Low_)› ‹kind a⇩1 = ⇑id›
have "get_proc n⇩1 = get_proc (_Low_)"
by(fastforce dest:get_proc_intra simp:intra_kind_def)
with get_proc_Low have "get_proc n⇩1 = Main" by simp
from ‹n -as⇩1→⇩√* n⇩1› have "n -as⇩1→⇘sl⇙* n⇩1"
by(cases as⇩1)
(auto dest!:vpa_Main_slpa intro:‹get_proc n⇩1 = Main› ‹get_proc n = Main›
simp:vp_def valid_path_def valid_call_list_def slp_def
same_level_path_def simp del:valid_path_aux.simps)
then obtain cfx r where cfx:"transfers (map kind as⇩1) [(cf⇩1,undefined)] = [(cfx,r)]"
by(fastforce elim:slp_callstack_length_equal simp:kinds_def)
from ‹kind ax = (λs. True)⇩√› ‹kind a = (λs. True)⇩√›
‹preds (kinds as⇩1) [(cf⇩1,undefined)]› ‹kind a⇩1 = ⇑id› cfx
have "preds (kinds (ax#((a#as⇩1)@[a⇩1]))) [(cf⇩1,undefined)]"
by(auto simp:kinds_def preds_split)
from ‹n ≜ c› ‹⟨c,[cf⇩2]⟩ ⇒ ⟨c',s⇩2⟩›
obtain n⇩2 as⇩2 cfs⇩2 where "n -as⇩2→⇩√* n⇩2" and "n⇩2 ≜ c'"
and "preds (kinds as⇩2) [(cf⇩2,undefined)]"
and "transfers (kinds as⇩2) [(cf⇩2,undefined)] = cfs⇩2" and "map fst cfs⇩2 = s⇩2"
by(fastforce dest:fundamental_property)
from ‹n -as⇩2→⇩√* n⇩2› ‹valid_edge a› ‹sourcenode a = (_High_)› ‹targetnode a = n›
‹kind a = (λs. True)⇩√›
have "(_High_) -a#as⇩2→⇩√* n⇩2" by(fastforce intro:Cons_path simp:vp_def valid_path_def)
from ‹final c'› ‹n⇩2 ≜ c'›
obtain a⇩2 where "valid_edge a⇩2" and "sourcenode a⇩2 = n⇩2"
and "targetnode a⇩2 = (_Low_)" and "kind a⇩2 = ⇑id" by(fastforce dest:final_edge_Low)
hence "n⇩2 -[a⇩2]→* (_Low_)" by(fastforce intro:path_edge)
with ‹(_High_) -a#as⇩2→⇩√* n⇩2› have "(_High_) -(a#as⇩2)@[a⇩2]→* (_Low_)"
by(fastforce intro!:path_Append simp:vp_def)
with ‹valid_edge ax› ‹sourcenode ax = (_Entry_)› ‹targetnode ax = (_High_)›
have "(_Entry_) -ax#((a#as⇩2)@[a⇩2])→* (_Low_)" by -(rule Cons_path)
moreover
from ‹(_High_) -a#as⇩2→⇩√* n⇩2› have "valid_path_aux [] (a#as⇩2)"
by(simp add:vp_def valid_path_def)
with ‹kind a⇩2 = ⇑id› have "valid_path_aux [] ((a#as⇩2)@[a⇩2])"
by(fastforce intro:valid_path_aux_Append)
with ‹kind ax = (λs. True)⇩√› have "valid_path_aux [] (ax#((a#as⇩2)@[a⇩2]))"
by simp
ultimately have "(_Entry_) -ax#((a#as⇩2)@[a⇩2])→⇩√* (_Low_)"
by(simp add:vp_def valid_path_def)
from ‹valid_edge a› ‹kind a = (λs. True)⇩√› ‹sourcenode a = (_High_)›
‹targetnode a = n›
have "get_proc n = get_proc (_High_)"
by(fastforce dest:get_proc_intra simp:intra_kind_def)
with get_proc_High have "get_proc n = Main" by simp
from ‹valid_edge a⇩2› ‹sourcenode a⇩2 = n⇩2› ‹targetnode a⇩2 = (_Low_)› ‹kind a⇩2 = ⇑id›
have "get_proc n⇩2 = get_proc (_Low_)"
by(fastforce dest:get_proc_intra simp:intra_kind_def)
with get_proc_Low have "get_proc n⇩2 = Main" by simp
from ‹n -as⇩2→⇩√* n⇩2› have "n -as⇩2→⇘sl⇙* n⇩2"
by(cases as⇩2)
(auto dest!:vpa_Main_slpa intro:‹get_proc n⇩2 = Main› ‹get_proc n = Main›
simp:vp_def valid_path_def valid_call_list_def slp_def
same_level_path_def simp del:valid_path_aux.simps)
then obtain cfx' r'
where cfx':"transfers (map kind as⇩2) [(cf⇩2,undefined)] = [(cfx',r')]"
by(fastforce elim:slp_callstack_length_equal simp:kinds_def)
from ‹kind ax = (λs. True)⇩√› ‹kind a = (λs. True)⇩√›
‹preds (kinds as⇩2) [(cf⇩2,undefined)]› ‹kind a⇩2 = ⇑id› cfx'
have "preds (kinds (ax#((a#as⇩2)@[a⇩2]))) [(cf⇩2,undefined)]"
by(auto simp:kinds_def preds_split)
from ‹[cf⇩1] ≈⇩L [cf⇩2]› ‹(_High_) ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹CFG_node (_Low_) ∈ S›
‹(_Entry_) -ax#((a#as⇩1)@[a⇩1])→⇩√* (_Low_)›
‹preds (kinds (ax#((a#as⇩1)@[a⇩1]))) [(cf⇩1,undefined)]›
‹(_Entry_) -ax#((a#as⇩2)@[a⇩2])→⇩√* (_Low_)›
‹preds (kinds (ax#((a#as⇩2)@[a⇩2]))) [(cf⇩2,undefined)]›
have "map fst (transfers (kinds (ax#((a#as⇩1)@[a⇩1]))) [(cf⇩1,undefined)]) ≈⇩L
map fst (transfers (kinds (ax#((a#as⇩2)@[a⇩2]))) [(cf⇩2,undefined)])"
by(rule nonInterference_path_to_Low)
with ‹kind ax = (λs. True)⇩√› ‹kind a = (λs. True)⇩√› ‹kind a⇩1 = ⇑id› ‹kind a⇩2 = ⇑id›
‹transfers (kinds as⇩1) [(cf⇩1,undefined)] = cfs⇩1› ‹map fst cfs⇩1 = s⇩1›
‹transfers (kinds as⇩2) [(cf⇩2,undefined)] = cfs⇩2› ‹map fst cfs⇩2 = s⇩2›
show ?thesis by(cases s⇩1)(cases s⇩2,(fastforce simp:kinds_def transfers_split)+)+
qed
end
end