Java Pathfinder on Android Devices
Java Pathfinder on Android Devices
复制标题
Android 设备上的 Java 探路者
DOI：
10.1145/3011286.3011292
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
and Yoshinori Tanabe
中科院分区：
文献类型：
--
作者：
Alexander Kohan;Mitsuharu Yamamoto;Cyrille Artho;Yoriyuki Yamagata;Lei Ma;Masami Hagiya;and Yoshinori Tanabe
因为Android应用程序是用Java编写的，并在虚拟机(VM)上执行，所以有机会使用Java探路器(JPF)进行验证。已经存在两个JPF扩展：jpf-android和jpf-pathdroid。前者在Java VM上执行Java字节码，而后者以其原始格式执行Android应用程序。两者都不支持本机方法，因此依赖于Android环境的模型。本文介绍了另一种方法：我们将JPF作为执行Java字节码的Android应用程序运行，这使我们可以直接访问Android环境。这种方法允许我们验证依赖于本机调用的富Android应用程序
Because Android apps are written in Java and executed on a virtual machine (VM), there is an opportunity to employ Java Pathfinder (JPF) for their verification. There already exist two JPF extensions, jpf-android and jpf-pathdroid. The former executes Java bytecode on the Java VM, while the latter executes Android applications in their original format. Both do not support native methods, and thus depend on a model of the Android environment. This paper introduces an alternative approach: we run JPF as an Android application that executes Java bytecode, which gives us direct access to the Android environment. This approach allows us to verify rich Android apps that rely on native calls