TLDR Tech / InfoSec
Attested TLS Was Supposed to Be the Last Trust Boundary. It Isn't. Formal Methods Show How
Researchers at TU Dresden used the symbolic verifier ProVerif to formally analyze seven attestation-to-TLS binding mechanisms shipping in Meta's WhatsApp Private Processing, Edgeless Systems' Contrast, and Cocos AI, and found all seven vulnerable to relay attacks (CVE-2026-33697, CVSS 7.5, CWE-322): an attacker holding the enclave's ephemeral TLS private key can present genuine attestation evidence to a client while terminating the session at their own relay point, passing every cryptographic check while encrypting to the wrong endpoint. Exploitation still requires extracting that key via physical hardware compromise, the same access class as wiretap.fail and TEE.fail, since none of the seven mechanisms bind evidence to application traffic or include a timing/liveness check to rule out relay. Vendors evaluating attested TLS should confirm binding extends to the client's application traffic key rather than just a handshake key or nonce, treat vendor-commissioned manual audits (Trail of Bits' review of the Meta system missed this) as insufficient without formal verification, and track the IETF TLS/RATS/SEAT/LAKE working groups' review of the paper's proposed level-2 mitigation.
Read the full story