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 begin context IFC begin 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 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, 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 qed end end