Advertisement

A Formally Verified Interpreter for a Shell-Like Programming Language

  • Nicolas JeannerodEmail author
  • Claude Marché
  • Ralf Treinen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

The shell language is widely used for various system administration tasks on UNIX machines, as for instance as part of the installation process of software packages in FOSS distributions. Our mid-term goal is to analyze these scripts as part of an ongoing effort to use formal methods for the quality assurance of software distributions, to prove their correctness, or to pinpoint bugs. However, the syntax and semantics of POSIX shell are particularly treacherous.

We propose a new language called CoLiS which, on the one hand, has well-defined static semantics and avoids some of the pitfalls of the shell, and, on the other hand, is close enough to the shell to be the target of an automated translation of the scripts in our corpus. The language has been designed so that it will be possible to compile automatically a large number of shell scripts into the CoLiS language.

We formally define its syntax and semantics in Why3, define an interpreter for the language in the WhyML programming language, and present an automated proof in the Why3 proof environment of soundness and completeness of our interpreter with respect to the formal semantics.

Keywords

Posix shell Programming language Deductive program verification 

Notes

Acknowledgements

We would like to thanks Mihaela Sighireanu, Ilham Dami, Yann Régis-Gianas, and the other members of the CoLiS project, for their contributions and feedback on the design of the CoLiS language.

References

  1. 1.
    Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657–683 (2001). http://doi.acm.org/10.1145/504709.504712 CrossRefGoogle Scholar
  2. 2.
    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_14. http://cvc4.cs.stanford.edu/web/ CrossRefGoogle Scholar
  3. 3.
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73368-3_34 CrossRefGoogle Scholar
  4. 4.
    Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover (2008). https://alt-ergo.ocamlpro.com/
  5. 5.
    Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: First International Workshop on Intermediate Verification Languages, Boogie 2011, Wrocław, Poland, pp. 53–64, August 2011. http://proval.lri.fr/publications/boogie11final.pdf
  6. 6.
    Braakman, R., Rodin, J., Gilbey, J., Hobley, M.: Checkbashisms. https://sourceforge.net/projects/checkbaskisms/
  7. 7.
    Chen, R., Clochard, M., Marché, C.: A formal proof of a UNIX path resolution algorithm. Research Report RR-8987, Inria Saclay Ile-de-France, December 2016Google Scholar
  8. 8.
    Clochard, M., Filliâtre, J.-C., Marché, C., Paskevich, A.: Formalizing semantics with an automatic program verifier. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 37–51. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-12154-3_3 Google Scholar
  9. 9.
    Filliâtre, J.-C., Gondelman, L., Paskevich, A.: The spirit of ghost code. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 1–16. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_1. https://hal.inria.fr/hal-00873187 Google Scholar
  10. 10.
    Greenberg, M.: Understanding the POSIX shell as a programming language. In: Off the Beaten Track 2017, Paris, France, January 2017Google Scholar
  11. 11.
  12. 12.
    IEEE and The Open Group: POSIX.1-2008/Cor 1–2013. http://pubs.opengroup.org/onlinepubs/9699919799/
  13. 13.
    Jeannerod, N.: Full Why3 code for the CoLiS language and its proofs. http://toccata.lri.fr/gallery/colis_interpreter.en.html
  14. 14.
    Jeannerod, N., Régis-Gianas, Y., Treinen, R.: Having fun with 31.521 shell scripts. Working paper, April 2017. https://hal.archives-ouvertes.fr/hal-01513750
  15. 15.
    Mazurak, K., Zdancewic, S.: ABASH: finding bugs in bash scripts. In: Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, PLAS 2007, San Diego, CA, USA, pp. 105–114, June 2007Google Scholar
  16. 16.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24. https://github.com/Z3Prover/z3 CrossRefGoogle Scholar
  17. 17.
    Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 223–228. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-25984-8_15. http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html CrossRefGoogle Scholar
  18. 18.
    The Debian Policy Mailing List: Debian policy manual. https://www.debian.org/doc/debian-policy/
  19. 19.
    Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140–145. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02959-2_10. http://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/classic-spass-theorem-prover/ CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Nicolas Jeannerod
    • 1
    • 2
    Email author
  • Claude Marché
    • 3
  • Ralf Treinen
    • 2
  1. 1.Dpt. d’Informatique, École normale supérieureParisFrance
  2. 2.Univ. Paris Diderot, Sorbonne Paris Cité, IRIF, UMR 8243, CNRSParisFrance
  3. 3.Inria & LRI, CNRS, Univ. Paris-Sud, Université Paris-SaclayOrsayFrance

Personalised recommendations