Attestable Builds: Compiling Verifiable Binaries on Untrusted Systems using Trusted Execution Environments
Daniel Hugenroth, Mario Lins, René Mayrhofer, Alastair Beresford
TL;DR
The paper tackles the challenge of verifying that a binary artifact was faithfully built from a given source snapshot in environments where the build pipeline is untrusted. It introduces Attestable Builds (A-Bs), a paradigm that uses modern TEEs and nested sandboxing to ensure integrity of the build process, while leveraging a transparent log to publish attestations and facilitate verification. The authors provide an architecture, threat model, and a formal verification (via Tamarin) showing security properties like code, asset, infrastructure, and repository integrity, and demonstrate practicality through a prototype built on AWS Nitro Enclaves with evaluation on diverse targets including LLVM Clang and the Linux kernel. They also show how A-Bs can compose with Reproducible Builds (R-Bs) to realize an anytrust model, discuss deployment considerations, and present case studies illustrating mitigations against real-world supply-chain attacks. Overall, A-Bs offer a pragmatic, scalable enhancement to software provenance and trust, enabling verification by downstream consumers even when the primary build infrastructure is untrusted.
Abstract
In this paper we present attestable builds, a new paradigm to provide strong source-to-binary correspondence in software artifacts. We tackle the challenge of opaque build pipelines that disconnect the trust between source code, which can be understood and audited, and the final binary artifact which is difficult to inspect. Our system uses modern trusted execution environments (TEEs) and sandboxed build containers to provide strong guarantees that a given artifact was correctly built from a specific source code snapshot. As such it complements existing approaches like reproducible builds which typically require time-intensive modifications to existing build configurations and dependencies, and require independent parties to continuously build and verify artifacts. In comparison, an attestable build requires only minimal changes to an existing project, and offers nearly instantaneous verification of the correspondence between a given binary and the source code and build pipeline used to construct it. We evaluate it by building open-source software libraries - focusing on projects which are important to the trust chain and have proven difficult to be built deterministically. The overhead (42 seconds start-up latency and 14% increase in build duration) is small in comparison to the overall build time. Importantly, our prototype can build complex projects such as LLVM Clang without requiring any modifications to their source code and build scripts. Finally, we formally model and verify the attestable build design to demonstrate its security against well-resourced adversaries.