Conceptio › Archive › arXiv CS
arXiv CSopen access

TPMSpy: Validation of Measured Boot Systems by Low-Level Tracing of TPM Usage

· arxiv_cs
arXiv CS · Papers · License: Open Access
Open Source ↗Direct PDF ↓
cryptographycybersecurityprivacysecurity
cryptography, security, privacy, cybersecurity

TPMSpy: Validation of Measured Boot Systems by Low-Level Tracing of TPM Usage Roman Lacko1

and Petr Švenda1

arXiv:2609.05011v1 [cs.CR] 4 Sep 2026

Masaryk University, Brno, Czechia

Abstract. Measured Boot extends trust in a booted system by recording cryptographic measurements of executed software and system state into a Trusted Platform Module (TPM), enabling subsequent verification through remote attestation. Although this mechanism is increasingly deployed in contemporary operating systems, its practical security depends on whether implementations measure the expected components under the expected conditions, yet this is not checked systematically. We propose a platform-agnostic method for analysing low-level TPM usage at the level of virtualized system–TPM interactions. It enables independent reconstruction and validation of the TPM Event Log without relying on the quoting mechanism itself. Because it does not depend on implementation details, it is applicable to both open and closed systems. We demonstrate the method on both Linux and Windows and conduct a systematic longitudinal analysis of Linux systems with systemd versions 245–258 (2020–2025), examining how Measured Boot usage evolved and observing wide divergence. No single usage pattern emerged amongst systems, warranting customized analysis. The analysis identifies undocumented behavioural changes, reveals inconsistent measurements of user-space systemd services, which prevent reliable remote attestation and LUKS disk decryption on such systems. Keywords: TPM · Measured Boot · systemd.

1

Introduction

Ensuring the boot integrity of a computing system is one element of an efficient defence against malware [39]. Firmware and bootloaders can be compromised to render the system inoperable, exfiltrate confidential information, or gain unrestricted access [42]. Two general approaches are used to address this: Verified Boot ensures only known components are allowed to run, while Measured Boot collects evidence in the form of the identities of executed components [32]. The collected evidence is then evaluated during remote attestation [15]. Especially on personal computers, the evidence is often used to unlock encrypted volumes automatically—BitLocker on Windows [34] and LUKS on Linux [2]. While Measured and Verified Boot, in principle, promise an effective defence against early-boot threats, their implementations evolve, and the behaviour of these mechanisms differs across vendors, versions, and configurations, necessitating a non-intrusive, scalable way to verify their properties as they evolve.

2

R. Lacko, P. Švenda

Common implementations of Verified and Measured Boot in PCs and servers utilize a Trusted Platform Module (TPM) [51], a secure coprocessor with tamperresistant key storage and dedicated measurement registers. Every boot component participating in Measured Boot measures the component that will be executed next in the chain. The measurements are passed to TPM, which incorporates them into the collected evidence using cryptographic hash functions, preventing a malicious component from erasing its own traces retrospectively. The appraisers request a copy of the registers signed by the TPM, called a TPM Quote. The system maintains a TPM Event Log that includes inputs and metadata for each measurement, which is intended to aid in interpreting the TPM Quote. While the correctness of the log can be verified by replaying the events and comparing the results with the evidence, a scalable and reliable method for verifying completeness (i.e., that all components were measured with matching events recorded in the log) is not yet available. Most boot components lack a precise description of their TPM usage, and directly observing TPM interactions to reconstruct independent evidence is technically challenging. Our paper aims to identify methods that allow this independent reconstruction. The systemd project [7] has been documenting its TPM utilization since version 248. Unlike other systems, which rarely disclose such details (notably Windows [36]), this allows for transparent development of attestation policies. Still, the documentation must match the behaviour, which aligns with the goal of this paper: verifying the completeness of the measurements. We investigate the following research questions: Research Questions RQ1: Can we independently reconstruct and validate the TPM Event Log sent with the signed TPM Quote without relying on the quoting mechanism? RQ2: Can we automatically assess how the Linux ecosystem built on systemd utilizes Measured Boot, and how it has evolved? RQ3: Do the uses of TPM Platform Configuration Registers (PCR) captured in RQ2 correspond to the documented behaviour of systemd? Contributions. To answer our research questions, we provide the following: 1. Survey of principal options for TPM usage tracing (Section 3). 2. Platform-agnostic and automatic method based on a virtualized system with a TPM, allowing to capture reads and writes between measured components and the TPM, and thus enabling the reconstruction and validation of the TPM Event Log (Section 3.3). 3. Systematic analysis of TPM access patterns of all major versions of systemdbased Linux distributions between 2020 (v245, before it had started to utilize TPM) and 2025 (v258) (Sections 4 and 5.1). 4. Detection and analysis of an inconsistency in the expected behaviour in TPM Event Log when measuring encrypted root volume, effectively rendering remote attestation ineffective for such setups (Section 5.2). All source code and experiment configurations are released under an opensource license at https://github.com/crocs-muni/tpmspy.

TPMSpy

2

3

Background: Protecting the Integrity of Boot Process

The firmware (BIOS or UEFI [52]) initializes the hardware and bootstraps the operating system [42]. The firmware can detect malfunctioning hardware and firmware, but it is not designed to detect malicious components, such as rootkits. Verified Boot and Measured Boot [17,42,46] are general mechanisms built on top of a secure hardware component to protect against these issues. 2.1

Verified and Measured Boot

Both methods rely on one or more Roots of Trust (RoT), trusted components (usually hardware) within the computer, with specific roles. The key difference is that while Verified Boot enforces a priori verification based on certified components, Measured Boot collects evidence and enables a posteriori verification by a remote party. Verified Boot or Secure Boot first executes the RoT, which validates signatures of firmware and its configuration against embedded keys or certificates [17,28,40,42]. A violation of this procedure usually halts the boot process and requires the administrator to investigate. In Measured Boot or Trusted Boot, multiple RoTs performing different roles exist. The RoT for Measurement starts by measuring itself, usually by hashing its own code [10,14,25,46,57]. The measurements are forwarded to the RoT for Reporting, which accumulates them using a cryptographic operation “extend” rather than storing them directly. The entire system is then measured iteratively: the currently running component must measure the next component before passing control [37,47]. This constructs a chain of measurements, also a chain of trust, that can be later inspected by a remote party during a remote attestation [15] by comparing the expected chain of hashes for the expected components. Based on the reported values, the party decides whether the system has reached a reliable state to perform sensitive tasks or is instead rejected and must be inspected. In principle, Measured Boot does not prevent malicious firmware and hardware from gaining control. However, if implemented correctly, the measurements of malicious components are also included in the collected evidence and cannot be retrospectively altered or erased without breaking the cryptographic properties imposed by the RoT. In practice, combinations of both methods can be deployed, such as Trusted Boot in Microsoft Windows [33], which builds on Verified Boot, but uses elements of Measured Boot during system initialization. 2.2

