By Michael Greenberg with Austin Blatt and Calvin Aylward
Smoosh (the Symbolic, Mechanized, Observable, Operational SHell) is a formalization of the POSIX shell standard.
As a trial of Smoosh's capabilities, we've built a web-based shell stepper (a/k/a the 'shtepper') that can symbolically step shell code through the various phases of expansion and evaluation.
The implementation of commands is limited to the core builtin operations of the shell; the filesystem and unknown executables are treated symbolically.
Smoosh's source code is open (MIT licensed) and freely available. The repository has several Dockerfiles to help you get started.
To cite Smoosh as a semantics, please use:
@inproceedings{Greenberg20Smoosh,
title = {Executable formal semantics for the POSIX shell},
author = { Michael Greenberg and Austin J. Blatt },
year = 2020,
booktitle = {POPL},
}
To cite Smoosh as an artifact or project, please use:
@misc{Smoosh,
title = {Smoosh: the Symbolic, Mechanized, Observable, Operational Shell},
author = { Michael Greenberg },
year = 2020,
url = {https://github.com/mgree/smoosh},
note = {Current version: 0.1}
}