May 23

Add to Calendar 2024-05-23 12:00:00 2024-05-23 13:00:00 America/New_York Modular Verification of Non-Leakage for Hardware Security Modules with K2 K2 is a framework for proving that an implementation of a hardware security module (HSM) leaks nothing more than what is mandated by its functional specification. K2's proof covers the software and the hardware of an HSM, which enables it to catch all bugs above the cycle-level digital circuit abstraction, including timing side channels. K2's key contribution is a novel approach to proving non-leakage in a modular fashion, using transitive information-preserving refinement. This enables K2 to use different techniques for verifying different layers (software and hardware), reuse existing verified components, and largely automate several parts of the proof, while still providing a single top-to-bottom combined theorem. We use K2 to develop several HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of the OpenTitan Ibex and PicoRV32 processors. K2 provides a strong guarantee for these HSMs; for instance, it proves that the ECDSA-on-Ibex HSM implementation (2,300 lines of code and 13,500 lines of Verilog) leaks nothing more than what is allowed by a 50-line specification of its behavior. D463 (Star)

May 16

Add to Calendar 2024-05-16 12:00:00 2024-05-16 13:00:00 America/New_York Building principled and practical secure systems using Wasm In this talk I'm going to talk about our adventures (ab)using WebAssembly tobuild more secure systems. Wasm---at least in my view---is a secure compilationintermediate representation. It makes it possible for us to compile(potentially unsafe) code to a single IR, where we enforce different securityproperties, and compile this retrofitted code to native code, where it runssecurely (e.g., isolated from every other piece of code). I'll start with ourwork sandboxing third-party C libraries in Firefox, our work speeding up andverifying Wasm compilers and runtimes, and our most recent work designinghardware extensions (and abusing existing ones) to both speed up Wasm andaddress different classes of attacks on Wasm especially as used by hyperscalers. D463 (Star)

April 25

Add to Calendar 2024-04-25 12:00:00 2024-04-25 13:00:00 America/New_York Constrained Pseudorandom Functions from Weaker Assumptions In this talk, I will present a framework for constructing Constrained Pseudorandom Functions (CPRFs) with inner-product constraint predicates, using ideas from subtractive secret sharing and related-key-attack (RKA) security. I will show three instantiations of the framework:1. an adaptively-secure construction in the random oracle model;2. a selectively-secure construction under the DDH assumption; and3. a selectively-secure construction under the assumption that one-way functions exist.All three instantiations are constraint-hiding and support inner-product predicates, leading to the first constructions of such expressive CPRFs under each corresponding assumption. Moreover, while the OWF-based construction is primarily of theoretical interest, the random oracle and DDH-based constructions are concretely efficient, which is shown via an implementation. D-463 (Star)

April 11