Measured Boot Based on Trusted Platform Module

The Trusted Platform Module (TPM) is a specification for trusted hardware designed by the Trusted Computing Group and currently at version 2.0. While it can serve as a generic secure coprocessor [51], this section focuses on aspects that the TPM provides for implementing Measured Boot. The secure component

4

R. Lacko, P. Švenda

implicitly trusted to measure itself reliably is called Core RoT for Measurement (CRTM), which passes these measurements to TPM. In turn, the TPM fulfils the role of RoT for Reporting, as it features 24 Platform Configuration Registers (PCRs) designed to securely collect and report the measurements. Components cannot write to the registers directly; instead, TPM exposes a PCR Extend operation, where a hash of the register’s previous value and the new measurement is stored in the register, i.e. PCR[n] ← h(PCR[n] || data). A single PCR is typically extended multiple times during a boot, accumulating contributions from several components assigned to the same register (Figure 1). When the measurements are finalized, a third party can request the values from PCR banks signed by the TPM’s private key, called a TPM Quote. The system maintains the TPM Event Log, which contains metadata for each measurement intended to aid interpretation of the TPM Quote. In theory, during remote attestation, the appraiser links the evidence [15,50]: 1. The Quote signed by a TPM, its certificate anchor is a trusted manufacturer. 2. The TPM Event Log records match the hash values of known components. 3. Simulation of the TPM Event Log yields the values in the TPM Quote. Unless the TPM’s private key is known to a malicious party, it should not be possible to craft a valid signature for a fabricated TPM Quote. The TPM Event Log then supports the collected evidence by explaining how the values were computed. Due to TPM’s memory limitations, the TPM Event Log is maintained by the system and must be handled carefully when passing execution context from the firmware to the operating system.

3

Methods for Analysing Measured Boot

To verify the validity of the TPM Event Log (our RQ1), it is necessary to provide independent evidence of the measurements recorded during system boot. The ideal method of capturing such evidence does not interfere with or interact with the processes running in the system, but can observe or validate all the interactions with the TPM. 3.1

Criteria for Method Selection

Measured Boot relies on Roots of Trust to record the measurements and hand them over when requested. The state reached by this process must follow from the TPM’s initial state and the measurements it received. Based on this observation, we devised four main criteria for selecting an appropriate method. The ideal method must observe the components performing the measurements, ideally during every stage of the boot process (Coverage). Once set up, the method should enable repeatable executions and facilitate quick validation of the measurements (Deployability). This targets practical use in development and Continuous Integration environments, where developers can validate that their changes align with expected behaviour.

TPMSpy

5

For the final properties, the method must not require modification of the observed system (Intrusive) or rely on its proper function (Independent). Such dependencies could compromise the method’s integrity when malicious components are present. We propose a method that observes the system in a virtualized environment, where communication with RoT is limited to a channel we can intercept and analyse. Platforms implementing Measured Boot on top of a Trusted Platform Module (TPM) fulfil our requirements. The properties and limitations of these approaches are discussed below, with summarization in Table 1. 3.2

Evaluated Methods for Measured Boot Analysis

In this section, we discuss five principal base approaches that can be utilized to observe the measurements: 1) TPM Event Log analysis, 2) formal verification of code, 3) hardware probes, 4) software probes, and 5) virtualization. TPM Event Log analysis is a baseline method for assessing the validity of measurements collected during the boot process and is already established as the core of remote attestation with TPM [15,50]. An appraiser obtains the TPM Quote, signed with the TPM’s private key, from the target system, along with the TPM Event Log. By simulating the events recorded in the log and comparing the results with the quote, the appraiser can verify the authenticity of the measurements. This approach is non-invasive and well established in practice, but does not address RQ1, as it does not provide evidence independent of the platform. It has been demonstrated that a malicious party can reset certain types of TPM without affecting the platform and re-measure parts of the system, thereby evading detection [24,55]. Furthermore, the log format accounts for constraints during early boot stages (such as memory and storage yet to be initialized) and limits the amount of metadata that can be stored. Any method that relies solely on the TPM Event Log inherits these constraints; therefore, an independent observation outside the mechanism is required. Formal verification can describe Measured Boot as a set of logical statements that can be used to validate the behaviour of the components participating in the boot process [22]. The approach works well for verifying runtime or security properties of components with explicitly and rigorously specified tasks, such as firmware and its interactions [41], CRTM [49], or bootloaders [21]. Furthermore, efforts are underway to extend verification to more complex software, including kernel drivers [13] and kernels themselves [12,29,38]. On the other hand, while methods for the formal analysis of every link in the boot chain exist [53,59], they are primarily limited to embedded systems, where the boot chain is comparatively smaller than that of PCs or servers. Analysis in more general settings is further complicated by the widespread use of hardware with closed-source firmware and by user-space services’ ability to participate in the boot process.

6

R. Lacko, P. Švenda

Therefore, formal verification is theoretically sufficient for answering RQ1, but applying it to the full boot chain of a general-purpose PC remains an unsolved problem.

Hardware probes are devices attached to an exposed data bus or power network that can observe or alter signals. This allows for analysing components’ behaviour directly (including TPM requests) [30] or revealing secret data or performing unintended operations [9]. Vulnerabilities in TPMs as physical, discrete chips (dTPMs) have been discovered by employing this method: an attacker can force-reset the TPM and reconstruct fabricated measurements that hide their presence [24,55,56] or bypass its security measures [58]. These attacks are not limited to dTPMs; TPMs running as firmware in the CPU’s trusted execution environment (fTPMs) can be attacked by manipulating the power network [26]. Furthermore, eavesdropping on dTPM communication packets on the data bus has been demonstrated [30]. Inexpensive, open-source probes designed for dTPMs already exist (e.g., TPM Genie [8]), allowing this method to be considered for dTPM chips at the very least. However, the method requires physical access to the system to attach such a probe to a bus. In the case of fTPMs, direct interaction with the system is required to inject faults and expose the TPM’s internal state. Finally, recent TPMs integrated into CPUs’ circuit boards (iTPMs), such as Microsoft Pluton [35], have a bus that is inaccessible without dismantling the chip casing, which is already a highly invasive and delicate process.

