Abstract Interpretation of Mobile Systems

Jérôme Feret

Description

Abstract Interpretation of Mobile Systems 1 Jerome Feret Departement d'Informatique de l'Ecole Normale Superieure, 75230 PARIS Cedex 5, FRANCE Abstract We propose an Abstract Interpretation-based context-free analysis for mobile sys- tems written in the pi-calculus. Our analysis automatically captures a sound – but not complete – description of the potential behavior of a mobile system interacting with an unknown context. It focuses on both the control flow and the occurrence number of agents during computation sequences. Control flow analysis detects all the possible interactions between the agents of a system, but also the potential interactions with the context. In order to deal with dynamic creation of both names and agents which is an inherent feature of mobility, our analysis distinguishes between recursive instances of the same agent. This way, we are able to prove the integrity of an ftp-server used by an unbounded number of clients. Occurrence counting analysis just consists in abstracting the occurrence number of instances of agents. Our abstraction is relational; this makes us able to detect both quickly and precisely mutual exclusion and non-exhaustion of resources. Key words: mobility, pi-calculus, static analysis, abstract interpretation, control flow analysis, occurrence counting analysis, worst case analysis. 1 Introduction The development of large scale communicating distributed systems demands the design of methods for analyzing mobile systems.

• agent can


• abstract interpretation


• comparisons between


• agent


• abstract interpretation-based analysis


• analysis just


• analysis detects


• dependent counts

Sujets

• Abstract interpretation

Informations

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

Extrait

AbstractInterpretationofMobileSystems
1

Je´roˆmeFeret
De´partementd’Informatiquedel’E´coleNormaleSupe´rieure,
75230PARISCedex5,FRANCE

Abstract
WeproposeanAbstractInterpretation-basedcontext-freeanalysisformobilesys-
temswritteninthe
π
-calculus.Ouranalysisautomaticallycapturesasound–but
notcomplete–descriptionofthepotentialbehaviorofamobilesysteminteracting
withanunknowncontext.Itfocusesonboththecontrolflowandtheoccurrence
numberofagentsduringcomputationsequences.
Controlflowanalysisdetectsallthepossibleinteractionsbetweentheagentsofa
system,butalsothepotentialinteractionswiththecontext.Inordertodealwith
dynamiccreationofbothnamesandagentswhichisaninherentfeatureofmobility,
ouranalysisdistinguishesbetweenrecursiveinstancesofthesameagent.Thisway,
weareabletoprovetheintegrityofan
ftp
-serverusedbyanunboundednumber
ofclients.Occurrencecountinganalysisjustconsistsinabstractingtheoccurrence
numberofinstancesofagents.Ourabstractionisrelational;thismakesusableto
detectbothquicklyandpreciselymutualexclusionandnon-exhaustionofresources.

Keywords:
mobility,
π
-calculus,staticanalysis,abstractinterpretation,control
flowanalysis,occurrencecountinganalysis,worstcaseanalysis.

1Introduction

Thedevelopmentoflargescalecommunicatingdistributedsystemsdemands
thedesignofmethodsforanalyzingmobilesystems.Insuchsystems,agent
distributiondynamicallychangesduringcomputation,makingtheiranalysisa
verydifficulttask.Furthermore,thesizeofthesesystems,suchastheInternet
forinstance,islargeenoughtopreventasinglepersonfromknowingthe
wholesystem.Thisiswhyweareinterestedinvalidatingpropertiesona
1
ThisworkwassupportedbytheRTDprojectIST-1999-20527“DAEDALUS”of
theEuropeanFP5programme.

PreprintsubmittedtoElsevierScience

11March2004

mobilesystemwhichbelongstoabiggerone,calleditscontext,withouthaving
preciseknowledgeofthiscontext.WeproposeafullyautomaticAbstract
Interpretation-basedanalysisfordetectingandprovingsomepropertiesof
suchmobilesystems.

