An Automatically Verified Prototype of the Android Permissions System

In a previous work we 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. In this work the Coq model is encoded in { l o g } (‘setlog’)—a satisfiability solver...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2023-06, Vol.67 (2), p.17, Article 17
Main Authors: Cristiá, Maximiliano, De Luca, Guido, Luna, Carlos
Format: Article
Language:English
Subjects:
Access control
Algorithms
Artificial Intelligence
Automation
Coding
Computer Science
Formal specifications
Linux
Logic programming
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Programming languages
Prototypes
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In a previous work we 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. In this work the Coq model is encoded in { l o g } (‘setlog’)—a satisfiability solver and a constraint logic programming language— which is then used to automatically discharge most of the proofs performed in Coq. We show how the Coq model is encoded in { l o g } and how automated proofs are performed. The resulting { l o g } 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 { l o g } is provided. The integration of Coq and { l o g } as to provide a framework featuring automated proof and prototype generation is discussed.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-023-09666-2