Software probes can intercept the data from measurement software before it is passed on to the TPM communication bus. Linux Kernel already provides several interfaces for tracing, notably function entry and exit probes [3], more general kernel instrumentation probes [4], and Berkeley Packet Filter subsystem [1]. While they are mainly designed for behaviour analysis, they can be utilized to detect malware [11,54]. Similar tracing mechanisms exist for Microsoft Windows [31,44], but are limited in scope since its source code is not disclosed. We will narrow this discussion to the Linux kernel, which provides an alternative option: operating systems expose abstract, high-level interfaces for communicating with devices via drivers. Their source code can be modified to intercept the measurements. The applicability of this approach breaks down with the components that execute before the kernel, as there is no such unifying interface. Additionally, the closed-source firmware prevents capturing measurements from the early stages of the boot. Even open-source early-boot firmware cannot be traced by kernel tracers and must be modified, which increases the complexity and volatility of this approach. Furthermore, such a method must rely on the system being rootkitfree, as malware running with elevated privileges could interfere with measurement capture. Ultimately, this method is feasible for measurements submitted by the kernel, but it falls short of reliably capturing early-boot measurements.

TPMSpy

7

Virtualization of both the system and TPM. The methods discussed so far are powerful but challenging to scale, automate, and interpret while minimizing interference with the observed system. Virtual TPMs (vTPMs) have been extensively researched since the advent of cloud computing, with the goal of providing a TPM instance for each guest, backed by real secure hardware [16,43,45], or of developing and testing TPM software [23]. In such a setup, the hypervisor mediates all communication between the virtual machine and the TPM backend, which is then fully observable from outside of the guest. Instead of a hardware TPM, the setup can be built on top of a software TPM (swTPM) [6,48]. This allows for independent observation of all TPM interactions, fulfilling the key requirement of RQ1, without altering the hardware or modifying the software. And since the measurements originate from the system rather than the TPM, the implementation differences between swTPM and real TPMs are out of scope for RQ1. This approach overall provides a better balance between independence and practicality than previous methods. Prior methods enable either the validation of specific components or the observation of TPM measurements as summarized in Table 1. Neither provides an independent, non-intrusive and scalable validation of the complete TPM Event Log. Virtualization provides most of the desired properties, except for the observation of the TPM behaviour, which we aim to fill in with this research. Method TPM Event Log Analysis Formal verification Hardware probes Software probes Virtualization

Independent Intrusive No Yes Yes No Yes

No No Yes Yes No

Coverage

Deployability

Full Isolated components Full Partial Full

High High Low Low High

Table 1: Summary of methods for analysing Measured Boot based on TPM. The properties (columns) are discussed in Section 3.1.

3.3

Technical Realization of TPM Measurement Tracing

This section describes a practical implementation of the independent TPM Event Log validation to answer RQ1, based on the previous discussion. The system consists of a virtualized platform and a separate software-emulated TPM. All TPM commands and responses in the guest are translated into messages passed between the hypervisor and TPM emulator processes. As discussed in the previous section, this approach already makes the validation non-intrusively independent of the configuration and software inside the virtual machine, guarantees complete observation of the boot process measurements, and can be deployed repeatably for any virtualized system. However, no existing tool applies this to validate the TPM Event Log.

8

R. Lacko, P. Švenda

The interaction between a virtualized system and a software-emulated TPM (swTPM) utilizes the following procedural steps: 1. swTPM exposes a communication channel, e.g. a UNIX socket. 2. When a guest system is started, the hypervisor connects to this channel. 3. TPM commands from the guest then appear on this channel as data flow. The second step enables interception by inserting a software interposer in place of the original swTPM channel, acting as a relay that can store, modify, or respond to passing messages (Figure 1). We implemented TPMSpy1 as a concrete implementation of this mechanism. As depicted in Figure 1, it sits on a channel between a guest running in QEMU [5] and a TPM emulator called swtpm2 [6]. In practice, the implementation is nontrivial: communication between QEMU and swTPM uses a two-stage protocol where a control channel dynamically negotiates a separate data channel for actual TPM commands, making a fixed-path relay insufficient. We considered patching swtpm or dynamically overriding a QEMU dispatcher function. However, both designs depend on the internal implementation of swtpm or QEMU and can break after updates. Therefore, we ultimately decided to create a helper program that relies on external behaviour: it impersonates swtpm and executes when QEMU sets up a new virtual machine. Then it starts the real swtpm daemon and TPMSpy, and sets up UNIX sockets so that TPMSpy’s socket is what QEMU actually connects to. Schema of measurement recording

Guest

PCR[0]

PCR[1]

PCR[2]

PCR[3]

h

h

h

h

Host swtpm

TPM

TPMSpy

CRTM

Platform Config

UEFI Code

UEFI Config

Platform

System

QEMU

Fig. 1: Schema of Measured Boot implemented with a software TPM. PCR banks (4 of 24 shown) reside inside the TPM and are extended only by hashing the input and the bank’s previous value (h). The operation starts with CRTM, which measures its configuration, passes control to UEFI, etc. In our setup, the Guest system is emulated by QEMU in the Host, except the TPM, which is emulated by swtpm. The PCR Extend command (represented by an upward arrow in Guest) is translated into data sent over a socket (represented by an upward arrow in Host) and intercepted by our TPMSpy component.

TPMSpy features a modular design in which the core handles connections and passes intercepted messages to plug-in modules. Message handling in the core 1 2

https://github.com/crocs-muni/tpmspy Here, swtpm is a concrete implementation of a software TPM (swTPM).

TPMSpy

9

