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

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