The Spectre family of speculative execution attacks have required a rethinking of formal methods for security. Approaches based on operational speculative semantics have made initial inroads towards finding vulnerable code and validating defenses. However, with each new attack grows the amount of microarchitectural detail that has to be integrated into the underlying semantics. We propose an alternative, light-weight and axiomatic approach to specifying speculative semantics that relies on insights from memory models for concurrency. We use the CAT modeling language for memory consistency to specify execution models that capture speculative control flow, store-to-load forwarding, predictive store forwarding, and memory ordering machine clears. We present a bounded model checking framework parametrized by our speculative CAT models and evaluate its implementation against the state of the art. Due to the axiomatic approach, our models can be rapidly extended to allow our framework to detect new types of attacks and validate defenses against them.

Side-channel analysis is one of the main threats against software and hardware implementations of cryptographic algorithms. Among those attacks, the profiling attacks are some of the most powerful though they present some weaknesses such as, for example, the need for synchronization between different execution of the algorithm. Recent years saw the use of deep neural networks to try to solve those weaknesses. Our work focused on trying to better understand the networks and how they make their predictions. This presentation will introduce some key concepts on which this research is based and then focus on understanding and exploring several results stemming from this work. Those results include a new method of performing the profiling attacks as well as the design of a new loss function derived from the Learning to Rank approach of the field of machine learning.

Visibility relations have been proposed by Henzinger et al. as an abstraction for proving linearizability of concurrent algorithms that obtains modular and reusable proofs. This is in contrast to the customary approach based on exhibiting the algorithm's linearization points.

In this talk I will show how to apply visibility relations to develop modular proofs for three elegant concurrent snapshot algorithms of Jayanti. The proofs are divided by signatures into components of increasing level of abstraction; the components at higher abstraction levels are shared, i.e., they apply to all three algorithms simultaneously. Importantly, the interface properties mathematically capture Jayanti's original intuitions that have previously been given only informally.

We provide a simple and efficient in practice algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSpace-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ called structural FORQ induced by the Büchi automata to the right of the inclusion sign. The resulting implementation, called Forklift, almost always outperforms the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics.

Bitcoin and many other cryptocurrencies suffer from scalability issues. Payment Channel Networks (PCNs) are the most prominent approach to overcome these issues. The main idea is to reduce the transactions on the blockchain by establishing payment channels between users and allowing any two users connected via a path of channels to perform payments. PCN are already deployed in practice, e.g., the Lightning Network currently has 80k channels, 30k users and 200M USD locked. However, the current state-of-the-art in PCNs (i) is limited to payments, (ii) has security issues (i.e., wormhole attacks), (iii) is costly (i.e., funds are locked for a time proportional to the payment path length), (iv) is inefficient (i.e., it takes two rounds to complete payments) and (v) has a dependency on specific scripting language functionality (e.g., hash time lock contracts).

In this talk, I will show some recent protocols that overcome some of these challenges. I first present Blitz, a new multi-hop payment scheme that aims to improve on security and efficiency. Second, I present Donner, a Virtual Channel scheme that allows to connect any 2 endpoints in a PCN for the purpose of direct payments. Finally, I would shortly overview some of the open challenges in this setting.

Refinement types are a type-based, static verification technique designed to be practical. They enrich the types of an existing programming language with logical predicates to specify program properties and automatically validate these specifications using SMT solvers. Refinement types are a promising verification technology that in the last decade has spread to mainstream languages (e.g., Haskell, C, Ruby, Scala, and the ML-family) to verify sophisticated properties of real world applications, e.g., safety of cryptographic protocols, memory and resource usage, and web security. But, the weakness of refinement types is that they do not meet the soundness standards set by theorem provers.

In this talk, we will see a brief overview of refinement types, the consequences of their practical design, and the presenter's future goals on the establishment of soundness.

Private Message Detection (PMD) as a new cryptographic primitive has been identified lately. A PMD protocol aims to allow users to efficiently and privately detect and retrieve their recipient-anonymous messages from a public bulletin board or an untrusted server. Such protocols have promising applications in anonymous messaging (e.g., Signal, Niwl) and privacy-preserving payment systems (Zcash, Monero, stealth payments for Bitcoin, Ethereum, and other privacy-enhancing overlays). A private but inherently inefficient solution would be downloading all the ciphertexts from the bulletin board or the server. Afterwards, users try to decrypt each ciphertext, and eventually, they'll find all their pertinent messages. PMD protocols aim to improve the efficiency of this naive approach without sacrificing recipient anonymity. Very recently, three works have been published as pre-prints (Fuzzy Message Detection (FMD) by Beck et al. (CCS'21), Private Signaling by Madathil et al. (under submission), and Oblivious Message Retrieval by Liu and Tromer (under submission)) proposing efficient and private message detection schemes under various privacy and security assumptions.

In this talk, we will briefly introduce and describe the three proposed PMD schemes. We make a comparison of the schemes, highlighting interesting trade-offs between them. Subsequently, we will give a privacy and anonymity analysis of the Fuzzy Message Detection (FMD) scheme proposed by Beck et al. (CCS'21). We will show how FMD fails to provide information-theoretic privacy guarantees (recipient unlinkability and relationship anonymity) and how it achieves weak notions of differential privacy. We describe a game-theoretical analysis of the incentives underlying the FMD scheme. We report our simulation of the FMD scheme on real-world communication networks. Finally, we conclude with open questions and future directions in the PMD field.

Nowadays, computing platforms use a mix of different hardware technologies, as a way to scale application performance, resource capacities and achieve cost effectiveness. However, this heterogeneity, along with the greater irregularity in the behavior of emerging workloads, render existing resource management approaches ineffective. In the first part of this talk, I will describe how we can use machine learning methods at the operating system-level, in order to make smarter resource management decisions and speed up application performance. In the second part of the talk, I will present how we can accelerate certain components of such systems using visualization and computer vision methods. Finally, I will conclude with my vision of coupling machine learning and computer vision at the system-level and present open questions that make this research area exciting to work on!