is not trivial for two reasons. First, QEMU dynamically creates the TPM data channel and sends it over the control channel to the TPM daemon as an open file descriptor; a UNIX mechanism which allows processes to share resources. Second, QEMU expects the TPM daemon to handle new sessions as additional VMs are started. TPMSpy therefore manages one control and one data channel on each side per VM and must correctly label them for later correlation. Plug-in modules enable future extensions, such as capturing context within the VM or altering measurements to verify the sensitivity of remote attestation tools. Currently, the module wraps the captured messages with metadata (timestamps, channel identities, and ancillary messages to link related channels for analysis) and stores them in a file. Additionally, we developed scripts that connect to the VM via SSH and collect metadata relevant to answering RQ1 and RQ2: the TPM Event Log, and versions of the bootloader, kernel, and systemd. Another set of scripts facilitates analysis of collected data by generating graphs of PCR modifications over time and variance across multiple runs, and by comparing the TPM Event Log with the TPMSpy trace, flagging discrepancies.

4

Evaluation Methodology of systemd Measurements

This section describes a practical application of the method described in Section 3.3 to a Measured Boot performed by a widely-used systemd-based Linux OS. The goal is to describe a concrete system for which it is possible to formulate expectations about its use of TPM for the Measured Boot, and changes to this system that would result in observable changes in this behaviour. The next section will then compare and discuss the expected behaviour with the actual observations made by TPMSpy. Trusted Computing Group (TCG) reserves PCR 0–7 for the platform and PCR 8–15 for the operating system and services [51]. While we captured access to all PCRs, we primarily focused on analysing the behaviour of software that extends PCRs 8–15, based on the documented and inspectable behaviour of firmware and systemd. 4.1

Threat Model

We assume the host, the hypervisor, and swTPM are benign, as TPMSpy only aims to observe and analyse the communication between the virtualized system and swTPM. The method requires the hypervisor to reliably forward guest measurements to the swTPM, and for the latter to correctly process them. The observed guest system may be compromised, running malicious or undocumented components, or attempting to tamper with its measurements. Once the guest’s TPM Event Log is obtained, TPMSpy can detect discrepancies, such as dropped, added, reordered or modified events, between the TPM Event Log and the observed measurements, including those caused by TPM reset or re-measurement attacks. However, it cannot detect components that were never measured by the guest system, as such components do not produce an observable event.

10

4.2

R. Lacko, P. Švenda

Analysis of Firmware Behaviour

On a platform that follows the TCG’s recommendations, updating the firmware or modifying its configuration should result in different hash values being extended into PCRs 0 or 1. Similarly, a modification of the bootloader should result in a different value being extended to PCR 4. Hardware vendors typically use their own proprietary, closed-source firmware with no documentation on TPM use in Measured Boot. Virtualization hypervisors generally default to open-source firmware (e.g. QEMU uses SeaBIOS for legacy and TianoCore for UEFI boot [5]), but we are not aware of a precise documentation of their PCR utilization being provided either. This limits an experiment based on firmware modifications: we can only formulate the expected behaviour by observing at least one different value in PCR banks when comparing two different firmware versions. Beyond this and TCG’s recommended description, no further expectations can be stated without auditing the source code of each version of the considered firmware. For this reason, we capture PCR 0–7 and compare them with other runs to detect unexpected changes, but we leave the interpretation of these measurements outside the evaluation. 4.3

Analysis of systemd’s Documented Behaviour

In a Linux-based operating system, after the kernel is loaded, the first process, called init, is started. It is tasked with setting up services and the user environment. The systemd project is a well-known init daemon implementation featured in most major contemporary distributions, such as Ubuntu, Debian and Fedora. Since v248 was released in 2021, the systemd-cryptenroll’s documentation has maintained a table describing the use of PCR banks by the project’s components. The documentation also mentions other projects that extend PCRs, as it is intended to help system administrators choose PCRs to bind the volume decryption keys to. Compared to firmware behaviour, this allows us to formulate more detailed expectations; specifically, each version of systemd describes the set of PCRs it extends. To the best of our knowledge, no other Linux init daemon features Measured Boot based on a TPM. We reviewed major versions of systemd’s manual pages in man [7] and noted the changes that mention TPM or PCR in Table 2. All systemd services and userspace tools, except systemd-boot mentioned in Table 2, require a specific setup: the kernel image, parameters, and initial RAM file system must be bundled into a Unified Kernel Image (UKI) with systemd-stub. 4.4

Experimental Setups

Based on the above description, we prepared two experimental setups: one to capture the evolution of PCRs extended by each version of systemd, and the other to test optional features based on UKI and an encrypted root volume.

TPMSpy

11

systemd PCR Default Component v247 v248 v249 v250 v251

v252 v253 v254 ... v258

8 10 14 4 8 9 12 11 13 15 15

no documented use of TPM up to this version systemd-boot no changes Linux Kernel’s Integrity Measurement Architecture† (IMA) Shim†, a trivial UEFI loader systemd-stub if using system extension images GRUB†; systemd-boot stops extending this PCR Linux Kernel† initial RAM filesystem since 5.17 systemd-boot; to avoid conflict with GRUB [19] systemd-stub,pcrphase if using Unified Kernel Image (UKI) systemd-sysext if using extension images systemd-cryptsetup if configured for encrypted volumes systemd-pcrmachine,pcrfs@ if using UKI no changes since v254

Table 2: Measurements declared by systemd-cryptenroll documentation. The Default column indicates measurements that require no additional configuration when systemd-boot is the only bootloader. Components marked † are not part of systemd, but are included in the documentation.

For reproducible compilation of older versions of systemd, we chose NixOS as the Linux distribution. One disadvantage of NixOS is that the UKI support required by the user-space tools has only been available in NixOS since January 2024, over a year after systemd v252 was released in October 2022. It supports systemd-cryptsetup, but is still considered experimental and lacks some systemd measurement services, such as systemd-pcrmachine. Therefore we additionally set up and analyzed measurements from Ubuntu 24 LTS (v255), Fedora 41 (v256), 42 (v257) and 43 (v258). In summary of the expected behaviour: 1. Base Setup consists of NixOS with configurations locked to specific versions (called flakes) describing versions of systemd from v245 to v258. Only PCRs 8 and 9 are to be extended up to v250, and 9 and 12 since v251. Fedora and Ubuntu are installed with disk encryption enabled, but no specific PCR measurement is set up. The behaviour of systemd utilities should not differ from NixOS. 2. Encrypted Root Setup adds Unified Kernel Image (UKI), which is a feature required by systemd-stub and user-space services to perform additional measurements. This setup also takes advantage of the encrypted root, where UKI and a kernel parameter are required for systemd-cryptsetup to measure the volume encryption key. We expect to see PCRs 11 and 15, in addition to PCRs 9 and 12, extended from the base setup in all experiments. The

