Theory PDG

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 
our characterisation. As such we can easily derive a corresponding correctness result.

theory PDG imports IFC

context IFC 

text We utilise our established dependencies on program paths to define the PDG. Note that PDGs 
usually only contain immediate control dependencies instead of the transitive ones we use here.
However 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 
security 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

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, 
is 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