CyLab faculty, students to present at ACM CCS 2023

Carnegie Mellon faculty and students will present on a wide range of topics at the Association for Computing Machinery Special Interest Group on Security, Audit and Control’s (SIGSAC’s) Conference on Computer and Communications Security (ACM CCS). Held at the Tivoli Congress Center in Copenhagen, Denmark on November 26-30, the event brings together information security researchers, practitioners, developers, and users from all over the world to explore cutting-edge ideas and results.

Lorrie Cranor, director of CyLab and professor in CMU’s Software and Societal Systems Public Policy departments, will serve as one of ACM CCS’s two keynote speakers, delivering a presentation on how her research has informed public policy discussions.

“I’ve worked with my students and colleagues to do research that directly informs policy issues, from providing empirical evidence to support password policy guidance to conducting user studies to inform the design of the new California privacy choice icon,” said Cranor. “I’m looking forward to sharing stories about our policy work with the CCS audience and hopefully inspiring them to do research with policy impact.”

Here, we’ve compiled a list of the papers and posters co-authored by CyLab Security and Privacy Institute members that are being presented at the event.

Papers

Galápagos: Developing Verified Low-Level Cryptography on Heterogeneous Hardware

Yi Zhou, Sydney Gibson, and Bryan Parno, Carnegie Mellon University; Sarah Cai, Databricks; Menucha Winchell, University of California, Berkeley

Abstract: The proliferation of new hardware designs makes it difficult to produce high-performance cryptographic implementations tailored at the assembly level to each platform, let alone to prove such implementations correct. Hence we introduce Galápagos, an extensible framework designed to reduce the effort of verifying cryptographic implementations across different ISAs. In Galápagos, a developer proves their high-level implementation strategy correct once and then bundles both strategy and proof into an abstract module. The module can then be instantiated and connected to each platform-specific implementation. Galápagos facilitates this connection by generically raising the abstraction of the targeted platforms, and via a collection of new verified libraries and tool improvements to help automate the proof process. We validate Galápagos via multiple verified cryptographic implementations across three starkly different platforms: a 256-bit special-purpose accelerator, a 16-bit minimal ISA (the MSP430), and a standard 32-bit RISC-V CPU. Our case studies are derived from a real-world use case, the OpenTitan security chip, which is deploying our verified cryptographic code at scale.

Riggs: Decentralized Sealed-Bid Auctions

Nirvan Tyagi, Cornell University; Arasu Arun and Joseph Bonneau, New York University; Cody Freitag, Cornell Tech; Riad Wahby, Carnegie Mellon University; David Mazières, Stanford University

Abstract: We introduce the first practical protocols for fully decentralized sealed-bid auctions using timed commitments. Timed commitments ensure that the auction is finalized fairly even if all participants drop out after posting bids or if 𝑛 − 1 bidders collude to try to learn the 𝑛th bidder’s bid value. Our protocols rely on a novel non-malleable timed commitment scheme which efficiently supports range proofs to establish that bidders have sufficient funds to cover a hidden bid value. This allows us to penalize users who abandon bids for exactly the bid value, while supporting simultaneous bidding in multiple auctions with a shared collateral pool. Our protocols are concretely efficient and we have implemented them in an Ethereum-compatible smart contract which automatically enforces payment and delivery of an auctioned digital asset.

Tainted Secure Multi-Execution to Restrict Attacker Influence

McKenna McCall and Limin Jia, Carnegie Mellon University; Abhishek Bichhawat, Indian Institute of Technology Gandhinagar

Abstract: Attackers can steal sensitive user information from web pages via third-party scripts. Prior work shows that secure multi-execution (SME) with declassification is useful for mitigating such attacks, but that attackers can leverage dynamic web features to declassify more than intended. The proposed solution of disallowing events from dynamic web elements to be declassified is too restrictive to be practical; websites that declassify events from dynamic elements cannot function correctly.

In this paper, we present SmeT, a new information flow monitor based on SME which uses taint tracking within each execution to remember what has been influenced by an attacker. The resulting monitor is more permissive than what was proposed by prior work and satisfies both knowledge- and influence-based definitions of security for confidentiality and integrity policies (respectively). We also show that robust declassification follows from our influence-based security condition, for free. Finally, we examine the performance impact of monitoring attacker influence with SME by implementing SmeT on top of Featherweight Firefox.

Posters

Mujaz: A Summarization-based Approach for Normalized Vulnerability Description

Hattan Althebeit and David Mohaisen, University of Central Florida; Brett Fazio, Two Sigma; William Chen, Carnegie Mellon University

WIP: Account ZK-Rollups from Sumcheck Arguments

Ray Fernando, Carnegie Mellon University; Arnab Roy, MystenLabs

Longitudinal Measurement of the Adoption Dynamics in Apple's Privacy Label Ecosystem