TY - JOUR
T1 - Executable formal semantics for the POSIX shell
AU - Greenberg, Michael
AU - Blatt, Austin J.
N1 - Publisher Copyright:
© 2020 Copyright held by the owner/author(s).
PY - 2020/1
Y1 - 2020/1
N2 - The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert's control panel, a necessary tool for configuring, compiling, installing, maintaining, and deploying systems. Even though it is powerful, critical infrastructure, the POSIX shell is maligned and misunderstood. Its power and its subtlety are a dangerous combination. We define a formal, mechanized, executable small-step semantics for the POSIX shell, which we call Smoosh. We compared Smoosh against seven other shells that aim for some measure of POSIX compliance (bash, dash, zsh, OSH, mksh, ksh93, and yash). Using three test suites - the POSIX test suite, the Modernish test suite and shell diagnostic, and a test suite of our own device - we found Smoosh's semantics to be the most conformant to the POSIX standard. Modernish judges Smoosh to have the fewest bugs (just one, from using dash's parser) and no quirks. To show that our semantics is useful beyond yielding a conformant, executable shell, we also implemented a symbolic stepper to illuminate the subtle behavior of the shell. Smoosh will serve as a foundation for formal study of the POSIX shell, supporting research on and development of new shells, new tooling for shells, and new shell designs.
AB - The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert's control panel, a necessary tool for configuring, compiling, installing, maintaining, and deploying systems. Even though it is powerful, critical infrastructure, the POSIX shell is maligned and misunderstood. Its power and its subtlety are a dangerous combination. We define a formal, mechanized, executable small-step semantics for the POSIX shell, which we call Smoosh. We compared Smoosh against seven other shells that aim for some measure of POSIX compliance (bash, dash, zsh, OSH, mksh, ksh93, and yash). Using three test suites - the POSIX test suite, the Modernish test suite and shell diagnostic, and a test suite of our own device - we found Smoosh's semantics to be the most conformant to the POSIX standard. Modernish judges Smoosh to have the fewest bugs (just one, from using dash's parser) and no quirks. To show that our semantics is useful beyond yielding a conformant, executable shell, we also implemented a symbolic stepper to illuminate the subtle behavior of the shell. Smoosh will serve as a foundation for formal study of the POSIX shell, supporting research on and development of new shells, new tooling for shells, and new shell designs.
KW - Command line interfaces
KW - Formalization
KW - POSIX
KW - Small-step semantics
UR - http://www.scopus.com/inward/record.url?scp=85082599338&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85082599338&partnerID=8YFLogxK
U2 - 10.1145/3371111
DO - 10.1145/3371111
M3 - Article
AN - SCOPUS:85082599338
VL - 4
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
IS - POPL
M1 - 43
ER -