We present a new approach to information ﬂow control (IFC), which exploits counterexample-guided abstraction reﬁnement (CEGAR) technology. The CEGAR process is built on top of our existing IFC analysis in which illegal ﬂows are characterized using program dependence graphs (PDG) and path conditions (as described in ). Although path conditions provide an already precise abstraction that can be used to generate witnesses to the illegal ﬂow, they may still cause false alarms. Our CEGAR process recognizes false witnesses by executing them and monitoring their executions, and eliminates them by automatically reﬁning 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 ﬁnds illegal ﬂow, and demonstrates how CEGAR eliminates false alarms.
Information flow analysis via path condition refinement
Mana Taghdiri, Gregor Snelting, Carsten Sinz
Formal Aspects of Security and Trust (FAST), 2010