research-article

Open access

Executable formal semantics for the POSIX shell

Authors:

Michael Greenberg,

Austin J. BlattAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue POPL

Article No.: 43, Pages 1 - 30

https://doi.org/10.1145/3371111

Published: 20 December 2019 Publication History

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

Supplementary Material

WEBM File (a43-greenberg.webm)

Download
91.88 MB

References

[1]

The Austin Group. 2018. POSIX.1 2017: The Open Group Base Specifications Issue 7 (IEEE Std 1003.1-2008).

[2]

Sandrine Blazy and Xavier Leroy. 2009. Mechanized Semantics for the Clight Subset of the C Language. Journal of Automated Reasoning 43, 3 (01 Oct 2009), 263–288.

[3]

Andy Chu. 2019. Oil Shell. https://www.oilshell.org/

[4]

Nick Collins, Alex McLean, Julian Rohrhuber, and Adrian Ward. 2003. Live coding in laptop performance. Organised Sound 8, 3 (2003), 321–330.

Digital Library

[5]

Loris D’Antoni, Rishabh Singh, and Michael Vaughn. 2016. NoFAQ: Synthesizing Command Repairs from Examples. CoRR abs/1608.08219 (2016). http://arxiv.org/abs/1608.08219

[6]

Martijn Dekker. 2019. Modernish. https://github.com/modernish/modernish

[7]

Jack B. Dennis and Earl C. Van Horn. 1966. Programming Semantics for Multiprogrammed Computations. Commun. ACM 9, 3 (March 1966), 143–155.

Digital Library

[8]

Chucky Ellison and Grigore Rosu. 2012. An Executable Formal Semantics of C with Applications. In Principles of Programming Languages (POPL). ACM, New York, NY, USA, 533–544.

Digital Library

[9]

Kathleen Fisher, Nate Foster, David Walker, and Kenny Q. Zhu. 2011. Forest: A Language and Toolkit for Programming with Filestores. In International Conference on Functional Programming (ICFP). ACM, New York, NY, USA, 292–306.

Digital Library

[10]

Simson Garfinkel, Daniel Weise (Ed.), and Steven Strassman (Ed.). 1994. The UNIX Hater’s Handbook. IDG Books Worldwide, Inc., San Mateo, CA, USA.

[11]

Gabriel Gonzalez. 2018. Turtle: shell programming, Haskell style. https://github.com/Gabriel439/Haskell- Turtle- Library

[12]

Michael Greenberg. 2018a. The POSIX shell is an interactive DSL for concurrency. DSLDI.

[13]

Michael Greenberg. 2018b. Word expansion supports POSIX shell interactivity. In Programming Companion (presented at Programming eXperience (PX)). ACM.

Digital Library

[14]

Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. 2010. The Essence of JavaScript. In ECOOP, Theo D’Hondt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 126–150.

[15]

William Gallard Hatch and Matthew Flatt. 2018. Rash: from reckless interactions to reliable programs. In Generative Programming: Concepts and Experiences (GPCE), Eric Van Wyk and Tiark Rompf (Eds.). ACM, 28–39.

Digital Library

[16]

Alec Heller and Jesse A. Tov. 2008. Caml-Shcaml: an ocaml library for unix shell programming. In ML. ACM, 79–90.

[17]

Nicolas Jeannerod. 2017. Le coquillage dans le CoLiS-mateur. In JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs. Gourette, France. https://hal.archives- ouvertes.fr/hal- 01432034

[18]

Nicolas Jeannerod, Claude Marché, and Ralf Treinen. 2017a. A Formally Verified Interpreter for a Shell-like Programming Language. In Verified Software: Theories, Tools, and Experiments (VSTTE) (Lecture Notes in Computer Science), Vol. 10712. Heidelberg, Germany. https://hal.archives- ouvertes.fr/hal- 01534747

[19]

Nicolas Jeannerod, Yann Régis-Gianas, and Ralf Treinen. 2017b. Having Fun With 31.521 Shell Scripts. (April 2017). https://hal.archives- ouvertes.fr/hal- 01513750 working paper or preprint.

[20]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the Foundations of the Rust Programming Language. Proc. ACM Program. Lang. 2, POPL, Article 66 (Dec. 2017), 34 pages.

Digital Library

[21]

Idan Kamara. 2016. explainshell. http://explainshell.com/

