An automatically verified prototype of the Android permissions system

DOI10.1007/S10817-023-09666-2MaRDI QIDQ6103592zbMATH OpenOpenAlexFDO

Authors Maximiliano Cristiá, Guido De Luca, Carlos Luna

Publication date 27 June 2023

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2209.10278

zbMATH Keywords

\(\{log\}\)Androidautomated proofCoqsecurity properties

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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 featuring automated proof and prototype generation is discussed.

Cites work

• A certified reference validation mechanism for the permission model of Android
• A set solver for finite set relation algebra
• An automatically verified prototype of the Tokeneer ID station specification
• Automated proof of Bell-LaPadula security properties
• Automated reasoning with restricted intensional sets
• Dafny: an automatic program verifier for functional correctness
• Extending Sledgehammer with SMT solvers
• Formal analysis of Android's permission-based security model
• Hammer for Coq: automation for dependent type theory
• scientific article; zbMATH DE number 1641581 (Why is no real title available?)
• scientific article; zbMATH DE number 3976287 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 50150 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Solving quantifier-free first-order constraints over finite sets and binary relations
• The B-Book
• The calculus of constructions
• Verifying Android's permission model
• ZB 2003: Formal specification and development in Z and B. Third international conference of B and Z users, Turku, Finland, June 4--6, 2003. Proceedings

Cited in

(2)

• EviCheck: Digital Evidence for Android
• A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers

This page was built for publication: An automatically verified prototype of the Android permissions system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6103592)