Article

Efficient Self-composition for Weakest Precondition Calculi

Authors:

Christoph Scheben,

Peter H. SchmittAuthors Info & Claims

Proceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 8442

Pages 579 - 594

https://doi.org/10.1007/978-3-319-06410-9_39

Published: 12 May 2014 Publication History

Abstract

This paper contributes to deductive verification of language based secure information flow. A popular approach in this area is self-composition in combination with off-the-shelf software verification systems to check for secure information flow. This approach is appealing, because 1 it is highly precise and 2 existing sophisticated software verification systems can be harnessed. On the other hand, self-composition is commonly considered to be inefficient.

We show how the efficiency of self-composition style reasoning can be increased. It is sufficient to consider programs only once, if the used verification technique is based on a weakest precondition calculus with an explicit heap model. Additionally, we show that in many cases the number of final symbolic states to be considered can be reduced considerably. Finally, we propose a comprehensive solution of the technical problem of applying software contracts within the self-composition approach. So far this problem had only been solved partially.

References

[1]

Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: Proceedings POPL, pp. 91---102. ACM 2006

Digital Library

[2]

Amtoft, T., Banerjee, A.: Verification condition generation for conditional information flow. In: Proceedings of the 2007 ACM Workshop on Formal Methods in Security Engineering, FMSE 2007, pp. 2---11. ACM, New York 2007

Digital Library

[3]

Amtoft, T., Hatcliff, J., Rodríguez, E.: Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays. In: Gordon, A.D. ed. ESOP 2010. LNCS, vol. 6012, pp. 43---63. Springer, Heidelberg 2010

Digital Library

[4]

Amtoft, T., Hatcliff, J., Rodríguez, E., Robby, Hoag, J., Greve, D.A.: Specification and checking of software contracts for conditional information flow. In: Cuellar, J., Maibaum, T., Sere, K. eds. FM 2008. LNCS, vol. 5014, pp. 229---245. Springer, Heidelberg 2008

Digital Library

[5]

Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. eds. FM 2011. LNCS, vol. 6664, pp. 200---214. Springer, Heidelberg 2011

Digital Library

[6]

Barthe, G., D'Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE Workshop on Computer Security Foundations, CSFW 2004, pp. 100---115. IEEE CS, Washington 2004

Digital Library

[7]

Bubel, R., Hähnle, R., Weiβ, B.: Abstract interpretation of symbolic execution with explicit state updates. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. eds. FMCO 2008. LNCS, vol. 5751, pp. 247---277. Springer, Heidelberg 2009

Digital Library

[8]

Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. eds. SPC 2005. LNCS, vol. 3450, pp. 193---209. Springer, Heidelberg 2005

Digital Library

[9]

Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 188, 453---457 1975

Digital Library

[10]

Dufay, G., Felty, A., Matwin, S.: Privacy-sensitive information flow with JML. In: Nieuwenhuis, R. ed. CADE 2005. LNCS LNAI, vol. 3632, pp. 116---130. Springer, Heidelberg 2005

Digital Library

[11]

Hammer, C., Krinke, J., Snelting, G.: Information flow control for Java based on path conditions in dependence graphs. In: IEEE International Symposium on Secure Software Engineering ISSSE 2006, pp. 87---96. IEEE March 2006

[12]

Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188, pp. 102---116. Springer 1971

[13]

McCarthy, J.: Towards a mathematical science of computation. In: Information Processing, pp. 21---28 1962

[14]

Myers, A.C.: JFlow: Practical mostly-static information flow control. In: POPL, pp. 228---241 1999

Digital Library

[15]

Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: 2011 IEEE Symposium on Security and Privacy SP, pp. 165---179 May 2011

Digital Library

[16]

Naumann, D.A.: From coupling relations to mated invariants for checking information flow. In: Gollmann, D., Meier, J., Sabelfeld, A. eds. ESORICS 2006. LNCS, vol. 4189, pp. 279---296. Springer, Heidelberg 2006

Digital Library

[17]

