TY - GEN
T1 - RV-android
T2 - 6th International Conference on Runtime Verification, RV 2015
AU - Daian, Philip
AU - Falcone, Yliès
AU - Meredith, Patrick
AU - Şerbǎnuţǎ, Traian Florin
AU - Shiriashi, Shin’Ichi
AU - Akihito, Akihito Iwai
AU - Rosu, Grigore
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - 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, efficiency, and battery life considerations. We demonstrate the developer usage of RV-Android with the standard Android build process, using instrumentation mechanisms effective 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 expressiveness 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.
AB - 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, efficiency, and battery life considerations. We demonstrate the developer usage of RV-Android with the standard Android build process, using instrumentation mechanisms effective 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 expressiveness 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.
UR - http://www.scopus.com/inward/record.url?scp=84950336313&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84950336313&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-23820-3_24
DO - 10.1007/978-3-319-23820-3_24
M3 - Conference contribution
AN - SCOPUS:84950336313
SN - 9783319238197
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 342
EP - 357
BT - Runtime Verification - 6th International Conference, RV 2015, Proceedings
A2 - Bartocci, Ezio
A2 - Majumdar, Rupak
PB - Springer
Y2 - 22 September 2015 through 25 September 2015
ER -