research-article

Open access

Inferring frame conditions with static correlation analysis

Authors:

Oana F. Andreescu,

Stéphane Lescuyer,

Benoît MontaguAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 47, Pages 1 - 29

https://doi.org/10.1145/3290360

Published: 02 January 2019 Publication History

Abstract

We introduce the abstract domain of correlations to denote equality relations between parts of inputs and outputs of programs. We formalise the theory of correlations, and mechanically verify their semantic properties. We design a static inter-procedural dataflow analysis for automatically inferring correlations for programs written in a first-order language equipped with algebraic data-types and arrays. The analysis, its precision and execution cost, have been evaluated on the code and functional specification of an industrial-size micro-kernel. We exploit the inferred correlations to automatically discharge two thirds of the proof obligations related to the preservation of invariants for this micro-kernel.

Supplementary Material

WEBM File (a47-montagu.webm)

Download
75.64 MB

References

[1]

Oana Andreescu, Thomas Jensen, and Stéphane Lescuyer. 2015. Dependency analysis of functional specifications with algebraic data structures. In Formal Methods and Software Engineering (LNCS), Michael Butler, Sylvain Conchon, and Fatiha Zaïdi (Eds.), Vol. 9407. Springer International Publishing, 116–133.

[2]

Oana Andreescu, Thomas Jensen, and Stéphane Lescuyer. 2016. Correlating structured inputs and outputs in functional specifications. In Software Engineering and Formal Methods (LNCS), Rocco De Nicola and Eva Kühn (Eds.), Vol. 9763. Springer International Publishing, 85–103.

[3]

Oana Fabiana Andreescu. 2017. Static analysis of functional programs with an application to the frame problem in deductive verification. Theses. Université Rennes 1. https://tel.archives- ouvertes.fr/tel- 01677897

[4]

Alexander Borgida, John Mylopoulos, and Raymond Reiter. 1995. On the frame problem in procedure specifications. IEEE Transactions on Software Engineering 21, 10 (1995), 785–798.

Digital Library

[5]

Bor-Yuh Evan Chang and K. Rustan M. Leino. 2005. Abstract Interpretation with Alien Expressions and Heap Structures. In Verification, Model Checking, and Abstract Interpretation (LNCS), Radhia Cousot (Ed.), Vol. 3385. Springer Berlin Heidelberg, Berlin, Heidelberg, 147–163.

Digital Library

[6]

Sylvain Conchon and Jean-Christophe Filliâtre. 2007. A persistent union-find data structure. In Proceedings of the 2007 Workshop on Workshop on ML (ML ’07). ACM, New York, NY, USA, 37–46.

Digital Library

[7]

Patrick Cousot and Radhia Cousot. 2002. Modular static program analysis. In Compiler Construction (LNCS), R. Nigel Horspool (Ed.), Vol. 2304. Springer Berlin Heidelberg, Berlin, Heidelberg, 159–179.

Digital Library

[8]

Manuvir Das. 2000. Unification-based pointer analysis with directional assignments. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI ’00). ACM, New York, NY, USA, 35–46.

Digital Library

[9]

Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, and Andreas Podelski. 2018. The Map Equality Domain. In VSTTE 2018, Proceedings of the 10th Working Conference on Verified Software: Theories, Tools, and Experiments (LNCS), Vol. 11294. Springer.

[10]

Azadeh Farzan and Zachary Kincaid. 2015. Compositional Recurrence Analysis. In Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design (FMCAD ’15). FMCAD Inc, Austin, TX, 57–64. http://dl.acm.org/citation.cfm? id=2893529.2893544

[11]

Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 — Where Programs Meet Provers. In Programming Languages and Systems (LNCS), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer Berlin Heidelberg, Berlin, Heidelberg, 125–128.

Digital Library

[12]

Sumit Gulwani, Ashish Tiwari, and George C. Necula. 2005. Join Algorithms for the Theory of Uninterpreted Functions. In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science (LNCS), Kamal Lodaya and Meena Mahajan (Eds.), Vol. 3328. Springer Berlin Heidelberg, Berlin, Heidelberg, 311–323.

Digital Library

[13]

John Hughes. 2007. QuickCheck testing for fun and profit. In Practical Aspects of Declarative Languages (LNCS), Michael Hanus (Ed.), Vol. 4354. Springer Berlin Heidelberg, Berlin, Heidelberg, 1–32.

Digital Library

[14]

Hugo Illous, Matthieu Lemerre, and Xavier Rival. 2017. A Relational Shape Abstract Domain. In NASA Formal Methods (LNCS), Clark Barrett, Misty Davies, and Temesghen Kahsai (Eds.), Vol. 10227. Springer International Publishing, 212–229.

[15]

Inria 2017. The Coq proof assistant reference manual. Inria. https://coq.inria.fr/distrib/current/refman/

[16]

Bertrand Jeannet, Alexey Loginov, Thomas Reps, and Mooly Sagiv. 2004. A Relational Approach to Interprocedural Shape Analysis. In Static Analysis (LNCS), Roberto Giacobazzi (Ed.), Vol. 3148. Springer Berlin Heidelberg, Berlin, Heidelberg, 246–264.

[17]

