Abdulla Aldoseri

Assistant Professor @ University of Bahrain, Bahrain




A scientific research paper discusses symbolic modelling for Android remote attestation protocols.

Presented by: Abdulla Aldoseri · Dr. Tom Chothia · José Moreira · Prof. David Oswald

Abstract

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.

Keywords: Android · Remote attestation · Android apps · App integrity · Device integrity · Root detection

Presentation and Demo videos


Demonstration of practical code protection model using Android Key attestation (PoC demo).