Inthisstudy,wefocusonmobilesystemsdescribedinthe
π
-calculus[22,23]
whichisaformalismwellsuitedforunderstandingtheproblemsrelatedtomo-
bility.The
π
-calculusdescribessystemsofagentswhichmayinteractviathe
communicationofchannelnamesthroughchannels.Whenreceivingachannel
name,anagentgetssomecontroloverthisname:itcancommunicatewith
otheragentssharingthisnameorevencommunicatethisnametootheragents.
Theexpressivepowerofthe
π
-calculusalsofollowsfromareplicationmecha-
nism,whichallowsthespawningofnumberofinstancesofasameagent.Thus,
eachinstanceofeachagentopensitsownchannelsandcanthencommuni-
catetheirnamestootheragents.Thesemanticsofthe
π
-calculusisusually
describeduptoacongruencerelation.Thisrelationallowsagentstointeract
bysolvingconflictbetweenchannelnamesandmakingtheagentsmoveinthe
syntacticdescriptionofthesystem.Nevertheless,becauseofthiscongruence
relation,itwouldbeverydifficulttoderiveanabstractionoftheusualse-
manticsofthe
π
-calculus.Tosolvethisproblem,weintroduceanon-standard
semantics.Thisnon-standardsemanticsisfullyoperational(i.e.itrequires
nocongruencerelation).Itusesafreshnameallocationscheme,inorderto
providefreshnamestoopenedchannels,anddescribesconfigurationsassets
ofagents,sothatthecongruencerelationisnolongerrequired.Moreover,this
freshnameallocationschemeallowsustoencodesomeinterestingproperties
inthesemantics,suchasthefactthattwochannelshavebeenopenedbythe
sameinstanceofanagent,orbytwosuccessiveinstancesofanagent.

Havingchosentheappropriatesemantics,weusetheAbstractInterpretation
frameworktodesigndecidableanalysesofthe
π
-calculus.Thisframeworkis
highlygeneric:itcanbeappliedtovariousanalyses,providedsomeabstract
primitivesaregiven.Moreover,itisextensible:itallowsustobuildthe(ap-
proximatedreduced)productofseveralanalysesexpressedinthisframework.
Wethenuseourframeworktoaddresstwoorthogonalissues:thecontrolflow
andtheoccurrencecounting.Controlflowanalysisconsistsindetectingthe
setofagentinstancesthatcanreceivethenamesofthechannelsopenedbya
giveninstanceofanagent.Thisanalysisiscontext-free:itwilldetectwhich
channelnamescanbecommunicatedtothecontext.Itisalsonon-uniform
inthesensethatitdistinguishesbetweenrecursiveinstancesofagents.Itcan
prove,forinstance,thatanamecanbecommunicatedtoonlyoneotherin-
stanceofanagent,andnottotheotherones.Inthecaseofthe
ftp
-server,
itdetectsthattheservercanreturnaqueryonlytothecorrectclienteven
inthecasewhereanunboundednumberofclientsarecreated.Occurrence
countinganalysisconsistsinabstractingtheoccurrencenumberofinstances
ofagentsduringcomputationsequences.Itisespeciallyusefultodetectmu-

2

tualexclusion.Italsohelpsindiscoveringaboundtothenumberofagents
duringcomputationsequences,sothatwecanverifythatsomepartofthe
systemswillnotexceedphysicallimitsimposedbytheimplementationofthe
system.Inthecaseofthe
ftp
-server,wecanautomaticallyinferthemaximum
numberofsimultaneousclientsessions.Ourapproachreliesontheuseofa
reducedproductbetweenanon-relationalandarelationaldomain.Complex-
ityproblemsaresolvedbyusingapproximatedalgorithmsforcalculatinga
reductionbetweenthesetwodomains.
Asaresultwegetapolynomialanalysiswhichhasbeenimplementedin
Ocaml
.Thecorrespondingprototypecanbeusedonthewebat:

http://www.di.ens.fr/~feret/prototypes/prototypes.html.en
Someexamplesandashorttutorialarealsoprovided.
RelatedworksarediscussedinSect.2.Thestandardsemanticsofthe
π
-
calculusisgiveninSect.3.ItisfirstrefinedinSect.4andextendedtoopen
systemsinSect.5.AgenericabstractanalysisisdesignedinSect.6.Itis
instantiatedinbothSect.7andSect.8toget,respectively,acontrolflowand
anoccurrencecountinganalysis.Complexityresultsandanalysistimesare
giveninSect.9.