Gowtham Kaki and Suresh Jagannathan. 2014. A relational framework for higher-order shape analysis. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). ACM, New York, NY, USA, 311–324.

Digital Library

[18]

Gary A. Kildall. 1973. A unified approach to global program optimization. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’73). ACM, New York, NY, USA, 194–206.

Digital Library

[19]

Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas Reps. 2017. Compositional Recurrence Analysis Revisited. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM, New York, NY, USA, 248–262.

Digital Library

[20]

Kevin Knight. 1989. Unification: a multidisciplinary survey. Comput. Surveys 21, 1 (March 1989), 93–124.

Digital Library

[21]

Gary T. Leavens, Albert L. Baker, and Clyde Ruby. 2006. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. SIGSOFT Softw. Eng. Notes 31, 3 (May 2006), 1–38.

Digital Library

[22]

Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. 2017. The Objective Caml system, documentation and user’s manual – release 4.06. INRIA. http://caml.inria.fr/pub/docs/manual- ocaml- 4.06/

[23]

Stéphane Lescuyer. 2015. ProvenCore: towards a verified isolation micro-kernel. In International Workshop on MILS: Architecture and Assurance for Secure Systems.

[24]

Ondvrej Lhoták and Laurie Hendren. 2003. Scaling Java points-to analysis using Spark. In Compiler Construction (LNCS), Görel Hedin (Ed.), Vol. 2622. Springer Berlin Heidelberg, Berlin, Heidelberg, 153–169.

Digital Library

[25]

J. McCarthy and P. J. Hayes. 1981. Some Philosophical Problems from the Standpoint of Artificial Intelligence. In Readings in Artificial Intelligence, Bonnie Lynn Webber and Nils J. Nilsson (Eds.). Morgan Kaufmann, 431–450.

[26]

Bertrand Meyer. 2015. Framing the frame problem. In Dependable Software Systems Engineering. 193–203.

[27]

Greg Nelson and Derek C. Oppen. 1980. Fast decision procedures based on congruence closure. J. ACM 27, 2 (April 1980), 356–364.

Digital Library

[28]

Flemming Nielson, Hanne R. Nielson, and Chris Hankin. 2010. Principles of Program Analysis. Springer Publishing Company, Incorporated.

[29]

Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’08). ACM, New York, NY, USA, 159–169.

Digital Library

[30]

Bjarne Steensgaard. 1996. Points-to analysis in almost linear time. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’96). ACM, New York, NY, USA, 32–41.

Digital Library

[31]

Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2017. Refinement Reflection: Complete Verification with SMT. Proceedings of the ACM on Programming Languages 2, POPL, Article 53 (Dec. 2017), 31 pages.

Digital Library

[32]

John Whaley and Monica S. Lam. 2002. An efficient inclusion-based points-to analysis for strictly-typed languages. In Static Analysis (LNCS), Manuel V. Hermenegildo and Germán Puebla (Eds.), Vol. 2477. Springer Berlin Heidelberg, Berlin, Heidelberg, 180–195.

Digital Library

Cited By

Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z
Bautista SJensen TMontagu B(2022)Lifting Numeric Relational Domains to Algebraic Data TypesStatic Analysis10.1007/978-3-031-22308-2_6(104-134)Online publication date: 5-Dec-2022
https://dl.acm.org/doi/10.1007/978-3-031-22308-2_6
Montagu BJensen T(2020)Stable relations and abstract interpretation of higher-order programsProceedings of the ACM on Programming Languages10.1145/34090014:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3409001

Index Terms

Inferring frame conditions with static correlation analysis
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
      2. Program verification

Recommendations

Source language representation of function summaries in static analysis
ICOOOLPS '16: Proceedings of the 11th Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems

Static analysis is a popular method to find bugs. In context-sensitive static analysis the analyzer considers the calling context when evaluating a function call. This approach makes it possible to find bugs that span across multiple functions. In order ...
Machine-learning-guided selectively unsound static analysis
ICSE '17: Proceedings of the 39th International Conference on Software Engineering

We present a machine-learning-based technique for selectively applying unsoundness in static analysis. Existing bug-finding static analyzers are unsound in order to be precise and scalable in practice. However, they are uniformly unsound and hence at ...
Machine-Learning-Guided Typestate Analysis for Static Use-After-Free Detection
ACSAC '17: Proceedings of the 33rd Annual Computer Security Applications Conference

Typestate analysis relies on pointer analysis for detecting temporal memory safety errors, such as use-after-free (UAF). For large programs, scalable pointer analysis is usually imprecise in analyzing their hard "corner cases", such as infeasible paths, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Check for updates

Badges

Artifacts Evaluated & Functional

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
573
Total Downloads

Downloads (Last 12 months)64
Downloads (Last 6 weeks)3

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z
Bautista SJensen TMontagu B(2022)Lifting Numeric Relational Domains to Algebraic Data TypesStatic Analysis10.1007/978-3-031-22308-2_6(104-134)Online publication date: 5-Dec-2022
https://dl.acm.org/doi/10.1007/978-3-031-22308-2_6
Montagu BJensen T(2020)Stable relations and abstract interpretation of higher-order programsProceedings of the ACM on Programming Languages10.1145/34090014:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3409001

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents