More Web Proxy on the site http://driver.im/

Article

ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs

Authors:

Atsushi Igarashi,

Naoki KobayashiAuthors Info & Claims

Programming Languages and Systems: 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings

Pages 684 - 714

https://doi.org/10.1007/978-3-030-44914-8_25

Published: 27 April 2020 Publication History

Abstract

We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.

References

[1]

Ahmed, A., Fluet, M., Morrisett, G.: L

^{3}

: a linear language with locations. Fundamenta Informaticae 77(4), 397–449 (2007)

[2]

Aiken, A., Foster, J.S., Kodumal, J., Terauchi, T.: Checking and inferring local non-aliasing. In: Conference on Programming Language Design and Implementation (PLDI). pp. 129–140 (2003).

[3]

Amtoft, T., Turbak, F.: Faithful translations between polyvariant flows and polymorphic types. In: European Symposium on Programming (ESOP). pp. 26–40. Springer (2000).

[4]

Bakst, A., Jhala, R.: Predicate abstraction for linked data structures. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 65–84. Springer, Berlin Heidelberg (2016).

[5]

Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Communications of the ACM 54(7), 68–76 (2011).

[6]

Banerjee, A.: A modular, polyvariant and type-based closure analysis. In: International Conference on Functional Programming (ICFP), pp. 1–10 (1997).

[7]

Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Communications of the ACM 54(6), 81–91 (2011).

[8]

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)

[9]

Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS) 33(2), 8:1–845 (2011).

[10]

Bhargavan, K., Bond, B., Delignat-Lavaud, A., Fournet, C., Hawblitzel, C., Hriţcu, C., Ishtiaq, S., Kohlweiss, M., Leino, R., Lorch, J., Maillard, K., Pan, J., Parno, B., Protzenko, J., Ramananandro, T., Rane, A., Rastogi, A., Swamy, N., Thompson, L., Wang, P., Zanella-Béguelin, S., Zinzindohoué, J.K.: Everest: Towards a verified, drop-in replacement of HTTPS. In: Summit on Advances in Programming Languages (SNAPL 2017). pp. 1:1–1:12. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017).

[11]

Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Symposium on Principles of Programming Languages (POPL). pp. 259–270 (2005).

[12]

Boyland, J.: Checking interference with fractional permissions. In: Symposion on Static Analysis (SAS). pp. 55–72. Springer (2003).

[13]

Champion, A., Kobayashi, N., Sato, R.: HoIce: An ICE-based non-linear Horn clause solver. In: Asian Symposium on Programming Languages and Systems (APLAS). pp. 146–156. Springer (2018).

[14]

Chugh, R., Herman, D., Jhala, R.: Dependent types for JavaScript. In: Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA). pp. 587–606 (2012).

[15]

Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: European Symposium on Programming (ESOP). pp. 21–30. Springer (2005).

[16]

De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 337–340. Springer (2008).

[17]

Degen, M., Thiemann, P., Wehr, S.: Tracking linear and affine resources with JAVA(X). In: European Conference on Object-Oriented Programming (ECOOP). pp. 550–574. Springer (2007).

[18]

DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Conference on Programming Language Design and Implementation (PLDI), pp. 59–69 (2001).

[19]

Fähndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: Conference on Programming Language Design and Implementation (PLDI), pp. 13–24 (2002).

[20]

Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. ACM Transactions on Software Engineering and Methodology (TOSEM) 17(2), 91–934 (2008).

[21]

Flanagan, C.: Hybrid type checking. In: Symposium on Principles of Programming Languages (POPL). pp. 245–256 (2006).

[22]

Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Conference on Programming Language Design and Implementation (PLDI). pp. 234–245 (2002).

[23]

Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Conference on Programming Language Design and Implementation (PLDI). pp. 1–12 (2002).

[24]

Freeman, T., Pfenning, F.: Refinement types for ML. In: Conference on Programming Language Design and Implementation (PLDI). pp. 268–277 (1991).

[25]

Gilray, T., Might, M.: A survey of polyvariance in abstract interpretations. In: Symposium on Trends in Functional Programming. pp. 134–148. Springer (2013).

[26]

Gordon, C.S., Ernst, M.D., Grossman, D.: Rely-guarantee references for refinement types over aliased mutable data. In: Conference on Programming Language Design and Implementation (PLDI). pp. 73–84 (2013).

[27]

Gordon, C.S., Ernst, M.D., Grossman, D., Parkinson, M.J.: Verifying invariants of lock-free data structures with rely-guarantee and refinement types. ACM Transactions on Programming Languages and Systems (TOPLAS) bf 39(3), 11:1–11:54 (2017).

[28]

Hardekopf, B., Wiedermann, B., Churchill, B., Kashyap, V.: Widening for control-flow. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 472–491 (2014).

[29]

Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S., Zill, B.: IronFleet: proving practical distributed systems correct. In: Symposium on Operating Systems Principles (SOSP). pp. 1–17. ACM (2015).

[30]