Pan, J.: A theorem proving approach to analysis of secure information flow using data abstraction. Master's thesis, Dept. of Computer Science and Engineering, Chalmers U. of Technology 2005

[18]

Phan, Q.-S.: Self-composition by symbolic execution. In: Imperial College Computing Student Workshop ICCSW 2013, pp. 95---102, Schloss Dagstuhl 2013

[19]

Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.2. Tr, U. of Iowa 2006

[20]

Scheben, C., Schmitt, P.H.: Verification of information flow properties of Java programs without approximations. In: Beckert, B., Damiani, F., Gurov, D. eds. FoVeOOS 2011. LNCS, vol. 7421, pp. 232---249. Springer, Heidelberg 2012

Digital Library

[21]

van Delft, B.: Abstraction, objects and information flow analysis. Master's thesis, Institute for Computing and Information Science, Radboud Uni Nijmegen 2011

Cited By

Blatter LKosmatov NPrevosto VLe Gall P(2022)An Efficient VCGen-Based Modular Verification of Relational PropertiesLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_28(498-516)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19849-6_28
Blatter LKosmatov NPrevosto VLe Gall P(2022)Certified Verification of Relational PropertiesIntegrated Formal Methods10.1007/978-3-031-07727-2_6(86-105)Online publication date: 7-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-07727-2_6
Klebanov VRümmer PUlbrich M(2018)Automating regression verification of pointer programs by predicate abstractionFormal Methods in System Design10.1007/s10703-017-0293-852:3(229-259)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10703-017-0293-8
Show More Cited By

Recommendations

Weakest precondition based verification tool that models spatial ordering

Weakest precondition based method for specification and verification of geographically distributed system is described. For this purpose spatial predicates have been defined. A distributed mutual exclusion algorithm is proposed and is used to illustrate ...
Weakest precondition based modelling and verification of a class of concurrent systems

A weakest precondition based modelling and verification technique for a class of concurrent systems is proposed. A system in this class is defined by a set of non-terminating interactive sequential processes. The constituent processes are allowed to ...
Counterexample-Guided precondition inference
ESOP'13: Proceedings of the 22nd European conference on Programming Languages and Systems

The precondition for an assertion inside a procedure is useful for understanding, verifying and debugging programs. As the procedure might be used in multiple calling-contexts within a program, the precondition should be sufficiently general to enable ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Proceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 8442

May 2014

748 pages

ISBN:9783319064093

Editors:
Cliff Jones
School of Computing Science, Newcastle University, Newcastle, UK
,
Pekka Pihlajasaari
Data Abstraction Pty Ltd., Johannesburg, South Africa
,
Jun Sun
Information System Technology and Design, Singapore University of Technology and Design, Singapore

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 12 May 2014

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Blatter LKosmatov NPrevosto VLe Gall P(2022)An Efficient VCGen-Based Modular Verification of Relational PropertiesLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_28(498-516)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19849-6_28
Blatter LKosmatov NPrevosto VLe Gall P(2022)Certified Verification of Relational PropertiesIntegrated Formal Methods10.1007/978-3-031-07727-2_6(86-105)Online publication date: 7-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-07727-2_6
Klebanov VRümmer PUlbrich M(2018)Automating regression verification of pointer programs by predicate abstractionFormal Methods in System Design10.1007/s10703-017-0293-852:3(229-259)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10703-017-0293-8
Beckert BKlebanov VUlbrich MMonahan R(2015)Regression verification for Java using a secure information flow calculusProceedings of the 17th Workshop on Formal Techniques for Java-like Programs10.1145/2786536.2786544(1-6)Online publication date: 7-Jul-2015
https://dl.acm.org/doi/10.1145/2786536.2786544
Dörre FKlebanov V(2015)Pseudo-Random Number Generator VerificationRevised Selected Papers of the 7th International Conference on Verified Software: Theories, Tools, and Experiments - Volume 959310.1007/978-3-319-29613-5_4(61-72)Online publication date: 18-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-29613-5_4

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents