section ‹Example: Program Dependence Graphs›
text_raw ‹\label{sec:pdg}›

text ‹Program dependence graph (PDG) based slicing provides a very crude but direct approximation of
  characterisation. As such we can easily derive a corresponding correctness result.›

theory PDG imports IFC
begin

context IFC 
begin

text ‹We utilise our established dependencies on program paths to define the PDG. Note that PDGs
  only contain immediate control dependencies instead of the transitive ones we use here.
  as slicing is considering reachability questions this does not affect the result.›
inductive_set pdg where 
‹[i cd^π→ k] ==> (π k, π i) ∈ pdg› |
‹[i dd^π,v→ k] ==> (π k, π i) ∈ pdg›

text ‹The set of sources is the set of nodes reading high variables.›
inductive_set sources where
‹n ∈ nodes ==> h ∈ hvars ==> h ∈ reads n ==> n∈ sources›

text ‹The forward slice is the set of nodes reachable in the PDG from the set of sources. To ensure
  slicing aims to prove that no observable node is contained in the ›
inductive_set slice where
‹n∈ sources ==> n ∈ slice› |
‹m ∈ slice ==> (m,n)∈pdg ==> n ∈ slice›


text ‹As the PDG does not contain data control dependencies themselves we have to decompose these.›
lemma dcd_pdg: assumes ‹n dcd^π,v→ m via π' m'› obtains l where ‹(π m,l)∈ pdg› and ‹(l,π n)∈pdg›
proof -
  assume r: ‹(∧l. (π m, l) ∈ pdg ==> (l, π n) ∈ pdg ==> thesis)›
  obtain l' n' where ln: ‹cs^π m = cs^π' m' ∧ cs^π n = cs^π' n' ∧ n' dd^π',v→ l' ∧ l' cd^π'→ m'› using assms unfolding is_dcdi_via_def by metis
  hence  mn: ‹π' m' = π m ∧ π' n' = π n› by (metis last_cs ln) 
  have 1: ‹(π m, π' l') ∈ pdg› by (metis ln mn pdg.intros(1)) 
  have 2: ‹(π' l', π n) ∈ pdg› by (metis ln mn pdg.intros(2)) 
  show thesis using 1 2 r by auto
qed

text ‹By induction it directly follows that the slice is an approximation of the single critical paths.›
lemma scp_slice: ‹(π, i)∈ scp ==> π i ∈ slice›
  apply (induction rule: scp.induct)
     apply (simp add: path_in_nodes slice.intros(1) sources.intros)
    using pdg.intros(1) slice.intros(2) apply blast
  using pdg.intros(2) slice.intros(2) apply blast
  by (metis dcd_pdg slice.intros(2))

lemma scop_slice: ‹(π, i) ∈ scop ==> π i ∈ slice ∩ dom(att)›  by (metis IntI scop.cases scp_slice) 

text ‹The requirement targeted by slicing, that no observable node is contained in the slice,
  thereby a sound criteria for security.›
lemma pdg_correct: assumes ‹slice ∩ dom(att) = {}› shows ‹secure›
proof (rule ccontr)
  assume ‹¬ secure›
  then obtain π i where ‹(π, i) ∈ scop› using scop_correct by force 
  thus ‹False› using scop_slice assms by auto 
qed

end

end