Information Flow and. Markus Müller-Olm Westfälische Wilhelms-Universität Münster, Germany. IFIP WG 2.2 Meeting Singapore, September 13-16, PDF

Description
Information Flow and Program Analysis Markus Müller-Olm Westfälische Wilhelms-Universität Münster, Germany IFIP WG 22 Meeting Singapore, September 13-16, 2016 Project Context Work in progress from a joint

Please download to get full document.

View again

of 19
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information
Category:

Retail

Publish on:

Views: 23 | Pages: 19

Extension: PDF | Download: 0

Share
Transcript
Information Flow and Program Analysis Markus Müller-Olm Westfälische Wilhelms-Universität Münster, Germany IFIP WG 22 Meeting Singapore, September 13-16, 2016 Project Context Work in progress from a joint project with G Snelting (KIT) Information flow control for mobile components based on precise analysis of paralle programs Part of priority programme 1496 Reliably Secure Software Systems (RS3) funded by DFG (German Research Foundation) Special thanks to Benedikt Nordhoff Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, What This Talk is About Theme: How can program analysis-like technology help PDG-based information flow analysis? Program analysis: Fixpoint-based methods: data-flow analysis, abstract interpretation Information flow analysis: see next slide Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Information Flow: Example Free -App Start of App Contacts and s Ad-Server Display Reference scenario of SPP RS3: Software security for mobile devices Prototype of certifying app store for Android (Lortz et al, ) Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Non-Interference For simplicity: transformational terminating programs only Semantic setup: Variables: Var = Low High States: Σ = { σ σ : Var Val } Program semantics: π : Σ Σ Low-equivalence of states: σ L σ : σ Low = σ Low Program π is called non-interferent iff fa σ,σ Σ: σ L σ π (σ) L π (σ ) Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Possibilistic Non-Interference Semantics of non-deterministic programs: π : Σ 2 Σ Refinement: π π σ: π (σ) π (σ ) Program π is called non-interferent iff fa σ 1,σ 2 Σ: σ L σ ρ π (σ) : ρ π (σ ) : ρ L ρ Observation: Non-interference is not preserved by refinement Example: l :=? is non-interferent, its refinement l := h is not Reason: Non-interference is a hyper-property Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, A Fundamental Problem Abstraction is inherent to program analysis However, as just observed: Non-interference does not transfer from abstractions Consequence: Program analysis cannot be directly applied to non-interference Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Program Dependence Graphs (PDGs) A structure known from program slicing Nodes correspond to statements and conditions; we add artificial nodes for initial and final value of program variables Edges capture data dependences and control dependences PDGs can be applied for non-interference analysis Analysis principle: If there is no path in PDG from high input to low output then the program is non-interferent Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Direct and Indirect Flows Direct flows: l := h h:= 99 h? captured by data dependence edges in PDG l :=h Indirect flows: if h 0 then l := 0 else l := 1 captured by control dependence edges in PDG if h 0 l :=0 l :=1 Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Example 1 h? l:=h l:=h if l 0 if l 0 l :=0 l :=1 l :=0 l :=1 l! There is a path from h? to l! Hence: Program may be interferent Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Example 2 h? l:=h l:=h l:=10 l:=10 if l 0 if l 0 l :=0 l :=1 l :=0 l :=1 l! There is no path from h? to l! Hence: Program is non-interferent Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Path Conditions [Snelting] Goal: Improve precision of PDG-based dependence analysis Idea: For each path in the PDG indicating critical flow, read off a necessary condition for flow from the guards If all these conditinos are unsatisfiable, there is no flow Caveat: Requires SSA-form of programs Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Path conditions improve precision of PDGs if flag h? x:= h x :=7 if flag x:= h x:=7 l := x if (! flag) if (! flag) PDG alone: alarm + path conditions: OK flag! flag l := x l! Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Further Improvements by Data Analysis Desirable if b h? y:= h goleft := x :=h goleft := y:= h if b x:=h l := y if (goleft) l := x if (goleft) PDG + path conditions: alarm + invariant: OK l := y For left path: b goleft goleft =! b For right path:! b! goleft goleft =! b l! l := x The Show Stopper l := x := if h x:= h? if h x:= x := l := l := if (!x) if (!x) l := PDG + path conditions + invariant: unsound l! h!x x = h Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, A Glimpse on Data Flow Slicing Guiding intuition: Flow happens along PDG paths only Add new type of dependencies (data control dependencies) to avoid soundness problem Define executions along a PDG path Prove: If program has no execution along a critical PDG path, then program is non-interferent (Isabelle!) Actual analysis Generate a program whose executions correspond exactly to the executions along critical PDG paths Check by data flow analysis/abstract interpretation whether final control point is reachable Note: Approach allows to check non-interference by safety analysis! Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, A Glimpse on Data Flow Slicing: Example if b if b y:= h goleft := x :=h goleft := y:= h goleft := x :=h goleft := l := y if (goleft) l := x if (goleft) l := y if (goleft) l := x Original program l! Generated program Constant propagation on the generated program proves absence of critical information flow Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Discussion Further work: Use DPNs to help PDG-based non-interference analysis of parallel programs based on LSOD Use DPNs to help type-based non-interference analysis of parallel programs Alternative approaches: Self-composition Hyper-logics Certifying App Store Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16, Thank you! Markus Müller-Olm, WWU Münster IFIP WG 22 Meeting, Singapore,, September 13-16,
Related Search
Similar documents
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks