We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Analysing installation scenarios of Debian packages

00:00

Formal Metadata

Title
Analysing installation scenarios of Debian packages
Title of Series
Number of Parts
22
Author
Contributors
License
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
The Debian distribution includes more than 28 thousand maintainer scripts, almost all of them are written in Posix 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.
Keywords
Demo (music)Standard Generalized Markup LanguageInstallation artError messageProcess (computing)CodeCache (computing)Scripting languageRun time (program lifecycle phase)Identity managementPermianFlowchartMessage passingFormal verificationComputing platformFormal languageGastropod shellGenetic programmingAtomic numberParsingInterpreter (computing)Network topologyConstraint (mathematics)Physical systemSystems engineeringPersonal digital assistantRootString (computer science)Equals signDirectory serviceConstructor (object-oriented programming)Computer configurationData miningMixed realityTranslation (relic)Regulärer Ausdruck <Textverarbeitung>Mathematical analysisCodeDiagramLogicOrder (biology)Theory of relativityParsingNetwork topologyFunction (mathematics)File systemModulare ProgrammierungSemantics (computer science)ParsingFluid staticsLevel (video gaming)Variable (mathematics)Well-formed formulaSoftware testingFiber bundleFlow separationComputer configurationConstraint (mathematics)State of matterArithmetic meanProof theoryForm (programming)Formal grammarContent (media)Interpreter (computing)Maxima and minimaAtomic numberPhysical systemFlowchartProjective planeResultantReal numberParameter (computer programming)CASE <Informatik>Standard Generalized Markup LanguageProcess (computing)Software bugDirectory serviceAbstractionSystem administratorError messagePresentation of a groupDistribution (mathematics)Gastropod shellSet (mathematics)outputInstallation artObservational studyLatent heatElectronic mailing listScripting languageTraffic reportingComputer fileInfinite setMiniDiscRepresentation (politics)Computing platformSymbol tableContext awarenessMultiplication signStandard deviationComputer animation
Transcript: English(auto-generated)