Add to Calendar 2024-04-11 12:00:00 2024-04-11 13:00:00 America/New_York Recent Results on Threshold Signatures: Supporting Weights and Adaptive Security Threshold signatures protect the signing key by sharing it among a group of signers so that an adversary must corrupt a threshold number of signers to be able to forge signatures. In this talk, I will cover two of our recent results on threshold signatures. First, I will talk about how we design a weighted, non-interactive threshold signature scheme (https://eprint.iacr.org/2023/598). Existing threshold signatures with succinct signatures and constant verification times do not work if signers have different weights. We present a new approach to designing threshold signatures for pairing- and discrete logarithm-based cryptosystems. Our scheme supports arbitrary weight distributions among signers, arbitrary thresholds, and is concretely very efficient. Second, I will talk about the adaptive security of threshold signatures (https://eprint.iacr.org/2023/1553). A popular choice of threshold signature scheme is the BLS threshold signature introduced by Boldyreva (PKC'03). Some attractive properties of Boldyreva's threshold signature are that the signatures are unique and short, the signing process is non-interactive, and the verification process is identical to that of non-threshold BLS. These properties have resulted in its practical adoption in several decentralized systems. However, despite its popularity and wide adoption, up until recently, the Boldyreva scheme has been proven secure only against a static adversary. In this paper, we present the first adaptively secure threshold BLS signature scheme based on standard assumptions while retaining all of its existing properties. Bio:Sourav Das is a Ph.D. candidate at UIUC working with Prof. Ling Ren on applied cryptography and consensus algorithms. He is a recipient of the Chainlink Ph.D. Fellowship, a best paper runner's up at ACM CCS 2021, and the Mavis Future Faculty fellow at UIUC. He received his Bachelor's degree from IIT Delhi, where his thesis “Scaling smart contracts in Proof-of-work Blockchains" won the best undergraduate thesis award in the department. D-463 Star

April 04

Add to Calendar 2024-04-04 12:00:00 2024-04-04 13:00:00 America/New_York End-to-End Encrypted Group Chats with MLS: Design, Implementation and Verification Messaging Layer Security (MLS), currently undergoing standardization at the IETF, is an asynchronous group messaging protocol that aims to be efficient for large dynamic groups, while providing strong guarantees like forward secrecy (FS) and post-compromise security (PCS). While prior work on MLS has extensively studied its group key establishment component (called TreeKEM), many flaws in early designs of MLS have stemmed from its group integrity and authentication mechanisms that are not as well-understood.In this work, we identify and formalize TreeSync: a sub-protocol of MLS that specifies the shared group state, defines group management operations, and ensures consistency, integrity, and authentication for the group state across all members. We present a precise, executable, machine-checked formal specification of TreeSync, and show how it can be composed with other components to implement the full MLS protocol. Our specification is written in F* and serves as a reference implementation of MLS; it passes the RFC test vectors and is interoperable with other MLS implementations. Using the DY* symbolic protocol analysis framework, we formalize and prove the integrity and authentication guarantees of TreeSync, under minimal security assumptions on the rest of MLS.Our analysis identifies a new attack and we propose several changes that have been incorporated in the latest MLS draft. Ours is the first testable, machine-checked, formal specification for MLS, and should be of interest to both developers and researchers interested in this upcoming standard. G-882 Hewlett Room

March 21

Add to Calendar 2024-03-21 12:00:00 2024-03-21 13:00:00 America/New_York Extracting Secret Keys from a Device's Power LED Using COTS Video Cameras Over the past 25 years, research has highlighted the fact that high-end hardware can be used by attackers to recover secret keys from devices. Numerous studies have demonstrated innovative secret key extraction techniques that rely on dedicated professional equipment to capture data-dependent physical leakage from target devices. These methods employ equipment like scopes to obtain power traces, software-defined radio and probes to capture electromagnetic radiation (EMR) traces, as well as ultrasonic microphones to capture acoustic traces. While these methods have deepened our understanding regarding the cryptanalytic risks associated with various types of leakage (EMR, acoustic, power) and high-end sensors to secret keys, much less is known about the cryptanalytic risks posed by optical leakage and accessible ubiquitous equipment such as video cameras.In this talk, we will reveal the findings from the two research papers, optical cryptanalysis (CCS’23) and video-based cryptanalysis (SP’24), and discuss how attackers can extract cryptographic keys using video footage of a device’s power LEDs captured by standard video cameras. In the first part of the talk, we will review the history of the side-channel cryptanalytic attacks from the first timing attack that was published in 1996, through the cryptanalytic power-based attacks and cryptanalytic EMR attacks that were published since 1998 until the acoustic attack that was published at 2014 and conclude interesting insights regarding the lessons we learned from these works. Next, we will discuss information leakage from power LEDs (based on the findings presented at CCS 23), and understand why the intensity of the light emitted by a device’s power LED can be used as an alternative to power traces obtained from the device to recover secret keys (2048-bit RSA, 256-bit ECDSA and 378-bit SIKE keys) from commonly used cryptographic libraries (Libgcrypt, GnuPG, PQCryptoSIDH) using a photodiode. In the second part of the talk, we will discuss how standard video cameras (e.g., of an iPhone 13 PRO Max, and security camera) can be used as alternatives for the photodiodes (based on the findings presented at SP’24) to extract secret keys (256-bit ECDSA and 378-bit SIKE keys). We will discuss a video camera’s rolling shutter and understand how it can be used to increase the sampling rate of a video camera from the frame-per-second rate (60 measurements per second) to the rolling shutter rate (60,000 measurements per second). We will see videos of secret key recoveries that were taken by a smartphone and by an Internet-connected security camera to recover a 256-bit ECDSA key (using the Minerva side-channel attack) and a 378-SIKE key (using the HertzBleed side-channel attack). At the end of the talk, we will discuss countermeasures, and provide insights regarding the real potential of extracting cryptographic keys by video cameras in our days and in the near future, taking into account the expected improvements in the specifications of video cameras expected by Moore’s Law.

March 20

Add to Calendar 2024-03-20 15:00:00 2024-03-20 16:00:00 America/New_York Key Overwriting Attacks n this talk, I will formally define key overwriting attacks and discuss some recent applications.After lying dormant for 20 years, a recent series of papers exploited key overwriting attacks to break the security of deployed end-to-end encrypted schemes. More and more, systems aim to protect users even against a malicious or compromised server. Together with complex key hierarchies, this lead to attacks where the adversary can overwrite (part of) the key material of users. By observing the client's operation on such (partially) corrupted key material, some attacks were able to go as far as recovering the key material.This talk is based on "MEGA: Malleable Encryption Goes Awry" and "Caveat Implementor! Key Recovery Attacks on MEGA" but I will also touch on other key recovery attacks. G-882 Hewlett Room

March 14

Add to Calendar 2024-03-14 12:00:00 2024-03-14 13:00:00 America/New_York Confidential Computing and Trusted Execution Environment: Challenges, Opportunities, and the Future Confidential Computing, or Trusted Execution Environment (TEE), represents a cutting-edge security feature in advanced server CPUs. This technology provides a shield for cloud tasks, ensuring they are safeguarded against various threats, including attacks from privileged software, physical attackers, and even untrustworthy hypervisors. As the demand for secure private data handling surges, the adoption of Confidential Computing has become widespread across industries. This is evidenced by the adoption of TEE support in the latest server-grade CPUs from major vendors like Intel, AMD, and ARM. Furthermore, leading cloud service providers, such as AWS, Google Cloud, Microsoft Azure, and IBM Cloud, now offer commercial Confidential Computing services. However, despite its increasing popularity, Confidential Computing still faces significant design and security challenges. These include finding the right balance between maintaining strong security and achieving efficient performance, as well as the need to reassess and possibly rebuild the kernel space or hypervisor, which may not be fully trustworthy.In this talk, I will delve into the design intricacies and potential vulnerabilities associated with Confidential Computing. I will start by discussing the ciphertext side-channel attack, which arises from compromising security for performance. This type of attack can lead to the exposure of execution states or the decryption of sensitive information, even enabling attackers to extract private keys from secure implementations like RSA and ECDSA in the latest OpenSSL library.Following this, I will discuss the CROSSLINE attack, which shows the dangers of not properly redesigning untrusted hypervisors. This attack exploits the unprotected management of resources like address space identifiers (ASID), threatening the security of confidential VMs protected by AMD Secure Encrypted Virtualization (SEV). This highlights the urgency of reevaluating the role of hypervisors in Confidential Computing. To conclude, I will outline ongoing efforts and future directions in enhancing the security and effectiveness of Confidential Computing, emphasizing the importance of addressing these vulnerabilities and design challenges to advance the field.

March 07

Add to Calendar 2024-03-07 12:00:00 2024-03-07 13:00:00 America/New_York Designing protocols that actually get deployed Designing good Internet protocols is hard. Designing protocols that actually get deployed is harder. We take a look at some protocols that have been widely deployed (e.g., TLS 1.3, QUIC, and the WebPKI), and some others which have been less so (e.g., IPsec, SCTP, and DNSSEC/DANE) and draw some lessons about the factors that lead to protocol success and failure.BioEric Rescorla has contributed extensively to many of the core security protocols used in the Internet, including TLS, DTLS, WebRTC, ACME, and QUIC. He was editor of the TLS 1.3 protocol, which secures the vast majority of Web traffic and co-founder of Let's Encrypt, a free and automated certificate authority that is now the largest on the Internet. He is the former Chief Technology Officer for Firefox and Internet Platform at Mozilla, where he was responsible for setting the overall technical strategy for the Firefox browser and Mozilla's participation in Internet standards and global policy. Star D463

February 29

Add to Calendar 2024-02-29 12:00:00 2024-02-29 13:00:00 America/New_York Cryptographic theory into applied technology Translating cryptographic theories into applied technologies is a complex process that requires both deep theoretical knowledge and practical insight. In this talk, Nick Sullivan, a cryptography industry veteran, will offer an insider’s view on some of the most significant cryptographic implementations of recent times. From his contributions to Apple's FairPlay system, which uses encryption for multimedia content protection, to leading the charge in securing web communications with TLS 1.3 and QUIC, to steering the post-quantum cryptography transition through industry standards, Sullivan's experiences cover a broad spectrum. This presentation will outline the real-world challenges and solutions encountered in applying cryptography, highlighting the research, development, and collaborative deployment cycle that Sullivan has experienced in his career. Through this lens, this talk hopes to offer insights into the critical role of applied cryptography in contemporary digital infrastructure, reflecting on both its technical intricacies and its broad impact on global security and privacy.nicholas.sullivan@gmail.com G-882, Hewlett Rm.

February 22

Add to Calendar 2024-02-22 12:00:00 2024-02-22 13:00:00 America/New_York Reef: Fast Succinct Non-Interactive Zero-Knowledge Regex Proofs This talk will present Reef, a system for generating publicly verifiable succinct non-interactive zero-knowledge proofs that a committed document matches or does not match a regular expression. I’ll describe applications such as proving the strength of passwords, the provenance of email despite redactions, the validity of oblivious DNS queries, and the existence of mutations in DNA. Reef supports the Perl Compatible Regular Expression syntax, including wildcards, alternation, ranges, capture groups, Kleene star, negations, and lookarounds. Reef introduces a new type of automata, Skipping Alternating Finite Automata (SAFA), that skips irrelevant parts of a document when producing proofs without undermining soundness, and instantiates SAFA with a lookup argument. Our experimental evaluation confirms that Reef can generate proofs for documents with 32M characters; the proofs are small and cheap to verify (under a second).

February 15

Add to Calendar 2024-02-15 12:00:00 2024-02-15 13:00:00 America/New_York Approximate Lower Bound Arguments Suppose a prover, in possession of a large body of valuable evidence, wants to quickly convince a verifier by presenting only a small portion of the evidence.We define an Approximate Lower Bound Argument, or ALBA, which allows the prover to do just that: to succinctly prove knowledge of a large number of elements satisfying a predicate (or, more generally, elements of a sufficient total weight when a predicate is generalized to a weight function). The argument is approximate because there is a small gap between what the prover actually knows and what the verifier is convinced the prover knows. This gap enables very efficient schemes.We present noninteractive constructions of ALBA in the random oracle and uniform reference string models and show that our proof sizes are nearly optimal. We also show how our constructions can be made particularly communication-efficient when the evidence is distributed among multiple provers, which is of practical importance when ALBA is applied to a decentralized setting.We demonstrate two very different applications of ALBAs: for large-scale decentralized signatures and for proving universal composability of succinct proofs.Based on https://eprint.iacr.org/2023/1655. Joint work with Pyrros Chaidos, Aggelos Kiayias and Leonid Reyzin. 32 D463

December 13

Add to Calendar 2023-12-13 16:00:00 2023-12-13 17:00:00 America/New_York Characterizing and Optimizing End-to-End Systems for Private Inference In two-party machine learning prediction services, the client's goal is to query a remote server's trained machine learning model to perform neural network inference in some application domain. However, sensitive information can be obtained during this process by either the client or the server, leading to potential collection, unauthorized secondary use, and inappropriate access to personal information. These security concerns have given rise to Private Inference (PI), in which both the client's personal data and the server's trained model are kept confidential. State-of-the-art PI protocols consist of a pre-processing or offline phase and an online phase that combine several cryptographic primitives: Homomorphic Encryption (HE), Secret Sharing (SS), Garbled Circuits (GC), and Oblivious Transfer (OT). Despite the need and recent performance improvements, PI remains largely arcane today and is too slow for practical use.This paper addresses PI's shortcomings with a detailed characterization of a standard high-performance protocol to build foundational knowledge and intuition in the systems community. Our characterization pinpoints all sources of inefficiency -- compute, communication, and storage. In contrast to prior work, we consider inference request arrival rates rather than studying individual inferences in isolation and we find that the pre-processing phase cannot be ignored and is often incurred online as there is insufficient downtime to hide pre-compute latency. Finally, we leverage insights from our characterization and propose three optimizations to address the storage (Client-Garbler), computation (layer-parallel HE), and communication (wireless slot allocation) overheads. G-882, Hewlett Room

November 16

Add to Calendar 2023-11-16 16:00:00 2023-11-16 17:00:00 America/New_York Flamingo: Multi-Round Single-Server Secure Aggregation with Applications to Private Federated Learning In this talk I will discuss Flamingo, a system for secure aggregation of dataacross a large set of clients. In secure aggregation, a server sums up theprivate inputs of clients and obtains the result without learning anythingabout the individual inputs beyond what is implied by the final sum. Flamingoworks particularly well in the multi-round setting found in federated learningin which many consecutive additions (averages) of model weights are performedto derive a good model. Furthermore, Flamingo can tolerate the failure ofclients (e.g., clients that go offline) in the middle of the computation. Ourimplementation of Flamingo shows that it can securely train a neural network onthe (Extended) MNIST and CIFAR-100 datasets significantly quicker than allprior secure aggregation systems, and the model converges without a loss inaccuracy, compared to a non-private federated learning system. Star (D463)

November 10

Add to Calendar 2023-11-10 12:00:00 2023-11-10 13:00:00 America/New_York Unitary Complexity and the Uhlmann Transformation Problem State transformation problems such decoding noisy quantum channels or breaking quantum commitments are fundamental quantum tasks. However, their computational difficulty cannot easily be characterized using traditional complexity theory, which focuses on tasks with classical inputs and outputs. In this talk, I will discuss how the ``Uhlmann Transformation Problem’’, an algorithmic version of Uhlmann’s theorem, serves as a useful framework to study the complexity of state transformation tasks. I will mainly focus on cryptographic applications of the Uhlmann Transformation Problem, such as the task of breaking quantum commitment schemes and one-way state generators, and even falsifiable quantum cryptographic assumptions more generally.No quantum background required. This talk is based on recent joint work with John Bostanci, Yuval Efron, Tony Metger, Luowen Qian and Henry Yuen:https://arxiv.org/abs/2306.13073 G-882, Hewlett Room

November 01

October 06

Add to Calendar 2023-10-06 14:00:00 2023-10-06 17:00:00 America/New_York An Efficient Quantum Factoring Algorithm We show that n-bit integers can be factorized by independently running a quantum circuit with \tilde{O}(n^{3/2}) gates for \sqrt{n}+4 times, and then using polynomial-time classical post-processing. In contrast, Shor's algorithm requires circuits with \tilde{O}(n^2) gates. The correctness of our algorithm relies on a number-theoretic heuristic assumption reminiscent of those used in subexponential classical factorization algorithms. It is currently not clear if the algorithm can lead to improved physical implementations in practice.No background in quantum computation will be assumed.Based on the recent arXiv preprint: https://arxiv.org/abs/2308.06572Zoom Link https://mit.zoom.us/j/91806514236 Kiva, G-449

October 04

Add to Calendar 2023-10-04 16:00:00 2023-10-04 17:00:00 America/New_York Security of Computer Systems with Non-Computational Sensor Side Channels Side channels are unintentional information channels caused by shared resources in complex systems, often leading to the security risk of information leakage. While the embedded security community has investigated how to eliminate these channels in the computation space, the increasingly complex sensor hardware employed by emerging cyber-physical systems (CPS) creates new side channels that compromise both the integrity and confidentiality of data generated by sensor hardware. Such sensor side channels are challenging to prevent due to the undefined interactions between physical signals, sensor semiconductors, and downstream software. Using the example of camera sensing, my talk explains how to characterize the causality, limits, and mitigations of sensor side channels through physics modeling and lab experiments. I will first explain how camera images can not only leak sensitive unintended optical information, but also leak unintended room audio modulated in pixels. Then I will demonstrate how the electromagnetic leakage from smart home camera circuits allow eavesdroppers to reconstruct real-time, high-quality camera images even through walls. Besides developing defenses to confine the problems, I will also explain how sensor side channels can be leveraged to defend sensing applications. Finally, I will discuss my research vision for software-defined sensors that leverage signal processing and modeling to guide the synthesis of unintended sensor transduction—effectively creating new sensor modalities with unchanged hardware. This research appears in IEEE Symposium on Security and Privacy 2023 and Network and Distributed System Security Symposium 2024. 32-G575

September 29

Add to Calendar 2023-09-29 10:30:00 2023-09-29 12:00:00 America/New_York PAC Privacy: Automatic Privacy Measurement and Control of Data Processing In this talk, I will introduce a new privacy definition, termed Probably Approximately Correct (PAC) Privacy. PAC Privacy characterizes the information-theoretic hardness to recover sensitive data given arbitrary information disclosure/leakage during/after any processing. Unlike the classic cryptographic definition and Differential Privacy (DP), which consider the adversarial (input-independent) worst case, PAC Privacy is a simulatable metric that quantifies the instance-based impossibility of inference. A fully automatic analysis and proof generation framework are proposed: security parameters can be produced with arbitrarily high confidence via Monte-Carlo simulation for any black-box data processing oracle. This appealing automation property enables analysis of complicated data processing, where the worst-case proof in the classic privacy regime could be loose or even intractable. Moreover, we show that the produced PAC Privacy guarantees enjoy simple composition bounds and the automatic analysis framework can be implemented in an online fashion to analyze the composite PAC Privacy loss even under correlated randomness. On the utility side, the magnitude of (necessary) perturbation required in PAC Privacy is not lower bounded by Theta(\sqrt{d}) for a d-dimensional release but could be O(1) for many practical data processing tasks, which is in contrast to the input-independent worst-case information-theoretic lower bound. I will also talk about practical applications to complicated data processing, including end-to-end privacy analysis of deep learning and clustering. G-882, Hewlett Room

September 27

Add to Calendar 2023-09-27 16:00:00 2023-09-27 17:00:00 America/New_York K9db: Privacy-Compliant Storage For Web Applications By Construction Data privacy laws like the EU's GDPR grant users new rights, such as the right to request access to and deletion of their data. Manual compliance with these requests is error-prone and imposes costly burdens especially on smaller organizations, as non-compliance risks steep fines.K9db is a new, MySQL-compatible database that complies with privacy laws by construction. The key idea is to make the data ownership and sharing semantics explicit in the storage system. This requires K9db to capture and enforce applications' complex data ownership and sharing semantics, but in exchange simplifies privacy compliance. Using a small set of schema annotations, K9db infers storage organization, generates procedures for data retrieval and deletion, and reports compliance errors if an application risks violating the GDPR.Our K9db prototype successfully expresses the data sharing semantics of real web applications, and guides developers to getting privacy compliance right. K9db also matches or exceeds the performance of existing storage systems, at the cost of a modest increase in state size. G882