RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial

Philip Daian 1 Yliès Falcone 2, 3, * Patrick Meredith 1 Traian Florin Serbanuta 1 Shin’ichi Shiriashi 4 Akihito Iwai 5 Grigore Rosu 1, 2
* Auteur correspondant
1 Runtime Verification
2 University of Illinois at Urbana-Champaign [Urbana]
3 CORSE - Compiler Optimization and Run-time Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
4 Toyota InfoTechnology Center [Mountain View]
5 Denso International America Inc. [Belleville]
Abstract : RV-Android is a new freely available open source runtime library for monitoring formal safety properties on Android. RV-Android uses the commercial RV-Monitor technology as its core monitoring library generation technology, allowing for the verification of safety properties during execution and operating entirely in userspace with no kernel or operating system modifications required. RV-Android improves on previous Android monitoring work by replacing the JavaMOP framework with RV-Monitor, a more advanced monitoring library generation tool with core algorithmic improvements that greatly improve resource consumption , e and battery life considerations. We demonstrate the developer usage of RV-Android with the standard Android build process, using instrumentation mechanisms e↵ective on both Android binaries and source code. Our method allows for both property development and advanced application testing through runtime verification. We showcase the user frontend of RV-Monitor, which is available for public demo use and requires no knowledge of RV concepts. We explore the extra expres-siveness the MOP paradigm provides over simply writing properties as aspects through two sample security properties, and show an example of a real security violation mitigated by RV-Android on-device. Lastly, we propose RV as an extension to the next-generation Android permissions system debuting in Android M.
Type de document :
Communication dans un congrès
6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015. Proceedings, Sep 2015, Vienne, Austria. Springer, LNCS (9333), pp.16, 2015, Runtime Verification. 〈10.1007/978-3-319-23820-3_24〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01248350
Contributeur : Yliès Falcone <>
Soumis le : lundi 28 décembre 2015 - 14:10:46
Dernière modification le : mercredi 11 avril 2018 - 01:54:15

Fichier

rv15-3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

LIG | INRIA | UGA | LIG-SRCPR-CORSE | LIG_SRCPR | INRIA-RENGRE

Citation

Philip Daian, Yliès Falcone, Patrick Meredith, Traian Florin Serbanuta, Shin’ichi Shiriashi, et al.. RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. 6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015. Proceedings, Sep 2015, Vienne, Austria. Springer, LNCS (9333), pp.16, 2015, Runtime Verification. 〈10.1007/978-3-319-23820-3_24〉. 〈hal-01248350〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

198

Téléchargements de fichiers

213

Contact


archive-ouverte@inria.fr