Heule, S., Kassios, I.T., Müller, P., Summers, A.J.: Verification condition generation for permission logics with abstract predicates and abstraction functions. In: European Conference on Object-Oriented Programming (ECOOP). pp. 451–476. Springer (2013).

[31]

Heule, S., Leino, K.R.M., Müller, P., Summers, A.J.: Abstract read permissions: Fractional permissions without the fractions. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 315–334 (2013).

[32]

Kahsai, T., Kersten, R., Rümmer, P., Schäf, M.: Quantified heap invariants for object-oriented programs. In: Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). pp. 368–384 (2017)

[33]

Kahsai, T., Rümmer, P., Sanchez, H., Schäf, M.: JayHorn: A framework for verifying Java programs. In: Conference on Computer Aided Verification (CAV). pp. 352–358. Springer (2016).

[34]

Kashyap, V., Dewey, K., Kuefner, E.A., Wagner, J., Gibbons, K., Sarracino, J., Wiedermann, B., Hardekopf, B.: JSAI: a static analysis platform for JavaScript. In: Conference on Foundations of Software Engineering (FSE). pp. 121–132 (2014).

[35]

Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In: Conference on Programming Language Design and Implementation (PLDI). pp. 304–315 (2009).

[36]

Kloos, J., Majumdar, R., Vafeiadis, V.: Asynchronous liquid separation types. In: European Conference on Object-Oriented Programming (ECOOP). pp. 396–420. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015).

[37]

Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Conference on Computer Aided Verification (CAV). pp. 846–862. Springer (2013).

[38]

Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). pp. 348–370. Springer (2010).

[39]

Leino, K.R.M., Müller, P., Smans, J.: Deadlock-free channels and locks. In: European Symposium on Programming (ESOP). pp. 407–426. Springer-Verlag (2010).

[40]

Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. In: European Symposium on Programming (ESOP). Springer (2020)

[41]

Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for Java. ACM Transactions on Software Engineering and Methodology (TOSEM) 14(1), 1–41 (2005).

[42]

Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 41–62. Springer-Verlag (2016).

[43]

Pierce, B.C.: Types and programming languages. MIT press (2002)

[44]

Protzenko, J., Zinzindohoué, J.K., Rastogi, A., Ramananandro, T., Wang, P., Zanella-Béguelin, S., Delignat-Lavaud, A., Hriţcu, C., Bhargavan, K., Fournet, C., Swamy, N.: Verified low-level programming embedded in F*. Proceedings of the ACM on Programming Languages 1(ICFP), 17:1–17:29 (2017).

[45]

Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science (LICS). pp. 55–74. IEEE (2002).

[46]

Rondon, P., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: Symposium on Principles of Programming Languages (POPL). pp. 131–144 (2010).

[47]

Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Conference on Programming Language Design and Implementation (PLDI). pp. 159–169 (2008).

[48]

Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Conference on Computer Aided Verification (CAV). pp. 347–363. Springer (2013).

[49]

Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, chap. 7, pp. 189–223. Prentice Hall (1981)

[50]

Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis, Carnegie Mellon University (1991)

[51]

Smaragdakis, Y., Bravenboer, M., Lhoták, O.: Pick your contexts well: Understanding object-sensitivity. In: Symposium on Principles of Programming Languages (POPL). pp. 17–30 (2011).

[52]

Smith, F., Walker, D., Morrisett, G.: Alias types. In: European Symposium on Programming (ESOP). pp. 366–381. Springer (2000).

[53]

Späth, J., Ali, K., Bodden, E.: Context-, flow-, and field-sensitive data-flow analysis using synchronized pushdown systems. Proceedings of the ACM on Programming Languages 3(POPL), 48:1–48:29 (2019).

[54]

Späth, J., Nguyen Quang Do, L., Ali, K., Bodden, E.: Boomerang: Demand-driven flow-and context-sensitive pointer analysis for Java. In: European Conference on Object-Oriented Programming (ECOOP). pp. 22:1–22:26. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016).

[55]

Suenaga, K., Fukuda, R., Igarashi, A.: Type-based safe resource deallocation for shared-memory concurrency. In: Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA). pp. 1–20 (2012).

[56]

Suenaga, K., Kobayashi, N.: Fractional ownerships for safe memory deallocation. In: Asian Symposium on Programming Languages and Systems (APLAS). pp. 128–143. Springer (2009).

[57]

Swamy, N., Hriţcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoué, J.K., Zanella-Béguelin, S.: Dependent types and multi-monadic effects in F*. In: Symposium on Principles of Programming Languages (POPL). pp. 256–270 (2016).

[58]

Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. In: Conference on Programming Language Design and Implementation (PLDI). pp. 387–398 (2013).

[59]

Terauchi, T.: Checking race freedom via linear programming. In: Conference on Programming Language Design and Implementation (PLDI). pp. 1–10 (2008).

[60]

Toman, J., Siqi, R., Suenaga, K., Igarashi, A., Kobayashi, N.: Consort: Context- and flow-sensitive ownership refinement types for imperative programs. https://arxiv.org/abs/2002.07770 (2020)

[61]

Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Conference on Principles and Practice of Declarative Programming (PPDP). pp. 277–288. ACM (2009).

[62]

Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: European Symposium on Programming (ESOP). pp. 209–228. Springer (2013).

[63]

Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for Haskell. In: International Conference on Functional Programming (ICFP). pp. 269–282 (2014).

[64]

Wells, J.B., Dimock, A., Muller, R., Turbak, F.: A calculus with polymorphic and polyvariant flow types. Journal of Functional Programming 12(3), 183–227 (2002).

[65]

Xi, H., Pfenning, F.: Dependent types in practical programming. In: Symposium on Principles of Programming Languages (POPL). pp. 214–227. ACM (1999).

[66]

Zave, P.: Using lightweight modeling to understand Chord. ACM SIGCOMM Computer Communication Review 42(2), 49–57 (2012).

[67]

Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). pp. 295–314. Springer (2013).

Cited By

Kobayashi N(2025)On Decidable and Undecidable Extensions of Simply Typed Lambda CalculusProceedings of the ACM on Programming Languages10.1145/37048759:POPL(1136-1166)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704875
Simonnet JLemerre MSighireanu M(2024)A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level CodeProceedings of the ACM on Programming Languages10.1145/36897128:OOPSLA2(30-59)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689712
Tanaka ISakayori KKobayashi NKeller GWang M(2024)Ownership Types for Verification of Programs with Pointer ArithmeticProceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3635800.3636965(94-106)Online publication date: 11-Jan-2024
https://dl.acm.org/doi/10.1145/3635800.3636965
Show More Cited By

Index Terms

ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
1. Software and its engineering
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Index terms have been assigned to the content through auto-classification.

Recommendations

Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems

Precise static analyses are context-, field- and flow-sensitive. Context- and field-sensitivity are both expressible as context-free language (CFL) reachability problems. Solving both CFL problems along the same data-flow path is undecidable, which is ...
Ownership transfer in universe types
OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications

Ownership simplifies reasoning about object-oriented programs by controlling aliasing and modifications of objects. Several type systems have been proposed to express and check ownership statically.

For ownership systems to be practical, they must allow ...
On-demand strong update analysis via value-flow refinement
FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

We present a new Strong UPdate Analysis for C programs, called Supa, that enables computing points-to information on-demand via value-flow refinement, in environments with small time and memory budgets such as IDEs. We formulate Supa by solving a graph-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Programming Languages and Systems: 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings

Apr 2020

784 pages

ISBN:978-3-030-44913-1

DOI:10.1007/978-3-030-44914-8

Editor:
Peter Müller
ETH Zurich, Zurich, Switzerland

© The Author(s) 2020.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 April 2020

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kobayashi N(2025)On Decidable and Undecidable Extensions of Simply Typed Lambda CalculusProceedings of the ACM on Programming Languages10.1145/37048759:POPL(1136-1166)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704875
Simonnet JLemerre MSighireanu M(2024)A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level CodeProceedings of the ACM on Programming Languages10.1145/36897128:OOPSLA2(30-59)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689712
Tanaka ISakayori KKobayashi NKeller GWang M(2024)Ownership Types for Verification of Programs with Pointer ArithmeticProceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3635800.3636965(94-106)Online publication date: 11-Jan-2024
https://dl.acm.org/doi/10.1145/3635800.3636965
Nakayama TMatsushita YSakayori KSato RKobayashi N(2024)Borrowable Fractional Ownership Types for VerificationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_11(224-246)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_11
Lehmann NGeller AVazou NJhala R(2023)Flux: Liquid Types for RustProceedings of the ACM on Programming Languages10.1145/35912837:PLDI(1533-1557)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591283
Ikeda RSato RKobayashi N(2023)Argument Reduction of Constrained Horn Clauses Using Equality ConstraintsProgramming Languages and Systems10.1007/978-981-99-8311-7_12(246-265)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_12
Lanzinger FBachmeier JUlbrich MDietl W(2023)Scalable and Precise Refinement Types for Imperative LanguagesiFM 202310.1007/978-3-031-47705-8_20(377-383)Online publication date: 13-Nov-2023
https://dl.acm.org/doi/10.1007/978-3-031-47705-8_20
Jiang KBao YWang SLiu ZZhang TYin HStavrou ACremers CShi E(2022)Cache Refinement Type for Side-Channel Detection of Cryptographic SoftwareProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security10.1145/3548606.3560672(1583-1597)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3548606.3560672
Gurfinkel A(2022)Program Verification with Constrained Horn Clauses (Invited Paper)Computer Aided Verification10.1007/978-3-031-13185-1_2(19-29)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_2
Lanzinger FWeigl AUlbrich MDietl W(2021)Scalability and precision by combining expressive type systems and deductive verificationProceedings of the ACM on Programming Languages10.1145/34855205:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485520
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents