--------------------------- MODULE AndroidRuntime ---------------------------
CONSTANT Apps, \* The set of all apps installed in the device.
Perms, \* The set of all permissions defined in Android or by App develoeprs (i.e. custom permissions).
SinkPerms, SourcePerms, \* Only to distinguish sink and source perms
CustomPerms, \* A Set of custom permissons defined by app developers
AppReqPerms, \* A function, where AppReqPerms[app] is the set of permissions requested by App app
AppDecPerms, \* A function, where AppReqPerms[app] is the set of permissions declared by App app
UnprotectedDB, \* The set of apps with unprotected DBS
UnprotectedIntentFilter \* A function, where AppIntentFilter[app, perm] determines whether app intentFilter that exposed a perm-required capability is protected
ASSUME AppReqPerms \in [Apps -> SUBSET Perms]
ASSUME AppDecPerms \in [Apps -> SUBSET CustomPerms]
ASSUME UnprotectedDB \in SUBSET Apps
ASSUME UnprotectedIntentFilter \in SUBSET (Apps \X Perms)
ASSUME SinkPerms \subseteq Perms
ASSUME SourcePerms \subseteq Perms
ASSUME CustomPerms \subseteq Perms
-----------------------------------------------------------------------------
VARIABLES appStat, \* The state of an application
permStat, \* The state of a permission
dbStat, \* The state of the phone db
collidingPerms \* The state of permission
TypeInvariant ==
/\ appStat \in [Apps -> {"Uninstalled", "Terminated", "Running"}]
/\ permStat \in [(Apps \X Perms) -> {"Granted", "Revoked"}]
/\ dbStat \in [Apps -> {"Sensitive", "Clear"}]
/\ collidingPerms \in [Apps -> {"Unique", "Colliding"}]
Init ==
/\ appStat = [app \in Apps |-> "Uninstalled"] \* App apps are not installed initially
/\ permStat = [<<app, perm>> \in (Apps \X Perms) |-> "Revoked"] \* No permission is granted initially
/\ dbStat = [app \in Apps |-> "Clear"] \* All app DBs are initially empty
/\ collidingPerms = [app \in (Apps) |-> "Unique"]
-----------------------------------------------------------------------------
CollidePerm(app) ==
IF \E perm \in AppDecPerms[app], oldApp \in Apps: /\ appStat[oldApp] # "Uninstalled"
/\ perm \in AppDecPerms[oldApp] \intersect AppDecPerms[app]
/\ perm \in AppReqPerms[oldApp]
THEN /\ collidingPerms' = [collidingPerms EXCEPT ![app]= "Colliding"]
ELSE /\ UNCHANGED collidingPerms
Install(app) ==
/\ appStat[app] = "Uninstalled"
/\ appStat' = [appStat EXCEPT ![app]="Terminated"]
/\ CollidePerm(app)
/\ UNCHANGED <<permStat, dbStat>>
Uninstall(app) ==
/\ appStat[app] # "Uninstalled"
/\ appStat' = [appStat EXCEPT ![app]="Uninstalled"]
/\ UNCHANGED <<permStat, dbStat, collidingPerms>>
Run(app) ==
/\ appStat[app] = "Terminated"
/\ appStat' = [appStat EXCEPT ![app]="Running"]
/\ UNCHANGED <<permStat, dbStat, collidingPerms>>
Terminate(app) ==
/\ appStat[app] = "Running"
/\ appStat' = [appStat EXCEPT ![app]="Terminated"]
/\ UNCHANGED <<permStat, dbStat, collidingPerms>>
Grant(app, perm) ==
/\ appStat[app] # "Uninstalled"
/\ permStat[<<app, perm>>] = "Revoked"
/\ perm \in AppReqPerms[app]
/\ permStat' = [permStat EXCEPT ![<<app, perm>>]="Granted"]
/\ UNCHANGED <<appStat, dbStat, collidingPerms>>
Revoke(app, perm) ==
/\ appStat[app] # "Uninstalled"
/\ permStat[<<app, perm>>] = "Granted"
/\ perm \in AppReqPerms[app]
/\ permStat' = [permStat EXCEPT ![<<app, perm>>]="Revoked"]
/\ UNCHANGED <<appStat, dbStat, collidingPerms>>
StoreUnprotected(app, perm) ==
/\ appStat[app] = "Running"
/\ permStat[<<app, perm>>] = "Granted"
/\ perm \in SourcePerms
/\ app \in UnprotectedDB
/\ dbStat' = [dbStat EXCEPT ![app]="Sensitive"]
/\ UNCHANGED <<appStat, permStat, collidingPerms>>
Next ==
\E app \in Apps :
\/ Install(app) \/ Run(app) \/ Terminate(app) \/ Uninstall(app)
\/ \E perm \in Perms: Grant(app, perm) \/ Revoke (app, perm) \/ StoreUnprotected(app, perm)
-----------------------------------------------------------------------------
Spec == Init /\ [][Next]_<<appStat, permStat, dbStat, collidingPerms>>
-----------------------------------------------------------------------------
NoPDL == \A app \in Apps:
\/ dbStat[app] = "Clear"
\/ ~ (\E malApp \in Apps, perm \in Perms: /\ perm \in AppReqPerms[malApp]
/\ perm \in SinkPerms
/\ app # malApp
/\ appStat[malApp] = "Running"
/\ permStat[<<malApp, perm>>] = "Granted")
NoPE == \A filter \in UnprotectedIntentFilter:
\/ appStat[filter[1]] # "Running"
\/ permStat[filter] # "Granted"
\/ ~ (\E malApp \in Apps, perm \in Perms: /\ perm \in AppReqPerms[malApp]
/\ perm = filter[2]
/\ malApp # filter[1]
/\ appStat[malApp] = "Running"
/\ permStat[<<malApp, perm>>] = "Granted")
NoICP == ~ (\E app \in Apps, malApp \in Apps, perm \in Perms: /\ app # malApp
/\ collidingPerms[app] = "Colliding"
/\ perm \in AppDecPerms[app]
/\ perm \in AppDecPerms[malApp]
/\ perm \in AppReqPerms[malApp]
/\ appStat[malApp] = "Running"
/\ permStat[<<malApp, perm>>] = "Granted")
THEOREM Spec => TypeInvariant /\ NoPDL /\ NoPE /\ NoICP
=============================================================================