An automatically verified prototype of the Android permissions system

DOI10.1007/s10817-023-09666-2arXiv2209.10278OpenAlexW4376271928MaRDI QIDQ6103592

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

Coqsecurity propertiesautomated proof\(\{log\}\)Android

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The calculus of constructions
• 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
• A set solver for finite set relation algebra
• Hammer for Coq: automation for dependent type theory
• A certified reference validation mechanism for the permission model of Android
• Automated proof of Bell-LaPadula security properties
• An automatically verified prototype of the Tokeneer ID station specification
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Extending Sledgehammer with SMT solvers
• Automated reasoning with restricted intensional sets
• Verifying Android’s Permission Model
• Dafny: An Automatic Program Verifier for Functional Correctness
• The B-Book
• Formal Analysis of Android's Permission-Based Security Model

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