Confidential Computing (CC) using hardware-based Trusted Execution Environments (TEEs) has emerged as a promising solution for protecting sensitive data in all forms. One of the fundamental characteristics of such TEEs is remote attestation which provides mechanisms for securely measuring and reporting the state of the remote platform and computing environment to a user. We present a novel approach combining TEE-agnostic attestation architecture and formal analysis enabling comprehensive and rigorous security analysis of attestation mechanisms in CC. We demonstrate the application of our approach for three prominent industrial representatives, namely Arm Confidential Compute Architecture (CCA) in architecture lead solutions, Intel Trust Domain Extensions (TDX) in vendor solutions, and Secure CONtainer Environment (SCONE) in frameworks. For each of these solutions, we provide a comprehensive specification of all phases of the attestation mechanism in confidential computing, namely provisioning, initialization, and attestation protocol. Our approach reveals design and security issues in Intel TDX and…
The EasyCrypt proof assistant offers—in a single tool—the ability to reason about cryptographic security at various scales from primitives to protocols. However, this flexibility comes at a huge cost in usability. This talk will discuss insights gained through the recent formalisation of primitives (SHA-3, XMSS), constructions (KMS, crypto_box) and protocols (distance-bounding, AKE) and explore plans for improvements to the tool that would enable its use on larger protocols, and for the creation of beginner-friendly tutorial material that would enable it to be used more broadly.
A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif
ProVerif is a popular tool for the fully automatic analysis of security protocols, offering very good support to detect flaws or prove security. One exception is the case of protocols with global states such as counters, tables, or more generally, memory cells. ProVerif fails to analyse such protocols, due to its internal abstraction.
In the original paper of GSVerif, our key idea was to devise a generic transformation of the security properties queried to ProVerif. We proved the soundness of our transformation and implemented it into a front-end GSVerif. Our experiments showed that our front-end (combined with ProVerif) outperforms the few existing tools, both in terms of efficiency and protocol coverage. We successfully applied our tool to a dozen of protocols of the literature, yielding the first fully automatic proof of a security API and a payment protocol of the literature.
In the newest version of ProVerif, the generic transformations of GSVerif can be fully described in term of axioms, thus taking advantage of this new ProVerif feature.
In this talk, we will look at the (in)security of contactless payments made via mobile apps. These systems are a composition of the mobile app (e.g., Samsung Pay, Apple Pay) and their underlying payment protocols provided via the card registered within (e.g., Visa, Mastercard, etc.). One added complexity comes also from the various “modes” in which the apps operate; for instance, there is a standard mode as well as transit/travel mode, in which the user authentication (via fingerprint or Face-ID) on the mobile device is foregone in order to provide better usability when paying at a metro/train ticketing gate. Primarily, we show that we can abuse this usability feature of Apple Pay in Travel Mode when set up with a Visa card. The abuse results in a fraudulent payment without user-authentication, of any value, to any point-of-sale including points-of-sales what are not linked to transport companies. Also, we show that the same attack does not apply to Apple Pay with a Mastercard registered with it, or to Samsung Pay. We will explain the practical aspects of the attack, as well as some elements of formal security verification.