Dalvik 字节码的计算可靠性

自动分析依赖具有计算安全性保证的加密操作的 Android 应用程序内的信息流面临着巨大挑战，现有的理解应用程序行为的方法难以应对这些挑战。这些方法不区分加密操作和非加密操作，因此未考虑加密保护：对于敏感消息 m，无论加密操作 f 可能提供何种保密性质，f(m) 都被视为敏感。因此，这些方法提供了应用程序行为的安全近似，但错误地将大量应用程序分类为潜在不安全，从而产生过于悲观的结果。在本文中，我们展示了如何将加密操作忠实地纳入现有的自动应用程序分析方法中。为此，我们首先展示了如何在全面的 Dalvik 字节码语言中将加密操作表示为符号抽象。这些抽象可供自动分析使用，并且只需对其语义进行微小更改即可方便地添加到现有的应用程序分析工具中。其次，我们通过提供 Dalvik 字节码的首个计算可靠性结果来证明我们的抽象是忠实的，即针对我们符号抽象程序的攻击缺失意味着针对合适加密程序实现的任何攻击也缺失。我们将计算可靠性结果置于 CoSP 框架中，这使得该结果具有模块化和可组合性。