12

R. Lacko, P. Švenda

documentation for v252 also suggests that we should expect more than one measurement in PCR 11 in NixOS.

PCR

≤247 248 15 14 13 12 11 10 9 8

249

250

251

Shim

systemd version 252 253 254

sd-cryptsetup 1

255

256

257

258

3 sd-pcr{fs@,machine}

sd-sysext

2 sd-{stub,pcrphase}

IMA Linux

sd-boot GRUB

Fig. 2: Use of PCRs as documented by systemd-cryptenroll. Green nodes represent measurements expected in all the experiments. Blue nodes are expected only in the experiments with UKI and disk encryption. Light nodes represent feature-dependent measurements that are disabled by default. A number in the node denotes that there are multiple tools utilizing the PCR. Unfilled paths represent measurements by projects that are not part of the systemd itself.

Figure 2 displays the evolution of PCR usage as documented by systemd. It also highlights measurements expected in the experiments. 4.5

Discussion of Expected Behaviour

Experimental setups are designed to enable automatic capture of multiple system images. In addition to verifying documented PCR usage, comparing captures of the same version can verify behaviour relevant for remote attestation: 1. The list of PCR extend commands in TPM Event Log must match the list in TPMSpy capture. 2. All captures of the same version must result in one set of PCR values. 3. The order of operations modifying PCRs must not differ. To illustrate the last point, if two commands extending the same PCR with different values are reordered, the resulting PCR will have a different hash and can be detected by comparing PCR banks. But if two consecutive commands targeting different PCRs get swapped in another capture, this will not affect PCR bank values. Comparing TPM Event Logs will reliably uncover this swap only if each boot component treats the PCR extension command and its TPM Event Log entry as atomic operations, i.e. both are guaranteed to finish before another measurement is started. TPMSpy does not rely on this requirement, as it intercepts the commands between the system and TPM, and comparing the captures will reliably uncover such swaps.

TPMSpy

5

13

Experimental Validation of systemd Interactions

We collected measurements from 1,000 executions (boots) of the experimental setup using TPMSpy and systemd for each version, ranging from v245 to v258. We observed an agreement between the captured traces and the TPM Event Logs recovered from the systems. When systemd’s user-space tools (specifically systemd-cryptsetup) and Integrity Measurement Architecture (IMA) were enabled, we observed that their measurements were not recorded in the same TPM Event Log used by the platform, but in two distinct files. Comparing the captures with the documentation of systemd’s utilities, we identified undocumented measurements in systemd-boot prior to v248. 5.1

Setup 1: Evolution of PCR use by systemd

With the first setup, we captured measurements of systemd from v245 to v258 and compared them to the documentation analysed in Section 4.3. Figure 3 shows PCR Extend operations of systemd versions where significant changes in behaviour were observed. TPMSpy captures every measurement, including PCRs 0–7 used by low-level firmware components. However, they lack the detailed documentation required for the same level of analysis we performed for systemd; we only compare the measurements between runs to detect unexpected changes. The graphs show a discrepancy with the documented behaviour: v245 extends PCR 8 beyond the documented behaviour, which first appears in v248. The graph for v249 contains the same measurements and is omitted for brevity. According to the commit history in systemd’s GitHub, support for measuring the kernel command line was merged into systemd-boot in the commit 92ed3bb4, dated February 2016, and was released with systemd v230 unannounced [27]. It remained undocumented until v248, in which TPM is first mentioned in the changelog [18]. Still, if remote attestation were performed for these versions of systemd-boot, the appraisers would need to investigate the source of this measurement. In Figure 3b, systemd-boot switched from PCR 8 to PCR 12. The documentation for v251 also notes that, since version 5.17, the Linux Kernel has extended PCR 9; however, no such measurements are visible in this figure. This is because NixOS used Linux Kernel 5.15 until February 2023, when it switched to 6.1, and later that month included systemd v253. To analyse features unavailable in NixOS, we captured TPM Fedora 41–43 (v256–v258) (v258 shown in Figure 3d) and Ubuntu 24 LTS (v255 in Figure 4a). Instead of systemd-boot, these systems use Shim to verify and start GRUB, and thus we observe extensions to PCR 14 and PCR 8, as predicted by the analysis. Kernel images are not yet unified in these versions, so systemd’s userspace tools do not extend any registers. On the other hand, we observe IMA measurements in PCR 10, which are not present in the TPM Event Log. IMA can produce hundreds of measurements, which may exceed the limited memory reserved for the platform TPM Event Log, and are accessible as a virtual file in the kernel’s sysfs. Appraisers wishing to validate PCR 10 must be aware of this

14

R. Lacko, P. Švenda

and request the file along with the TPM Quote, or derive a set of acceptable values beforehand.

(a) NixOS, systemd v245

(b) NixOS, systemd v251

(c) NixOS, systemd v253

(d) Fedora 43, systemd v258

Fig. 3: PCR Extend operations captured by TPMSpy. Nodes denote PCR Extend commands in the TPMSpy capture; those with a corresponding TPM Event Log entry are green. In v245, the PCR 8 measurement (blue arrow) is undocumented behaviour expected since v248. In v251, systemd-boot moved to use PCR 12 (red arrow) instead of PCR 8 (red circle); Linux measurements in PCR 9 (the same red circle) are missing. In v253, Linux Kernel extends PCR 9 (red arrow). Fedora 43 features Shim by default in PCR 14 (blue arrow), GRUB in PCR 8, and IMA, which extends PCR 10 multiple times (red arrow).

To demonstrate the independence of the TPMSpy tool from the platform, we also captured Windows 11 with BitLocker (Figure 4b), where no equivalent documentation exists but a distinct pattern using PCR 11–14 is visible. We repeated experiment 1,000 times for each systemd version in NixOS. We compared the traces and metadata to verify the deterministic order of events, the absence of race conditions, and the absence of unexpected changes in measured values. To measure impact on system performance, we observed 10 runs of Fedora 43 (which has more features enabled than NixOS) from startup to systemd reporting readiness, taking 22.13 ± 1.26s. Without TPMSpy, the same setup took 23.77 ± 1.48s; the 1.64s is comparable to variability and thus not statistically significant. Direct resource measurements showed TPMSpy using only 40.073 ± 3.387ms of CPU time, confirming negligible overhead.

