Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Combination of Abstractions in the ASTREE Static Analyzer

De
29 pages
Combination of Abstractions in the ASTREE Static Analyzer? Patrick Cousot 2, Radhia Cousot 1, Jerome Feret 2, Laurent Mauborgne 2, Antoine Mine 2, David Monniaux 1,2 & Xavier Rival 2 1 Centre National de la Recherche Scientifique (CNRS) 2 Ecole Normale Superieure, Paris, France (Firstname.Lastname @ens.fr) Abstract. We describe the structure of the abstract domains in the Astree static analyzer, their modular organization into a hierarchical network, their cooperation to over-approximate the conjunction/reduced product of different abstractions and to ensure termination using collab- orative widenings and narrowings. This separation of the abstraction into a combination of cooperative abstract domains makes Astree extensi- ble, an essential feature to cope with false alarms and ultimately provide sound formal verification of the absence of runtime errors in very large software. 1 Introduction Astree is a static program analyzer based on abstract interpretation [1,2] which is aimed at proving automatically the absence of run time errors in programs written in a subset of the C programming language. It has been applied suc- cessfully to large embedded control/command safety-critical real-time software generated automatically from synchronous specifications, producing correctness proofs for complex software without any false alarm, within only a few hours of computation on personal computers [3,4,5,6]. More recently [7], it has been extended to handle other kinds of embedded software, some of which are hand- written.

  • abstract domains

  • program

  • run time

  • application domain-specific

  • dependencies between

  • centre national de la recherche scientifique

  • astree


Voir plus Voir moins
CombinationofAbstractionsintheASTRE´EStaticAnalyzerPatrickCousot2,RadhiaCousot1,Je´roˆmeFeret2,LaurentMauborgne2,AntoineMine´2,DavidMonniaux1,2&XavierRival21CentreNationaldelaRechercheScientifique(CNRS)2E´coleNormaleSupe´rieure,Paris,France(Firstname.Lastname@ens.fr)http://www.astree.ens.fr/Abstract.WedescribethestructureoftheabstractdomainsintheAstre´estaticanalyzer,theirmodularorganizationintoahierarchicalnetwork,theircooperationtoover-approximatetheconjunction/reducedproductofdifferentabstractionsandtoensureterminationusingcollab-orativewideningsandnarrowings.ThisseparationoftheabstractionintoacombinationofcooperativeabstractdomainsmakesAstre´eextensi-ble,anessentialfeaturetocopewithfalsealarmsandultimatelyprovidesoundformalverificationoftheabsenceofruntimeerrorsinverylargesoftware.1IntroductionAstre´eisastaticprogramanalyzerbasedonabstractinterpretation[1,2]whichisaimedatprovingautomaticallytheabsenceofruntimeerrorsinprogramswritteninasubsetoftheCprogramminglanguage.Ithasbeenappliedsuc-cessfullytolargeembeddedcontrol/commandsafety-criticalreal-timesoftwaregeneratedautomaticallyfromsynchronousspecifications,producingcorrectnessproofsforcomplexsoftwarewithoutanyfalsealarm,withinonlyafewhoursofcomputationonpersonalcomputers[3,4,5,6].Morerecently[7],ithasbeenextendedtohandleotherkindsofembeddedsoftware,someofwhicharehand-written.Astre´ewasdesignedusing:asyntax-directedrepresentationoftheprogramcontrolflow(functions,blockstructures);functionalrepresentationofabstractenvironmentswithsharing[3],formem-oryandtimeefficiency,andlimitedsupportforanalysisparallelization[8];basicabstractdomains,trackingvariablesindependently(integerandfloating-pointintervals[9]usingstagedwidenings);relationalabstractdomainstrackingdependenciesbetweenvariables–symboliccomputationandlinearizationofexpressions[10],–packedoctagons[11],ThisworkwassupportedinpartbytheFrenchexploratoryprojectAstre´eoftheRe´seauNationalderechercheetd’innovationenTechnologiesLogicielles(RNTL).
2P.Cousot,R.Cousot,J.Feret,L.Mauborgne,A.Mine´,D.Monniaux,X.Rival–application-awaredomains(suchastheellipsoidabstractdomainfordig-italfilters[12]orthearithmetic-geometricprogressionabstractdomain[13],e.g.toboundpotentiallydivergingcomputations);abstractdomainstrackingdependenciesbetweenbooleanvariablesandothervariables(booleanpartitioningdomain[4]),orthehistoryofcontrolflowbranchesandvaluesalongtheexecutiontrace(tracepartitioning[14]);amemoryabstractdomain[4]recentlyextendedtocopewithunionsandpointerarithmetics[7].Contrarytomanyprogramanalysissystems,Astre´edoesnothaveseparatephasesforpointer/aliasinganalysisandarithmeticanalysis.Toadjustthecost/precisionratiooftheanalysis,someoftheabstractdo-mainsareparametrized(e.g.maximalheightofdecisiontrees)andappliedlo-cally(e.g.tovariablespacks[4])accordingtolocaldirectivesautomaticallyin-sertedbytheanalyzer3.Theabstractdomainscommunicateasanapproximatereducedproduct[15]toorganizethecooperationbetweenabstractdomainsandallowforamodulardesignandrefinementoftheabstractionusedbyAstre´e.Inthispaperwedescribehowabstractdomainsareorganizedanddocooperate.Thismodulardesignallowsabstractdomainstobeturnedonandoffbyruntimeoptions,easyadditionofnewdomains,andthesuppressionofolderdomainsthathavebeensupersededbynewerones(suchastheclockdomain[3],nowsupersededbythearithmetic-geometricprogressionabstractdomain[5]).Finally,itallowstheadditionofnewreductions/communicationsbetweenexistingdomains.Astre´eisthereforeanextensibleabstractinterpreter,anessentialfeaturetocopewithfalsealarmsandultimatelyreachzerofalsealarm.Astre´eisprogrammedmostlyinOCaml[16](apartfromtheoctagondo-mainlibrary[17]andsomeplatform-specificdependencies,e.g.tocontroltheroundingbehavioroftheFPU).Itiscurrentlyapproximately80000lineslong.2HandlingFalseAlarmsAsallabstractinterpretation-basedstaticprogramanalyzers,Astre´emaybesubjecttofalsealarms;thatis,itmayreportpotentialbugsthathappeninnopossibleconcreteexecution,becauseoftheover-approximationofprogrambehaviorsentailedbyabstractions.Thus,whenAstre´eraisesanalarm,itmaybeatruealarm,duetoaruntimeerrorappearingatleastinoneprogramexecution,butitmayalsobeafalsealarmduetoexcessiveover-approximation.Thisisthecaseofallautomaticsoundformalmethodswhich,becauseofundecidabilityandinabsenceofhumaninteraction,mustbeincomplete,andhence,inmanycases,eitherexhausttimeorspaceresourcesorterminatewithfalsealarms.3Thesedirectivescanalsobeinsertedmanually,butsuchinterventionofend-usersmustbeavoided,inparticularforprogramssubjecttolong-termmodifications.