Prototyping symbolic execution engines for interpreted languages. / Bucur, Stefan; Kinder, Johannes; Candea, George.

Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014). ACM, 2014. p. 239-254.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Standard

Prototyping symbolic execution engines for interpreted languages. / Bucur, Stefan; Kinder, Johannes; Candea, George.

Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014). ACM, 2014. p. 239-254.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Bucur, S, Kinder, J & Candea, G 2014, Prototyping symbolic execution engines for interpreted languages. in Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014). ACM, pp. 239-254. https://doi.org/10.1145/2541940.2541977

APA

Bucur, S., Kinder, J., & Candea, G. (2014). Prototyping symbolic execution engines for interpreted languages. In Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014) (pp. 239-254). ACM. https://doi.org/10.1145/2541940.2541977

Vancouver

Bucur S, Kinder J, Candea G. Prototyping symbolic execution engines for interpreted languages. In Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014). ACM. 2014. p. 239-254 https://doi.org/10.1145/2541940.2541977

Author

Bucur, Stefan ; Kinder, Johannes ; Candea, George. / Prototyping symbolic execution engines for interpreted languages. Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014). ACM, 2014. pp. 239-254

BibTeX

@inproceedings{06f2109ac53c47ce867633aad6cfbb68,
title = "Prototyping symbolic execution engines for interpreted languages",
abstract = "Symbolic execution is being successfully used to automatically test statically compiled code. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways.We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called Chef) for turning a vanilla interpreter into a sound and complete symbolic execution engine. Chef symbolically executes the target program by symbolically executing the interpreter's binary while exploiting inferred knowledge about the program's high-level structure.Using Chef, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 person-days. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. Chef-produced engines are up to 1000 times more performant than if directly executing the interpreter symbolically without Chef.",
author = "Stefan Bucur and Johannes Kinder and George Candea",
year = "2014",
doi = "10.1145/2541940.2541977",
language = "English",
pages = "239--254",
booktitle = "Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014)",
publisher = "ACM",

}

RIS

TY - GEN

T1 - Prototyping symbolic execution engines for interpreted languages

AU - Bucur, Stefan

AU - Kinder, Johannes

AU - Candea, George

PY - 2014

Y1 - 2014

N2 - Symbolic execution is being successfully used to automatically test statically compiled code. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways.We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called Chef) for turning a vanilla interpreter into a sound and complete symbolic execution engine. Chef symbolically executes the target program by symbolically executing the interpreter's binary while exploiting inferred knowledge about the program's high-level structure.Using Chef, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 person-days. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. Chef-produced engines are up to 1000 times more performant than if directly executing the interpreter symbolically without Chef.

AB - Symbolic execution is being successfully used to automatically test statically compiled code. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways.We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called Chef) for turning a vanilla interpreter into a sound and complete symbolic execution engine. Chef symbolically executes the target program by symbolically executing the interpreter's binary while exploiting inferred knowledge about the program's high-level structure.Using Chef, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 person-days. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. Chef-produced engines are up to 1000 times more performant than if directly executing the interpreter symbolically without Chef.

U2 - 10.1145/2541940.2541977

DO - 10.1145/2541940.2541977

M3 - Conference contribution

SP - 239

EP - 254

BT - Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014)

PB - ACM

ER -