An Automatically Verified Prototype of the Android Permissions System
Maximiliano Cristi\'a, Guido De Luca, Carlos Luna

TL;DR
This paper demonstrates how the setlog satisfiability solver can be used to automatically verify and generate an executable prototype of the Android permissions system based on a formal Coq model.
Contribution
It introduces a novel approach integrating Coq and setlog for automated proof and prototype generation of Android permissions system models.
Findings
Successful encoding of Coq model in setlog
Automated proofs verified the model's correctness
Generated executable prototype of Android permissions system
Abstract
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 is about 23 KLOC of Coq code, including proofs. This work aims at showing that {log} (`setlog') -- a satisfiability solver and a constraint logic programming language -- can be used as an effective automated prover for the class of proofs that must be discharged in the formal verification of systems such as the one carried out by De Luca and Luna. We show how the Coq model is encoded in {log} and how automated proofs are performed. The resulting {log} model is an automatically verified executable prototype of the Android permissions system. Detailed data on the empirical evaluation resulting after executing all the proofs in {log} is provided. The integration of Coq and {log} as to provide a framework…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsService-Oriented Architecture and Web Services · Model-Driven Software Engineering Techniques · Advanced Software Engineering Methodologies
