Towards a certified reference monitor of the android 10 permission system

DOI10.4230/LIPICS.TYPES.2020.3MaRDI QIDQ7232180zbMATH OpenFDO

Authors Guido De Luca, Carlos Luna

Publication date 22 April 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2020.3

zbMATH Keywords

androidcertified implementationCoqformal idealized modelformal proofspermission modelreference monitor

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites work

• A certified reference validation mechanism for the permission model of Android
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• scientific article; zbMATH DE number 1670732 (Why is no real title available?)
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• Producing certified functional code from inductive specifications
• Turning Inductive into Equational Specifications

This page was built for publication: Towards a certified reference monitor of the android 10 permission system

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