arXiv subjects

Shale Xiong

Publications and source records attributed to Shale Xiong.

5 recordsLinked to original sources

arXiv2025

Careful Whisper: Attestation for peer-to-peer Confidential Computing networks

Trusted Execution Environments (TEEs) are designed to protect the privacy and integrity of data in use. They enable secure data processing and sharing in peer-to-peer networks, such as vehicular ad hoc networks of autonomous vehicles, without compromising confidentiality. In these networks, nodes must establish mutual trust to collaborate securely. TEEs can achieve this through remote attestation, where a prover presents evidence of its trustworthiness to a verifier, which then decides whether or not to trust the prover. However, a naive peer-to-peer attestation approach, where every TEE directly attests every other TEE, results in quadratic communication overhead. This is inefficient in dynamic environments, where nodes frequently join and leave the network. To address this, we present Careful Whisper, a gossip-based protocol that disseminates trust efficiently, reducing attestation overhead to linear complexity under ideal conditions. It enables interoperability by enabling transitive trust across heterogeneous networks, and supports trust establishment with offline nodes via relayed attestations. Using a custom discrete-event simulator, we show that Careful Whisper propagates trust both faster and more widely than naive approaches across various network topologies. Our results demonstrate that our protocol is resource efficient, sending ~21.5 KiB and requiring 0.158 seconds per round in a 200-node network, and that our protocol is resilient to attestation failures across various network topologies.

cs.CR↗

arXiv2024

Verifying components of Arm(R) Confidential Computing Architecture with ESBMC

Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA). Previous work applies formal techniques to verify the specification and prototype reference implementation of RMM. However, relying solely on a single verification tool may lead to the oversight of certain bugs or vulnerabilities. This paper discusses the application of ESBMC, a state-of-the-art Satisfiability Modulo Theories (SMT)-based software model checker, to further enhance RRM verification. We demonstrate ESBMC's ability to precisely parse the source code and identify specification failures within a reasonable time frame. Moreover, we propose potential improvements for ESBMC to enhance its efficiency for industry engineers. This work contributes to exploring the capabilities of formal verification techniques in real-world scenarios and suggests avenues for further improvements to better meet industrial verification needs.

cs.SE↗

arXiv2022

ALARM: Active LeArning of Rowhammer Mitigations

Rowhammer is a serious security problem of contemporary dynamic random-access memory (DRAM) where reads or writes of bits can flip other bits. DRAM manufacturers add mitigations, but don't disclose details, making it difficult for customers to evaluate their efficacy. We present a tool, based on active learning, that automatically infers parameter of Rowhammer mitigations against synthetic models of modern DRAM.

cs.CR↗

arXiv2022

Private delegated computations using strong isolation

Sensitive computations are now routinely delegated to third-parties. In response, Confidential Computing technologies are being introduced to microprocessors, offering a protected processing environment, which we generically call an isolate, providing confidentiality and integrity guarantees to code and data hosted within -- even in the face of a privileged attacker. Isolates, with an attestation protocol, permit remote third-parties to establish a trusted "beachhead" containing known code and data on an otherwise untrusted machine. Yet, the rise of these technologies introduces many new problems, including: how to ease provisioning of computations safely into isolates; how to develop distributed systems spanning multiple classes of isolate; and what to do about the billions of "legacy" devices without support for Confidential Computing? Tackling the problems above, we introduce Veracruz, a framework that eases the design and implementation of complex privacy-preserving, collaborative, delegated computations among a group of mutually mistrusting principals. Veracruz supports multiple isolation technologies and provides a common programming model and attestation protocol across all of them, smoothing deployment of delegated computations over supported technologies. We demonstrate Veracruz in operation, on private in-cloud object detection on encrypted video streaming from a video camera. In addition to supporting hardware-backed isolates -- like AWS Nitro Enclaves and Arm Confidential Computing Architecture Realms -- Veracruz also provides pragmatic "software isolates" on Armv8-A devices without hardware Confidential Computing capability, using the high-assurance seL4 microkernel and our IceCap framework.

cs.CR↗

arXiv2019

Data Consistency in Transactional Storage Systems: a Centralised Approach

We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. We provide operational definitions of consistency models for our key-value stores which are shown to be equivalent to the well-known declarative definitions of consistency model for execution graphs. We explore two immediate applications of our semantics: specific protocols of geo-replicated databases (e.g. COPS) and partitioned databases (e.g. Clock-SI) can be shown to be correct for a specific consistency model by embedding them in our centralised semantics; programs can be directly shown to have invariant properties such as robustness results against a weak consistency model.

cs.LO↗