29 Pages
English

Combination of Abstractions in the ASTREE Static Analyzer

-

Gain access to the library to view online
Learn more

Description

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


Subjects

Informations

Published by
Reads 18
Language English

Exrait

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.