Recent & Upcoming Events

WebAssembly is a new low-level programming language designed with the goal to increase interoperability and security across the software ecosystem. The WebAssembly specification is defined by the World Wide Web Consortium, with a multitude of implementors, ranging from browsers to standalone runtimes.

In order to ensure adherence to the specification, some WebAssembly implementations use formally-verified interpreters as testing oracles. This thesis explores a novel approach to designing a formally-verified interpreter, by using an intrinsically-typed representation of the WebAssembly syntax.

This intrinsically-typed interpreter is implemented in the Lean 4 proof assistant, leveraging its functional-but-in-place features to achieve good performance without sacrificing functional purity.

It has been five years since the General Data Protection Regulation (GDPR) went into effect in the EU. Ever since, research has continued to show that the creators of online services find it difficult to implement the legal requirements of EU legislation into practice. They mainly resort to lengthy privacy policies and often deceptive cookie notices to ask users for their consent to data processing, rather than revise their own data processing practices and opt for approaches that collect less personal data. This comes to the detriment of service providers and users, who are both faced with decreased usability of websites, apps, and devices.

This talk investigates approaches to both understand the roadblocks that keep system creators and users from adopting a privacy-by-design mindset and to find ways to address them. This is ever more important in the light of new European platform regulations that intend to create boundaries for personalized advertising and introduce interoperability requirements, which in turn pose new opportunities to empower system creators and users alike to take control of users' privacy.

Microarchitectural optimizations, such as caches, or speculative out-of-order execution, play a crucial role for enhancing system performance. However, these optimizations also enable attacks that undermine software-enforced security policies. The conventional approach of constant-time programming, while widely adopted for safeguarding cryptographic implementations against microarchitectural attacks, has its limitations. From a security perspective, it relies on certain assumptions about the underlying hardware and, for instance, does not suffice to protect against Spectre attacks. In terms of performance, it imposes an additional overhead due to, among other things, control-flow linearization.

In this presentation, we introduce two novel hardware-software co-design solutions to address some of the shortcomings of constant-time programming. First, we present ProSpeCT, a generic formal processor model that guarantees that constant-time programs (under a non-speculative semantics) are free from Spectre attacks, while still enabling speculative out-of-order execution. Second, Architectural Mimicry, a novel ISA extension that provides dedicated hardware support for efficient control-flow balancing and linearization of secret-dependent branches. Both defenses have been implemented and evaluated on top of Proteus, an extensible RISC-V processor. To conclude, we will discuss some of the remaining challenges that still need to be addressed to achieve provable end-to-end security guarantees.

Contact discovery allows new users of a messaging service to find existing contacts that already use that service. Existing users are similarly informed of new users that join. Current contact discovery protocols allow the server to reconstruct the social graph (i.e. the graph describing who is a contact of who), which is a serious privacy issue, unless they use trusted hardware to prevent this. But even in the latter case, privacy is still at stake: anyone already on the service that has your number on their contact list gets notified that you joined. Even if you don’t know that person, or if it is an ex or former colleague that you long parted with and whose contact details you deleted long ago.

To solve this, we propose a mutual contact discovery protocol, that only allow users to discover each other when both are (still) in each other’s contact list. Mutual contact discovery has the additional advantage that it can be implemented in a more privacy friendly fashion (e.g. protecting the social graph from the server) than traditional, one-sided contact discovery, without necessarily relying on trusted hardware.

Block, Inc. (NYSE: SQ) is a global technology company with a focus on financial services. Made up of Square, Cash App, Spiral, TIDAL, and TBD, we build tools to help more people access the economy. Square helps sellers run and grow their businesses with its integrated ecosystem of commerce solutions, business software, and banking services. With Cash App, anyone can easily send, spend, or invest their money in stocks or Bitcoin. Spiral builds and funds free, open-source Bitcoin projects. Artists use TIDAL to help them succeed as entrepreneurs and connect more deeply with fans. TBD is building an open developer platform to make it easier to access Bitcoin and other blockchain technologies without having to go through an institution.

This session will cover my transition from academic security research at Northeastern’s Seclab into a role of industrial security engineering. We will dive into recent major infrastructure security projects at Block, such as a system to integrate acquisitions into the Block service mesh and bringing security infrastructure features from our Data Center and AWS EKS to AWS Lambda. Through these deep dives we will share how an academic background helps in industrial security engineering.

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 we will look at the protocol that allows two parties who know their locations on a Euclidean plane to check whether they are within distance R of each other or not. A distinguishing feature of this protocol is that it does not require the parties to communicate with each other directly and be online at the same time. We introduce a pair of servers to which one client may submit their data and go offline with the other client coming online later, finishing the protocol and fetching the matching result.

We build the protocols by combining existing off-the-shelf Cryptographic techniques. Interestingly, the protocol has better parameters (w.r.t. performance and security) than some of the hand-crafted protocols. So the importance of our protocol is in showing what can be achieved in this field “for free” using the generic techniques, and setting the bar for anyone who tries to make a “smarter” protocol for this problem in the future.

During the talk we will have an intro to how Multi-Party Computation protocols work, then show how our CatNap is built from them, and finally discuss the practical implications of this work.