{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:50:06Z","timestamp":1743130206406,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452360"},{"type":"electronic","value":"9783030452377"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T00:00:00Z","timestamp":1587081600000},"content-version":"vor","delay-in-days":107,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The Debian distribution includes more than 28 thousand maintainer scripts, almost all of them are written in P<jats:sc>osix<\/jats:sc> shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for system maintenance. While Debian policy provides guidance for package maintainers producing the scripts, few tools exist to check the compliance of a script to it. We report on the application of a formal verification approach based on symbolic execution to find violations of some non-trivial properties required by Debian policy in maintainer scripts. We present our methodology and give an overview of our toolchain. We obtained promising results: our toolchain is effective in analysing a large set of Debian maintainer scripts and it pointed out over 150 policy violations that lead to reports (more than half already fixed) on the Debian Bug Tracking system.<\/jats:p>","DOI":"10.1007\/978-3-030-45237-7_14","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"235-253","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Analysing installation scenarios of Debian packages"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0819-8344","authenticated-orcid":false,"given":"Benedikt","family":"Becker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1969-1246","authenticated-orcid":false,"given":"Nicolas","family":"Jeannerod","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3035-1269","authenticated-orcid":false,"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0745-8730","authenticated-orcid":false,"given":"Yann","family":"R\u00e9gis-Gianas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1925-089X","authenticated-orcid":false,"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Treinen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"14_CR1","unstructured":"Lintian. https:\/\/lintian.debian.org"},{"key":"14_CR2","unstructured":"Piuparts. https:\/\/piuparts.debian.org\/"},{"issue":"1\u20132","key":"14_CR3","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0304-3975(94)90209-7","volume":"122","author":"H A\u00eft-Kaci","year":"1994","unstructured":"A\u00eft-Kaci, H., Podelski, A., Smolka, G.: A feature-based constraint system for logic programming with entailment. Theor. Comput. Sci. 122(1\u20132), 263\u2013283 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR4","unstructured":"Allbery, R., Whitton, S.: Debian policy manual (Oct 2019), https:\/\/www.debian.org\/doc\/debian-policy\/"},{"key":"14_CR5","unstructured":"Becker, B., March\u00e9, C.: Ghost Code in Action: Automated Verification of a Symbolic Interpreter. In: Chakraborty, S., A.Navas, J. (eds.) Verified Software: Tools, Techniques and Experiments. Lecture Notes in Computer Science (2019), https:\/\/hal.inria.fr\/hal-02276257"},{"key":"14_CR6","unstructured":"Becker, B., March\u00e9, C., Jeannerod, N., Treinen, R.: Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. Technical report, HAL Archives Ouvertes (Oct 2019), https:\/\/hal.inria.fr\/hal-02321743"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Let\u2019s verify this with Why3. International Journal on Software Tools for Technology Transfer (STTT) 17(6), 709\u2013727 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0314-5, http:\/\/hal.inria.fr\/hal-00967132\/en, see also http:\/\/toccata.lri.fr\/gallery\/fm2012comp.en.html","DOI":"10.1007\/s10009-014-0314-5"},{"key":"14_CR8","unstructured":"Debian Bug Tracker: dibbler-server: postinst contains invalid command. Debian Bug Reports 841934 (Oct 2016), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=841934"},{"key":"14_CR9","unstructured":"Debian Bug Tracker: authbind: maintainer script(s) not using strict mode. Debian Bug Report 866249 (Jun 2017), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=866249"},{"key":"14_CR10","unstructured":"Debian Bug Tracker: dict-freedict-all: postinst script has a wrong redirection. Debian Bug Report 908189 (Sep 2018), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=908189"},{"key":"14_CR11","unstructured":"Debian Bug Tracker: python3-neutron-fwaas-dashboard: incorrect test in postrm. Debian Bug Report 900493 (May 2018), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=900493"},{"key":"14_CR12","unstructured":"Debian Bug Tracker: [dpkg-maintscript-helper] bug in finish$$\\_$$dir$$\\_$$to$$\\_$$symlink. Debian Bug Report 922799 (Feb 2019), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=922799"},{"key":"14_CR13","unstructured":"Debian Bug Tracker: ndiswrapper: when \"postrm purge\" fails it may have deleted some config files. Debian Bug Report 942392 (Oct 2019), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=942392"},{"key":"14_CR14","unstructured":"Debian Bug Tracker: oz: non-idempotent postrm script. Debian Bug Report 942395 (Oct 2019), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=942395"},{"key":"14_CR15","unstructured":"Debian Bug Tracker: preinst script not posix compliant. Debian Bug Report 925006 (Mar 2019), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=925006"},{"key":"14_CR16","unstructured":"Debian Bug Tracker: rancid-cgi: preinst may fail and not rollback a change. Debian Bug Report 942388 (Oct 2019), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=942388"},{"key":"14_CR17","unstructured":"Debian Bug Tracker: sgml-base: preinst may fail *silently*. Debian Bug Report 929706 (May 2019), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=929706"},{"key":"14_CR18","unstructured":"Developer\u2019s Reference Team: Debian developers reference (Oct 2019), https:\/\/www.debian.org\/doc\/manuals\/developers-reference\/"},{"issue":"12","key":"14_CR19","doi-asserted-by":"publisher","first-page":"1144","DOI":"10.1016\/j.scico.2010.11.001","volume":"76","author":"R Di Cosmo","year":"2011","unstructured":"Di Cosmo, R., Di Ruscio, D., Pelliccione, P., Pierantonio, A., Zacchiroli, S.: Supporting software evolution in component-based FOSS systems. Science of Computer Programming 76(12), 1144\u20131160 (2011). https:\/\/doi.org\/10.1016\/j.scico.2010.11.001","journal-title":"Science of Computer Programming"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Gardner, P., Ntzik, G., Wright, A.: Local reasoning for the POSIX file system. In: European Symposium On Programming. Lecture Notes in Computer Science, vol. 8410, pp. 169\u2013188. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_10","DOI":"10.1007\/978-3-642-54833-8_10"},{"key":"14_CR21","unstructured":"Greenberg, M., Blatt, A.J.: Executable formal semantics for the POSIX shell. CoRR abs\/1907.05308 (2019), http:\/\/arxiv.org\/abs\/1907.05308"},{"key":"14_CR22","unstructured":"IEEE, The Open Group: The open group base specifications issue 7. http:\/\/pubs.opengroup.org\/onlinepubs\/9699919799\/ (2018)"},{"key":"14_CR23","unstructured":"Jeannerod, N., March\u00e9, C., Treinen, R.: A Formally Verified Interpreter for a Shell-Like Programming Language. In: 9th Working Conference on Verified Software:\nTheories, Tools, and Experiments. Lecture Notes in Computer Science, vol. 10712 (2017), https:\/\/hal.archives-ouvertes.fr\/hal-01534747"},{"key":"14_CR24","unstructured":"Jeannerod, N., R\u00e9gis-Gianas, Y., March\u00e9, C., Sighireanu, M., Treinen, R.: Specification of UNIX utilities. Technical report, HAL Archives Ouvertes (Oct 2019), https:\/\/hal.inria.fr\/hal-02321691"},{"key":"14_CR25","unstructured":"Jeannerod, N., R\u00e9gis-Gianas, Y., Treinen, R.: Having fun with 31.521 shell scripts. Tech. rep., HAL Archives Ouvertes (2017), https:\/\/hal.archives-ouvertes.fr\/hal-01513750"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Jeannerod, N., Treinen, R.: Deciding the First-Order Theory of an Algebra of Feature Trees with Updates. In: Galmiche, D., Schulz, S., Sebastiani, R.  (eds.) 9th International Joint Conference on Automated Reasoning. Lecture Notes in\nComputer Science, vol. 10900, pp. 439\u2013454. Springer, Oxford, UK (Jul 2018),\nhttps:\/\/hal.archives-ouvertes.fr\/hal-01807474","DOI":"10.1007\/978-3-319-94205-6_29"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Mazurak, K., Zdancewic, S.: ABASH: finding bugs in bash scripts. In: Workshop on Programming Languages and Analysis for Security. pp. 105\u2013114 (2007)","DOI":"10.1145\/1255329.1255347"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Ntzik, G., Gardner, P.: Reasoning about the POSIX file system: local update and global pathnames. In: Object-Oriented Programming, Systems, Languages and Applications. pp. 201\u2013220. ACM (2015). https:\/\/doi.org\/10.1145\/2814270.2814306","DOI":"10.1145\/2814270.2814306"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Ntzik, G., da Rocha Pinto, P., Sutherland, J., Gardner, P.: A concurrent specification of POSIX file systems. In: European Conference on Object-Oriented Programming. LIPIcs, vol. 109, pp. 4:1\u20134:28. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2018.4","DOI":"10.4230\/LIPIcs.ECOOP.2018.4"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"R\u00e9gis-Gianas, Y., Jeannerod, N., Treinen, R.: Morbig: A static parser for POSIX shell. In: Pearce, D., Mayerhofer, T., Steimann, F. (eds.) ACM SIGPLAN International Conference on Software Language Engineering. pp. 29\u201341. Boston, MA, USA (Nov 2018). https:\/\/doi.org\/10.1145\/3276604.3276615, https:\/\/hal.archives-ouvertes.fr\/hal-01890044","DOI":"10.1145\/3276604.3276615"},{"key":"14_CR31","unstructured":"Rosenfeld, R.: Package rancid-cgi: looking glass cgi based on rancid tools (2019), https:\/\/packages.debian.org\/en\/sid\/rancid-cgi"},{"key":"14_CR32","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0743-1066(92)90039-6","volume":"12","author":"G Smolka","year":"1992","unstructured":"Smolka, G.: Feature constraint logics for unification grammars. Journal of Logic Programming 12, 51\u201387 (1992)","journal-title":"Journal of Logic Programming"},{"issue":"3","key":"14_CR33","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0743-1066(94)90044-2","volume":"18","author":"G Smolka","year":"1994","unstructured":"Smolka, G., Treinen, R.: Records for logic programming. Journal of Logic Programming 18(3), 229\u2013258 (1994)","journal-title":"Journal of Logic Programming"},{"key":"14_CR34","unstructured":"The CoLiS project: The CoLiS bench. http:\/\/ginette.informatique.univ-paris-diderot.fr\/~niols\/colis-batch\/"},{"key":"14_CR35","unstructured":"The CoLiS project: The CoLiS toolchain. https:\/\/github.com\/colis-anr"},{"key":"14_CR36","doi-asserted-by":"publisher","unstructured":"The CoLiS project: Artifact for Analysing installation scenarios of Debian Packages. Zenodo Repository (Feb 2020). https:\/\/doi.org\/10.5281\/zenodo.3678390","DOI":"10.5281\/zenodo.3678390"},{"key":"14_CR37","unstructured":"The Debian Project: Bugs tagged colis, https:\/\/bugs.debian.org\/cgi-bin\/pkgreport.cgi?tag=colis-shparser;users=treinen@debian.org"},{"key":"14_CR38","unstructured":"The Linux Foundation: Filesystem hierarchy standard, version 3.0 (Mar 2015), https:\/\/refspecs.linuxfoundation.org"},{"key":"14_CR39","unstructured":"Ucko, A.M.: cmigrep: broken emacsen-install script. Debian Bug Report 431131 (Jun 2007), https:\/\/bugs.debian.org\/cgi-bin\/bugreport.cgi?bug=431131"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45237-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:06:17Z","timestamp":1616436377000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45237-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452360","9783030452377"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45237-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"155","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}