TPMSpy

5.2

15

Setup 2: Evaluation of Setup with Unified Kernel Image

In the second setup, we installed Unified Kernel Image and enabled LUKS volume key measurement. In the case of Fedora, we also replaced Shim and Grub with systemd-boot to enable user-space measurements.

(a) Ubuntu 24, systemd v255

(b) Windows 11, no systemd

(c) Fedora 43, v258, UKI

(d) LUKS volume key measurement

Fig. 4: Top: PCR Extend operations of systemd v255 in Ubuntu 24 (left) and Windows 11 (right). The documentation for Windows’ measurements is not specific enough to allow PCR analysis we performed for systemd, but it shows a distinct pattern (red arrows) not seen with systemd. Bottom: PCR extends on systemd v258 with Unified Kernel Image. Aside from IMA measurements, user-space utilities extend PCR 11 and PCR 15 (blue arrows). An earlier measurement to PCR 15 is missing in the default setting (left, red circle) but appears when enabled explicitly (right, red arrow).

Figure 4c shows Fedora 43 with v258, UKI and default kernel parameters. According to the documentation and Figure 2, PCRs 9, 11, 12, and 15 should be extended. Early measurements to PCR 11 (green nodes) accounted for by TPMSpy and TPM Event Log are issued by systemd-stub, which measures parts of the kernel and the initial file system. Later PCR 11 measurements are submitted by systemd-pcrphase and are not recorded in the TPM Event Log. PCR 12 measurements of the kernel command by systemd-boot are missing. There is one PCR 15 measurement by systemd-pcrmachine, though the documentation suggests that systemd-pcrfs should have submitted measurements as well. In Figure 4d, we enabled the kernel parameter for systemd-cryptsetup to extend PCR 15 with the encrypted volume key. This time, the measurement was detected by TPMSpy but not recorded in the TPM Event Log.

16

R. Lacko, P. Švenda

The v255 changelog announces that user-space measurements from systemd are logged into /run/log/systemd/tpm2-measure.log, and that these measurements were previously logged to the journal only [20]. The TPM Event Log alone is thus insufficient for remote attestation: PCR 11 (v252), PCR 15 (v253–v254) and PCR 10 (IMA) measurements appear in specific files only. In this case, TPMSpy provides a comprehensive set of observations in a single capture, enabling the system developer to trace all event logs stored in the system and document them for appraisers.

6

Conclusion

In this paper, we propose a novel methodology for the independent verification of the TPM Event Log based on virtualization. We designed and implemented TPMSpy, a virtual TPM interposer, which observes the complete communication between a virtual system and a software TPM emulator. Other available methods either require specialized hardware, focus on specific parts of the boot process, or verify shorter boot chains. In contrast, our method enables repeated, automated, and non-intrusive assessment for every stage of the boot process, independent of the system, as demonstrated by capturing runs of NixOS, Fedora, Ubuntu and Windows. It thus allows for the systematic evaluation of Measured Boot on any platform that features a TPM, including those without available source code. We observed an increasing use of PCR over time, which agreed with the documentation in most cases. We also observed deviations from expected behaviour for systemd user-space services and IMA, which store their measurement metadata outside the TPM Event Log. This deviation affects remote attestation: an appraiser unaware of these locations will fail to attest to the measured values. Our method enables the independent observation of TPM commands and responses, providing complete coverage of TPM interactions during boot. The strict independence from the observed system limits available context: currently, only timestamps and channel metadata are recorded along with the captured events. Future research may address this limitation by querying the virtual machine’s state at the time of event capture and, ideally, precisely identifying the component that originated the event. Furthermore, the method verifies TPM Event Log completeness but does not replace formal verification, as it cannot guarantee that every component executed during boot was measured. The absence of a specific measurement will not cause a discrepancy between the TPM Quote and the TPM Event Log, and thus cannot be detected solely by our method. Future research can address this limitation by deriving expectations from static code analysis or by verifying that every piece of code loaded into memory is measured, as wide divergence warrants systematic analysis. Acknowledgments. The authors of this paper were supported by the EU project CHESS #101087529. Disclosure of Interests. The authors have no competing interests to declare that are relevant to the content of this article.

TPMSpy

17