[22]

Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis. 2015. A Formal C Memory Model Supporting Integer-pointer Casts. In Programming Language Design and Implementation (PLDI). ACM, New York, NY, USA, 326–335.

Digital Library

[23]

Robbert Krebbers, Xavier Leroy, and Freek Wiedijk. 2014. Formal C Semantics: CompCert and the C Standard. In Interactive Theorem Proving, Gerwin Klein and Ruben Gamboa (Eds.). Springer International Publishing, Cham, 543–548.

[24]

Sergio Maffeis, John C. Mitchell, and Ankur Taly. 2008. An Operational Semantics for JavaScript. In Asian Symposium on Programming Languages and Systems (APLAS). Springer-Verlag, Berlin, Heidelberg, 307–325.

Digital Library

[25]

Karl Mazurak and Steve Zdancewic. 2007. ABASH: Finding Bugs in Bash Scripts. In PLAS. 105–114.

Digital Library

[26]

Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, and Peter Sewell. 2016. Into the Depths of C: Elaborating the De Facto Standards. In Programming Language Design and Implementation (PLDI). ACM, New York, NY, USA, 1–15.

Digital Library

[27]

Scott Moore, Christos Dimoulas, Dan King, and Stephen Chong. 2014. Shill: A Secure Shell Scripting Language. In USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX.

[28]

Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. 2014. Lem: Reusable Engineering of Real-world Semantics. In International Conference on Functional Programming (ICFP). ACM, New York, NY, USA, 175–188.

Digital Library

[29]

Marius Nita, Dan Grossman, and Craig Chambers. 2008. A theory of platform-dependent low-level software. In Principles of Programming Languages (POPL), George C. Necula and Philip Wadler (Eds.). ACM, 209–220.

Digital Library

[30]

Gian Ntzik. 2017. Reasoning About POSIX File Systems. Ph.D. Dissertation. Imperial College London.

[31]

Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. 2018. A Concurrent Specification of POSIX File Systems. In ECOOP.

[32]

Joe Gibbs Politz, Matthew J. Carroll, Benjamin S. Lerner, Justin Pombrio, and Shriram Krishnamurthi. 2012. A Tested Semantics for Getters, Setters, and Eval in JavaScript. In Dynamic Languages Symposium (DLS). ACM, New York, NY, USA, 1–16.

Digital Library

[33]

Yann Régis-Gianas, Nicolas Jeannerod, and Ralf Treinen. 2018. Morbig: A Static Parser for POSIX Shell. In Software Language Engineering (SLE). Boston, United States.

Digital Library

[34]

