Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-26T04:57:14.723Z Has data issue: false hasContentIssue false
  • English
  • Français

Higher order symbolic execution for contract verification and refutation*

Part of: JFP Research Articles

Published online by Cambridge University Press:  21 December 2016

PHÚC C. NGUYÊN ,
SAM TOBIN-HOCHSTADT  and
DAVID VAN HORN
PHÚC C. NGUYÊN
Affiliation:
University of Maryland, College Park, Maryland, USA (e-mail: [email protected])
SAM TOBIN-HOCHSTADT
Affiliation:
Indiana University, Bloomington, Indiana, USA (e-mail: [email protected])
DAVID VAN HORN
Affiliation:
University of Maryland, College Park, Maryland, USA (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We present a new approach to automated reasoning about higher-order programs by endowing symbolic execution with a notion of higher-order, symbolic values. To validate our approach, we use it to develop and evaluate a system for verifying and refuting behavioral software contracts of components in a functional language, which we call soft contract verification. In doing so, we discover a mutually beneficial relation between behavioral contracts and higher-order symbolic execution. Contracts aid symbolic execution by providing a rich language of specifications serving as a basis of symbolic higher-order values; the theory of blame enables modular verification and leads to the theorem that verified components can't be blamed; and the run-time monitoring of contracts enables soft verification whereby verified and unverified components can safely interact. Conversely, symbolic execution aids contracts by providing compile-time verification and automated test case generation from counter-examples to verification. This relation between symbolic exuection and contracts engenders a virtuous cycle encouraging the gradual use of contracts.

Our approach is able to analyze first-class contracts, recursive data structures, unknown functions, and control-flow-sensitive refinements of values, which are all idiomatic in dynamic languages. It makes effective use of off-the-shelf solvers to decide problems without heavy encodings. Counterexample search is sound and relatively complete with respect to a first-order solver for base type values and counter-examples are reported as concrete values, including functions. Therefore, it can form the basis of automated verification and bug-finding tools for higher-order programs. The approach is competitive with a range of existing tools—including type systems, flow analyzers, and model checkers—on their own benchmarks. We have built a prototype to analyze programs written in Racket and report on its effectiveness in verifying and refuting contracts.

Type
Articles
Information
Journal of Functional Programming , Volume 27 , 2017 , e3
Copyright
Copyright © Cambridge University Press 2016 

Footnotes

*

This material is based on research sponsored by the NSF under award 1218390, the NSA under the Science of Security program, and DARPA under the programs Automated Program Analysis for Cybersecurity (FA8750-12-2-0106) and Clean-slate design of Resilient Adaptive Secure Hosts. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon.

References

Aiken, A., Wimmers, E. L. & Lakshman, T. K. (1994) Soft typing with conditional types. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM - New York, New York, USA, pp. 163–173.Google Scholar
Austin, T. H., Disney, T. & Flanagan, C. (2011, October) Virtual values for language extension. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 921–938.Google Scholar
Barrett, C., Conway, C., Deters, Hadarean L., Jovanović, D., King, T., Reynolds, A. & Tinelli, C. (2011) Cvc4. In International Conference on Computer-Aided Verification. Springer, pp. 171–177.Google Scholar
Cadar, C., Dunbar, D. & Engler, D. (2008) KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. USENIX Association, pp. 209–224.Google Scholar
Cadar, C., Ganesh, V., Pawlowski, P. M., Dill, D. L. & Engler, D. R. (2006) EXE: Automatically generating inputs of death. In Proceedings of the 13th ACM Conference on Computer and Communications Security. ACM, pp. 322–335.Google Scholar
Cartwright, R. & Fagan, M. (1991) Soft typing. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. ACM, pp. 278–292.Google Scholar
Cartwright, R. & Felleisen, M. (1996, June) Program verification through soft typing. ACM Comput. Surv. 28 (2) 349–351.Google Scholar
Chugh, R., Herman, D. & Jhala, R. (2012a, October) Dependent types for JavaScript. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 587–606.Google Scholar
Chugh, R., Rondon, P. M. & Jhala, R. (2012b, January) Nested refinements: A logic for duck typing. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 231–244.Google Scholar
Claessen, K. & Hughes, J. (2000) QuickCheck: A lightweight tool for random testing of Haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 268–279.Google Scholar
Dimoulas, C., Findler, R. B., Flanagan, C. & Felleisen, M. (2011, January) Correct blame for contracts: No more scapegoating. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 215–226.CrossRefGoogle Scholar
Disney, T. (2013, July) contracts.coffee.Google Scholar
Disney, T., Flanagan, C. & McCarthy, J. (2011, September) Temporal higher-order contracts. In ICFP '11 Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 176–188.CrossRefGoogle Scholar
Fähndrich, M. & Logozzo, F. (2011) Static contract checking with abstract interpretation. In Proceedings of the 2010 International Conference on Formal Verification of Object-Oriented Software. Springer, pp. 10–30.CrossRefGoogle Scholar
Findler, R. B. & Felleisen, M. (2002, September) Contracts for higher-order functions. In ICFP '02: Proceedings of the seventh ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 48–59.Google Scholar
Flanagan, C. & Felleisen, M. (1999, March) Componential set-based analysis. ACM Trans. Program. Lang. Syst. 21 (2) 370–416.Google Scholar
Flanagan, C., Flatt, M., Krishnamurthi, S., Weirich, S. & Felleisen, M. (1996, May) Catching bugs in the web of program invariants. In PLDI '96: Proceedings of the ACM SIGPLAN 1996 Conference on Programming Language Design and Implementation. ACM, pp. 23–32.Google Scholar
Flatt, M. & PLT (2010) Reference: Racket. Technical Report PLT-TR-2010-1, PLT Inc.Google Scholar
Foster, J. S., Terauchi, T. & Aiken, A. (2002, May) Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 1–12.Google Scholar
Freeman, T. & Pfenning, F. (1991, June) Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. ACM, pp. 268–277.CrossRefGoogle Scholar
Godefroid, P., Klarlund, N. & Sen, K. (2005, June) DART: Directed automated random testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 213–223.Google Scholar
Greenberg, M., Pierce, B. C. & Weirich, S. (2010) Contracts made manifest. In POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 353–364.CrossRefGoogle Scholar
Heidegger, P. & Thiemann, P. (2010) Contract-Driven testing of JavaScript code. In Objects, Models, Components, Patterns. Berlin Heidelberg: Springer, pp. 154–172.Google Scholar
Henglein, F. (1994, June) Dynamic typing: Syntax and proof theory. Sci. Comput. Program. 22 (3) 197–230. Elsevier, Amsterdam, Netherlands.Google Scholar
Hickey, R., Fogus, M. & contributors (2013, July). core.contracts.Google Scholar
Johnson, J. I. & Van Horn, D. (2014, October) Abstracting abstract control. In Proceedings of the 10th ACM Symposium on Dynamic Languages. ACM, pp. 11–22.Google Scholar
Kawaguchi, M., Rondon, P. & Jhala, R. (2010) Dsolve: Safety verification via liquid types. In Computer Aided Verification. Berlin Heidelberg: Springer, pp. 123–126.Google Scholar
Klein, C., Flatt, M. & Findler, R. B. (2010) Random testing for higher-order, stateful programs. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 555–566.Google Scholar
Knowles, K. & Flanagan, C. (2010, February) Hybrid type checking. ACM Trans. Program. Lang. Syst. 32 (2) article 6.Google Scholar
Kobayashi, N. (2009a) Model-checking higher-order functions. In Proceedings of the 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. ACM, pp. 25–36.Google Scholar
Kobayashi, N. (2009b, January) Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 416–428.Google Scholar
Kobayashi, N. & Igarashi, A. (2013) Model-Checking Higher-Order programs with recursive types. In European Symposium on Programming. Berlin Heidelberg: Springer, pp. 431–450.Google Scholar
Kobayashi, N. & Ong, C. H. L. (2009, August) A type system equivalent to the modal Mu-Calculus model checking of Higher-Order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic In Computer Science. IEEE, pp. 179–188.Google Scholar
Kobayashi, N., Sato, R. & Unno, H. (2011, June) Predicate abstraction and CEGAR for higher-order model checking. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 222–233.Google Scholar
Kobayashi, N., Tabuchi, N. & Unno, H. (2010, January) Higher-order multi-parameter tree transducers and recursion schemes for program verification. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 495–508.Google Scholar
Meunier, P., Findler, R. B. & Felleisen, M. (2006, January) Modular set-based analysis from contracts. In POPL '06: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 218–231.CrossRefGoogle Scholar
Meyer, B. (1991, October) Eiffel: The Language. Prentice Hall.Google Scholar
Moura, L. D. & Bjørner, N. (2008) Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, pp. 337–340.Google Scholar
Nguyên, P. C., Tobin-Hochstadt, S. & Van Horn, D. (2014) Soft contract verification. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 139–152.Google Scholar
Nguyên, P. C. & Van Horn, D. (2015) Relatively complete counterexamples for higher-order programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 446–456.Google Scholar
Ong, C. H. L. (2006) On Model-Checking trees generated by Higher-Order recursion schemes. In 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06). IEEE, pp. 81–90.CrossRefGoogle Scholar
Ong, C. H. L. & Ramsay, S. J. (2011, January) Verifying higher-order functional programs with pattern-matching algebraic data types. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 587–598.Google Scholar
Plosch, R. (1997, December) Design by contract for Python. In Proceedings of the Joint Asia Pacific Software Engineering Conference. IEEE, pp. 213–219.Google Scholar
Rondon, P. M., Kawaguci, M. & Jhala, R. (2008) Liquid types. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 159–169.Google Scholar
Seidel, E., Vazou, N. & Jhala, R. (2015) Type targeted testing. In Programming Languages and Systems. Berlin Heidelberg: Springer, pp. 812–836.Google Scholar
Shivers, O. (1988) Control flow analysis in Scheme. In PLDI '88: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation. ACM, pp. 164–174.Google Scholar
St-Amour, V., Tobin-Hochstadt, S., Flatt, M. & Felleisen, M. (2012) Typing the numeric tower. In Practical Aspects of Declarative Languages. Berlin Heidelberg, Springer, pp. 289–303.Google Scholar
Strickland, T. S., Tobin-Hochstadt, S., Findler, R. B. & Flatt, M. (2012, October) Chaperones and impersonators: Run-time support for reasonable interposition. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 943–962.Google Scholar
Terauchi, T. (2010) Dependent types from counterexamples. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 119–130.Google Scholar
Tobin-Hochstadt, S. & Felleisen, M. (2010, September) Logical types for untyped languages. In ICFP '10: International Conference on Functional Programming. ACM, pp. 117–128.CrossRefGoogle Scholar
Tobin-Hochstadt, S., St-Amour, V., Culpepper, R., Flatt, M. & Felleisen, M. (2011, June) Languages as libraries. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, pp. 132–141.Google Scholar
Tobin-Hochstadt, S. & Van Horn, D. (2012) Higher-order symbolic execution via contracts. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM, pp. 537–554.Google Scholar
Tsukada, T. & Kobayashi, N. (2010) Untyped recursion schemes and infinite intersection types. In Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures. Springer-Verlag, pp. 343–357.Google Scholar
Van Horn, D. & Might, M. (2010, September) Abstracting abstract machines. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 51–62.Google Scholar
Van Horn, D. & Might, M. (2012) Systematic abstraction of abstract machines. Journal of Functional Programming 22(Special Issue 4–5) Cambridge University Press, 705–746.Google Scholar
Vazou, N., Rondon, P. & Jhala, R. (2013) Abstract refinement types. In European Symposium on Programming. Berlin Heidelberg: Springer, pp. 209–228.Google Scholar
Vazou, N., Seidel, E. L., Jhala, R., Vytiniotis, D. & Jones, S. P. (2014, August) Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. ACM, pp. 269–282.Google Scholar
Vytiniotis, D., Jones, S. P., Claessen, K. & Rosén, D. (2013) Halo: Haskell to logic through denotational semantics. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 431–442.Google Scholar
Wright, A. K. & Cartwright, R. (1997, January) A practical soft type system for Scheme. ACM Trans. Program. Lang. Syst. 19 (1) ACM, 87–152.Google Scholar
Xie, Y. & Aiken, A. (2005, January) Scalable error detection using boolean satisfiability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 351–363.Google Scholar
Xu, D. N. (2012) Hybrid contract checking via symbolic simplification. In Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation. ACM, pp. 107–116.Google Scholar
Xu, D. N., Peyton Jones, S. & Claessen, S. (2009) Static contract checking for Haskell. In POPL '09: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, pp. 41–52.Google Scholar
Yang, J., Twohey, P., Engler, D. & Musuvathi, M. (2004) Using model checking to find serious file system errors. In Proceedings of the 6th Symposium on Operating Systems Design and Implementation. USENIX, pp. 273–287.Google Scholar
Zhu, H. & Jagannathan, S. (2013) Compositional and lightweight dependent type inference for ML. In Conference on Verification, Model-Checking and Abstract Interpretation Springer, 295–314.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.