| File | Mode | Size |
|---|---|---|
| .Makefile.d | -rw-r--r-- | 53.6 KB |
| .gitignore | -rw-r--r-- | 264 bytes |
| AuxFunsCorrect.v | -rw-r--r-- | 113.3 KB |
| CallIsSound.v | -rw-r--r-- | 3.7 KB |
| CanAutoGrantWithoutPerms.v | -rw-r--r-- | 9.0 KB |
| CertAndroidSec.hs | -rw-r--r-- | 95.4 KB |
| DangPermAutoGranted.v | -rw-r--r-- | 1.7 KB |
| DangPermMissing.v | -rw-r--r-- | 9.2 KB |
| DefBasicas.v | -rw-r--r-- | 6.7 KB |
| DelegateGrantPRevoke.v | -rw-r--r-- | 9.5 KB |
| Eavesdropping.v | -rw-r--r-- | 8.0 KB |
| EqTheorems.v | -rw-r--r-- | 4.9 KB |
| ErrorManagement.v | -rw-r--r-- | 15.4 KB |
| Estado.v | -rw-r--r-- | 10.7 KB |
| Exec.v | -rw-r--r-- | 3.1 KB |
| GrantAutoIsInvariant.v | -rw-r--r-- | 2.6 KB |
| GrantAutoIsSound.v | -rw-r--r-- | 12.7 KB |
| GrantIsInvariant.v | -rw-r--r-- | 4.2 KB |
| GrantIsSound.v | -rw-r--r-- | 13.8 KB |
| GrantPIsInvariant.v | -rw-r--r-- | 2.1 KB |
| GrantPIsSound.v | -rw-r--r-- | 8.8 KB |
| HasPermissionIsSound.v | -rw-r--r-- | 794 bytes |
| IfOldAppRunThenVerified.v | -rw-r--r-- | 6.8 KB |
| IfPermThenGranted.v | -rw-r--r-- | 6.9 KB |
| Implementacion.v | -rw-r--r-- | 66.9 KB |
| InstallIsInvariant.v | -rw-r--r-- | 16.5 KB |
| InstallIsSound.v | -rw-r--r-- | 15.6 KB |
| IntentSpoofing.v | -rw-r--r-- | 2.6 KB |
| ListAuxFuns.v | -rw-r--r-- | 6.6 KB |
| Makefile | -rw-r--r-- | 27.6 KB |
| Makefile.conf | -rw-r--r-- | 6.6 KB |
| Maps.v | -rw-r--r-- | 13.6 KB |
| ModelProperties.v | -rw-r--r-- | 12.1 KB |
| MyList.v | -rw-r--r-- | 3.1 KB |
| Operaciones.v | -rw-r--r-- | 1.7 KB |
| PropertiesAuxFuns.v | -rw-r--r-- | 3.9 KB |
| README.md | -rw-r--r-- | 571 bytes |
| ReadIsSound.v | -rw-r--r-- | 3.0 KB |
| ReceiveIntentIsInvariant.v | -rw-r--r-- | 5.8 KB |
| ReceiveIntentIsSound.v | -rw-r--r-- | 19.8 KB |
| ResolveIntentIsInvariant.v | -rw-r--r-- | 3.3 KB |
| ResolveIntentIsSound.v | -rw-r--r-- | 14.0 KB |
| RevokeDelIsInvariant.v | -rw-r--r-- | 2.5 KB |
| RevokeDelIsSound.v | -rw-r--r-- | 21.0 KB |
| RevokeGroupIsInvariant.v | -rw-r--r-- | 3.2 KB |
| RevokeGroupIsSound.v | -rw-r--r-- | 6.6 KB |
| RevokeIsInvariant.v | -rw-r--r-- | 2.9 KB |
| RevokeIsSound.v | -rw-r--r-- | 4.0 KB |
| RuntimePermissions.v | -rw-r--r-- | 2.5 KB |
| RvkAndNotGrant.v | -rw-r--r-- | 3.5 KB |
| RvkCanStart.v | -rw-r--r-- | 4.8 KB |
| SameEnvLemmas.v | -rw-r--r-- | 5.3 KB |
| Semantica.v | -rw-r--r-- | 62.0 KB |
| SendBroadcastIsInvariant.v | -rw-r--r-- | 3.0 KB |
| SendBroadcastIsSound.v | -rw-r--r-- | 4.6 KB |
| SendOrderedBroadcastIsSound.v | -rw-r--r-- | 952 bytes |
| SendStickyBroadcastIsSound.v | -rw-r--r-- | 918 bytes |
| Soundness.v | -rw-r--r-- | 2.3 KB |
| StartActivityForResIsSound.v | -rw-r--r-- | 924 bytes |
| StartActivityIsInvariant.v | -rw-r--r-- | 3.0 KB |
| StartActivityIsSound.v | -rw-r--r-- | 4.7 KB |
| StartServiceIsInvariant.v | -rw-r--r-- | 3.0 KB |
| StartServiceIsSound.v | -rw-r--r-- | 4.7 KB |
| StopIsInvariant.v | -rw-r--r-- | 2.8 KB |
| StopIsSound.v | -rw-r--r-- | 4.0 KB |
| Tacticas.v | -rw-r--r-- | 3.5 KB |
| Trace.v | -rw-r--r-- | 3.8 KB |
| TraceRelatedLemmas.v | -rw-r--r-- | 24.6 KB |
| UninstallIsInvariant.v | -rw-r--r-- | 12.4 KB |
| UninstallIsSound.v | -rw-r--r-- | 17.0 KB |
| ValidStateLemmas.v | -rw-r--r-- | 11.0 KB |
| ValidityInvariance.v | -rw-r--r-- | 2.5 KB |
| VerifyOldAppIsInvariant.v | -rw-r--r-- | 2.6 KB |
| VerifyOldAppIsSound.v | -rw-r--r-- | 5.2 KB |
| WitnessesFactory.v | -rw-r--r-- | 1.6 KB |
| WriteIsInvariant.v | -rw-r--r-- | 2.5 KB |
| WriteIsSound.v | -rw-r--r-- | 4.7 KB |
| _CoqProject | -rw-r--r-- | 8 bytes |
| makeMakefile.sh | -rwxr-xr-x | 41 bytes |
