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

research-article

Open access

Symbolic types for lenient symbolic execution

Authors:

Emina TorlakAuthors Info & Claims

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

Article No.: 40, Pages 1 - 29

https://doi.org/10.1145/3158128

Published: 27 December 2017 Publication History

Abstract

We present lambda_sym, a typed λ-calculus for lenient symbolic execution, where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our calculus extends a base occurrence typing system with symbolic types and mutable state, making it a suitable model for both functional and imperative symbolically executed languages. Naively allowing mutation in this mixed setting introduces soundness issues, however, so we further add concreteness polymorphism, which restores soundness without rejecting too many valid programs. To show that our calculus is a useful model for a real language, we implemented Typed Rosette, a typed extension of the solver-aided Rosette language. We evaluate Typed Rosette by porting a large code base, demonstrating that our type system accommodates a wide variety of symbolically executed programs.

Supplementary Material

WEBM File (symbolictypesforlenientsymbolicexecution.webm)

Download
109.23 MB

References

[1]

Régis Blanc, Viktor Kuncak, Etienne Kneuss, and Philippe Suter. 2013. An Overview of the Leon Verification System: Verification by Translation to Recursive Functions. In Proceedings of the 4th Workshop on Scala. 1:1–1:10.

Digital Library

[2]

James Bornholt and Emina Torlak. 2017. Synthesizing Memory Models from Framework Sketches and Litmus Tests. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). 467–481.

Digital Library

[3]

James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. 2016. Optimizing Synthesis with Metasketches. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 775–788.

Digital Library

[4]

Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. 1975. SELECT—a Formal System for Testing and Debugging Programs by Symbolic Execution. In Proceedings of the International Conference on Reliable Software. 234–245.

Digital Library

[5]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 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. 209–224.

[6]

Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. 2006. EXE: Automatically Generating Inputs of Death. In Proceedings of the 13th ACM Conference on Computer and Communications Security. 322–335.

Digital Library

[7]

Stephen Chang, Alex Knauth, and Ben Greenman. 2017. Type Systems As Macros. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 694–705.

Digital Library

[8]

Dorothy E. Denning and Peter J. Denning. 1977. Certification of Programs for Secure Information Flow. Commun. ACM 20, 7 (1977), 504–513.

Digital Library

[9]

Dorothy Elizabeth Robling Denning. 1982. Cryptography and Data Security. Addison-Wesley Longman Publishing Co., Inc.

[10]

Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. 2006. Modular Verification of Code with SAT. In Proceedings of the 2006 International Symposium on Software Testing and Analysis. 109–120.

Digital Library

[11]

Azadeh Farzan, Andreas Holzer, Niloofar Razavi, and Helmut Veith. 2013. Con2Colic Testing. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. 37–47.

Digital Library

[12]

Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. MIT Press.

Digital Library

[13]

Matthew Flatt. 2002. Composable and Compilable Macros: You Want It when?. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming. 72–83.

Digital Library

[14]

Matthew Flatt. 2016. Binding As Sets of Scopes. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 705–717.

Digital Library

[15]

Matthew Flatt and PLT. 2010. Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design Inc. https://racket- lang.org/tr1/ .

[16]

Tim Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. 268–277.

Digital Library

[17]

Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed Automated Random Testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. 213–223.

Digital Library

[18]

Patrice Godefroid, Michael Y. Levin, and David Molnar. 2012. SAGE: Whitebox Fuzzing for Security Testing. Queue 10, 1 (2012), 20:20–20:27.

[19]

Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. 2011. Synthesis of Loop-free Programs. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. 62–73.

Digital Library

[20]

Daniel Jackson. 2002. Alloy: A Lightweight Object Modelling Notation. ACM Trans. Softw. Eng. Methodol. 11, 2 (2002), 256–290.

Digital Library

[21]

Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, and Andrew E. Santosa. 2012. TRACER: A Symbolic Execution Tool for Verification. In Computer Aided Verification: 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. 758–766.

Digital Library

[22]

James C. King. 1975. A New Approach to Program Testing. In Proceedings of the International Conference on Reliable Software. 228–233.

Digital Library

[23]

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. 2012. Constraints As Control. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 151–164.

Digital Library

[24]

Andrew C. Myers. 1999. JFlow: Practical Mostly-static Information Flow Control. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 228–241.

Digital Library

[25]

Joseph P. Near and Daniel Jackson. 2012. Rubicon: Bounded Verification of Web Applications. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. 60:1–60:11.

