Projects per year
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 | |
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
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.Projects
- 2 Active
-
CAP-TEE: Capability Architectures in Trusted Execution
Ryan, M. (Co-Investigator), Thomas, R. (Co-Investigator), Ordean, M. (Co-Investigator), Garcia, F. (Co-Investigator), Oswald, D. (Principal Investigator), Muench, M. (Co-Investigator) & Sinha Roy, S. (Researcher)
Engineering & Physical Science Research Council
12/08/20 → 28/02/25
Project: Research Councils
-
User-controlled hardware security anchors: evaluation and designs
Garcia, F. (Co-Investigator), Oswald, D. (Co-Investigator) & Ryan, M. (Principal Investigator)
Hewlett-Packard Incorporated Uk Ltd, Engineering & Physical Science Research Council
1/02/18 → 31/03/25
Project: Research