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.
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.