Digital Library

[26]

Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Jonathan Jacky. 2016. Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. In Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. 23–41.

[27]

Phitchaya Mangpo Phothilimthana, Tikhon Jelvis, Rohin Shah, Nishant Totla, Sarah Chasins, and Rastislav Bodik. 2014. Chlorophyll: Synthesis-aided Compiler for Low-power Spatial Architectures. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 396–407.

Digital Library

[28]

Benjamin C. Pierce and David N. Turner. 1998. Local Type Inference. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 252–265.

Digital Library

[29]

François Pottier and Vincent Simonet. 2003. Information Flow Inference for ML. ACM Trans. Program. Lang. Syst. 25, 1 (2003), 117–158.

Digital Library

[30]

Corina S. P ˇ as ˇ areanu, Peter C. Mehlitz, David H. Bushnell, Karen Gundy-Burlet, Michael Lowry, Suzette Person, and Mark Pape. 2008. Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software. In Proceedings of the 2008 International Symposium on Software Testing and Analysis. ACM, New York, NY, USA, 15–26.

[31]

Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A Concolic Unit Testing Engine for C. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering. 263–272.

Digital Library

[32]

Rohin Shah and Rastislav Bodik. 2017. Automated Incrementalization through Synthesis. In Proceedings of the First Workshop on Incremental Computing.

[33]

Armando Solar-Lezama, Rodric Rabbah, Rastislav Bodík, and Kemal Ebcioğlu. 2005. Programming by Sketching for Bit-streaming Programs. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. 281–294.

Digital Library

[34]

T. Stephen Strickland, Sam Tobin-Hochstadt, and Matthias Felleisen. 2009. Practical Variable-Arity Polymorphism. In Proceedings of the 18th European Symposium on Programming Languages and Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009. 32–46.

Digital Library

[35]

Sam Tobin-Hochstadt and Matthias Felleisen. 2010. Logical Types for Untyped Languages. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. 117–128.

Digital Library

[36]

Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, and Matthias Felleisen. 2011. Languages As Libraries. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation. 132–141.

Digital Library

[37]

Emina Torlak and Rastislav Bodik. 2013. Growing Solver-aided Languages with Rosette. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software. 135–152.

Digital Library

[38]

Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 530–541.

Digital Library

[39]

Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. 2016. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. 765–780.

Digital Library

[40]

A.K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (1994), 38–94.

Digital Library

Cited By

Zhang CHartline JDimoulas CJhala RDillig I(2022)Karp: a language for NP reductionsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523732(762-776)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523732
Naus NSteenvoorden T(2020)Generating Next Step Hints for Task Oriented Programs Using Symbolic ExecutionTrends in Functional Programming10.1007/978-3-030-57761-2_3(47-68)Online publication date: 18-Aug-2020
https://doi.org/10.1007/978-3-030-57761-2_3

Index Terms

Symbolic types for lenient symbolic execution
1. Software and its engineering
  1. Software notations and tools
    1. Context specific languages
      1. Specialized application languages

Recommendations

A lightweight symbolic virtual machine for solver-aided host languages
PLDI '14

Solver-aided domain-specific languages (SDSLs) are an emerging class of computer-aided programming systems. They ease the construction of programs by using satisfiability solvers to automate tasks such as verification, debugging, synthesis, and non-...
Gradually typed symbolic expressions
PEPM '18: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

Embedding a domain-specific language (DSL) in a general purpose host language is an efficient way to develop a new DSL. Various kinds of languages and paradigms can be used as host languages, including object-oriented, functional, statically typed, and ...
A lightweight symbolic virtual machine for solver-aided host languages
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

Solver-aided domain-specific languages (SDSLs) are an emerging class of computer-aided programming systems. They ease the construction of programs by using satisfiability solvers to automate tasks such as verification, debugging, synthesis, and non-...

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 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
513
Total Downloads

Downloads (Last 12 months)119
Downloads (Last 6 weeks)29

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhang CHartline JDimoulas CJhala RDillig I(2022)Karp: a language for NP reductionsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523732(762-776)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523732
Naus NSteenvoorden T(2020)Generating Next Step Hints for Task Oriented Programs Using Symbolic ExecutionTrends in Functional Programming10.1007/978-3-030-57761-2_3(47-68)Online publication date: 18-Aug-2020
https://doi.org/10.1007/978-3-030-57761-2_3

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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