References 1. BPF and XDP Reference Guide Cilium 1.19.0-dev documentation, https://docs. cilium.io/en/latest/reference-guides/bpf/index.html, accessed: 2025-12-31 2. Disk Encryption User Guide, https://docs.fedoraproject.org/en-US/quick-docs/ encrypting-drives-using-LUKS/, accessed: 2026-01-07 3. Fprobe - Function entry/exit probe The Linux Kernel documentation, https:// docs.kernel.org/trace/fprobe.html, accessed: 2025-12-31 4. Kernel Probes (Kprobes) The Linux Kernel documentation, https://docs.kernel. org/trace/kprobes.html, accessed: 2025-12-31 5. QEMU User Documentation QEMU documentation, https://www.qemu.org/ docs/master/system/qemu-manpage.html, accessed: 2025-12-29 6. swtpm (Dec 2025), https://github.com/stefanberger/swtpm 7. systemd (Dec 2025), https://github.com/systemd/systemd 8. TPMGenie (Dec 2025), https://github.com/nccgroup/TPMGenie 9. Anderson, R., Kuhn, M.: Tamper Resistance – a Cautionary Note. In: 2nd USENIX Workshop on Electronic Commerce (EC 96). USENIX Association, Oakland, CA (Nov 1996) 10. Berger, S., Goldman, K., Pendarakis, D., Safford, D., Valdez, E., Zohar, M.: Scalable Attestation: A Step Toward Secure and Trusted Clouds. In: 2015 IEEE International Conference on Cloud Engineering. pp. 185–194 (Mar 2015). https: //doi.org/10.1109/IC2E.2015.32 11. Caviglione, L., Mazurczyk, W., Repetto, M., Schaffhauser, A., Zuppelli, M.: Kernellevel tracing for detecting stegomalware and covert channels in Linux environments. Computer Networks 191, 108010 (May 2021). https://doi.org/10.1016/j.comnet. 2021.108010 12. Chen, X., Li, Z., Mesicek, L., Narayanan, V., Burtsev, A.: Atmosphere: Towards Practical Verified Kernels in Rust. In: Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification. pp. 9–17. KISV ’23, Association for Computing Machinery, New York, NY, USA (Oct 2023). https://doi.org/10.1145/3625275. 3625401 13. Chen, X., Li, Z., Zhang, J., Burtsev, A.: Veld: Verified Linux Drivers. In: Proceedings of the 2nd Workshop on Kernel Isolation, Safety and Verification. pp. 23–30. KISV ’24, Association for Computing Machinery, New York, NY, USA (Nov 2024). https://doi.org/10.1145/3698576.3698766 14. Chevalier, R., Cristalli, S., Hauser, C., Shoshitaishvili, Y., Wang, R., Kruegel, C., Vigna, G., Bruschi, D., Lanzi, A.: BootKeeper: Validating Software Integrity Properties on Boot Firmware Images. In: Proceedings of the Ninth ACM Conference on Data and Application Security and Privacy. pp. 315–325. ACM, Richardson Texas USA (Mar 2019). https://doi.org/10.1145/3292006.3300026 15. Coker, G., Guttman, J., Loscocco, P., Herzog, A., Millen, J., OHanlon, B., Ramsdell, J., Segall, A., Sheehy, J., Sniffen, B.: Principles of Remote Attestation. International Journal of Information Security 10(2), 63–81 (Jun 2011). https://doi.org/10.1007/s10207-011-0124-7 16. De Benedictis, M., Jacquin, L., Pedone, I., Atzeni, A., Lioy, A.: A novel architecture to virtualise a hardware-bound trusted platform module. Future Generation Computer Systems 150, 21–36 (Jan 2024). https://doi.org/10.1016/j.future.2023. 08.012 17. Dietrich, K., Winter, J.: Secure Boot Revisited. In: 2008 The 9th International Conference for Young Computer Scientists. pp. 2360–2365. IEEE, Hunan, China (Nov 2008). https://doi.org/10.1109/ICYCS.2008.535

18

R. Lacko, P. Švenda

18. Freedesktop.org: systemd 248 released (Mar 2021), https://lists.freedesktop.org/ archives/systemd-devel/2021-March/046289.html, accessed: 2025-11-24 19. Freedesktop.org: systemd 251 released (May 2022), https://lists.freedesktop.org/ archives/systemd-devel/2022-May/047976.html, accessed: 2025-11-24 20. Freedesktop.org: systemd 255 released (Dec 2023), https://lists.freedesktop.org/ archives/systemd-devel/2023-December/049745.html, accessed: 2025-11-24 21. Gordon, N., Weinhold, C.: Applying Modern Verification Techniques to a Rootof-Trust Bootloader. In: Proceedings of the 13th Workshop on Programming Languages and Operating Systems. pp. 34–41. PLOS ’25, Association for Computing Machinery, New York, NY, USA (Oct 2025). https://doi.org/10.1145/3764860. 3768324 22. Grimm, T., Lettnin, D., Hübner, M.: A Survey on Formal Verification Techniques for Safety-Critical Systems-on-Chip. Electronics 7(6), 81 (Jun 2018). https://doi. org/10.3390/electronics7060081 23. Haas, R., Pirker, M.: The State of Boot Integrity on Linux - a Brief Review. In: Proceedings of the 19th International Conference on Availability, Reliability and Security. pp. 1–6. ACM, Vienna Austria (Jul 2024). https://doi.org/10.1145/ 3664476.3670910 24. Han, S., Shin, W., Park, J.H., Kim, H.: A Bad Dream: Subverting Trusted Platform Module While You Are Sleeping. pp. 1229–1246 (2018) 25. Huang, C., Hou, C., Dai, H., Ding, Y., Fu, S., Ji, M.: Research on Linux Trusted Boot Method Based on Reverse Integrity Verification. Scientific Programming 2016, 1–12 (2016). https://doi.org/10.1155/2016/4516596 26. Jacob, H.N., Werling, C., Buhren, R., Seifert, J.P.: faulTPM: Exposing AMD fTPMs Deepest Secrets. In: 2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P). pp. 1128–1142 (Jul 2023). https://doi.org/10.1109/ EuroSP57164.2023.00069 27. Jdrzejewski-Szmek, Z.: systemd v230 (May 2016), https://lists.freedesktop.org/ archives/systemd-devel/2016-May/036583.html, accessed: 2025-12-29 28. Khalid, O., Rolfes, C., Ibing, A.: On Implementing Trusted Boot for Embedded Systems. In: 2013 IEEE International Symposium on Hardware-Oriented Security and Trust (HOST). pp. 75–80 (Jun 2013). https://doi.org/10.1109/HST.2013. 6581569 29. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. pp. 207–220. SOSP ’09, Association for Computing Machinery, New York, NY, USA (Oct 2009). https://doi.org/10.1145/1629575.1629596 30. Kursawe, K., Schellekens, D., Preneel, B.: Analyzing trusted platform communication. ECRYPT Workshop on Cryptographic Advances in Secure Hardware (CRASH) (2025) 31. Lanzi, A., Sharif, M., Lee, W.: K-Tracer: A System for Extracting Kernel Malware Behavior. Proceedings of Network and Distributed System Security Symposium (Feb 2009) 32. Ling, Z., Yan, H., Shao, X., Luo, J., Xu, Y., Pearson, B., Fu, X.: Secure boot, trusted boot and remote attestation for ARM TrustZone-based IoT Nodes. Journal of Systems Architecture 119, 102240 (Oct 2021). https://doi.org/10.1016/j.sysarc. 2021.102240

TPMSpy

19

