Smoosh - The Symbolic, Mechanized, Observable, Operational Shell

By Michael Greenberg with Austin Blatt and Calvin Aylward

Smoosh (the Symbolic, Mechanized, Observable, Operational SHell) is a formalization of the POSIX shell standard.

Symbolic
The formal model can run in a purely symbolic mode, working with a model of a POSIX system.
Mechanized
The formal model is code, written in Lem.
Observable
The formal model uses small-step operational semantics and produce a trace of how the shell evaluated a given term.
Operational
The formal model can run in a non-symbolic mode, making real system calls via OCaml drivers.
Shell
The formal model's drivers yield a functioning, POSIX compliant shell.

Demo: the web-based 'shtepper'

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.

Code

Smoosh's source code is open (MIT licensed) and freely available. The repository has several Dockerfiles to help you get started.

Papers

Executable formal semantics for the POSIX shell
Michael Greenberg and Austin Blatt, POPL 2020.
Smoosh's debut paper, describing the semantics and implementation in detail. Includes comparisons to other shells and discussion of the POSIX standard.
The POSIX shell is an interactive DSL for concurrency
Michael Greenberg, DSLDI 2018.
An argument for understanding the shell as a DSL for managing concurrent tasks; the first demo of the Smoosh shtepper.
Word expansion supports POSIX shell interactivity
Michael Greenberg, PX/2018.
An argument about how the shell's use of word expansion dovetails with the shell's interactivity.
Understanding the POSIX Shell as a Programming Language
Michael Greenberg, OBT 2017.
The initial proposal of the Smoosh project.

Cite Smoosh

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}
}