< Back

Attested TLS and Formalization

June 6, 3:10 PM - 3:30 PM
Grand Ballroom Salon B

Transport Layer Security (TLS) is a widely used protocol for secure channel establishment. However, it lacks any inherent mechanism for validating the security state of the workload and its platform. To address this, remote attestation can be integrated into TLS, named attested TLS. In this session, we present a survey of the three approaches for this integration, namely pre-handshake attestation, post-handshake attestation, and intra-handshake attestation. We also present our ongoing research on formal verification of the three approaches using the state-of-the-art symbolic security analysis tool ProVerif to provide high confidence for use in security-critical applications.

Key takeaways: Our preliminary analysis shows that pre-handshake attestation is potentially vulnerable to replay and relay attacks. On the other hand, post-handshake attestation results in high latency. Intra-handshake attestation offering high security via formal verification and low latency by avoiding the additional roundtrip forms a good ground for further research and analysis.

Technologies discussed in this session: Arm CCA.

About the speakers

Muhammad Usama Sardar

Research Associate, TU Dresden

Muhammad Usama is a Research Associate at TU Dresden, working for the Transregional Collaborative Research Centre 248 "Foundations of Perspicuous Software Systems" (CPEC) since October 2021. His current research focus is on the formal specification and verification of architecturally defined remote attestation for confidential computing, specifically Intel SGX, TDX, and Arm CCA. He leads the formal specification project in CCC Attestation SIG and contributes to various research networks, such as EuroProofNet (WG3), Méthodes formelles pour la sécurité, Internet Engineering Task Force (IETF) Remote ATtestation procedureS (RATS) WG and Trusted Execution Environment Provisioning (TEEP) WG, and Internet Research Task Force (IRTF) Usable Formal Methods Research Group (UFMRG).

Thomas Fossati

Principal Engineer, Linaro

Thomas is an engineer in the Linux Kernel WG at Linaro.