Additionallysourceforge.jp

ModelingandEnhancingAndroid'sPermissionSystemElliFragkaki,LujoBauer,LiminJia,andDavidSwaseyCarnegieMellonUniversity,Pittsburgh,PA,USAAbstract.
SeveralworkshaverecentlyshownthatAndroid'ssecurityarchitecturecannotpreventmanyundesiredbehaviorsthatcompromisetheintegrityofapplicationsandtheprivacyoftheirdata.
ThispapermakestwomaincontributionstothebodyofresearchonAndroidse-curity:rst,itdevelopsaformalframeworkforanalyzingAndroid-stylesecuritymechanisms;and,second,itdescribesthedesignandimple-mentationofSorbet,anenforcementsystemthatenablesdeveloperstousepermissionstospecifysecrecyandintegritypolicies.
Ourformalframeworkiscomposedofanabstractmodelwithseveralspecicinstan-tiations.
Themodelenablesustoformallydenesomedesiredsecurityproperties,whichwecanproveholdonSorbetbutnotonAndroid.
WeimplementSorbetontopofAndroid2.
3.
7,testitonaNexusSphone,anddemonstrateitsusefulnessthroughacasestudy.
1IntroductionRecentyearshavewitnessedanexplosionintheuseofmobilecomputingthankstotheproliferationoffeature-richsmartphones,andassociatedappstoresandeasy-to-installapplications.
Smartphoneshavepowerfulhardware,withmanyusefulsensors(e.
g.
,GPS,camera,microphone,accelerometer)exposedviarichAPIs,andenoughcomputingpowertoruncomplexapplications.
ApplicationstakeadvantageoftheserichAPIstoperformconvenientanduseful,butpoten-tiallyprivacy-sensitivetaskssuchasaccessingaddress-bookorlocationinfor-mation;accessingonlinebankingandmedicalaccounts;andcontrollinghomesecuritysystems.
Appstoresmakeiteasyforuserstoinstallandrunapplica-tions,whileprovidingfewguaranteesabouttheirprovenanceorbehavior.
Toprotectsensitiveresourcesfromapplications,andapplicationsfromeachother,AndroidandothermobileOSesimplementsecuritymechanismssuchaspermissionsystemsandstrongisolationbetweenapplications.
Thesemecha-nisms,however,haveinpracticeprovedinsucient,withanincreasingnumberofmaliciousapplicationsstartingtotargetsmartphones[15,23,16].
Anumberofworkshaveinvestigatedtheseweaknessesfromvariousperspec-tives,includingdemonstratinghowapplicationscancommunicatethroughcovertchannels[24,18],developingtoolstodetectinformationleaks[8,5,14],andim-plementingmorepowerfulprotectionmechanisms(e.
g.
,[22,20,7,2]).
ThispaperaddstothebodyofresearchonAndroidsecurityintwomainways:rst,bydevelopingaformalframeworkforanalyzingAndroid-stylese-curitymechanisms,includingdeningpropertiesdesiredofthose,andverifyingS.
Foresti,M.
Yung,andF.
Martinelli(Eds.
):ESORICS2012,LNCS7459,pp.
1–18,2012.
cSpringer-VerlagBerlinHeidelberg20122E.
Fragkakietal.
whetherthesepropertieshold;and,second,bydesigningandimplementinganenforcementsystemthatprovidesapplicationdeveloperswithsimplelanguageconstructstospecifyexiblesecrecyandintegritypolicies,andprovablyexhibitsdesirablesecurityproperties.
Toremainpracticallyrelevant,weconstrainouren-forcementsystem,whichwecallSorbet,tobeeasilyretrottableintoAndroid'scurrentarchitecture.
ThedesignandimplementationofSorbetimprovesexist-ingAndroidpermissionsysteminthefollowingaspects:(1)weformallystatethepropertiesthatwewishournewmechanismstoachieve,andformallyprovethatoursystemdesignsupportsthem;(2)weenhanceAndroid'spermissionsystemtosupportcoarse-grainedsecrecyandintegritypolicies;and(3)weprovidemoreexiblesupportforne-grainedandscope-limiteddelegationofpermissions.
Formalanalysis.
OneofourmaingoalsistoimproveourunderstandingofthesecuritypropertiesthatwedesireofAndroid-likepermissionsystems,andtoverifythatspecicsystemsarecapableofspecifyingandenforcingdesiredproperties.
Wepursuethisgoalbybuildingageneralized,abstractmodeloftheAndroidpermissionsystem,andstatingasetofdesirablepropertiesintermsofthemodel.
WethendevelopinstantiationsofthismodelbothforthecurrentAndroidpermissionsystemandforSorbet.
Basedonthisformalaccount,westudythepropertiesofthecurrentsystem;ourinvestigationrevealsbothdesignandimplementationaws,whichguidethedesignofSorbet.
WealsoprovethatSorbet'sdesignissucienttosupportthepropertiesthatwehavedened.
Coarse-grainedsecrecyandintegritypolicies.
Sorbet'skeyinnovationiscoarse-grainedmechanismsthatallowdeveloperstoprotecttheirapplicationsagainstprivilegeescalationandundesiredinformationows(e.
g.
,[6,8]).
Android'sper-missionsystemonlypreventsapplicationsthatdonothavethecorrectpermis-sionsfromdirectlycallingaprotectedcomponent.
Thisisinadequatetoprotectagainstamaliciousapplicationthatreachesaprotectedcomponentindirectly,viaachainofcallstoinnocentapplications.
Toprotectagainstsuchattacks,weenrichAndroid'spermissionsystemwiththeabilitytospecifyinformation-owconstraintsandexplicitdeclassicationpermissions,andimplementalight-weightcalling-contexttrackingandcheckingmechanism.
Akeychallengehereistosupportlocalspecicationofglobalproperties.
Flexibleandne-graineddelegation.
Run-timedelegationofURIpermissionsisakeyfeatureinAndroid,andallowsapplicationstousethird-partycomponents(e.
g.
,avieweractivity)tomanipulatecontentthatthosecomponentsnormallywouldnotbepermittedtoaccess.
Onexamination,wediscoveredthatAndroid'simplementationofpermissiondelegationisplaguedbyanumberofawsandquestionabledesigndecisions.
Sorbetsupportsmoreexibleandprincipledper-missiondelegationandrevocation,andallowsdeveloperstospecifyconstraintsthatlimitthelifespanandredelegationscopeofthedelegatedpermissions.
De-velopingamechanismthatcorrectlyenforceslifetimeandscopeconstraintsturnsouttobeunexpectedlytricky,duetoredelegationandthedynamicnatureofAndroidapplicationsandcomponents,includingapplicationinstallationanduninstallation,andinstantiationandterminationofcomponents.
ModelingandEnhancingAndroid'sPermissionSystem3ContributionsandRoadmap.
Thispapermakesthefollowingcontributions:–WedevelopaformalmodelthatgeneralizesAndroid-stylepermissions(§2.
2).
WeshowhowAndroid'scurrentpermissionsystemcanberepresentedasaninstantiationofourabstractmodel(§2.
3).
–Buildingonthismodel,wedeneasetofsecuritypropertiesthatonemaydesireofAndroid-stylepermissionsystems(§3.
1).
WeshowthatAndroidcurrentlyobeyssomeofthedesiredsecurityproperties,butnotothers,andexposeseveraldesigninconsistenciesandimplementationaws(§3.
2).
–WedescribeSorbet,asetofimprovementstoAndroid'spermissionsys-temthatsupportsdeveloper-speciedcoarse-grainedinformation-owandprivilege-escalationpolicies.
WeformalizeSorbetasaninstantiationofourmodelandshowthatitbettersupportsthedesiredsecurityproperties(§4).
–Finally,weimplementSorbetontopofAndroid2.
3.
7,testitonaNexusSphone,anddemonstrateseveralnewscenariosthatitenables(§5).
2PreliminariesWerstreviewtheAndroidarchitectureasitpertainstopermissions(§2.
1).
WethendevelopanabstractmodelofAndroid-stylepermissionsystems(§2.
2),andaninstantiationofitthatcapturesdetailsofAndroid'simplementation(§2.
3).
2.
1AndroidOverviewAndroidisaLinux-basedopen-sourceOSdesignedforsmartphones.
Androidap-plicationsarewritteninJavaandcompiledtoDalvikbytecode.
EachapplicationisexecutedinaseparateDalvikVirtualMachine(DVM)instance.
Androidapplicationsarecomposedoffourtypesofcomponents:Activitiesdenetheuserinterface.
Onlyoneactivityinteractswiththeuseratatime.
Userstypicallyinteractwithasequenceofactivitiestoperformatask.
Servicesruninthebackgroundandhavenouserinterface.
Unlikeactivities,servicesremainactiveregardlessofwhichapplicationisintheforeground.
Broadcastreceiverslistenforsystem-widebroadcasts,andinformotherapplica-tioncomponentsuponthereceiptofabroadcast.
Contentprovidersstoredataandarethemainwaytosharedatabetweenappli-cations.
EachproviderexposesapublicURIthatuniquelyidentiesitsdataset.
ComponentsandapplicationscanaccessorupdatethedataviaSQLqueries.
Activities,services,andbroadcastreceiverscommunicateviaintents,asyn-chronousmessagesthatdeliverdataand,ifneeded,causeanewinstanceoftherecipientcomponenttobecreated.
TheOSmediatesbothcross-andintra-applicationcommunicationsviaintents.
Therecipientofanintentcanbespec-iedexplicitlybyitspackageandclassname,orimplicitlyviatheactiontheintentattemptstoinitiate.
Wewilloftenwritethatacomponentcallsanothercomponentinlieuofexplainingthatthecommunicationisviaanintent.
4E.
Fragkakietal.
StaticConstructsComponentsC::=Ccode|CdataCodeComponentsCcode::=(name,A,ckCallee,ckCaller,Pdecl,Preq,Pgrnt)DataComponentsCdata::=(name,ckCaller,Pdecl)ComponentGroupsC::=(name,ckCallee,ckCaller,Pdecl,Preq,Pgrnt,{C1,Cn})Run-timeConstructsRun-timeInstancesIns::=iC|iCCompInstancesiC::=(namer,C,Pgrnt)CompGroupInstancesiC::=(namer,C,Pgrnt,{iC1,iCn})PrincipalsPrin::=Ins|userTargetsTgt::=Ins|C|CEventsE::=x=E1;E2|calliC1iC2I|returniC1iC2I|resolveiC|grantPrinTgtPF|revokePrin({Tgt1,Tgtn})P|checkguardiCTgt|exitIns|installPrinC|uninstallPrinCFig.
1.
SyntaxofpermissionmodelAndroiduses(application)permissionstoprotectcomponentsandsensitiveAPIs.
Permissionsarestrings(e.
g.
,android.
permission.
INTERNET)denedbythesystemordeclaredbyapplications.
AcomponentorAPIprotectedbyapermis-sioncanbeaccessedonlybyapplicationsthatholdthispermission.
Applicationsacquire(application)permissionsonlyatinstalltime,withtheuser'sconsent.
Additionally,contentproviderscanuseURIpermissionstograntad-hocac-cesstospecicpiecesofdatathattheycontrol(records,tables,ordatabases).
URIpermissionscanbedynamicallygrantedandrevoked.
2.
2AbstractModelTobeabletoformallystatethepropertiesdesiredofapermissionsarchitecture,wedevelopanabstract,formalmodelofAndroid-stylepermissionssystems.
Themodelcomprises:(1)staticelements,whicharethecodeanddatawewanttoprotect;(2)run-timeelements,suchassystemeventsandcomponentinstances;and(3)atransitionsystemthatcapturesthebehavioroftheprotectionmecha-nisms.
ThemodelismoregeneralthanAndroid'simplementationasitspurposeistoencompassawiderdesignspaceofpermissionsystems,includingpreviouslysuggestedextensions(e.
g.
,[22]).
Weonlysketchthemodelhere;seeourtechnicalreport[13]fordetails.
Fig.
1showsthemodel'sstaticandrun-timeelements.
StaticConstructs.
FollowingAndroid,applicationsinourmodelarebuiltfromcomponents.
Wedistinguishbetweencodecomponents(Ccode)anddatacompo-nents(Cdata).
Codecomponents—activities,services,andbroadcastreceivers—mayactbothascallersandascallees;datacomponents—contentproviders—arepassiveandonlyreceivecalls.
Acodecomponentiscomprisedofaname(name),theactionsAtowhichthecomponentiswillingtorespond,permissions(Pdecl,Preq,andPgrnt),andguards(ckCallee,ckCaller).
InAndroid,callstoacomponentareguardedbyapermissioncheck.
Wegen-eralizethischecktoanabstractguardmodeledbyabooleanfunctionckCaller.
Fornow,wespecifyonlythatckCallertakesasargumentsacomponentandModelingandEnhancingAndroid'sPermissionSystem5thecallingcontextandreturnstrueorfalse.
Asecondgeneralguard,ckCallee,specieswhenoutgoingcallsshouldbeallowed.
Wedistinguishbetweenpermissionsthataredeclared(Pdecl),requestedfromtheuser(Preq),andgranted(Pgrnt).
Thisallowsustomodelbehaviorssuchasdynamicdelegationofpermissions.
Wemodelapplications,C,asasetofcomponents({C1,Cn})withguardsandpermissionsthatapplytoall.
ThisisconsistentwithAndroid,whereper-missionsaretypicallydeclared,requested,andgrantedattheapplicationlevel,butindividualcomponentscanprotectthemselveswithadditionalpermissions.
Run-TimeConstructs.
Itisimportanttodistinguishstaticcomponentsfromrun-timeinstances,andrun-timeinstancesfromeachother.
AstaticcomponentCmayhavemultiplerun-timeinstancesiC,composedofauniqueidentier(e.
g.
,pointer),namer,andthepermissionsPgrntgrantedtothisinstance.
Wesimilarlymodelrun-timecomponentgroupsiC(e.
g.
,arunningapplication).
PrincipalsPrinareentitiesthatcangrantandrevokepermissions:run-timecomponentsandcomponentgroups,andtheuser(i.
e.
,humanwhoinstallsap-plications).
TargetsTgtaretheobjectsofsuchoperations,andcanbeeitherrun-timeorstaticcomponentsorcomponentgroups.
Abstractingdetail,wefocusonsystemeventsthatconcernpermissions,suchascomponentcommunicationviaintents(calliC1iC2I),andgranting(grant)andrevokingpermissions(revoke).
Wediscussthesefurtherin§2.
3and§4.
1whenwefocusontheAndroidandSorbetinstantiationoftheabstractmodel.
TransitionSystem.
Wecapturethedynamicsofthemodelasatransitionsystem.
WemodelasystemstateΣasatuplecomposedofasetofentities(run-timeandstatic)andauxiliarydatastructuresAux.
WewriteEtodenoteasequenceofeventstobeprocessedbythesystem.
WeassumethateacheventisassociatedwithauniqueeventIDn.
Theevolutionofthesystemisaseriesoftransitions(Σ;Eo→Σ;E),whereorecordswhethertheevaluationofeventnissuccessful(o=ok(n))orfails(o=fail(n)).
Evaluationofacalleventwillfail,forexample,iftheappropriateguardsdon'tevaluatetotrue.
Atrace,denotedbyT,isasequenceoftransitions:Σ0;E0o1→Σ1;E1···ok→Σk;Ek.
Thespecicrulesinthetransitionsystemdependontheconcreteimplemen-tationsbeingmodeled.
Hereweshowtheruleschemaforasuccessfulcallevent.
Thecallsucceedsonlyifbothguardsevaluatetotrue.
call-t(Σ;E,n::calliC1iC2I)ok(n)→(Σ;E)whereΣ=updateCall(Σ,calliC1iC2I)ifiC2.
ckCaller(Σ,iC1)=trueandiC1.
ckCallee(Σ,iC2)=trueAparallelrule,call-f,speciesthatacallfailsifeitherguardreturnsfalse.
2.
3AndroidModelWeinstantiateourabstractmodeltodescribethekeybehaviorsofAndroid'spermissionsystem1.
Thishashelpedustoidentifyawsinitsimplementation1WhenwerefertoAndroid,wemeanversion2.
3.
7,whichwasthenewestversionavailablewhilewewerecarryingoutourinvestigation.
Thebehaviorswedescribegenerallyholdin4.
0aswell.
6E.
Fragkakietal.
andpeculiaritiesinitsdesign.
Weomitafulldescription,butshowexampleinstantiationsofguards(uriP)andtransitionrulesforgrantingpermissions.
Guards.
TheguarduriPcheckswhetheracomponenthastheURIpermissionsspeciedinP.
uriPcanbeusedasckCallerwhenPisthesetofURIpermissionsprotectingacomponent.
Werstdenefunctionstolookupthepermissionsassociatedwitharun-timecomponentfromthecurrentstate.
FunctiongrantedByUsrPerm(iC,Σ)returnspermissionsgrantedatinstalltime,andfunctionURIPerm(iC,Σ)returnstheURIpermissionsdynamicallygrantedtoiC;URIPerminturnreliesonadatastructureMtotracktheURIpermissionsgrantedtoeachapplication.
Then,wedeneuriPasfollows.
uriPf(iC,Σ)=PgrantedByUsrPerm(iC,Σ)∪URIPerm(iC,Σ)GrantingPermissions.
URIpermissionscanbegrantedtemporarily,viaanintent,orpermanently,viagrantUriPermission.
Wemodeltheformeras:grantiC1iC2PFtmp;calliC1iC2I.
Here,iC1grantspermissionPwithagFtmptoiC2beforetransferringcontroltoiC2.
GrantingpermanentlywemodelasgrantiC1CPFprm.
FlagsFtmpandFprmconstrainthelifetimeofthedelegationofPandthescopeofitspotentialredelegationbyiC2.
MirroringAndroid,thelifetimeofpermissionsgrantedwithFtmpisconnedtothelifetimeoftherecipient(iC2)ofthegrantoperation.
WhengrantingwithFprm,therecipientwillhavethepermissionuntilthesystemrebootsorthepermissionisrevoked.
Neitheragrestrictsthescopeofredelegation.
ThefollowingruleshowshowgrantcurrentlyworksinAndroid.
(Σ;E,n::grantiC1iC2PFtmp)ok(n)→(Σ;E)ifuri{P}(iC1,Σ)=truewhereΣ=updateGrant(Σ,iC1,iC2,P,Ftmp)GrantingsucceedsonlyifthegranterhaspermissionP.
Afterwards,updateGrantupdatesstate,byrecordinginMthattheenclosingapplicationofiC2nowhaspermissionPwithagFtmp,andthattheinstanceiC2hasPinPgrnt.
TheruleforgrantingwithFprm(omittedhere)diersonlyinitsupdatefunction:MrecordsthatnowChaspermissionPwiththeagFprm.
TheserulesmakeexplicitthatAndroiddoesnotdistinguishbetweenFtmpandFprmwhendecidingwhetheracomponentcangrantpermissions.
Thiscausesproblemswhencomponentsredelegatepermissions,aswediscussin§3.
2.
3SecurityPropertiesWedeneseveralpropertiesthatonemightdesireofanAndroid-stylesecurityarchitecture(§3.
1)andinvestigatewhethertheycurrentlyhold(§3.
2).
3.
1SpecifyingDesiredSecurityPropertiesWeformulatethepropertiesdesiredofAndroid'ssecurityarchitecturebasedontheresourcesthatneedprotection.
ThesearetypicallyinterfacesthatallowModelingandEnhancingAndroid'sPermissionSystem7accesstofunctionalitythatcouldcauseharmorinconvenience(e.
g.
,sendingexpensivetextmessages)andtosensitivedatathatshouldnotleavetheposses-sionofcomponentsthatlegitimatelyrequireit(e.
g.
,nancialinformationinabankingapplication;locationinformation).
Weabstractlydeneaccess-controlpropertiesthatspecifywhenandhowaprotectedinterfacecanbecalledandinformation-owpropertiesthatspecifywhenandwhatinformationcanowtoorfromacomponent.
Wealsoinvestigatelower-level,functional-correctnesspropertiesconcerninggrantingandrevokingpermissions,sincethesedirectlyaecttheaccess-controlandinformation-owproperties.
LocalProperties.
Thefollowingtwopropertiesstatethattheimmediaterestrictionsspeciedbyacomponentonitscallersorcalleesarealwaysobeyed.
Property1.
(Localcalleeprotection)IfacomponentAiscalledbyanothercomponentB,thenA'sguardckCalleeevaluatestotrue.
Property2.
(Localcallerprotection)IfacomponentAcallsanothercompo-nentB,thenA'sguardckCallerevaluatestotrue.
ItiseasytoshowthatProp.
1and2holdonanyinstantiationthatincludesruleslikecall-tandcall-f(see§2.
2).
DelegationandRevocationProperties.
Property3.
(Delegation)AcomponentAhasapermissionPifAownsP,orthereisadelegationchainfromacomponentBtoAsuchthatAsatisesthescopeandlifetimeconstraintsimposedbyeverycomponentonthechain,andthateverycomponentonthechainalsohasP.
Intuitively,Prop.
3ensuresthattheuseofaredelegatedpermissionisconnedbythelifetimeandscopeconstraintsspeciedbytheoriginalgranter.
Forinstance,ifanemailcomponentgivestoaviewercomponenttheURIpermissionPfordisplayinganattachment,twosensibleconstraintsarethatPisconnedtoaspecicinstanceoftheviewer,andthattheviewercannotredelegateP.
Property4.
(Revocation)IfArevokesPfromB,thenthereisadelegationchainfromAtoB,orAownsP.
Thisisabasiccorrectnesspropertyforrevocation.
Allowingarbitrarycompo-nentstorevokepermissionsislikelytobedisruptive;hence,onlytheownerorgrantershouldbeallowedtorevokeapermission.
GlobalProperties.
Thenexttwopropertiesaresimpliednoninterference.
Wecustomizethegeneralnotionthatsecretinputscannotaectpublicoutputsandtaintedinputscannotaectendorsedoutputstotthepermission-basedAndroidmodel.
Property5.
(Privilegeescalation)GivenanycomponentBprotectedbyper-missionP,andanycomponentAthatdoesnothavethatpermission,ifSABisasystemthatcontainsAandB(andothercomponents),andSBisthesamesystemwithoutA,thenacallchainendingwithBexistsinSABifandonlyifitexistsinSB.
AdditionalcallchainsendingwithBmayexistinSABifexplicitlyallowedbypolicy.
8E.
Fragkakietal.
Inotherwords,withrespecttoaccessingB,asystemwithunprivilegedcompo-nentAshouldbehavethesameasasystemwithoutA.
TheonlyexceptionisifadditionalpolicyexplicitlyallowsAtoaectB.
Withoutsuchexceptions,thispropertywouldlikelybetoorestrictive.
Forexample,letBbetheinterface,guardedbypermissionP,forrebootingthephone.
SupposethatcomponentChasP(whichallowsittocallB),andapublicinterface,suchthatanycallstothatinterfacewillcauseCtocallB.
Then,acomponentAthatdoesnothavePcanindirectlycauseBtobeinvokedbycallingC.
C'sindiscriminateinvocationofBisanexampleoftheconfused-deputyproblem.
SinceatraceculminatinginthatinvocationofBcannotexistinasystemwithoutA,Prop.
5prohibitsthisbehavior.
Intheotherdirection,wemaywanttopreventsensitiveinformationfrombeingleaked,whichpermissionsystemstypicallycannotspecifydirectly.
Weleveragepermissionstostateanundesiredinformationowasfollows.
SupposethatpermissionP1guardsthesourceofsomeinformationandpermissionP2guardsthesink.
Then,anundesiredinformationowcanbespeciedasacallchainfromacomponentthatusesP1toacomponentthatusesP2.
Asystemthathasnoundesiredinformationowsshouldthenobeythefollowingproperty.
Property6.
(Informationow)GivenanundesiredinformationowfromacomponentAguardedbyP1toacomponentBguardedbyP2,acallchainthatendswithBexistsinasystemwithAifandonlyifthesamecallchainexistsinasystemwithoutA.
AdditionalcallchainsendingwithBmayexistinthesystemwithAonlyifexplicitlyallowedbypolicy.
Withoutamoreexpressivepolicyspecicationlanguage,thesepropertiescan-notbespeciedprecisely.
3.
2AnalyzingAndroidPermissionsWeinvestigatedtheextenttowhichAndroid'scurrentpermissionsystem,asrepresentedbyourmodel,supportsthepropertiesdenedin§3.
1.
LocalPropertiesHold.
Android'spermissionsystemimplementsthecall-tandcall-frules,andtheguardsspeciedbythecomponentsarecheckedatruntime;hence,Prop.
1and2hold.
However,Prop.
2holdstrivially,becausecallerscannotstateusefulguardsoncallees.
DelegationandRevocationPropertiesDoNotHold.
Prop.
3requiresthatapermissiondoesnotoutlivethelifespanspeciedbyitsgranter.
Android'simplementation,however,doesnotdistinguishbetweenFtmpandFprmwhendecidingwhetheracomponentcangrantpermissions.
ThisviolatesProp.
3andcausesseveralbugs(seeourcompaniontechnicalreport[13]),e.
g.
,acomponentthatgainedtemporarypermissioncanredelegatethepermissionpermanently,includingtoitself.
Android'srevokeURIPermissionrevokesaURIpermissionfromallcomponentstowhichitwasdynamicallygranted,andcanbecalledbyanycomponentthatwasgrantedthepermissionatinstalltime.
ThisviolatesProp.
4,whichrequiresModelingandEnhancingAndroid'sPermissionSystem9thatacomponentAcanrevokeonlyfromentitiestowhichitgrantedpermission(unlessAownsthepermission).
Suchviolationscaneasilycauseconfusion,asunrelatedapplicationscanrevokeeachother'spermissions.
GlobalPropertiesDoNotHold.
PreviousworkhaspointedoutthatAndroidsuersfromprivilege-escalationaws(e.
g.
,[6]);i.
e.
,Prop.
5doesnothold.
Prop.
6alsodoesnothold,asAndroiddoesnothaveamechanismforpreventing,orevenspecifying,undesiredinformationows.
Anapplicationcanaccessanycomponentforwhichithasthepermissiontodoso,regardlessofwhetherithadpreviouslyaccessedprotectedinformation.
Previousworkhasshownthatthisresultsinvariousspecicundesiredinformationows[24,18,8].
ExaminingAndroidinlightofthesepropertiesalsorevealedseveraldesignandimplementationbugs,whichwereportedtoGoogle.
Theseincludetheabilityofcomponentsthatreceivedatemporarypermissiontoredelegatethatpermissionpermanently,andimproperbookkeepingofgrantedpermissionsduringapplica-tionuninstallationandinstallationthatcanleadtoprivilegeescalation.
Theseawsarediscussedinmoredetailinourcompaniontechnicalreport[13].
4Sorbet:AndroidPermissions++Motivatedbythepropertiesof§3.
1,wedevelopSorbet,animprovedpermis-sionsystemthatsupports(1)developer-denedpoliciestomitigateundesiredinformationowsandprivilege-escalationattacks;and(2)well-behavedpermis-siondelegationandrevocation.
OurgoalsweretoenabledevelopersanduserstospecifyricherpoliciesontheirapplicationswithoutdramaticallyalteringAn-droid,andtoconstructanenforcementsystemthatisprovablywellbehaved.
Someofthemechanismsweusehavebeendiscussedpreviously[10,22,14,7];weintegratetheseandotherideasintoasystemthatwecanformallyshowsatisesinterestingsecuritypropertiesandenablesnewusecases.
4.
1NewFeaturesinSorbetCoarse-GrainedInformation-FlowProtection.
SorbetextendsAn-droid'spermissionlabelstomakethemsuitableforspecifyingcoarse-grainedinformation-owpolicies,andenforcessuchpoliciesatcomponentandapplica-tionboundaries.
Byreusingpermissionlabels,thisapproachrequireslittlenewsyntax.
InSorbet,acomponentAguardedbyP1(e.
g.
,thecontactspermission)canspecify(intheapplicationmanifest)information-owpoliciesoftheformdisallow-ow(P1,P2).
ThisindicatesthatanycomponentBthatmadeuseofP1toaccessAcannot(includingtransitively)usepermissionP2.
Acompo-nentcanalsorequestatinstalltimethepermissionallow-declassify(P1,P2)todeclassifysensitiveinformation,i.
e.
,toescapetherestrictionimposedbydisallow-ow(P1,P2).
Weformalizethismechanismandthepropertyitenforcesin§4.
2and§4.
3.
10E.
Fragkakietal.
Ourmechanismcanbeusedbyprogrammerstostrengthentheirowncodebyseparatingtrustedinformationthatshouldremaininternaltoanapplica-tionfromuntrustedowsthatmaybecommunicatedtotheoutside,therebydecreasingthechanceoftheapplicationbeingmisusedbymaliciousones.
Themechanismcanalsobeusedtodefendagainstmaliciousapplicationsordevel-opers,byspecifyingpoliciesthatshouldholdbetweenapplications.
Coarse-GrainedPrivilege-EscalationProtection.
Tomitigatetheconfused-deputyproblem,Sorbettracksthepermissionsofallcomponentsonthecallstack.
WhenacomponentAiscalled,andAisprotectedbypermissionP,SorbetchecksifeverycomponentonthecallstackhasP.
However,thisistoorestrictiveforpracticaluse;e.
g.
,anemailapp,whichneedstousetheINTERNETpermissiontosendemail,coulddosoonlywhenstartedbyappli-cationsthathavetheINTERNETpermission.
Toaddressthis,SorbetallowscomponentstorequestaprivilegedpermissionP.
WhenacomponentBhasthepermissionP,itispermittedtocallAevenwhenothercomponentsonitscallstackdonothaveP.
PissimilartotheenableprivilegeoperationinJavastackinspection.
Otherworkshavealsotrackedthecallstackforsimilarpurposes(e.
g.
,[7]);Sorbet'snoveltyhereisinallowingdeveloperstospecifypolicies,andinenablingproofsthatthisandotherdesignfeaturesallowthesystemtoexhibitdesiredproperties.
FlagRecipientRedelegationscopeLifetimeFcompactivitynoredelegationactivityexitFtaskactivityactivitiesinthesametaskactivityexitFappTmpactivityactivitiesinthesameappactivityexitFallTmpactivityanycomponentactivityexitFappappnoredelegationappuninstallFallappunrestrictedappuninstallFig.
2.
Flagsforconstrainingdelegation.
Columnsshowtherecip-ientscope,thescopingconstraintsofredelegation,andthelifetimeofthegrantedpermission.
Aswithinformationow,Sorbetprotectsagainstprivilegeescala-tionatbothcomponentlevelandapplicationlevel.
ToaccountforAndroid'sinabilitytocompletelymediatecom-munication(e.
g.
,viapublicstaticelds)be-tweencomponentswithinanapplication,thepolicyenforcedattheapplicationlevelassumesthatcompo-nentboundarieswithinanapplicationarenotrespected.
PrincipledRedelegationandRevocation.
SorbetalsoaddressesAn-droid'sproblemswithindiscriminateredelegation.
Thechallengehereistodesigna(correct)mechanismtoallowprogrammerstopredictablycontroldelegationlifetimeandredelegationscope.
BuildingonAndroid'snotionoftemporaryandpersistentpermissions,weenablethegrantoperationtopreciselyconveytheintendedscopeoftherecipient(acomponentoranapplication),thescopeofredelegation(none,componentsinthesametask,componentsinthesameappli-cation,andunrestricted),andthelifetimeofthepermission(untiltherecipientactivityexits,orisuninstalled).
Forsimplicity,weconvergeonsixcombinationsoftheseconstraints(summarizedinFig.
2),whichtheprogrammercanspecifyviaagspassedasargumentstogrant.
Theenforcementmechanismenforcesthetransitivepropertiesthattheconstraintsimplicitlyrequire.
ModelingandEnhancingAndroid'sPermissionSystem11SorbetallowsacomponentAtorevokeapermissionPfromcomponentBonlyifAgrantedPtoB(orAownsP).
Inotherwords,theactofdelegatingcreatesanewlinkinadelegationchain,andrevocationremovesthatlink.
4.
2ImplementationofImprovementsinAbstractModelWenowbrieydescribeSorbetasaninstantiationoftheabstractmodel.
Wefocusonmechanismsforenforcinginformationow,andbrieydiscussprivilegeescalation.
Delegationandrevocationarediscussedinourtechnicalreport[13].
Information-FlowProtection.
Toenforceinformation-owpoliciesspeciedbydisallow-ow(P1,P2)andallow-declassify(P1,P2),weaugmentthemodelwithanauxiliarydatastructureN,whichkeepstrackofinformation-owconstraints.
Moreconcretely,NmapsacomponentinstanceiCtothesetofinformation-owconstraintsthatincludesallsuchpoliciesspeciedbycomponentsinthecallchainbeforeandincludingiC.
WedeneforbidP(N,iC)toreturnthesetofpermissionsthatarefor-biddenfrombeingusedbyconstraintsinN(iC).
Forinstance,ifN(iC)={disallow-ow(P1,P2)},thenforbidPreturns{P2}.
FunctionguardP(Σ,iC)re-turnsthesetofpermissionsthatguardsthecallstocomponentiC.
Asuccessfulcallbetweencomponentsinthesamegroupcannowbedenedasfollows.
call-t(Σ;E,n::calliC1iC2I)ok(n)→(updateCall(Σ,calliC1iC2I);E)ifiC2.
ckCaller(Σ,iC1)=trueandiC1.
ckCallee(Σ,iC2)=trueandguardP(Σ,iC2)∩forbidP(N,iC1)=Thelastlineistheaddedcheckforinformation-owpolicies.
Thecallsucceedsonlyifthepermissionrequiredtoaccessthecalleeisnotforbiddenbythepolicy.
Ifthecallsucceeds,informationwillowfromthecallertothecallee,andcon-straintsneedtobesimilarlypropagated.
Inaddition,thecalleehasitsowncon-straintsthatneedtobeincorporatedinN.
Forthis,wedenetwonewfunctions.
updFlow(N,iC,Fl)returnsanewmappingN,whereN(iC)=N(iC)∪Fl.
updDeclassify(N,iC,allow-declassify(P1,P2))returnsanewmappingN,whichremovesdisallow-ow(P1,P2)fromNforiC.
Hence,afteradeclassicationper-missionallow-declassify(P1,P2)isencountered,theconstraintthatforbadeaccesstocomponentsguardedbyP2islifted.
E.
g.
,iftheuserexplicitlyallowsaccesstotheInternetafterprivatedataisread,thenthiswillbeallowed.
WedenefunctionowP(Σ,iC)toreturnthesetofinformation-owcon-straintsthatguardthecallstoiC,andgetDeclassify(iC)toreturnthesetofdeclassicationpermissionsofiC.
ThefunctionupdateCallrstcomputesN=updFlow(N,iC2,owP(Σ,iC1)),thenN=updFlow(N,iC2,N(iC1)),andnallyN=updDeclassify(N,iC2,getDeclassify(iC2)).
Androiddoesnotmediateallcommunicationsbetweencomponentswithinthesameapplication(e.
g.
,viasharedstaticelds).
Sorbetconservativelyas-sumesthatcomponentswithinanapplicationhavecommunicated,andtreatscross-applicationcallsdierently.
WewriteNA(iC)tobetheunionofsetsofinformation-owconstraintsN(iC),foreachiCthatisinthesameap-plicationasiC.
WedeneforbidPA(N,iC)=NA(iC).
Wedenefunction12E.
Fragkakietal.
guardPA(Σ,iC)toreturnthesetofpermissionsthatguardsthecallstoallcomponentsinthesameapplicationascomponentiC.
Intheruleforcross-applicationcalls,NAtakestheplaceofN,andguardPAtakestheplaceofguardP.
Thismeansthatifanycomponentinanapplicationhasaccessedprivatedataprotectedbydisallow-ow(P1,P2),thennocomponentinthatapplicationcanusepermissionP2.
Theupdatefunctionsimilarlyaccumulatesallconstraintsintheentireapplication,ratherthanjustonecomponent.
Returnsaretreatedsimilarlytocalls,withthecallerandcalleedesignationsswitched.
Weomitthedenitionshereforspacereasons.
Privilege-EscalationProtection.
Topreventprivilegeescalation,weuseauxiliarytree-likedatastructurestokeeptrackofthefullcallhistory.
WedeneacallforestTSasalistofcalltreesT,asfollows:CallForestTS::=[T1,Tn]CallTreeT::=(TS,(iC,P))WeuseMTStodenoteamappingfromrun-timecomponentstocallforests.
Eachcalltreerepresentsacallchain,andtherootofthetreeisthelastcom-ponentonthecallchain.
Thechildoftherootisacallforest,whichisalistofcallchains,eachrepresentingapastcallchaintotherootcomponent.
Ifcom-ponentA(whichhaspermissionsPA)callsB(withpermissionsPB),andC(withpermissionsPC)alsocallsB,andBhasonlyonerun-timeinstance,thenMTS(B)A,PA)C,PC))].
Inotherwords,eachcalltreeinthecallforestMTS(B)recordsthefullcontextofthecallstack.
IfBnowcallsD,thecalltreeA,PA)C,PC))],(B,PB))willbestoredinMTS(D).
AcallfromcomponentAtocomponentBisallowedonlywhenforanypermissionPthatguardstheaccesstoB,eitherAhasP;orAhasPandforeverycallchainrecordedinMTS(A),either(1)allthecomponentshavepermissionP;or(2)thereexistsacomponentCthathaspermissionP,andallthecomponentsinthecallstackafterChaveP.
Aswithinformationow,theruleforcross-applicationcallsassumesthatallcomponentswithinanapplicationhavecommunicatedwitheachother.
4.
3PropertiesWeproveSorbetobeysProp.
1–6.
Hereweshowonlythemoreconcretere-statementsofProp.
5and6madepossiblebySorbet'snewpolicystatements(disallow-ow,allow-declassify,andP).
Forbrevity,detailsandproofsketchesarerelegatedtoourcompaniontechnicalreport[13].
Werstdeneanindirectcallchain.
Definition1.
(Indirectcallchain)GivencomponentsAandB,thereexistsanindirectcallchainfromAtoBifthereexist1.
componentsD1,Dk;and2.
callchainsfromAtoD1,fromD1toD2,andfromDktoB.
WesaythatacomponentAcaninuenceanothercomponentBifthereisanindirectcallchainfromAtoB.
Forexample,AcanaectthebehaviorofModelingandEnhancingAndroid'sPermissionSystem13B(i.
e.
,theintentsthatBsends)ifeither(1)AispartofacallchaintoB,or(2)AappearsinacallchaintosomecomponentD,andthischainsharesacomponentwithadierentcallchaintoB.
ThesharedcomponentcarriesA'sinuencetoB.
Property5*.
(Privilegeescalation(2))GivenacomponentBprotectedbypermissionP,andacomponentAthatdoesnothavePandbelongstoadif-ferentapplicationthanB,ifSABisasystemthatcontainsAandB(andothercomponents),andSBisthesamesystemwithoutA,thena(possiblyindirect)callchainthatendsinBexistsinSABifandonlyifitexistsinSB.
Additional(possiblyindirect)callchainsmayexistinSABonlyifeachsuchchainhasacommonsuxwitha(possiblyindirect)callchainfromAtoB,andthereexistsacomponentbetweenAandBthathaspermissionP;orthereisacomponentBbetweenAandB,thepathbetweenBandBcontainscomponentsofthesameapplication,andBisnotprotectedbypermissionPbutcommunicatedtoBviaunmonitoredchannels.
Property6*.
(Informationow(2))SupposeacomponentAisguardedbypermissionP1andaninformation-owpolicydisallow-ow(P1,P2),andacom-ponentBisguardedbyP2,andAandBbelongtodierentapplications.
Then,a(possiblyindirect)callchainthatendswithB,inasystemwithA,existsifandonlyifthesamecallchainexistsinasystemwithoutA.
Additional(possiblyindirect)callchainsmayexistinthesystemwithAonlyifeachsuchchainhasacommonsuxwitha(possiblyindirect)callchainfromAtoB,andthereexistsacomponentbetweenAandBthathaspermissionallow-declassify(P1,P2).
5ImplementingandEvaluatingSorbetWeimplementedSorbetontopofAndroid2.
3.
7.
Thissectiondescribesthemostsalientimplementationdetails,includingthesyntacticadditionsforex-pressingSorbet'spolicies,andacasestudythatillustratesSorbet'sfeatures.
SyntacticAdditions.
WeextendedAndroid'smanifestlesyntaxtosupportinformation-owandintegritypolicies.
ThecomponentprotectedbyP1canspecifydisallow-ow(P1,P2)byaddingandroid:forbiddenPermissions=["P2"]tothepermissionsbywhichthiscomponentisprotected.
allow-declassify(P1,P2)isspeciedas.
Aper-missionislabeledasprivilegedPbytheadditionofa"privileged"attributetoitsdeclaration:.
ImplementationOverview.
Sorbet'skeystoneisareferencemonitorbuiltontopofAndroid'sActivityManager(Fig.
3).
ActivityManageralreadymedi-atesinter-componentcommunication,whichincludespreventingcallsthatareillegalbyAndroid'spolicy;SorbetmodiesitsothatmediationofrelevantcallsishandledbySorbetinsteadofbythelegacypartsofActivityManager.
EnforcingSorbet'spoliciesalsorequiresadditionalbookkeeping,includingofinstancedata(e.
g.
,torecognizethataparticularapplicationhasaccessedare-sourceprotectedbya"forbidden"permission),andricherstaticpolicyspecied14E.
Fragkakietal.
inapplicationmanifests.
Hence,asignicantcomponentofSorbet'simplemen-tationisthedatastructuresthatimplementthisbookkeeping.
Thebookkeepingincludeskeepingtrackofindividuallesaccessedbyapplications;forenforce-mentpurposes,thesearetreatedascomponents.
!
"!
"Fig.
3.
Sorbetarchitecture:additionstoAndroidareshaded;arrowsindicateinter-actionsbetweensystemcomponentsThemostchallengingpartinim-plementingSorbetwastoidentifynotjustwhichapplicationinvokedaprotectedresource(whichAndroidtypicallyalreadydoes)butwhichspe-ciccomponentinstancewasrespon-sibleforthecall;weaccomplishedthisbyenhancingAndroid'sIPCdatastructurestocarrymoreinformationaboutthecaller.
Anotherchallengewastocaptureoperationsnotme-diatedbyActivityManager,suchasopeningasocketorale.
Androidenforcespermission-basedpoliciesonsuchoperationsbyLinux-levelchecksbasedonthe(Linux)groupIDofthecallingapplication;applicationsareassignedgroupIDsatinstallationtimebythepackagemanager.
Tome-diateaccesstotheseoperations,weusedTOMOYOLinux[21],asetofLinuxkernelpatchesthatreplacesscat-tered,ad-hocaccess-controlcheckswithcentralizedones.
2WefurtherextendedTOMOYOLinuxsothataccessattemptsforwhichpolicywasenforcedatLinuxlevel(e.
g.
,toopenasocketorale)triggeracalltoSorbet'sreferencemonitor.
ThisalsoallowsSorbettomediatesecurity-relevantbehaviorsimplementedinnativecodethatmaybeincludedinAndroidapplications.
CaseStudy.
TotestSorbetandillustrateitsusefulness,weusedittoimple-mentseveralpolicies;somethatcanbeimplemented(sometimespartially)bypreviouslyproposedmechanisms(e.
g.
,[2,7]),andsomethatrequireSorbet'sfeatures.
Ourmaincasestudyinvolvesfourapplications:alemanagerforstor-ingandmanipulatingprivateles(e.
g.
,adiaryorlistofaccountnumbers);atexteditor;anencryptionapplication;andanemailapplication.
Thehigh-levelpolicywefocusonistopreventprivatelesfrombeingleakedontheInternet,buttoallowthemtobemanipulatedbyvariousapplicationsattheuser'sbe-hest(e.
g.
,byusingtheprivatelemanagertolaunchaneditor).
Privatelesarekeptinacontentproviderimplementedbythelemanager,andprotectedbyseparatepermissionsthatallowreadandwriteaccess.
Applicationscanaccessprivatelesonlywhendynamicallydelegatedtheappropriatepermissionsbythelemanager.
Wenextdescribeseveralspecicscenarios(summarizedinFig.
4)thatexaminevariantsofthispolicyandshowhowtheycouldbeimplemented.
2TOMOYOLinuxhassimilarlybeenusedbyotherresearchers[2].
ModelingandEnhancingAndroid'sPermissionSystem15ScenarioPrivateFileManagerEditorEncryptionAppEmailAppPEIF1PrivatelescannotbesentoverthenetworkaprotectedbyR/WpermsbprotectedbyR/WpermsuseInternetuseInternetuseInternet–cprotectedbyR/WpermsforbidInternetuseInternetuseInternetuseInternet–2PrivatelessentovernetworkonlyviaemailaprotectedbyR/WpermsuseInternetuseInternetuseInternet–bprotectedbyR/WpermsforbidInternetuseInternetuseInternetuseInternetdeclassifyR/W→Internet–3PrivatelessentovernetworkonlyviaemailandifencryptedprotectedbyR/WpermsforbidInternetuseInternetuseInternetdeclassifyR/W→InternetuseInternetFig.
4.
Threescenariosfromourcasestudy.
Columnsindicatethepermissionsassignedtoeachapplication,andwhetherenforcementisviaprotectionfromprivilegeescalation(PE),orinformationowprevention(IF).
Scenario1.
Westartfromabasecaseinwhichprivatelesmustnotbesentoverthenetwork(Fig.
4,Scenario1).
InAndroid,theonlywaytopreventoneoftheseapplicationsfromleakinglestothenetworkistoavoidgrantinganyoftheapplicationstheInternetpermission(Scenario1a).
InSorbet,thispolicycanbeenforcedbyeitherthemechanismthatpreventsprivilegeescalationortheonethatpreventsundesiredinformationows.
Intherstcase,allotherapplicationscanbegrantedtheInternetpermission,butwillnolongerbeabletouseitifthelemanager,whichdoesnothavethispermission,isonthecallstack(Scenario1b).
Inthesecondcase,thelemanagerdeclarestheInternetpermissionasforbidden,withthesameeect(Scenario1c).
Scenario2.
Wenowextendthedesiredpolicytoallowonlytheemailclienttosendaprivatele(anactivitythattheuserexplicitlyinitiates),whileotherap-plicationscanusetheInternetforotherpurposes.
ThiscannotbeimplementedinstockAndroid,butcanstillbedonewitheitherofSorbet'sprotectionmech-anisms.
Forenforcementviatheprivilege-escalationmechanism,theemailappmustdeclareandbegrantedtheprivilegedversionoftheInternetpermission.
ToenforcethesamepolicyviaSorbet'sinformation-owmechanism,thelemanagerwoulddeclaretheInternetpermissionasforbidden(asinScenario1),andtheemailwoulddeclarethepermissiontodeclassifyfromR/WtoInternet.
Scenario3.
Finally,weextendthepolicyfromScenario2toallowemailingpri-vatelesonlyiftheyareencrypted.
Enforcingthiswithoutlimitingreasonableusesoftheemailapprequiresboththeinformation-owandprivilege-escalationmechanisms.
AsinScenario2a,theemailappisgiventheprivilegedInternetpermission,sothatitcansendemailevenifindirectlyinvokedbytheleman-ager,whichdoesnothavetheInternetpermission.
Inaddition,thelemanagerdeclarestheInternetpermissionforbidden,andtheencryptionappisallowedtodeclassify.
Now,theonlypathtoemailingprivatelesisviatheencryptionapp,whichistrustedtoinvoketheemailapponlywithencrypteddata.
16E.
Fragkakietal.
ThelastscenarioshowsthatSorbetallowseasyspecicationofusefulpoli-ciessignicantlybeyondwhatAndroidoers.
Ourcasestudyusedminimallymodiedo-the-shelfapplications:OpenManagerv2.
1.
8,QuteTextEditorv0.
1,AndroidPrivacyGuardv1.
0.
9,Emailv2.
3.
4.
Wemodiedmanifestles,addedsendingfunctionalitytosome,andaddedacontentprovidertoOpenManager.
Sorbet'soverheadwassucientlysmalltobeunobservablebytheuser.
36RelatedWorkResearchershaveanalyzedthesecurityofAndroid'spermissionsystem[5,10],developedanalysistoolsforAndroidapplications[11],andproposednewpro-tectionmechanisms(e.
g.
,[20,22]).
ManyworksstudiedAndroid'sattacksurface(e.
g.
,[19]),includingcovertchannels[24],DoS[1]andwebattacks[17],andunauthorizedapplicationrepackaging[27].
SeveralworkshavepointedoutawsinAndroid'spermissionsystem.
Oneweaknessisthelackofglobalproperties:Android'spermissionsystemdoesnotpreventprivilegeescalationorinformationleakage.
Davietal.
[6]andFeltetal.
[12]havestudiedprivilege-escalationattacksindetail.
Bugieletal.
devel-opedasystemthatmonitorsinteractionsbetweenapplicationsatruntimeandmitigatesawiderangeofprivilege-escalationattacks[2].
Ourmechanismhasmanysimilarities,butwefocusonallowingdeveloperstospecifypoliciesonaper-applicationbasis,andemphasizeformalanalysisofmechanisms.
Dietzetal.
proposedaframework,Quire,forprovenancetrackingtomitigatetheconfuseddeputyproblem[7].
Ourgoalsoverlap,butSorbetdiersinseveralways:Wedonottrackfullprovenanceinformation,butinsteadfocusonexible,application-levelpolicyspecicationbasedonpermissions;werelyontheAndroidruntimeforbookkeeping,ratherthanusingdigitalsignatures.
Wealsosupportdeclas-sication,andformallyinvestigateSorbet'sproperties.
Anotherapproachtomitigatingapplicationcollusionisthroughdomainisolation.
Bugieletal.
as-signedtrustlevelstoapplications,allowingthemtocommunicateonlyiftheyareatthesamelevel[3].
Theyfocusondeningpolicyforasetofapplicationsatthesametrustlevel,whereasweletapplicationsdenepolicyindividually.
SeveralworkshaveinvestigatedprivacyleaksinAndroid[8,24,4,9].
Wepro-videaformalframeworkthatallowssuchawstobeseenasviolationsofdesiredsecurityproperties.
ProjectssuchasTaintDroid[8]andAppFence[14]aimtoautomaticallydetectandpreventdangerousinformationleaks.
Ourworkisinseveralwayscomplementary.
TaintDroidandAppFenceoperateatamuchnergranularity,trackingtaintingatthelevelofvariables,andenforcexedpolicies.
Incontrast,ourenforcementisatthecomponentlevel,andallowsdeveloperstospecifypolicies,including,e.
g.
,declassication,whichiskeytoenablingap-plicationsthathavelegitimatereasontosendtainteddatatooperate.
Wealsoformallyprovethatourdesignenforcesdesiredhigh-levelsecurityproperties.
3Weranmicrobenchmarks,but,ascommoninthissetting,thesmallchanges—andsometimesimprovements—inlatencyweredwarfedbythevariancesbetweenruns.
ModelingandEnhancingAndroid'sPermissionSystem17SystemssuchasSaint[22]andApex[20]alsoimproveAndroid'spermissionsystem,e.
g.
,byprotectingcallerswithguardsthatconsidercontextbeyondjustpermissions,whilestayinggenerallyclosetotheoriginaldesign.
Wefocusondeeperrevisionstothepermissionmodelandenforcingtransitiveproperties.
FormalanalysisofAndroid-relatedsecurityissueshasreceivedlessattention.
Shinetal.
[25]developedaformalmodelinordertoverifyfunctionalcorrectnesspropertiesofAndroid,whichrevealedaawinthenamingschemeforpermis-sionsandapossibleattack[26].
Incontrast,ourworkdevelopsamoreabstractmodelsuitableforreasoningaboutextensionstoAndroid'spermissionsystem.
7ConclusionThispaperdevelopsaframeworkforformallyanalyzingAndroid-stylepermis-sionsystems,andshowshowtoenhanceAndroid'spermissionsystemtosupportrichpolicieswhilemaintainingconvenient,application-centricpolicyspecica-tion.
Wehaveprovedthedesignofourenforcementsystemsatisesasetofsecu-rityproperties,showeditsfeasibilitybyimplementingandrunningitonaNexusSphone,anddemonstrateditsusefulnessthroughacasestudy.
Indoingso,wediscoverthatAndroid'sinabilitytoprovidestrongisolationbetweencomponentsconstrainstheexpressivenessofoursystemandcomplicatesitsimplementation.
Oursystemsuccessfullyprovidesbothapplication-andcomponent-levelprotec-tions,butitwouldneedtoresorttoapplication-levelprotectionlessoftenifAndroid'scomponent-levelabstractionsweremorerobust.
Acknowledgments.
ThisresearchwassupportedbyNSFgrants0917047and1018211;byCyLabatCarnegieMellonundergrantsDAAD19-02-1-0389andW911NF-09-1-0273fromtheArmyResearchOce;andbyagiftfromKDDIR&DLaboratoriesInc.
References1.
Armando,A.
,Merlo,A.
,Verderame,M.
M.
:WouldyoumindforkingthisprocessAdenialofserviceattackonAndroid(andsomecountermeasures).
In:Proc.
IFIPSEC(2012)2.
Bugiel,S.
,Davi,L.
,Dmitrienko,A.
,Fischer,T.
,Sadeghi,A.
R.
,Shastry,B.
:To-wardstamingprivilege-escalationattacksonAndroid.
In:Proc.
NDSS(2012)3.
Bugiel,S.
,Davi,L.
,Dmitrienko,A.
,Heuser,S.
,Sadeghi,A.
R.
,Shastry,B.
:Prac-ticalandlightweightdomainisolationonAndroid.
In:Proc.
SPSM(2011)4.
Chaudhuri,A.
:Language-basedsecurityonAndroid.
In:PLASWorkshop(2009)5.
Chin,E.
,Felt,A.
P.
,Greenwood,K.
,Wagner,D.
:Analyzinginter-applicationcom-municationinAndroid.
In:Proc.
MobiSys(2011)6.
Davi,L.
,Dmitrienko,A.
,Sadeghi,A.
R.
,Winandy,M.
:PrivilegeEscalationAttacksonAndroid.
In:Burmester,M.
,Tsudik,G.
,Magliveras,S.
,Ilic,I.
(eds.
)ISC2010.
LNCS,vol.
6531,pp.
346–360.
Springer,Heidelberg(2011)7.
Dietz,M.
,Shekhar,S.
,Pisetsky,Y.
,Shu,A.
,Wallach,D.
S.
:Quire:Lightweightprovenanceforsmartphoneoperatingsystems.
In:Proc.
USENIXSecurity(2011)18E.
Fragkakietal.
8.
Enck,W.
,Gilbert,P.
,GonChun,B.
,Cox,L.
P.
,Jung,J.
,McDaniel,P.
,Sheth,A.
N.
:TaintDroid:Aninformation-owtrackingsystemforrealtimeprivacymonitoringonsmartphones.
In:Proc.
USENIXOSDI(2010)9.
Enck,W.
,Octeau,D.
,McDaniel,P.
,Chaudhuri,S.
:AstudyofAndroidapplicationsecurity.
In:Proc.
USENIXSecurity(2011)10.
Enck,W.
,Ongtang,M.
,McDaniel,P.
D.
:Onlightweightmobilephoneapplicationcertication.
In:Proc.
CCS(2009)11.
Felt,A.
P.
,Chin,E.
,Hanna,S.
,Song,D.
,Wagner,D.
:Androidpermissionsdemys-tied.
In:Proc.
CCS(2011)12.
Felt,A.
P.
,Wang,H.
,Moshchuk,A.
,Hanna,S.
,Chin,E.
:Permissionre-delegation:Attacksanddefenses.
In:Proc.
USENIXSecurity(2011)13.
Fragkaki,E.
,Bauer,L.
,Jia,L.
:ModelingandenhancingAndroid'spermissionsys-tem.
Tech.
Rep.
CMU-CyLab-11-020,CyLab,CarnegieMellonUniversity(2011)14.
Hornyack,P.
,Han,S.
,Jung,J.
,Schechter,S.
,Wetherall,D.
:Thesearen'tthedroidsyou'relookingfor:RetrottingAndroidtoprotectdatafromimperiousapplications.
In:Proc.
CCS(2011)15.
Lineberry,A.
,Richardson,D.
L.
,Wyatt,T.
:Thesearen'tthepermissionsyou'relookingfor(2010),www.
defcon.
org/images/defcon-18/dc-18-presentations/Lineberry/DEFCON-18-Lineberry-Not-The-Permissions-You-Are-Looking-For.
pdf(accessedApril10,2012)16.
Loftus,J.
:DefCondingsrevealGoogleproductsecurityrisks(2011),gizmodo.
com/5828478(accessedApril10,2012)17.
Luo,T.
,Hao,H.
,Du,W.
,Wang,Y.
,Yin,H.
:AttacksonWebViewintheAndroidsystem.
In:Proc.
ACSAC(2011)18.
Marforio,C.
,Francillon,A.
,ˇCapkun,S.
:Applicationcollusionattackonthepermission-basedsecuritymodelanditsimplicationsformodernsmartphonesys-tems.
Tech.
Rep.
724,ETHZurich(2011)19.
Mylonas,A.
,Dritsas,S.
,Tsoumas,B.
,Gritzalis,D.
:Smartphonesecurityevalua-tion–Themalwareattackcase.
In:Proc.
SECRYPT(2011)20.
Nauman,M.
,Khan,S.
,Zhang,X.
:Apex:extendingAndroidpermissionmodelandenforcementwithuser-denedruntimeconstraints.
In:Proc.
ASIACCS(2010)21.
NTTDataCorporation:TOMOYOLinux(2012),tomoyo.
sourceforge.
jp/(accessedApril10,2012)22.
Ongtang,M.
,McLaughlin,S.
E.
,Enck,W.
,McDaniel,P.
D.
:Semanticallyrichapplication-centricsecurityinAndroid.
In:Proc.
ACSAC(2009)23.
Passeri,P.
:OneyearofAndroidmalware(fulllist)(2011),hackmageddon.
com/2011/08/11/one-year-of-android-malware-full-list/(accessedJune20,2012)24.
Schlegel,R.
,Zhang,K.
,Zhou,X.
,Intwala,M.
,Kapadia,A.
,Wang,X.
:Sound-comber:Astealthyandcontext-awaresoundTrojanforsmartphones.
In:Proc.
NDSS(2011)25.
Shin,W.
,Kiyomoto,S.
,Fukushima,K.
,Tanaka,T.
:AformalmodeltoanalyzethepermissionauthorizationandenforcementintheAndroidframework.
In:Proc.
SocialCom/PASSAT(2010)26.
Shin,W.
,Kwak,S.
,Kiyomoto,S.
,Fukushima,K.
,Tanaka,T.
:Asmallbutnon-negligibleawintheAndroidpermissionscheme.
In:Proc.
POLICY(2010)27.
Zhou,W.
,Zhou,Y.
,Jiang,X.
,Ning,P.
:Detectingrepackagedsmartphoneappli-cationsinthird-partyAndroidmarketplaces.
In:Proc.
CODASPY2012(2012)