论文标题
自动验证的Android权限系统的原型
An Automatically Verified Prototype of the Android Permissions System
论文作者
论文摘要
在先前的工作中，de luca和Luna介绍了COQ证明助理中Android许可模型的理想化表述的形式规格。这种正式开发约为COQ代码的23个KLOC，包括证明。这项工作旨在表明{log}（``setLog'）（一种满意性的求解器和约束逻辑编程语言）可以用作有效的自动化供体，用于在正式验证系统中必须放电的一系列证明类别，例如由de Luca和Luna进行的系统。我们展示了如何在{log}中编码COQ模型以及如何执行自动证明。结果{log}模型是自动验证的Android权限系统的可执行原型。提供了有关执行{log}中所有证明后产生的经验评估的详细数据。讨论了COQ和{log}的集成，以提供具有自动证明和原型生成的框架。
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.
