Android字节码的形式化认证

Android是一种用于大多数移动设备的操作系统。Android中每个应用运行在Dalvik虚拟机的一个实例中，这是一种基于寄存器的虚拟机（VM）。大多数Android应用使用Java开发，编译为Java字节码，然后使用Android SDK中的dx工具翻译为DEX字节码。本工作中，我们旨在开发一种基于类型的方法，用于认证DEX字节码的非干扰属性，遵循Barthe等人针对Java字节码认证所提出的方法论。为此，我们开发了Dalvik VM的形式化操作语义、一个DEX字节码类型系统，并证明了该类型系统相对于非干扰概念的可靠性。然后我们研究了Android SDK中dx工具实现的从Java字节码到DEX字节码的翻译过程。我们展示了从Java字节码到DEX字节码翻译的抽象版本保持非干扰属性。更精确地，我们展示如果Java字节码在Barthe等人的类型系统（保证非干扰）中可类型化，则其翻译在我们的类型系统中可类型化。该结果开启了利用现有Java字节码验证器来认证Android字节码非干扰属性的可能性。