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.

This paper analyzes the vulnerability space arising in Trusted Execution Environments (TEEs) when interfacing a trusted enclave application with untrusted, potentially malicious code. Considerable research and industry effort has gone into developing TEE runtime libraries with the purpose of transparently shielding enclave application code from an adversarial environment. However, our analysis reveals that shielding requirements are generally not well-understood in real-world TEE runtime implementations. We expose several sanitization vulnerabilities at the level of the Application Binary Interface (ABI) and the Application Programming Interface (API) that can lead to exploitable memory safety and side-channel vulnerabilities in the compiled enclave. Mitigation of these vulnerabilities is not as simple as ensuring that pointers are outside enclave memory. In fact, we demonstrate that state-of-the-art mitigation techniques such as Intel's edger8r, Microsoft's "deep copy marshalling", or even memory-safe languages like Rust fail to fully eliminate this attack surface. Our analysis reveals 35 enclave interface sanitization vulnerabilities in 8 major open-source shielding frameworks for Intel SGX, RISC-V, and Sancus TEEs. We practically exploit these vulnerabilities in several attack scenarios to leak secret keys from the enclave or enable remote code reuse. We have responsibly disclosed our findings, leading to 5 designated CVE records and numerous security patches in the vulnerable open-source projects, including the Intel SGX-SDK, Microsoft Open Enclave, Google Asylo, and the Rust compiler.