The number of online services, accounts, apps, and devices that we use is constantly increasing and so is the complexity of the interconnections between them. These interconnections have been exploited in targeted attacks that range from account takeovers to cryptocurrency theft. Protecting users from such attacks is difficult because each user’s account ecosystem is individual.
In this talk I will introduce account access graphs which are a formal model to represent a user’s account ecosystem, i.e., the collection of accounts, apps, and devices, as well as their interconnections. I will show examples of account access graphs from our user studies and present some of the insights we have gained from them. I will then discuss some of the challenges we must overcome in order to build an account management tool aimed at empowering users to better protect their individual account ecosystem.
This talk is based on joint work published at CCS 2019, CHI 2022 and carried out at ETH Zurich, the University of Dundee and Heriot-Watt University.
[Joint FM-SEC talk] The security protocol verifier ProVerif and its recent improvements: lemmas, induction, fast subsumption, and much more
ProVerif is a widely used automatic security protocol verifier that relies on symbolic model of cryptography. It can prove various security properties (secrecy, correspondences, some equivalences) for an unbounded number of sessions, as well as find attacks. In this talk, we will present an overview of ProVerif and its recent improvements. These improvements are twofold. First, we extended ProVerif with lemmas, axioms, proofs by induction, natural numbers, and temporal queries. These features not only extend the scope of ProVerif, but can also be used to improve its precision (that is, avoid false attacks) and make it terminate more often. Second, we reworked and optimized many of the algorithms used in ProVerif (generation of clauses, resolution, subsumption, …), resulting in impressive speed-ups on large examples. These improvements are joint work with Vincent Cheval and Véronique Cortier, to appear at IEEE Security and Privacy 2022. Joint talk with the FM-SEC network. Zoom…
The X.509 Public-Key Infrastructure (PKI) is one of the most prominent and widely used authentication mechanisms, which plays a crucial role in different applications such as secure communication (e.g., SSL/TLS, IPSec), software updates, and emails. Flaws in an X.509 PKI implementation can make an application relying on X.509 PKI susceptible to impersonation attacks or interoperability issues. In this talk, I will discuss my group’s effort in developing a high-assurance and specification-compliant implementation of X.509 PKI.
First, I will discuss the Symcerts system that uses domain-specific optimizations, symbolic execution, and differential analysis to automatically identify specification non-compliance in open-source SSL/TLS libraries. Second, I will discuss Morpheus, a black-box analysis engine, that automatically checks the logical correctness of RSA signature verification implementations in open-source SSL/TLS libraries through a formally verified oracle. Third, I will discuss my group’s effort to formalize and re-engineer the specification of the X.509 certificate chain validation using an executable specification. I will conclude my talk with a sneak peek of our ongoing work on developing a formally verified implementation of the X.509 PKI.
The Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. We present such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically,we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of existing countermeasures including constant time and serializing instructions.