Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 5/2022

23-09-2022 | General

The CoLiS platform for the analysis of maintainer scripts in Debian software packages

Authors: Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen

Published in: International Journal on Software Tools for Technology Transfer | Issue 5/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The software packages of the Debian distribution include more than twenty-seven thousand maintainer scripts in total, almost all of them being written in the Posix shell language. These scripts are executed with root privileges at installation, update, and removal of a package, which makes them critical for system maintenance. While the Debian policy provides guidance for package maintainers producing the scripts, only few tools exist to check the compliance of a script to that policy. We present CoLiS, a software platform for discovering violations of non-trivial properties required by the Debian policy in maintainer scripts. We describe our methodology which is based on symbolic execution and feature tree constraints, and we give an overview of the toolchain. We obtain promising results: our toolchain is effective in analysing a large set of Debian maintainer scripts, and it has already detected over 150 policy violations that have led to bug reports, more than two-third of them now being fixed.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
According to the POSIX standard, the maximal number of bytes in a filename is defined by the constant NAME_MAX in the file limits.h, the value of which must not be smaller than  14.
 
Literature
2.
go back to reference Aït-Kaci, Hassan, Podelski, Andreas, Smolka, Gert: A feature-based constraint system for logic programming with entailment. Theoret. Comput. Sci. 122(1–2), 263–283 (1994)MathSciNetCrossRefMATH Aït-Kaci, Hassan, Podelski, Andreas, Smolka, Gert: A feature-based constraint system for logic programming with entailment. Theoret. Comput. Sci. 122(1–2), 263–283 (1994)MathSciNetCrossRefMATH
4.
go back to reference Bach, M.J.: The Design of the UNIX Operating System, Prentice-Hall (1986) Bach, M.J.: The Design of the UNIX Operating System, Prentice-Hall (1986)
5.
go back to reference Becker, B., Marché, C., Jeannerod, N., Treinen, R.: Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. Technical report, HAL Archives Ouvertes, October 2019. URL: https://hal.inria.fr/hal-02321743 Becker, B., Marché, C., Jeannerod, N., Treinen, R.: Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. Technical report, HAL Archives Ouvertes, October 2019. URL: https://​hal.​inria.​fr/​hal-02321743
7.
go back to reference Becker, B. and Marché, C.: Ghost Code in Action: Automated Verification of a Symbolic Interpreter. In: Chakraborty, S. and Navas, J.A. (eds.), Verified Software: Tools, Techniques and Experiments, Lecture Notes in Computer Science, 2019. URL: https://hal.inria.fr/hal-02276257 Becker, B. and Marché, C.: Ghost Code in Action: Automated Verification of a Symbolic Interpreter. In: Chakraborty, S. and Navas, J.A. (eds.), Verified Software: Tools, Techniques and Experiments, Lecture Notes in Computer Science, 2019. URL: https://​hal.​inria.​fr/​hal-02276257
9.
go back to reference Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Let’s verify this with Why3. Int. J. Softw. Tools Technol. Transf. (STTT) 17(6), 709–727 (2015)CrossRef Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Let’s verify this with Why3. Int. J. Softw. Tools Technol. Transf. (STTT) 17(6), 709–727 (2015)CrossRef
24.
26.
go back to reference Jeannerod, N., Marché, C., Treinen, R.: A Formally Verified Interpreter for a Shell-like Programming Language. In: 9th Working Conference on Verified Software: Theories, Tools, and Experiments, volume 10712 of Lecture Notes in Computer Science, 2017. URL: https://hal.archives-ouvertes.fr/hal-01534747 Jeannerod, N., Marché, C., Treinen, R.: A Formally Verified Interpreter for a Shell-like Programming Language. In: 9th Working Conference on Verified Software: Theories, Tools, and Experiments, volume 10712 of Lecture Notes in Computer Science, 2017. URL: https://​hal.​archives-ouvertes.​fr/​hal-01534747
29.
go back to reference Jeannerod, N., Treinen, R.: Deciding the first-order theory of an algebra of feature trees with updates. In: Galmiche, D., Schulz, S. and Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning, volume 10900 of Lecture Notes in Computer Science, pp. 439–454, Oxford, UK, July 2018. Springer. URL: https://hal.archives-ouvertes.fr/hal-01807474 Jeannerod, N., Treinen, R.: Deciding the first-order theory of an algebra of feature trees with updates. In: Galmiche, D., Schulz, S. and Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning, volume 10900 of Lecture Notes in Computer Science, pp. 439–454, Oxford, UK, July 2018. Springer. URL: https://​hal.​archives-ouvertes.​fr/​hal-01807474
31.
go back to reference Mazurak, K., Zdancewic, S.: ABASH: finding bugs in bash scripts. In: Workshop on Programming Languages and Analysis for Security, pp. 105–114, (2007) Mazurak, K., Zdancewic, S.: ABASH: finding bugs in bash scripts. In: Workshop on Programming Languages and Analysis for Security, pp. 105–114, (2007)
32.
go back to reference Ntzik, G., da Rocha Pinto, P., Sutherland, J., and Gardner, P.: A concurrent specification of Posix file systems. In: European Conference on Object-Oriented Programming, volume 109 of LIPIcs, pp. 4:1–4:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018). https://doi.org/10.4230/LIPIcs.ECOOP.2018.4 Ntzik, G., da Rocha Pinto, P., Sutherland, J., and Gardner, P.: A concurrent specification of Posix file systems. In: European Conference on Object-Oriented Programming, volume 109 of LIPIcs, pp. 4:1–4:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018). https://​doi.​org/​10.​4230/​LIPIcs.​ECOOP.​2018.​4
34.
go back to reference Régis-Gianas, Y., Jeannerod, N., Treinen, R.: Morbig: a static parser for POSIX shell. J. Comput. Lang. 57, 100944 (2020)CrossRef Régis-Gianas, Y., Jeannerod, N., Treinen, R.: Morbig: a static parser for POSIX shell. J. Comput. Lang. 57, 100944 (2020)CrossRef
Metadata
Title
The CoLiS platform for the analysis of maintainer scripts in Debian software packages
Authors
Benedikt Becker
Nicolas Jeannerod
Claude Marché
Yann Régis-Gianas
Mihaela Sighireanu
Ralf Treinen
Publication date
23-09-2022
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 5/2022
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00671-1

Other articles of this Issue 5/2022

International Journal on Software Tools for Technology Transfer 5/2022 Go to the issue

Premium Partner