An Automatically Verified Prototype of the Android Permissions System

Maximiliano Cristiá, Guido De Luca, Carlos Luna

In a previous work De Luca and Luna presented formal specifications of idealized formulations of the permission model of Android in the Coq proof assistant. This formal development…