Combination of Abstractions in the ASTREE Static Analyzer

Patrick Cousot

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

Sujets

• Family name
• Structure
• Program
• Run time
• Centre national de la recherche scientifique
• Astrée

Informations

• Publié par: pefav
• Nombre de lectures: 18
• Langue: English

Extrait

CombinationofAbstractionsintheA STRE ´ E StaticAnalyzer ⋆ PatrickCousot 2 ,RadhiaCousot 1 ,Je´roˆmeFeret 2 ,LaurentMauborgne 2 , AntoineMine´ 2 ,DavidMonniaux 1,2 &XavierRival 2 1 CentreNationaldelaRechercheScientifique(CNRS) 2 E ´ coleNormaleSupe´rieure,Paris,France( Firstname . Lastname @ens.fr ) http://www.astree.ens.fr/ Abstract. Wedescribethestructureoftheabstractdomainsinthe Astre ´ estaticanalyzer,theirmodularorganizationintoahierarchical network,theircooperationtoover-approximatetheconjunction/reduced productofdifferentabstractionsandtoensureterminationusingcollab- orativewideningsandnarrowings.Thisseparationoftheabstractioninto acombinationofcooperativeabstractdomainsmakes Astre ´ e extensi- ble,anessentialfeaturetocopewithfalsealarmsandultimatelyprovide soundformalverificationoftheabsenceofruntimeerrorsinverylarge software. 1Introduction Astre ´ e isastaticprogramanalyzerbasedonabstractinterpretation[1,2]which isaimedatprovingautomaticallytheabsenceofruntimeerrorsinprograms writteninasubsetoftheCprogramminglanguage.Ithasbeenappliedsuc- cessfullytolargeembeddedcontrol/commandsafety-criticalreal-timesoftware generatedautomaticallyfromsynchronousspecifications,producingcorrectness proofsforcomplexsoftwarewithoutanyfalsealarm,withinonlyafewhours ofcomputationonpersonalcomputers[3,4,5,6].Morerecently[7],ithasbeen extendedtohandleotherkindsofembeddedsoftware,someofwhicharehand- written. Astre ´ ewasdesignedusing: – asyntax-directedrepresentationoftheprogramcontrolflow(functions,block structures); – functionalrepresentationofabstractenvironmentswithsharing[3],formem- oryandtimeefficiency,andlimitedsupportforanalysisparallelization[8]; – basicabstractdomains,trackingvariablesindependently(integerandfloating- pointintervals[9]usingstagedwidenings); – relationalabstractdomainstrackingdependenciesbetweenvariables –symboliccomputationandlinearizationofexpressions[10], –packedoctagons[11], ⋆ ThisworkwassupportedinpartbytheFrenchexploratoryproject Astre ´ e ofthe Re´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); – abstractdomainstrackingdependenciesbetweenbooleanvariablesandother variables(booleanpartitioningdomain[4]),orthehistoryofcontrolflow branchesandvaluesalongtheexecutiontrace(tracepartitioning[14]); – amemoryabstractdomain[4]recentlyextendedtocopewithunionsand pointerarithmetics[7]. Contrarytomanyprogramanalysissystems, Astre ´ e doesnothaveseparate phasesforpointer/aliasinganalysisandarithmeticanalysis. Toadjustthecost/precisionratiooftheanalysis,someoftheabstractdo- mainsareparametrized(e.g.maximalheightofdecisiontrees)andappliedlo- cally(e.g.tovariablespacks[4])accordingtolocaldirectivesautomaticallyin- sertedbytheanalyzer 3 . Theabstractdomainscommunicateasanapproximatereducedproduct[15] toorganizethecooperationbetweenabstractdomainsandallowforamodular designandrefinementoftheabstractionusedby Astre ´ e .Inthispaperwe describehowabstractdomainsareorganizedanddocooperate. Thismodulardesignallowsabstractdomainstobeturnedonandoffby runtimeoptions,easyadditionofnewdomains,andthesuppressionofolder domainsthathavebeensupersededbynewerones(suchastheclockdomain [3],nowsupersededbythearithmetic-geometricprogressionabstractdomain [5]).Finally,itallowstheadditionofnewreductions/communicationsbetween existingdomains. Astre ´ e isthereforeanextensibleabstractinterpreter,an essentialfeaturetocopewithfalsealarmsandultimatelyreachzerofalsealarm. Astre ´ eisprogrammedmostlyinOCaml[16](apartfromtheoctagondo- mainlibrary[17]andsomeplatform-specificdependencies,e.g.tocontrolthe roundingbehavioroftheFPU).Itiscurrentlyapproximately80000lineslong. 2HandlingFalseAlarms Asallabstractinterpretation-basedstaticprogramanalyzers, Astre ´ e maybe subjecttofalsealarms;thatis,itmayreportpotentialbugsthathappenin nopossibleconcreteexecution,becauseoftheover-approximationofprogram behaviorsentailedbyabstractions.Thus,when Astre ´ e raisesanalarm,itmay beatruealarm,duetoaruntimeerrorappearingatleastinoneprogram execution,butitmayalsobeafalsealarmduetoexcessiveover-approximation. Thisisthecaseofallautomaticsoundformalmethodswhich,becauseof undecidabilityandinabsenceofhumaninteraction,mustbeincomplete,and hence,inmanycases,eitherexhausttimeorspaceresourcesorterminatewith falsealarms. 3 Thesedirectivescanalsobeinsertedmanually,butsuchinterventionofend-users mustbeavoided,inparticularforprogramssubjecttolong-termmodifications.