33. Microsoft: Secure Boot and Trusted Boot (Jul 2024), https://learn.microsoft. com/en-us/windows/security/operating-system-security/system-security/ trusted-boot, accessed: 2025-01-15 34. Microsoft: BitLocker Overview (Jul 2025), https://learn.microsoft.com/en-us/ windows/security/operating-system-security/data-protection/bitlocker/, accessed: 2025-01-20 35. Microsoft: Microsoft Pluton as Trusted Platform Module (TPM 2.0) (Apr 2025), https://learn.microsoft.com/en-us/windows/security/hardware-security/pluton/ pluton-as-tpm, accessed: 2025-12-31 36. Microsoft: Understand PCR banks on TPM 2.0 devices (Aug 2025), https://learn.microsoft.com/en-us/windows/security/hardware-security/tpm/ switch-pcr-banks-on-tpm-2-0-devices, accessed: 2025-11-24 37. Mitchell, C., Institution of Electrical Engineers (eds.): Trusted Computing. No. 6 in IEE professional applications of computing series, Institution of Electrical Engineers, London (2005) 38. de Oliveira, D.B., Cucinotta, T., de Oliveira, R.S.: Efficient Formal Verification for the Linux Kernel. In: Software Engineering and Formal Methods. pp. 315– 332. Springer International Publishing, Cham (2019). https://doi.org/10.1007/ 978-3-030-30446-1_17 39. Parno, B., McCune, J.M., Perrig, A.: Bootstrapping Trust in Modern Computers, SpringerBriefs in Computer Science, vol. 10. Springer New York, New York, NY (2011). https://doi.org/10.1007/978-1-4614-1460-5 40. Profentzas, C., Günes, M., Nikolakopoulos, Y., Landsiedel, O., Almgren, M.: Performance of Secure Boot in Embedded Systems. In: 2019 15th International Conference on Distributed Computing in Sensor Systems (DCOSS). pp. 198–204 (May 2019). https://doi.org/10.1109/DCOSS.2019.00054 41. Ray, S., Ghosh, N., Masti, R.J., Kanuparthi, A., Fung, J.M.: Formal Verification of Security Critical Hardware-Firmware Interactions in Commercial SoCs. In: Proceedings of the 56th Annual Design Automation Conference 2019. pp. 1–4. DAC ’19, Association for Computing Machinery, New York, NY, USA (Jun 2019). https://doi.org/10.1145/3316781.3323478 42. Ruan, X.: Boot with Integrity, or Dont Boot. In: Platform Embedded Security Technology Revealed, pp. 143–163. Apress, Berkeley, CA (2014). https://doi.org/ 10.1007/978-1-4302-6572-6_6 43. Sadeghi, A.R., Stüble, C., Winandy, M.: Property-Based TPM Virtualization. In: Information Security. pp. 1–16. Springer, Berlin, Heidelberg (2008). https://doi. org/10.1007/978-3-540-85886-7_1 44. Shan, Z., Wang, X., Chiueh, T.c.: Tracer: enforcing mandatory access control in commodity OS with the support of light-weight intrusion detection and tracing. In: Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security. ASIACCS ’11, Association for Computing Machinery, New York, NY, USA (Mar 2011). https://doi.org/10.1145/1966913.1966932 45. Shi, Y., Zhao, B., Yu, Z., Zhang, H.: A security-improved scheme for virtual TPM based on KVM. Wuhan University Journal of Natural Sciences 20(6), 505–511 (Dec 2015). https://doi.org/10.1007/s11859-015-1126-5 46. Smith, D., Tomov, D., Oliver, I.: Boot with TPM: Secure vs Verified vs Measured (Jun 2024), https://github.com/tpm2dev/tpm.dev.tutorials/blob/master/ Boot-with-TPM/README.md, accessed: 2025-01-14 47. Smith, S.W.: Trusted Computing Platforms: Design and Applications. EBSCOhost eBook Collection, Springer, New York (2005)

20

R. Lacko, P. Švenda

48. Strasser, M., Stamer, H.: A Software-Based Trusted Platform Module Emulator. In: Trusted Computing - Challenges and Applications. pp. 33–47. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68979-9_3 49. Tao, Z., Rastogi, A., Gupta, N., Vaswani, K., Thakur, A.V.: DICE*: A Formally Verified Implementation of DICE Measured Boot. pp. 1091–1107 (2021) 50. TCG: TCG Guidance on Integrity Measurements and Event Log https://trustedcomputinggroup.org/resource/ Processing (Mar 2025), tcg-guidance-integrity-measurements-event-log-processing-v1-0-r131/ 51. TCG: Trusted Platform Module (TPM) (Mar 2025), https:// trustedcomputinggroup.org/work-groups/trusted-platform-module/ 52. UEFI Forum: Unified Extensible Firmware Interface (UEFI) Specification (Nov 2024) 53. Vasudevan, S., Ravi, P., Jati, A., Bhasin, S., Chattopadhyay, A.: Formal Verification of Secure Boot Process. In: 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE). pp. 1–6 (Mar 2024). https://doi.org/10.23919/ DATE58400.2024.10546576, iSSN: 1558-1101 54. Vurdelja, I., Blai, I., Nikoli, B.: Detection of Linux Malware Using System Tracers An Overview of Solutions. IcEtran (2020) 55. Winter, J., Dietrich, K.: A Hijackers Guide to the LPC Bus. In: Public Key Infrastructures, Services and Applications. pp. 176–193. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29804-2_12 56. Winter, J., Dietrich, K.: A Hijackers Guide to Communication Interfaces of the Trusted Platform Module. Computers & Mathematics with Applications 65(5), 748–761 (Mar 2013). https://doi.org/10.1016/j.camwa.2012.06.018 57. Yeluri, R., Castro-Leon, E.: Platform Boot Integrity: Foundation for Trusted Compute Pools. In: Building the Infrastructure for Cloud Security: A Solutions view, pp. 37–64. Apress, Berkeley, CA (2014). https://doi.org/10.1007/978-1-4302-6146-9_3 58. Yli-Mäyry, V., Perianin, T., Guilley, S.: Automated Search of Instructions Vulnerable to Fault Injection Attacks in Command Authorization Checks of a TPM 2.0 Implementation. In: 2024 Asian Hardware Oriented Security and Trust Symposium (AsianHOST). pp. 1–6 (Dec 2024). https://doi.org/10.1109/AsianHOST63913. 2024.10838483 59. Yuan, S., Talpin, J.P.: Verified functional programming of an IoT operating system’s bootloader. In: Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design. pp. 89–97. MEMOCODE ’21, Association for Computing Machinery, New York, NY, USA (Dec 2021). https://doi.org/10.1145/3487212.3487347

Record · ID 660747 · SHA-256 20c65e4edc7984b2
Retrieved via Conceptio — every document is proof-bundled with source, license, and retrieval metadata.