Symbolic Modelling of Remote Attestation Protocols for Device and App Integrity on Android

Abdulla Aldoseri, Tom Chothia, Jose Moreira-Sanchez, David Oswald

Research output: Chapter in Book/Report/Conference proceedingConference contribution

129 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationASIA CCS '23
Subtitle of host publicationProceedings of the 2023 ACM on Asia Conference on Computer and Communications Security
EditorsJoseph Liu, Yang Xiang, Surya Nepal, Gene Tsudik
PublisherAssociation for Computing Machinery (ACM)
Pages218–231
Number of pages14
ISBN (Electronic)9798400700989
DOIs
Publication statusPublished - 10 Jul 2023
Event18th ACM ASIA Conference on Computer and Communications Security - Melbourne, Australia
Duration: 10 Jul 202314 Jul 2023

Conference

Conference18th ACM ASIA Conference on Computer and Communications Security
Abbreviated titleACM ASIACCS 2023
Country/TerritoryAustralia
CityMelbourne
Period10/07/2314/07/23

Keywords

  • Remote attestation
  • Android apps
  • App integrity
  • Device integrity
  • Root detection

Fingerprint

Dive into the research topics of 'Symbolic Modelling of Remote Attestation Protocols for Device and App Integrity on Android'. Together they form a unique fingerprint.

Cite this