Abstract Interpretation of Mobile Systems

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