Abstract
We present a new approach to information flow control (IFC), which exploits 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 conditions 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: SPIN Workshop on Model Checking of Software, pp. 103–122 (2001)
Barthe, G., Beringer, L., Crégut, P., Grégoire, B., Hofmann, M.O., Müller, P., Poll, E., Puebla, G., Stark, I., Vétillard, E.: Mobius: Mobility, ubiquity, security. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 10–29. Springer, Heidelberg (2007)
Barthe, G., Nieto, L.P.: Secure information flow for a concurrent language with scheduling. Journal of Computer Security 15(6), 647–689 (2007)
Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294–298. Springer, Heidelberg (2008)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The mathSAT 4 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Cytron, R., Ferrante, J., Rosen, B., et al.: Efficiently computing static single assignment and control dependence graph. TOPLAS 13(4), 451–490 (1991)
Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Giffhorn, D., Hammer, C.: Precise slicing of concurrent programs, an evaluation of precise slicing algorithms for concurrent programs. JASE 16(2), 197–234 (2009)
Hammer, C.: Information Flow Control for Java, A Comprehensive Approach on Path Conditions in Dependence Graphs. PhD thesis, Universität Karlsruhe (2009)
Hammer, C.: Experiences with PDG-based IFC. In: Massacci, F., Wallach, D., Zannone, N. (eds.) ESSoS 2010. LNCS, vol. 5965, pp. 44–60. Springer, Heidelberg (2010)
Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. J. of Information Security 8(6), 399–422 (2009)
Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002)
Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, pp. 79–90. ACM, New York (2006)
Jackson, D.: Hazards of verification. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, p. 1. Springer, Heidelberg (2009)
Krinke, J.: Context-sensitive slicing of concurrent programs. In: ESEC/FSE 2003, pp. 178–187. ACM, New York (2003)
Krinke, J.: Program slicing. In: Handbook of Software Engineering and Knowledge Engineering. Recent Advances, vol. 3. World Scientific Publishing, Singapore (2005)
Myers, A.C.: JFlow: practical mostly-static information flow control. In: POPL 1999, pp. 228–241. ACM Press, New York (1999)
Podelski, A., Rybalchenko, A.: Armc: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2006)
Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1) (January 2003)
Seghir, M., Podelski, A., Wies, T.: Abstraction refinement for quantified array assertions. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 3–18. Springer, Heidelberg (2009)
Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: POPL 1998, San Diego, CA, pp. 355–364 (January 1998)
Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. TOSEM 15(4), 410–457 (2006)
Taghdiri, M., Jackson, D.: Inferring specifications to detect errors in code. Journal of Automated Software Engineering 14(1), 87–121 (2007)
Tripp, O., Pistoia, M., Fink, S., Sridharan, M., Weismani, O.: TAJ: effective taint analysis of web applications. In: PLDI 2009, pp. 87–97. ACM, New York (2009)
Wasserrab, D., Lohner, D.: Proving information flow noninterference by reusing a machine-checked correctness proof for slicing. In: VERIFY 2010 (2010)
Wasserrab, D., Lohner, D., Snelting, G.: On PDG-based noninterference and its modular proof. In: PLAS 2009. ACM, New York (2009)
Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker. In: DATE 2003, pp. 10880–10886 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Taghdiri, M., Snelting, G., Sinz, C. (2011). Information Flow Analysis via Path Condition Refinement. In: Degano, P., Etalle, S., Guttman, J. (eds) Formal Aspects of Security and Trust. FAST 2010. Lecture Notes in Computer Science, vol 6561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19751-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-19751-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19750-5
Online ISBN: 978-3-642-19751-2
eBook Packages: Computer ScienceComputer Science (R0)