Analisi Empirica e Formale della Google Play Integrity API nei dispositivi Android

Abstract

I sistemi operativi mobili moderni eseguono sempre più spesso transazioni di alto valore all’interno di ambienti client non attendibili, rendendo l’attestazione remota un meccanismo fondamentale per stabilire l’autenticità delle applicazioni e delle piattaforme. Nell’ecosistema Android, Google ha introdotto la Play Integrity API in sostituzione di SafetyNet, fondando le garanzie di attestazione su radici di fiducia supportate dall’hardware, sul provisioning remoto delle chiavi e su dati telemetrici dinamici per il contrasto agli abusi. Nonostante l’ampia diffusione, il funzionamento operativo dell’API e le relative garanzie formali di sicurezza non sono documentati, costringendo le entità remote che si basano sull’attestazione a considerare la pipeline di attestazione come un sottosistema opaco.

Questa tesi presenta una valutazione empirica e formale completa della sicurezza del Google Play Integrity Classic Flow. Avvalendoci di un ambiente di test Android 15 strumentato, abbiamo sottoposto a reverse engineering i formati dei messaggi non documentati, le routine di telemetria in background e le comunicazioni interprocesso, individuando un’architettura disaccoppiata composta da una fase asincrona di inizializzazione e da una richiesta di attestazione sincrona. Abbiamo formalizzato il protocollo ricostruito nel framework di analisi simbolica Tamarin-Prover, specificando regole di riscrittura di multinsiemi e lemmi di sicurezza per domini di dispositivi attendibili e non attendibili, in presenza di un avversario attivo secondo il modello di Dolev-Yao.

La verifica simbolica dimostra che il protocollo garantisce la freschezza dei messaggi, la protezione dagli attacchi di replay tramite il consumo lineare dello stato lato server e la riservatezza degli esiti rispetto agli ambienti di esecuzione client non attendibili. Tuttavia, Tamarin-Prover confuta la proprietà di integrità della co-localizzazione del dispositivo, rivelando una vulnerabilità strutturale dovuta all’ass

Modern mobile operating systems increasingly execute high-value transactions within untrusted client environments, making remote attestation a fundamental mechanism for establishing application and platform authenticity. Within the Android ecosystem, Google introduced the Play Integrity API to replace SafetyNet, anchoring attestation guarantees to hardware-backed roots of trust, remote key provisioning, and dynamic anti-abuse telemetry. Despite its widespread adoption, the operational mechanics and formal security guarantees of the API remain undocumented, leaving remote relying parties to treat the attestation pipeline as an opaque subsystem.

This thesis presents a comprehensive empirical and formal security evaluation of the Google Play Integrity Classic Flow. Using an instrumented Android 15 testbed, we reverse-engineered the undocumented message formats, background telemetry routines, and inter-process communications, identifying a decoupled architecture comprising an asynchronous warm-up phase and a synchronous attestation request. We formalized the reconstructed protocol in the Tamarin-Prover symbolic analysis framework, specifying multiset rewriting rules and security lemmas across trusted and untrusted device domains under an active Dolev-Yao adversary.

Symbolic verification demonstrates that the protocol guarantees message freshness, anti-replay protection through linear server-state consumption, and verdict confidentiality against untrusted client runtimes. However, Tamarin-Prover falsifies device co-location integrity, revealing a structural vulnerability caused by the absence of cryptographic channel binding between the client-server transport session and the attestation token issued by Google. We validated the practical viability of this finding through an application-level proof-of-concept exploit that requires no operating system-level modifications or dynamic instrumentation tools (such as Magisk or Frida), confirming that an adversary on an untrus