An automatically verified prototype of the Android permissions system
From MaRDI portal
Publication:6103592
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
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
