Bernhard Beckert
ABSTRACT
Regression verification and checking for illicit information flow in programs are probably the two most prominent instances of so-called relational program reasoning. Regression verification is concerned with proving that two programs behave either equally or differently in a formally specified manner; information-flow checking aims to establish that an attacker cannot distinguish executions of a program that vary in a part of the initial state designated as secret. While the theoretical connections between the two problems are well understood, there are also subtle but significant pragmatic differences. This paper reports the results of an experiment to adapt a state-of-the-art deductive information-flow verification system for Java to the problem of regression verification.
- Ammann, P., and Offutt, J. Introduction to Software Testing, first ed. Cambridge University Press, New York, NY, USA, 2008. Google Scholar
Digital Library
- Barthe, G., Crespo, J. M., and Kunz, C. Relational verification using product programs. In FM 2011 (2011), vol. 6664 of LNCS, Springer, pp. 200--214. Google ScholarDigital Library
- Barthe, G., D'Argenio, P. R., and Rezk, T. Secure information flow by self-composition. CSFW '04, IEEE CS, pp. 100--115. Google ScholarDigital Library
- Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P. H., and Ulbrich, M. Information flow in object-oriented software. In LOPSTR 2013, Revised Selected Papers (2014), vol. 8901 of LNCS, Springer, pp. 19--37.Google ScholarCross Ref
- Beckert, B., Hähnle, R., and Schmitt, P. H., Eds. Verification of Object-Oriented Software: The KeY Approach, vol. 4334 of LNCS. Springer, 2007. Google ScholarDigital Library
- Bubel, R., Hähnle, R., and Weiss, B. Abstract interpretation of symbolic execution with explicit state updates. In FMCO (2008), pp. 247--277.Google Scholar
- Darvas, Á., Hähnle, R., and Sands, D. A theorem proving approach to analysis of secure information flow. In SPC 2005 (2005), vol. 3450 of LNCS, Springer, pp. 193--209. Google ScholarDigital Library
- Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., and Ulbrich, M. Automating regression verification. In ASE 2014 (2014), ACM, pp. 349--360. Google ScholarDigital Library
- Godlin, B., and Strichman, O. Regression verification: proving the equivalence of similar programs. JSTVR 23, 3 (2013), 241--258.Google Scholar
- Hammer, C., Krinke, J., and Snelting, G. Information flow control for Java based on path conditions in dependence graphs. In ISSSE (March 2006), IEEE, pp. 87--96.Google Scholar
- Harel, D., Kozen, D., and Tiuryn, J. Dynamic Logic. MIT Press, 2000. Google ScholarDigital Library
- Hawblitzel, C., Kawaguchi, M., Lahiri, S. K., and Rebêlo, H. Towards modularly comparing programs using automated theorem provers. In CADE-24 (2013), vol. 7898 of LNCS, Springer, pp. 282--299. Google ScholarDigital Library
- Hoare, C. A. R. An axiomatic basis for computer programming. Communications of the ACM 12, 10 (Oct. 1969), 576--580. Google ScholarDigital Library
- Klebanov, V. Precise quantitative information flow analysis -- a symbolic approach. Theoretical Computer Science 538, 0 (2014), 124--139.Google ScholarCross Ref
- Leavens, G. T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D. M., and Dietl, W. JML Reference Manual, 2008.Google Scholar
- Myers, A. C. JFlow: Practical mostly-static information flow control. In POPL (1999), pp. 228--241. Google ScholarDigital Library
- Nanevski, A., Banerjee, A., and Garg, D. Verification of information flow and access control policies with dependent types. In SP (2011), pp. 165--179. Google ScholarDigital Library
- Sabelfeld, A., and Myers, A. C. Language-based information-flow security. IEEE J. Sel. Areas Commun. 21, 1 (2003), 5--19. Google ScholarDigital Library
- Scheben, C. Program-level Specification and Deductive Verification of Security Properties. PhD thesis, Karlsruhe Institute of Technology, 2014.Google Scholar
- Scheben, C., and Schmitt, P. H. Verification of information flow properties of Java programs without approximations. In FoVeOOS 2011, Revised Selected Papers (2011), vol. 7421 of LNCS, Springer, pp. 232--249. Google ScholarDigital Library
- Scheben, C., and Schmitt, P. H. Efficient self-composition for weakest precondition calculi. In FM 2014 (2014), vol. 8442 of LNCS, Springer, pp. 579--594.Google ScholarDigital Library
- Verdoolaege, S., Janssens, G., and Bruynooghe, M. Equivalence checking of static affine programs using widening to handle recurrences. In CAV 2009 (2009), vol. 5643 of LNCS, Springer, pp. 599--613. Google ScholarDigital Library
- Welsch, Y., and Poetzsch-Heffter, A. Verifying backwards compatibility of object-oriented libraries using Boogie. In FTfJP 14 (2012), FTfJP '12, ACM, pp. 35--41. Google ScholarDigital Library
Index Terms
- Regression verification for Java using a secure information flow calculus
Recommendations
Automating regression verification
ASE '14: Proceedings of the 29th ACM/IEEE International Conference on Automated Software EngineeringRegression verification is an approach complementing regression testing with formal verification. The goal is to formally prove that two versions of a program behave either equally or differently in a precisely specified way. In this paper, we present a ...
Automating regression verification of pointer programs by predicate abstraction
Regression verification is an approach complementing regression testing with formal verification. The goal is to formally prove that two versions of a program behave either equally or differently in a precisely specified way. In this paper, we present a ...
Using DEv-PROMELA for Modelling and Verification of Software
SIGSIM-PADS '16: Proceedings of the 2016 ACM SIGSIM Conference on Principles of Advanced Discrete SimulationEfficient modelling and verification of models need an accurate representation of systems. Especially, PROMELA cannot represent time as quantitative properties. That means some properties depending on time cannot be checked with SPIN model-checker. ...
Comments