A gentle introduction to formal verification of computer systems

Patrick Cousot

Description

A gentle introduction to formal verification of computer systems by abstract interpretation Patrick COUSOT a, Radhia COUSOT b a École normale supérieure and New York University b École normale supérieure and CNRS Abstract. We introduce and illustrate basic notions of abstract interpretation theory and its applications by relying on the readers general scientific culture and basic knowledge of computer programming. Keywords. Abstract interpretation, Formal methods, Verification, Static analysis. 1. Introduction Software is in all mission-critical and safety-critical industrial infrastructures since it is, in principle, the cheapest and most effective way to control complex systems in real time. However, all computer scientists have experienced costly bugs in embedded software. The failure of the Ariane 5.01 maiden flight [40] (due to an overflow), the failure of the Patriot missile [57] during the Gulf war (due to an accumulated rounding error), the loss of Mars orbiter [1] (due to a unit error), the crash of the twin-engined Chinook ZD 576 helicopter [8]1 are a few examples showing that mission-critical and safety-critical software can be far from being safe. Computer scientists agree on the fact that it is preferable to verify that mission- critical or safety critical software (and nowadays hardware) programs do not go wrong before running them. As an alternative to testing, which hardly scales up at reasonable costs and with a satisfactory coverage, automated formal verification has emerged, this last decade, as a promising useful complement, with interesting potential industrial ap- plications.

• runtime properties


• all mission-critical


• int fact


• make automatic proofs


• program yields


• static analysis


• bugs


• software


• verify program

Sujets

• Neumann
• Static analysis
• Software

Informations

• Publié par: pefav
• Nombre de lectures: 14
• Langue: English
• Poids de l'ouvrage: 11 Mo

Extrait

Agentleintroductionto formalverificationofcomputersystems byabstractinterpretation PatrickCOUSOT a ,RadhiaCOUSOT b a ÉcolenormalesupérieureandNewYorkUniversity b ÉcolenormalesupérieureandCNRS Abstract.Weintroduceandillustratebasicnotionsofabstractinterpretationtheory anditsapplicationsbyrelyingonthereadersgeneralscientificcultureandbasic knowledgeofcomputerprogramming. Keywords.Abstractinterpretation,Formalmethods,Verification,Staticanalysis. 1.Introduction Softwareisinallmission-criticalandsafety-criticalindustrialinfrastructuressinceitis, inprinciple,thecheapestandmosteffectivewaytocontrolcomplexsystemsinrealtime. However,allcomputerscientistshaveexperiencedcostlybugsinembeddedsoftware. ThefailureoftheAriane5.01maidenflight[40](duetoanoverflow),thefailureof thePatriotmissile[57]duringtheGulfwar(duetoanaccumulatedroundingerror),the lossofMarsorbiter[1](duetoauniterror),thecrashofthetwin-enginedChinookZD 576helicopter[8] 1 areafewexamplesshowingthatmission-criticalandsafety-critical softwarecanbefarfrombeingsafe. Computerscientistsagreeonthefactthatitispreferabletoverifythatmission- criticalorsafetycriticalsoftware(andnowadayshardware)programsdonotgowrong beforerunningthem.Asanalternativetotesting,whichhardlyscalesupatreasonable costsandwithasatisfactorycoverage,automatedformalverificationhasemerged,this lastdecade,asapromisingusefulcomplement,withinterestingpotentialindustrialap- plications. Formalmethodsdatebacktotheearlydaysofcomputerscience(theFloyd/Naur/ Hoareverificationmethod[33,51,37]appearedinthesixtieswithantecedentsgoingback toVonNeumannandTuring[38])andthepowerofpresent-daycomputersmakethem applicabletolargescaleindustrialprojects.Theideaistomakeautomaticproofsat compile-timetoverifyprogramruntimeproperties. 1 “Inthesummerof1993anindependentdefenceITcontractor,EDS-SCICON,wasinstructedtoreviewthe FADEC[FullAuthorityDigitalEngineControl]software;afterexaminingonly18percentofthecodethey found486anomaliesandstoppedthereview.”[8]

Beyondthedifficultyofspecifyingwhichruntimepropertiesareofinterest,allfor- malmethodsarefacedwithundecidability(themathematicalimpossibilityforacom- puter,whichisafinitedevice,toproveforsurenon-trivialpropertiesofthe(infiniteor extremelylarge)runtimebehaviorsofcomputerprograms)andcomplexity(theimpos- sibilityforcomputerstosolvedecidablequestionswithinareasonableamountoftime andmemoryforlargeinputdata,suchasprogramexecutionsobservedoververylong periodsoftime). Besidestestingwhichisnotaformalmethod,threemainapproacheshavebeencon- sideredforformalverification,allofthembeingapproximationsoftheprogramseman- tics(formallydefiningthepossibleexecutionsinallpossibleenvironments)formalized byabstractinterpretationtheory: • Deductivemethodsproduceformalmathematicalcorrectnessproofsusingtheo- remproversorproofassistantsandneedhumaninteractiontoprovideinductive arguments(whichhardlyscalesupforlargeprogramswhicharemodifiedover longperiodsoftimes)andhelpinproofs(suchasproofhintsorstrategies); • Model-checkingexhaustivelyexploresfinitarymodelsofprogramexecutions, whichcanbesubjecttocombinatorialexplosion,requiresthehumanproduction ofmodels(ormaynotterminateincaseofautomaticrefinementofthemodel). Analternativeistoexplorepartiallythemodelbutthisisthendebugging,not verification; • Staticanalysis,whichautomatestheabstractionoftheprogramexecution,always terminatesbutcanbesubjecttofalsealarms(thatiswarningsthatthespecification maynotbesatisfiedalthoughnoactualexecutionoftheprogramcanviolatethis specification). Inthispaper,weexplaininformallyandintuitivelytheunderlyingideasofabstract interpretation-basedstaticanalysis,whichconsistsinabstractingtheprogramsemantics (formalizingprogramexecutions)toprovideasoundover-approximationofthepotential errorswithrespecttoaspecification. Staticanalysisinvolvesabstractionsoftheprogramsemanticsthatmustbecoarse enoughtobeeffectivelycomputableandpreciseenoughtoimplythepropertiesrequired bythespecification.Toshowthatsuchabstractionsdoexistforgivenfamiliesofappli- cationsandspecifications,wereportontheA STRÉE analyzer( www.astree.ens.fr/ ), whichisastaticanalyzerforprovingtheabsenceofruntime-errorsinsynchronous,time- triggered,real-time,safetycritical,embeddedsoftwarewrittenorautomaticallygener- atedintheCprogramminglanguage.Ithasbeensuccessfullyappliedtoprovetheab- senceofruntimeerrorsinthecontrol-commandpartoftheprimaryflightcontrolsoft- wareofthefly-by-wiresystemofairplanes. 2.Softwarebugs 2.1.Numericalsoftwarebugs Letusstartbyconsideringclassicalbugsinnumericalcomputations.