Symbolic modelling of remote attestation protocols for device and app integrity on Android

Symbolic modelling of remote attestation protocols for device and app integrity on Android
复制标题

DOI：
10.1145/3579856.3582812
复制
发表时间：
2023-07
期刊：
Proceedings of the 2023 ACM Asia Conference on Computer and Communications Security
影响因子：
--
通讯作者：
Abdulla Aldoseri;Tom Chothia;José Moreira;David F. Oswald
Abdulla Aldoseri;Tom Chothia;José Moreira;David F. Oswald
中科院分区：
其他
文献类型：
--
作者：
Abdulla Aldoseri;Tom Chothia;José Moreira;David F. Oswald

文献摘要

相似文献

确保远程应用或设备的完整性是Android生态系统最具挑战性的问题之一。基于软件的解决方案提供有限的保护，通常可以通过重新包装移动的应用程序或root设备来规避。较新的协议使用可信硬件来提供更强的远程证明保证，例如，Google SafetyNet、Samsung Knox（V2和V3认证）和Android密钥认证。到目前为止，这些系统所使用的协议受到的关注相对较少。在本文中，我们使用Tamarin Prover对这些平台进行了正式建模，并在密码学的符号模型中验证了它们的安全属性，揭示了两个漏洞：我们发现了针对Samsung Knox V2的中继攻击，该攻击允许恶意应用程序伪装成诚实的应用程序，以及Android Key Attestation的推荐用例中的错误，这意味着可以重播旧的-可能过时的-证明。我们利用我们的研究结果和建模平台来解决Android安全中最具挑战性的问题之一，即代码保护，提出并正式建模一个代码保护方案，该方案使用硬件信任根来确保移动的应用程序的源代码保护。
Ensuring the integrity of a remote app or device is one of the most challenging concerns for the Android ecosystem. Software-based solutions provide limited protection and can usually be circumvented by repacking the mobile app or rooting the device. Newer protocols use trusted hardware to provide stronger remote attestation guarantees, e.g., Google SafetyNet, Samsung Knox (V2 and V3 attestation), and Android Key Attestation. So far, the protocols used by these systems have received relatively little attention. In this paper, we formally model these platforms using the Tamarin Prover and verify their security properties in the symbolic model of cryptography, revealing two vulnerabilities: we found a relay attack against Samsung Knox V2 that allows a malicious app to masquerade as an honest app, and an error in the recommended use case for Android Key Attestation that means that old—possibly out of date—attestations can be replayed. We employed our findings and the modelled platforms to tackle one of the most challenging problems in Android security, namely code protection, proposing and formally modelling a code protection scheme that ensures source code protection for mobile apps using a hardware root of trust.