SEAL - Terminator

TLA+ Android Module

--------------------------- 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 = [<> \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 <>

Uninstall(app) ==
          /\ appStat[app] # "Uninstalled"
          /\ appStat' = [appStat EXCEPT ![app]="Uninstalled"]
          /\ UNCHANGED <>

Run(app) ==
          /\ appStat[app] = "Terminated"
          /\ appStat' = [appStat EXCEPT ![app]="Running"]
          /\ UNCHANGED <>

Terminate(app) ==
          /\ appStat[app] = "Running"
          /\ appStat' = [appStat EXCEPT ![app]="Terminated"]
          /\ UNCHANGED <>

Grant(app, perm) ==
          /\ appStat[app] # "Uninstalled"
          /\ permStat[<>] = "Revoked"
          /\ perm \in AppReqPerms[app]
          /\ permStat' = [permStat EXCEPT ![<>]="Granted"]
          /\ UNCHANGED <>

Revoke(app, perm) ==
          /\ appStat[app] # "Uninstalled"
          /\ permStat[<>] = "Granted"
          /\ perm \in AppReqPerms[app]
          /\ permStat' = [permStat EXCEPT ![<>]="Revoked"]
          /\ UNCHANGED <>

StoreUnprotected(app, perm) ==
          /\ appStat[app] = "Running"
          /\ permStat[<>] = "Granted"
          /\ perm \in SourcePerms
          /\ app \in UnprotectedDB
          /\ dbStat' = [dbStat EXCEPT ![app]="Sensitive"]
          /\ UNCHANGED <>

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]_<>

-----------------------------------------------------------------------------
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[<>] = "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[<>] = "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[<>] = "Granted")

THEOREM Spec => TypeInvariant /\ NoPDL /\ NoPE /\ NoICP

=============================================================================