Gregor Richards, Christian Hammer, Brian Burg, and Jan Vitek. 2011. The Eval That Men Do. In ECOOP, Mira Mezini (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 52–78.

[35]

Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell. 2015. SibylFS: Formal Specification and Oracle-based Testing for POSIX and Real-world File Systems. In Symposium on Operating Systems Principles (SOSP). ACM, New York, NY, USA, 38–53.

Digital Library

[36]

Grigore Roşu and Traian Florin Şerbănuţă. 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397–434.

[37]

Henry Schreiner, Tomer Filiba, et al. 2018. Plumbum: shell combinators. http://plumbum.readthedocs.io/en/latest/

[38]

Anthony Scopatz et al. 2019. Xonsh. https://xon.sh/

[39]

Olin Shivers. 2006. SCSH manual 0.6.7. https://scsh.net/docu/html/man.html

[40]

Philipp Emanuel Weidmann. 2016. maybe. https://github.com/p- e- w/maybe

[41]

Aaron Weiss, Daniel Patterson, and Amal Ahmed. 2018. Rust Distilled: An Expressive Tower of Languages. CoRR abs/1806.02693 (2018). arXiv: 1806.02693 http://arxiv.org/abs/1806.02693

[42]

Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019. Oxide: The Essence of Rust. CoRR abs/1903.00982 (2019). arXiv: 1903.00982 http://arxiv.org/abs/1903.00982

Cited By

Yun HPark D(2024)Low-Power Lane Detection Unit With Sliding-Based Parallel Segment Detection Accelerator for FPGAIEEE Access10.1109/ACCESS.2023.334847812(4339-4353)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2023.3348478
Melançon OFeeley MSerrano MSaraiva JDegueule TScott E(2023)An Executable Semantics for Faster Development of Optimizing Python CompilersProceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3623476.3623529(15-28)Online publication date: 23-Oct-2023
https://dl.acm.org/doi/10.1145/3623476.3623529
Liargkovas GKallas KGreenberg MVasilakis NBaumann ACrooks NSchwarzkopf M(2023)Executing Shell Scripts in the Wrong Order, CorrectlyProceedings of the 19th Workshop on Hot Topics in Operating Systems10.1145/3593856.3595891(103-109)Online publication date: 22-Jun-2023
https://dl.acm.org/doi/10.1145/3593856.3595891
Show More Cited By

Index Terms

Executable formal semantics for the POSIX shell

Recommendations

Word expansion supports POSIX shell interactivity
Programming '18: Companion Proceedings of the 2nd International Conference on the Art, Science, and Engineering of Programming

The POSIX shell is the standard tool to deploy, control, and maintain systems of all kinds; the shell is used on a sliding scale from one-off commands in an interactive mode all the way to complex scripts managing, e.g., system boot sequences. For all ...
Formal test specifications in IEEE POSIX
Special issue on formal description techniques
Porting Multimedia Applications to the Open System Environment

To migrate DOS-based courseware to the Open System Environment (OSE), process creation and communication in Posix, a portable operating-system interface, were merged with a multilevel client-server architecture. This helped identify some problems that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution-ShareAlike International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
1,557
Total Downloads

Downloads (Last 12 months)398
Downloads (Last 6 weeks)197

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yun HPark D(2024)Low-Power Lane Detection Unit With Sliding-Based Parallel Segment Detection Accelerator for FPGAIEEE Access10.1109/ACCESS.2023.334847812(4339-4353)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2023.3348478
Melançon OFeeley MSerrano MSaraiva JDegueule TScott E(2023)An Executable Semantics for Faster Development of Optimizing Python CompilersProceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3623476.3623529(15-28)Online publication date: 23-Oct-2023
https://dl.acm.org/doi/10.1145/3623476.3623529
Liargkovas GKallas KGreenberg MVasilakis NBaumann ACrooks NSchwarzkopf M(2023)Executing Shell Scripts in the Wrong Order, CorrectlyProceedings of the 19th Workshop on Hot Topics in Operating Systems10.1145/3593856.3595891(103-109)Online publication date: 22-Jun-2023
https://dl.acm.org/doi/10.1145/3593856.3595891
Park JYoun DLee KRyu S(2023)Feature-Sensitive Coverage for Conformance Testing of Programming Language ImplementationsProceedings of the ACM on Programming Languages10.1145/35912407:PLDI(493-515)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591240
Dong YLi ZTian YSun CGodfrey MNagappan M(2023)Bash in the Wild: Language Usage, Code Smells, and BugsACM Transactions on Software Engineering and Methodology10.1145/351719332:1(1-22)Online publication date: 13-Feb-2023
https://dl.acm.org/doi/10.1145/3517193
Greenberg M(2021)Files-as-Filesystems for POSIX Shell Data ProcessingProceedings of the 11th Workshop on Programming Languages and Operating Systems10.1145/3477113.3487265(17-23)Online publication date: 25-Oct-2021
https://dl.acm.org/doi/10.1145/3477113.3487265
Handa SKallas KVasilakis NRinard M(2021)An order-aware dataflow model for parallel Unix pipelinesProceedings of the ACM on Programming Languages10.1145/34735705:ICFP(1-28)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473570
Greenberg MKallas KVasilakis NAngel SKasikci BKohler E(2021)The future of the shellProceedings of the Workshop on Hot Topics in Operating Systems10.1145/3458336.3465296(240-241)Online publication date: 1-Jun-2021
https://dl.acm.org/doi/10.1145/3458336.3465296
Greenberg MKallas KVasilakis NAngel SKasikci BKohler E(2021)Unix shell programmingProceedings of the Workshop on Hot Topics in Operating Systems10.1145/3458336.3465294(104-111)Online publication date: 1-Jun-2021
https://dl.acm.org/doi/10.1145/3458336.3465294
Doenges RArashloo MBautista SChang ANi NParkinson SPeterson RSolko-Breslin AXu AFoster N(2021)Petr4: formal foundations for p4 data planesProceedings of the ACM on Programming Languages10.1145/34343225:POPL(1-32)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434322
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents