Four papers by CSE researchers appearing at CCS 2023

Four papers by researchers in CSE are being presented at the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS), taking place November 26-30 in Copenhagen, Denmark. CCS is the flagship conference of the ACM Special Interest Group on Security, Audit, and Control (SIGSAC) and the leading international forum for new research in information security. Held annually, the conference seeks to bring together experts and practitioners from across the field to share the latest ideas, innovations, and findings.

The papers authored by CSE researchers that are appearing at the conference cover a range of topics related to computer security. This includes testing the resilience of Apple products’ security architecture, performing formal verification of low-trust architectures, exploring the efficacy of stateful defense models in warding off black-box attacks, and more.

The papers by U-M researchers being presented at CCS are as follows, with authors affiliated with CSE in bold:

“iLeakage: Browser-based Timerless Speculative Execution Attacks on Apple Devices”

Jason Kim, Stephan Van Schaik, Daniel Genkin, Yuval Yarom

Abstract: Over the past few years, the high-end CPU market has been undergoing a transformational change. Moving away from using x86 as the sole architecture for high performance devices, we have witnessed the introduction of computing devices with heavyweight Arm CPUs. Among these, perhaps the most influential was the introduction of Apple’s M-series architecture, aimed at completely replacing Intel CPUs in the Apple ecosystem. However, while significant effort has been invested analyzing x86 CPUs, the Apple ecosystem remains largely unexplored.

In this paper, we set out to investigate the resilience of the Apple ecosystem to speculative side-channel attacks. We first establish the basic toolkit needed for mounting side-channel attacks, such as the structure of caches and CPU speculation depth. We then tackle Apple’s degradation of the timer resolution in both native and browser-based code. Remarkably, we show that distinguishing cache misses from cache hits can be done without time measurements, replacing timing based primitives with timerless and architecture-agnostic counterparts based on race conditions. Finally, we use our distinguishing primitive to construct eviction sets and mount Spectre attacks, all while avoiding the use of timers.

We then evaluate Safari’s side-channel resilience. We bypass the compressed 35-bit addressing and the value poisoning countermeasures, creating a primitive that can speculatively read and leak any 64-bit address within Safari’s rendering process. Combining this with a new method for consolidating websites from different domains into the same renderer process, we demonstrate end-to-end attacks leaking sensitive information, such as passwords, inbox content, and locations from popular services such as Google.

“Security Verification of Low-Trust Architectures”

Qinhan Tan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik, and Todd Austin

Abstract: Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component. In this paper, we perform a complete formal verification of a specific low-trust

architecture, the Sequestered Encryption (SE) architecture, to show that the design is secure against direct data disclosures and digital side channels for all possible programs. We first define the security requirements of the ISA of SE low-trust architecture. Looking upwards, this ISA serves as an abstraction of the hardware for the software, and is used to show how any program comprising these instructions cannot leak information, including through digital side

channels. Looking downwards this ISA is a specification for the hardware, and is used to define the proof obligations for any RTL implementation arising from the ISA-level security requirements. These cover both functional and digital side-channel leakage. Next, we show how these proof obligations can be successfully discharged using commercial formal verification tools. We demonstrate the efficacy of our RTL security verification technique for seven different correct and buggy implementations of the SE architecture.

“Stateful Defenses for Machine Learning Models Are Not Yet Secure Against Black-box Attacks”

Ryan Feng, Ashish Hooda, Neal Mangaokar, Kassem Fawaz, Somesh Jha, Atul Prakash

Abstract: Recent work has proposed stateful defense models (SDMs) as a compelling strategy to defend against a black-box attacker who only has query access to the model, as is common for online machine learning platforms. Such stateful defenses aim to defend against black-box attacks by tracking the query history and detecting and rejecting queries that are “similar” and thus preventing black-box attacks from finding useful gradients and making progress towards

finding adversarial attacks within a reasonable query budget. Recent SDMs (e.g., Blacklight and PIHA) have shown remarkable success in defending against state-of-the-art black-box attacks. In this paper, we show that SDMs are highly vulnerable to a new class of adaptive black-box attacks. We propose a novel adaptive black-box attack strategy called Oracle-guided Adaptive Rejection Sampling (OARS) that involves two stages: (1) use initial query patterns to infer key properties about an SDM’s defense; and, (2) leverage those extracted properties to design subsequent query patterns to evade the SDM’s defense while making progress towards finding adversarial inputs. OARS is broadly applicable as an enhancement to existing black-box attacks – we show how to apply the strategy to enhance six common black-box attacks to be more effective against current class of SDMs. For example, OARS-enhanced versions of black-box attacks improved attack success rate against recent stateful defenses from almost 0% to almost 100% for multiple datasets within reasonable query budgets.

“ASMesh: Anonymous and Secure Messaging in Mesh Networks Using Stronger, Anonymous Double Ratchet”

Alexander Bienstock, Paul Rösler, Yi Tang

Abstract: The majority of secure messengers have single, centralized service providers that relay ciphertexts between users to enable asynchronous communication. However, in some scenarios such as mass protests in censored networks, relying on a centralized provider is

fatal. Mesh messengers attempt to solve this problem by building ad hoc networks in which user clients perform the ciphertext-relaying task. Yet, recent analyses of widely deployed mesh messengers discover severe security weaknesses (Albrecht et al. CT-RSA’21 &

USENIX Security’22).

To support the design of secure mesh messengers, we provide a new, more complete security model for mesh messaging. Our model captures forward and post-compromise security, as well as forward and post-compromise anonymity, both of which are especially important in this setting. We also identify novel, stronger confidentiality goals that can be achieved due to the special characteristics of mesh networks (e.g., delayed communication, distributed

network and adversary).

Finally, we develop a new protocol, called ASMesh, that provably satisfies these security goals. For this, we revisit Signal’s Double Ratchet and propose non-trivial enhancements. On top of that, we add a mechanism that provides forward and post-compromise anonymity. Thus, our protocol efficiently provides strong confidentiality and anonymity under past and future user corruptions. Most of our results are also applicable to traditional messaging. 

We prove security of our protocols and evaluate their performance in simulated mesh networks. Finally, we develop a proof of concept implementation.