# Executable formal semantics for the POSIX shell

## TL;DR

This paper introduces Smoosh, a formal, executable semantics for the POSIX shell, demonstrating high conformity and minimal bugs compared to existing shells, and providing a tool for shell analysis and development.

## Contribution

We present Smoosh, the first formal, mechanized small-step semantics for the POSIX shell, enabling precise analysis and comparison of shell behaviors.

## Key findings

- Smoosh is the most conformant shell according to POSIX standards.
- Smoosh has the fewest bugs among tested shells.
- A symbolic stepper was implemented to analyze shell behavior.

## Abstract

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 diagnosis, 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.