csstalk

Computer security research is on a long-running quest for a universal framework to reason about security properties. Such a framework ought to be expressive enough to capture any security policy conceived of, while also being independent of syntactic details and enforcement mechanisms, applicable to any system on which we may wish to impose security, and intuitive enough that humans can grasp the meaning of any given property (and not experience surprises due to a false sense of grasping). In this talk, I will present a framework based on modal logic which we have recently introduced in pursuit of these goals. In our approach, we combine established techniques for modal reasoning about knowledge with modalities of time and possible actions, and carefully distinguish between agents' capabilities and the effects we wish to permit them to achieve.

In this talk, Matteo Maffei will give an overview on this research line, illustrating how formal methods can positively impact browser and web security. He will initially exemplify how web security properties can be formalized and enforced, both in browsers and at the level of web specifications. He will then focus on WebSpec, a framework encompassing a formal model of the browser in Coq and a compiler turning Coq specifications into SMT-Lib formulas, thereby enabling the usage of off-the-shelf SMT solvers to automatically discover vulnerabilities and prove security properties. This line of research brings together formal methods and applied security in a cross-fertilizing feedback loop: vulnerabilities identified in the model are measured in the wild and large-scale evaluations often bring back new threat models that are then fed into the formal specification. This approach allowed us to identify a number of vulnerabilities in the specification and interaction of web components, and to identify fixes that we proved correct in our model.

Differential privacy is a formal model of privacy protection that has received sustained attention from the research community, whose work has shown that it is possible to reveal accurate information about a population while rigorously protecting the privacy of its constituents. While DP offers a compelling promise, organizations that choose to adopt it as their privacy standard face a number of challenges doing so.

Since the disclosure of Spectre attacks in 2018, both academia and industry have made considerable efforts to defend against all variants of transient execution attacks, the class of attacks to which Spectre belongs to. The first part of this presentation will be dedicated to discovering how these attacks change the way we reason about threat models in security. The second part of the presentation will introduce a new generic formal processor model - called ProSpeCT - to prevent transient execution attacks by construction. ProSpeCT has also been implemented on top of an open-source RISC-V processor and will be presented in Usenix Security 23 in a joint work with Lesly-Ann Daniel, Marton Bognar, Job Noorman, Sébastien Bardin, and Frank Piessens.

We formalize the simulation paradigm of cryptography in terms of category theory and show that protocols secure against abstract attacks form a symmetric monoidal category (≈ can be composed sequentially and in parallel). This gives an abstract model of composable security definitions in cryptography that is not tied to any particular machine model. Our model is able to incorporate computational security, set-up assumptions and various attack models such as colluding or independently acting subsets of adversaries in a modular, flexible fashion. We conclude by using string diagrams to rederive the security of the one-time pad and no-go results concerning the limits of bipartite and tripartite cryptography, ruling out e.g., composable commitments and broadcasting.

In this talk, I will give an overview of techniques to compile Sigma protocols—a popular class of interactive cryptographic proofs—to non-interactive proofs that guarantee security when used in any larger protocol context. The aim of the talk will be to provide an introduction to the area to system designers who typically use cryptographic tools as a black box, while also providing insight into some interesting technical subtleties that I uncovered in a recent work.

In this talk, Sofía will present FrodoPIR, a highly configurable, stateful, singleserver Private Information Retrieval (PIR) scheme that involves an offline phase that is completely client-independent.

In this talk, Raul will present a novel methodology to quantify and prevent privacy risks by focusing on polygenic scores and phenotypic information.

This seminar presents research on anonymous credentials with Publicly Auditable Privacy Revocation (PAPR). PAPR credentials simultaneously provide conditional user privacy and auditable privacy revocation for credential systems.

Felix will introduce PrePaMS, an efficient participation management system that supports prerequisite checks and reward procedures in a privacy-preserving way. By using a set of proven cryptographic primitives and mechanisms, participations are protected so that service providers and organizers cannot derive the identity of participants even within the reward process.