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

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

doi:10.1145/3579856.3582812

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

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

167 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 language	English
Title of host publication	ASIA CCS '23
Subtitle of host publication	Proceedings of the 2023 ACM on Asia Conference on Computer and Communications Security
Editors	Joseph Liu, Yang Xiang, Surya Nepal, Gene Tsudik
Publisher	Association for Computing Machinery (ACM)
Pages	218–231
Number of pages	14
ISBN (Electronic)	9798400700989
DOIs	https://doi.org/10.1145/3579856.3582812
Publication status	Published - 10 Jul 2023
Event	18th ACM ASIA Conference on Computer and Communications Security - Melbourne, Australia Duration: 10 Jul 2023 → 14 Jul 2023

Conference

Conference	18th ACM ASIA Conference on Computer and Communications Security
Abbreviated title	ACM ASIACCS 2023
Country/Territory	Australia
City	Melbourne
Period	10/07/23 → 14/07/23

Keywords

Remote attestation
Android apps
App integrity
Device integrity
Root detection

Access to Document

10.1145/3579856.3582812

AldoseriA2023Symbolic
© Owner/Author 2023. This is the author's version of the work. The definitive Version of Record was published in ASIA CCS '23: Proceedings of the 2023 ACM Asia Conference on Computer and Communications Security, https://doi.org/10.1145/3579856.3582812
Accepted author manuscript, 815 KBLicence: Creative Commons: Attribution (CC BY)

CAP-TEE: Capability Architectures in Trusted Execution
Ryan, M., Thomas, R., Ordean, M., Garcia, F., Oswald, D., Muench, M. & Sinha Roy, S.
Engineering & Physical Science Research Council
12/08/20 → 28/02/25
Project: Research Councils
User-controlled hardware security anchors: evaluation and designs
Garcia, F., Oswald, D. & Ryan, M.
Hewlett-Packard Incorporated Uk Ltd, Engineering & Physical Science Research Council
1/02/18 → 31/03/25
Project: Research

Cite this

Aldoseri, A., Chothia, T., Moreira-Sanchez, J., & Oswald, D. (2023). Symbolic Modelling of Remote Attestation Protocols for Device and App Integrity on Android. In J. Liu, Y. Xiang, S. Nepal, & G. Tsudik (Eds.), ASIA CCS '23: Proceedings of the 2023 ACM on Asia Conference on Computer and Communications Security (pp. 218–231). Association for Computing Machinery (ACM). https://doi.org/10.1145/3579856.3582812

Aldoseri, Abdulla ; Chothia, Tom ; Moreira-Sanchez, Jose et al. / Symbolic Modelling of Remote Attestation Protocols for Device and App Integrity on Android. ASIA CCS '23: Proceedings of the 2023 ACM on Asia Conference on Computer and Communications Security. editor / Joseph Liu ; Yang Xiang ; Surya Nepal ; Gene Tsudik. Association for Computing Machinery (ACM), 2023. pp. 218–231

@inproceedings{035475bdca21482392f28c19ac16b51c,

title = "Symbolic Modelling of Remote Attestation Protocols for Device and App Integrity on Android",

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 = "Remote attestation, Android apps, App integrity, Device integrity, Root detection",

author = "Abdulla Aldoseri and Tom Chothia and Jose Moreira-Sanchez and David Oswald",

year = "2023",

month = jul,

day = "10",

doi = "10.1145/3579856.3582812",

language = "English",

pages = "218–231",

editor = "Joseph Liu and Yang Xiang and Surya Nepal and Gene Tsudik",

booktitle = "ASIA CCS '23",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

note = "18th ACM ASIA Conference on Computer and Communications Security , ACM ASIACCS 2023 ; Conference date: 10-07-2023 Through 14-07-2023",

}

Aldoseri, A, Chothia, T, Moreira-Sanchez, J & Oswald, D 2023, Symbolic Modelling of Remote Attestation Protocols for Device and App Integrity on Android. in J Liu, Y Xiang, S Nepal & G Tsudik (eds), ASIA CCS '23: Proceedings of the 2023 ACM on Asia Conference on Computer and Communications Security. Association for Computing Machinery (ACM), pp. 218–231, 18th ACM ASIA Conference on Computer and Communications Security , Melbourne, Victoria, Australia, 10/07/23. https://doi.org/10.1145/3579856.3582812

Symbolic Modelling of Remote Attestation Protocols for Device and App Integrity on Android. / Aldoseri, Abdulla; Chothia, Tom; Moreira-Sanchez, Jose et al.
ASIA CCS '23: Proceedings of the 2023 ACM on Asia Conference on Computer and Communications Security. ed. / Joseph Liu; Yang Xiang; Surya Nepal; Gene Tsudik. Association for Computing Machinery (ACM), 2023. p. 218–231.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Aldoseri, Abdulla

AU - Chothia, Tom

AU - Moreira-Sanchez, Jose

AU - Oswald, David

PY - 2023/7/10

Y1 - 2023/7/10

N2 - 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.

AB - 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.

KW - Remote attestation

KW - Android apps

KW - App integrity

KW - Device integrity

KW - Root detection

UR - https://asiaccs2023.org/

U2 - 10.1145/3579856.3582812

DO - 10.1145/3579856.3582812

M3 - Conference contribution

SP - 218

EP - 231

BT - ASIA CCS '23

A2 - Liu, Joseph

A2 - Xiang, Yang

A2 - Nepal, Surya

A2 - Tsudik, Gene

PB - Association for Computing Machinery (ACM)

T2 - 18th ACM ASIA Conference on Computer and Communications Security

Y2 - 10 July 2023 through 14 July 2023

ER -

Aldoseri A, Chothia T, Moreira-Sanchez J, Oswald D. Symbolic Modelling of Remote Attestation Protocols for Device and App Integrity on Android. In Liu J, Xiang Y, Nepal S, Tsudik G, editors, ASIA CCS '23: Proceedings of the 2023 ACM on Asia Conference on Computer and Communications Security. Association for Computing Machinery (ACM). 2023. p. 218–231 doi: 10.1145/3579856.3582812

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

Abstract

Conference

Keywords

Access to Document

Fingerprint

Projects

CAP-TEE: Capability Architectures in Trusted Execution

User-controlled hardware security anchors: evaluation and designs

Cite this