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 |
README.md

Loading README.md ...