Sciweavers

IFIP
2010
Springer

Information Flow Analysis via Path Condition Refinement

13 years 7 months ago
Information Flow Analysis via Path Condition Refinement
We present a new approach to information flow control (IFC), ploits counterexample-guided abstraction refinement (CEGAR) technology. The CEGAR process is built on top of our existing IFC analysis in which illegal flows are characterized using program dependence graphs (PDG) and path conditions (as described in [12]). Although path ns provide an already precise abstraction that can be used to generate witnesses to the illegal flow, they may still cause false alarms. Our CEGAR process recognizes false witnesses by executing them and monitoring their executions, and eliminates them by automatically refining path conditions in an iterative way as needed. The paper sketches the foundations of CEGAR and PDG-based IFC, and describes the approach in detail. An example shows how the approach finds illegal flow, and demonstrates how CEGAR eliminates false alarms. Key words: Information flow control, CEGAR, program dependence ath condition, abstraction refinement, constraint solving
Mana Taghdiri, Gregor Snelting, Carsten Sinz
Added 18 May 2011
Updated 18 May 2011
Type Journal
Year 2010
Where IFIP
Authors Mana Taghdiri, Gregor Snelting, Carsten Sinz
Comments (0)