2Relatedwork

Flowanalysis.
Controlflowanalysesfocusontheexplicitflowofinformation.
Nielson
etal.
useabstractinterpretationin[1–3]toinferauniformdescrip-
tionoftheinteractionsbetweenagentsandapplySeidl’ssolvertogetacubic
implementationoftheiranalysisin[25].HennessyandRielyhavedesigneda
type-basedanalysiswiththesameexpressivepowerin[19].Theseanalysesuse
explicitinformationflowtodetectwhethersomesecurityconstraintsspecified
usingasecuritylevelcannotbeviolated.Nevertheless,theseanalyzesareuni-
form(or
mono-variant
).Theycannotdistinguishbetweendistinctinstances
ofthesameagent.Forexample,itisimpossibletogivedistinctsecuritylevels
todistinctinstancesofthesameagent.Systemspecificationcouldberewrit-
tensothatseveralinstancesofagivenagentaresyntacticlydistinguished
fromtheothers.Therefore,thisrequiresahumaninterventiontoguesswhich
replicationhavetobesyntacticallyunfoldedandhowmanyinstanceshave
tobedistinguished.Ouranalysisrequiresnohumananalysis,andcanfind
interestingpropertiesevenifanarbitrarynumberofinstanceshavetobe
distinguished.Moreover,itisnotobviousinmanycasesthatthereexistsa
syntacticrewritingofthesystemsothatseveraldifferentrecursiveinstances
canbedistinguishedonpurelysyntacticgroundandwherethesecuritypolicy

3

ischeckableusingpurelyuniformanalyses.

Cardelli
etal.
usegroupcreationin[4]toassigndependentsecuritylevels
tochannelnames.Agroupcanbeassociatedwitheachrecursiveinstanceof
anagent,andcanthenbeusedtopreventnamesofchannelsfromexiting
thescopeoftheinstancewhichhasopenedthesechannels.Nevertheless,our
analysisismuchmoreexpressive:wecaninferalgebraiccomparisonsbetween
agentinstances,whichallowsustoexpressthefactthataninstanceofan
agentcanonlycommunicatewiththenextinstanceofitorwiththeprevious
one.Asaconsequence,wecanprovethatthenameofachannelissentback
totheinstancewhichhaspreviouslyopenedthischannel,evenifthisnameis
notconfinedintothescopeofthisrecursiveinstance.

Venethasalreadyproposedanon-uniformanalysisin[30,31].Thisanalysis
infersasoundnon-uniformdescriptionofthetopologyofcommunications
betweentheagentsof
friendlysystems
[22],inwhichreplicationguardscannot
benestedandsystemsareclosed.Themaincontributionswithrespectto
Venet’sworkare:

(1)theextensionofthenon-uniformanalysistoagentswithnestedreplica-
tionguards;
(2)theextensiontoopensystemsactinginapossiblyunknowncontext;
(3)theoccurrencecountinganalysis.

Occurrencecountinganalysis.
Onlyveryfewanalysesforcountingoccur-
rencesofagentshavebeenpublished.Nevertheless,thisproblemisveryclose
totheproblemofapproximatingthebehaviorofaPetrinet,andofoccur-
rencecountinginmobileambients.In[18],Nielson
etal.
proposeanexponen-
tialanalysisforcountingoccurrencesofagentsinsideambients.In[26],they
usecontext-dependentcountsforinferringamoreaccuratedescriptionofthe
internalstructureofagents,attheexpenseofahighertimecomplexity(an
exponentialnumberofagentsaredistinguished).Theseanalysesrelyonthe
useofanon-relationaldomaintoabstractthecontentofanambient.Then,
theyusedisjunctivecompletion,andabstractthesetofallthepotentialcon-
tentsofasyntacticambientasthepowersetofthisabstractdomain.These
twoanalysesencounterthesameproblem:inthecasethatseveralinstances
ofthesameagentmaycoexist,whenoneinstanceofthisagentperformsa
computationstep,theseanalysescannotdecid