Automated-Security-Certification-of-Android-Applic

SCanDroid:AutomatedSecurityCertificationofAndroidApplicationsAdamP.Fuchs,AvikChaudhuri,andJeffreyS.FosterUniversityofMaryland,CollegeParkfafuchs,avik,[e-mail]ularmobile-deviceplatformdevelopedbyGoogle.Android’sapplicationmodelisdesignedtoencourageapplicationstosharetheircodeanddatawithotherapplications.Whilesuchsharingcanbetightlycon-trolledwithpermissions,ingeneraluserscannotdeterminewhatapplicationswilldowiththeirdata,andtherebycan-notdecidewhatpermissionssuchapplicationsshouldrunwith.InthispaperwepresentSCANDROID,atoolforrea-soningautomaticallyaboutthesecurityofAndroidappli-cations.SCANDROID’sanalysisismodulartoallowin-crementalcheckingofapplicationsastheyareinstalledonanAndroiddevice.Itextractssecurityspecificationsfrommanifeststhataccompanysuchapplications,andcheckswhetherdataflowsthroughthoseapplicationsareconsis-tentwiththosespecifications.Toourknowledge,SCAN-DROIDisthefirstprogramanalysistoolforAndroid,andweexpectittobeusefulforautomatedsecuritycertificationofAndroidapplications.1IntroductionAndroid[3]isGoogle’sopen-sourceplatformformobiledevices,whichisrecentlyenjoyingwideadoptionbythein-dustry.Designedtobeacompletesoftwarestack,Androidincludesanoperatingsystem,middleware,andcoreappli-cations.Furthermore,itcomeswithanSDKthatprovidesthetoolsandAPIsnecessarytodevelopnewapplicationsfortheplatforminJava[3].DevelopersofnewapplicationshavefullaccesstothesameframeworkAPIsusedbythecoreapplications.Android’sapplicationmodelhasseveralinterestingfea-tures.First,applicationsmustfollowaspecificstructure,i.e.,theymustbecomposedofsomebasickindsofcom-ponentsunderstoodbyAndroid.Thisdesignencouragessharingofcodeanddataacrossapplications.Next,inter-actionsbetweencomponentscanbetightlycontrolled.Bydefault,componentswithinanapplicationaresandboxedbyAndroid,andotherapplicationsmayaccesssuchcom-ponentsonlyiftheyhavetherequiredpermissionstodoso.Thisdesignpromisessomemeasureofprotectionfromma-liciousapplications.However,enforcingpermissionsisnotsufficienttopre-ventsecurityviolations,sincepermissionsmaybemisused,intentionallyorunintentionally,tointroduceinsecuredataflows.Indeed,supposethatAlicedownloadsandinstallsanewapplication,developedbyBob,onherAndroid-basedphone.Saythisapplication,wikinotes,interactswithacoreapplication,notes,topublishsomenotesfromthephonetoawiki,andtosynceditsbackfromthewikitothephone.Ofcourse,Alicewouldnotlikeallhernotestobepublished,andwouldnotlikeallherpublishednotestobeedited;forinstance,hernotesmayincludedetailsofherongoingre-search.Howcansheknowwhetheritissafetoruntheapplication?Canshetrusttheapplicationtosafelyaccessherdata?Conversely,BobmaywanttobeabletoconvinceAlicethathisapplicationcanberunsafelyonherphone.Inthispaper,wepresentSCANDROID,1atoolforautomatedsecuritycertificationofAndroidapplications.SCANDROIDstaticallyanalyzesdataflowsthroughAn-droidapplications,andcanmakesecurity-relevantdeci-sionsautomatically,basedonsuchflows.Inparticular,itcandecidewhetheritissafeforanapplicationtorunwithcertainpermissions,basedonthepermissionsenforcedbyotherapplications.Alternatively,itcanprovideenoughcon-texttotheusertomakeinformedsecurity-relevantdeci-sions.SCANDROIDcanalsobeusefulinvariousproof-carryingcode(PCC)[11]settings.Forexample,applica-tionscanbereviewedofflinewithSCANDROIDbyanappli-cationstore[2],andAndroiddevicescancheckcertificatesofsecurityissuedbytheapplicationstoreatinstalltime.Alternatively,thedevelopercanconstructasafetyprooffortheapplicationbyusingouranalysis,andthedevicecanverifythatproofbeforeinstallingtheapplication.AttheheartofSCANDROIDisamodulardataflowanal-ysisforAndroidapplications,designedtoallowincremen-talcheckingofapplicationsastheyareinstalledonanAn-droiddevice.Ouranalysistracksdataflowsthroughandacrosscomponents,whilerelyingonanunderlyingabstractsemanticsforAndroidapplications.Thedataflowscanbefairlycomplicated,duetosophisticatedprotocolsrunbyAndroidtoroutecontrolbetweencomponents.OurabstractsemanticsforAndroidapplicationsexposesthesecontrolroutestoouranalysis.1Thenameisintendedtoabbreviate“SecurityCertifierforanDroid”,althoughvariouspunsmightbeintendedaswell.1Weformalizethebasicelementsofourdataflowanaly-sisasaconstraintsystem,basedonanexistingcorecalcu-lustodescribeandreasonaboutAndroidapplications[7].Weshowhowend-to-endsecuritycanbeenforcedwithourdataflowanalysis.Inourformalism,wefocusonlyonconstructsthatareuniquetoAndroid,whileignoringtheotherusualJavaconstructsthatmayappearinAndroidap-plications.ThissimplificationallowsustostudyAndroid-specificfeaturesinisolation.Oursystemreliesontheac-cesscontrolmechanismsalreadyprovidedbyAndroid,andenforces“bestpractices”fordevelopingsecureapplicationswiththesemechanisms.Theresultingguaranteesincludestandarddata-flowsecuritypropertiesforwell-constrainedapplicationsdescribedinthecalculus.Next,weextendandimplementthiscoreanalysistorea-sonaboutactualAndroidapplications.Forthispurpose,wemustconsidertheusualJavaconstructsincombinationwithAndroid-specificconstructs.Thisposessomesignifi-cantchallenges:forinstance,weneedastringanalysis