Access the full text.
Sign up today, get DeepDyve free for 14 days.
Loading next page...
/lp/springer-journals/an-automatically-verified-prototype-of-the-android-permissions-system-1yVE3o0v2a
References (65)
-
Maximiliano Cristi'a, G. Rossi (2022)
A Set-Theoretic Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted QuantifiersArXiv, abs/2208.03518
-
M. Cristiá, G. Rossi (2018)
A Set Solver for Finite Set Relation Algebra -
M. Cristiá, G. Rossi (2020)
Automated Proof of Bell–LaPadula Security PropertiesJournal of Automated Reasoning, 65
-
J. Blanchette, S. Böhme, Lawrence Paulson (2011)
Extending Sledgehammer with SMT SolversJournal of Automated Reasoning, 51
-
Lukasz Czajka, C. Kaliszyk (2018)
Hammer for Coq: Automation for Dependent Type TheoryJournal of Automated Reasoning, 61
-
Gustavo Betarte, J. Campo, C. Luna, A. Romano (2015)
Verifying Android's Permission Model -
L., lifinscm Field
Secure Computer Systems : Mathematical Foundations -
Maximiliano Cristi'a, G. Rossi (2021)
An Automatically Verified Prototype of a Landing Gear SystemArXiv, abs/2112.15147
-
(2023)
Formal verification of the security model of Android -
Gustavo Betarte, J. Campo, Felipe Gorostiaga, C. Luna (2017)
A certified reference validation mechanism for the permission model of AndroidArXiv, abs/1709.03652
-
J. Schwartz, R. Dewar, E. Schonberg, E. Dubinsky (1986)
Programming with Sets: An Introduction to SETL -
(2022)
Smartphone market share -
Gustavo Betarte, J. Campo, C. Luna, A. Romano (2016)
Formal Analysis of Android's Permission-Based Security Model,Sci. Ann. Comput. Sci., 26
-
A. Dovier, Enrico Pontelli, G. Rossi (2001)
Set unificationTheory and Practice of Logic Programming, 6
-
D. Jackson (2003)
Alloy: A Logical Modelling Language -
Z. Users, Didier Bert, Jonathan Bowen, S. King, M. Waldén (2003)
ZB 2003: Formal Specification and Development in Z and B, 2651
-
Domenico Cantone, E. Omodeo, A. Policriti, J. Schwartz (2011)
Set Theory for Computing: From Decision Procedures to Declarative Programming with Sets -
L. LaPadula (1996)
Secure Computer Systems: A Mathematical Model -
Wook Shin, S. Kiyomoto, Kazuhide Fukushima, Toshiaki Tanaka (2010)
A Formal Model to Analyze the Permission Authorization and Enforcement in the Android Framework2010 IEEE Second International Conference on Social Computing
-
A. Chlipala (2013)
Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant -
Pierre Letouzey (2004)
Programmation fonctionnelle certifiée : L'extraction de programmes dans l'assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant) -
(2017)
Common Criteria Recognition Arrangement: Common criteria for information technology security evaluation, part 1: Introduction and general model, version 3.1. release 5 -
Maximiliano Cristi'a, G. Rossi (2021)
A Decision Procedure for a Theory of Finite Sets with Finite Integer IntervalsACM Transactions on Computational Logic
-
establishing the existence of a state where some predicate holds -
J. Schwartz, R. Dewar, E. Dubinsky, E. Schonberg (1986)
Programming with Sets -
Kristopher Micinski, Jonathan Fetter-Degges, Jinseong Jeon, J. Foster, Michael Clarkson (2015)
Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution -
Yves Bertot, P. Castran (2010)
Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions -
(1996)
Android Developers : Application Fundamentals -
T. Coquand, G. Huet (1988)
The Calculus of ConstructionsInf. Comput., 76
-
Samir Talegaon, R. Krishnan (2019)
A Formal Specification of Access Control in Android with URI PermissionsInformation Systems Frontiers, 23
-
C. Hawblitzel, Jon Howell, Manos Kapritsos, Jacob Lorch, Bryan Parno, Michael Roberts, Srinath Setty, Brian Zill (2015)
IronFleet: proving practical distributed systems correctProceedings of the 25th Symposium on Operating Systems Principles
-
Christian Holzbaur (1995)
OFAI clp(Q,R) Manual -
W Khan, H Ullah, A Ahmad, K Sultan, AJ Alzahrani, SD Khan, M Alhumaid, S Abdulaziz (2018)
Crashsafe: a formal model for proving crash-safety of android applicationsHum. Centric Comput. Inf. Sci., 8
-
(2020)
{ log } user’s manual. Technical report, Dipartimento di Matematica, -
L. Lamport, Lawrence Paulson (1999)
Should your specification language be typedACM Trans. Program. Lang. Syst., 21
-
Dragos Sbirlea, M. Burke, Salvatore Guarnieri, Marco Pistoia, Vivek Sarkar (2013)
Automatic detection of inter-application permission leaks in Android applicationsIBM J. Res. Dev., 57
-
(2020)
The Coq Team: The Coq Proof Assistant Reference Manual -Version V8.12.0. LogiCal Project -
M. Cristiá, G. Rossi, C. Frydman (2013)
{log} as a Test Case Generator for the Test Template Framework -
Maximiliano Cristi'a, G. Rossi (2021)
log: Set Formulas as ProgramsArXiv, abs/2104.08130
-
Elli Fragkaki, Lujo Bauer, Limin Jia, David Swasey (2012)
Modeling and Enhancing Android's Permission System -
Maximiliano Cristi'a, G. Rossi (2020)
An Automatically Verified Prototype of the Tokeneer ID Station SpecificationJournal of Automated Reasoning, 65
-
F. Boniol, V. Wiels, Y. Ameur, K. Schewe (2014)
ABZ 2014: The Landing Gear Case Study Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z Toulouse, France, June 2-6, 2014, Proceedings -
C. Paulin-Mohring (1993)
Inductive Definitions in the system Coq - Rules and Properties -
Mohamed El-Zawawy, Parvez Faruki, M. Conti (2022)
Formal model for inter-component communication and its security in androidComputing, 104
-
A. Dovier, C. Piazza, Enrico Pontelli, G. Rossi (2000)
Sets and constraint logic programmingACM Trans. Program. Lang. Syst., 22
-
Patrick Spettel (2010)
Dafny: An Automatic Program Verifier for Functional Correctness -
Joey Coleman, Cliff Jones, I. Oliver, A. Romanovsky, E. Troubitsyna (2005)
RODIN (Rigorous Open Development Environment for Complex Systems) -
J. Abrial (1996)
The B-book - assigning programs to meanings -
Maximiliano Cristi'a, G. Rossi (2021)
Integrating Cardinality Constraints into Constraint Logic Programming with SetsTheory Pract. Log. Program., 23
-
A. Mammar, Régine Laleau (2014)
Modeling a landing gear system in Event-BInternational Journal on Software Tools for Technology Transfer, 19
-
C. Hoare, Jifeng He, C. Morgan, J. Sanders, I. Sørensen, J. Spivey, B. Sufrin (1992)
The Z notation - a reference manual -
Domenico Cantone, E. Omodeo, A. Policriti (1990)
What Is Computable Set Theory -
Alireza Sadeghi, Reyhaneh Jabbarvand, Negar Ghorbani, H. Bagheri, S. Malek (2018)
A Temporal Permission Analysis and Enforcement Framework for Android2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE)
-
H. Bagheri, Eunsuk Kang, S. Malek, D. Jackson (2017)
A formal approach for detection of security flaws in the android permission systemFormal Aspects of Computing, 30
-
M. Cristiá, G. Rossi (2019)
Automated Reasoning with Restricted Intensional SetsJournal of Automated Reasoning, 65
-
M. Cristiá, G. Rossi (2019)
Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary RelationsJournal of Automated Reasoning, 64
-
Domenico Cantone, E. Omodeo, A. Policriti (2001)
Set Theory for Computing -
G. Luca, C. Luna (2020)
Towards a certified reference monitor of the Android 10 permission systemArXiv, abs/2011.00720
-
F. Boniol, V. Wiels (2014)
The Landing Gear System Case Study -
Maximiliano Cristi'a, G. Rossi (2022)
A Typechecker for a Set-Based Constraint Logic Programming LanguageArXiv, abs/2205.01713
-
Erika Chin, A. Felt, K. Greenwood, D. Wagner (2011)
Analyzing inter-application communication in Android -
Available at: //source.android.com/. Last access -
Yves Bertot, P. Castéran (2004)
Interactive Theorem Proving and Program Development -
Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations -
Wilayat Khan, H. Ullah, Aakash Ahmad, K. Sultan, Abdullah Alzahrani, Sultan Khan, M. Alhumaid, Sultan Abdulaziz (2018)
CrashSafe: a formal model for proving crash-safety of Android applicationsHuman-centric Computing and Information Sciences, 8
- Publisher
- Springer Journals
- Copyright
- Copyright © The Author(s), under exclusive licence to Springer Nature B.V. 2023. Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- DOI
- 10.1007/s10817-023-09666-2
- Publisher site
- See Article on Publisher Site
Abstract
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 {log}\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\{log\}$$\end{document} (‘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 {log}\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\{log\}$$\end{document} and how automated proofs are performed. The resulting {log}\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\{log\}$$\end{document} 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}\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\{log\}$$\end{document} is provided. The integration of Coq and {log}\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\{log\}$$\end{document} as to provide a framework featuring automated proof and prototype generation is discussed.
Journal
Journal of Automated Reasoning – Springer Journals
Published: Jun 1, 2023
Keywords: Android; Coq; {log}\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\{log\}$$\end{document}; Security properties; Automated proof