The transformative potential of deep learning in enhancing computer science solutions has not gone unnoticed in the fields of security and privacy. However, the sheer volume of related scientific literature and the significant gap between a lab context and real-world environments make it extremely challenging to assess the current progress in the area. In this talk, I will review underlying mechanisms and main principles behind deep learning when applied to offensive and defensive cybersecurity solutions. I will focus on two primary use cases: traffic analysis attacks on Tor and network-based intrusion detection systems, analyzing the expected benefits and potential pitfalls of using deep learning. This analysis effectively challenges the common perception of a purely end-to-end approach. To that end, the presentation emphasizes the importance of explainability and error analysis for validating and troubleshooting deep neural networks. This discussion is meant to equip cybersecurity researchers and practitioners to begin incorporating deep learning in their toolbox while maintaining a critical and holistic perspective.
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.
In the Internet of Things era, edge devices have been considerably diversified and are often designed using high level synthesis (HLS), which translates behavioral descriptions into hardware descriptions, for improved design productivity. However, HLS tools were originally developed in a security-unaware manner, resulting in vulnerabilities to side-channel attacks. In our recent work that was published at ACM Trans. on Embedded Computing Systems, we integrated side-channel security in the state-of-the-art high-level-synthesis-based hardware design flow, leveraging a provably countermeasure called the threshold implementation. As case studies for lightweight block ciphers composed of addition/rotation/XOR (ARX)-based permutations, our evaluation using an FPGA board demonstrated that our proposed method can successfully improve the side-channel security for all ARX-based ciphers used as benchmarks.
Smart contracts are distributed applications, which govern financial assets in cryptocurrencies such as Ethereum and, hence, can implement advanced financial instruments, such as decentralized exchanges or autonomous organizations (DAOs). In this talk, I will overview our advances in developing static analyzers that come with provable guarantees. I will first show how to define generic security properties that characterize the absence of prominent attack classes (such as reentrancy or transaction order dependence) and then discuss different forms of static analysis that can prove these properties and that can be efficiently implemented to analyze real-world smart contracts.
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.
The Tor anonymous communication system helps millions of users every day to use the Internet more safely, protecting their identity, blocking tracking, and in some cases circumventing censorship. Since its creation in 2005, the Tor Project has worked to enhance the usability and security of Tor, bringing it from a research prototype with a handful of users to an easy-to-use modern application today. In this talk, I’ll discuss the research challenges that had to be addressed during this journey and open research questions that remain, including on usability, traffic-analysis resistance, ethical considerations, and post-quantum cryptography.
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, 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.