Verify TDX lite ACPI tables against the declared VM shape

docs/security/security-model.md

@@ -282,30 +282,40 @@ For TDX evidence, the event log shipped alongside an attestation is stripped dow
 
 The reason boot-time event log entries are not the verifier contract is that downstream policy compares boot measurements directly to independently reproduced expected measurements. Keeping full boot event logs would bloat evidence and expose extra detail without adding verification capability. Application identity events, by contrast, include deployment-specific values such as compose-hash, key-provider, instance-id, and runtime events. Their event log is the data a verifier needs to prove what was extended into the application measurement lane.
 
-### Why TDX lite mode does not validate ACPI table contents
-
-TDX lite mode verifies the OS image without downloading the image and without
-running QEMU to regenerate ACPI tables. It still uses the three RTMR0 `ACPI
-DATA` digests from the attestation event log as measurement inputs. The guest
-labels those three events as `acpi-loader`, `acpi-rsdp`, and `acpi-tables`
-before exposing the event log, and the verifier checks that the recomputed RTMR
-values match the hardware-signed quote. What it does not do is reconstruct and
-byte-compare the full ACPI table contents.
-
-This is safe for dstack's threat model because ACPI tables are treated as
-untrusted host-provided platform description, not as trusted guest code. The
-dangerous executable part of ACPI is AML (ACPI Machine Language): malicious AML
-can try to use `SystemMemory` operation regions through the Linux ACPICA
-interpreter to read or write guest physical memory. dstack kernels include the
-BadAML sandbox patch (`0002-acpi-sandbox-block-aml-systemmemory-ram-access.patch`),
-which hooks the ACPI `SystemMemory` region handler, walks the guest page tables,
-and denies AML access to encrypted/private guest RAM. AML can only access
-unencrypted/shared mappings.
-
-Therefore, an infrastructure operator can still provide bad ACPI data and cause
-misconfiguration or denial of service, but unvalidated ACPI/AML cannot tamper
-with confidential private memory or extract secrets. That residual availability
-risk is already outside dstack's confidentiality/integrity guarantees.
+### Why ACPI table verification fails closed on both TDX paths
+
+RTMR0 covers the three ACPI blobs QEMU hands to OVMF (`acpi-loader`,
+`acpi-rsdp`, `acpi-tables`). Both TDX paths regenerate those blobs from the VM
+shape declared in `vm_config` and require the recomputed digests to equal the
+ones the event log reports, then rebuild the expected RTMR0 from the recomputed
+values — so the expected measurement depends on nothing the host asserted about
+the table contents.
+
+TDX lite mode did not always do this. It used to replay the three reported
+digests as measurement inputs, which made RTMR0 reconstruct consistently while
+leaving the table contents unconstrained. Regenerating them required running
+QEMU, which the lite path exists to avoid; once ACPI generation became a pure
+in-process Rust implementation, the reason for the exception disappeared.
+
+Verification is mandatory rather than a reported outcome because the inputs are
+host-declared. `swtpm` and `qemu_version` in `vm_config` are asserted by the
+untrusted host and are not independently constrained by any other measurement,
+so a verifier that accepted "could not generate" as a pass would let a host opt
+out of the check by declaring a shape the generator does not model. Both a
+digest mismatch and an unmodelable shape therefore reject the attestation. The
+practical consequence is that CVMs using the TPM key provider (`swtpm = true`)
+cannot be verified on either TDX path, which is what the full-image path
+already did.
+
+The guest-side mitigation remains in place as defense in depth. The dangerous
+executable part of ACPI is AML (ACPI Machine Language): malicious AML can try to
+use `SystemMemory` operation regions through the Linux ACPICA interpreter to
+read or write guest physical memory. dstack kernels include the BadAML sandbox
+patch (`0002-acpi-sandbox-block-aml-systemmemory-ram-access.patch`), which hooks
+the ACPI `SystemMemory` region handler, walks the guest page tables, and denies
+AML access to encrypted/private guest RAM. Verification now rejects tampered
+tables before the CVM is trusted with keys; the sandbox bounds what tampered
+AML could have done in the first place.
 
 ### TCB status is surfaced, not gated, during verification
 

dstack/dstack-mr/src/tdx.rs

@@ -62,8 +62,14 @@ fn validate_bytes_field(value: &[u8], field: &str, expected_len: usize) -> Resul
     Ok(value.to_vec())
 }
 
-fn select_mrtd(measurement: &TdxOsImageMeasurement, vm_config: &VmConfig) -> Result<Vec<u8>> {
-    let machine = crate::Machine::builder()
+/// Build the machine description the lite path measures against.
+///
+/// Only the VM-shape inputs matter here: the firmware, kernel and initrd paths
+/// stay empty because the lite path never reads image files, and the callers
+/// (MRTD candidate selection and ACPI table generation) only consume the QEMU
+/// topology knobs.
+fn machine_from_vm_config(vm_config: &VmConfig, ovmf_variant: OvmfVariant) -> crate::Machine<'_> {
+    crate::Machine::builder()
         .cpu_count(vm_config.cpu_count)
         .memory_size(vm_config.memory_size)
         .firmware("")
@@ -87,8 +93,34 @@ fn select_mrtd(measurement: &TdxOsImageMeasurement, vm_config: &VmConfig) -> Res
         .swtpm(vm_config.swtpm)
         .num_nvswitches(vm_config.num_nvswitches)
         .host_share_mode(vm_config.host_share_mode.clone())
-        .ovmf_variant(measurement.tdvf.ovmf_variant)
-        .build();
+        .ovmf_variant(ovmf_variant)
+        .build()
+}
+
+/// Recompute the three RTMR0 ACPI digests from the VM shape in `vm_config`.
+///
+/// The ACPI tables QEMU hands to OVMF depend only on the deployment topology
+/// (vCPU count, RAM size, PCI devices, QEMU version), never on the OS image, so
+/// they can be regenerated without downloading anything. The lite path
+/// otherwise replays the digests the guest reported in its event log, which
+/// makes those three RTMR0 entries self-consistent but unconstrained; comparing
+/// against these expected digests is what turns them into a verified value.
+pub fn expected_rtmr0_acpi_hashes(
+    vm_config: &VmConfig,
+    ovmf_variant: OvmfVariant,
+) -> Result<TdxRtmr0AcpiHashes> {
+    let tables = machine_from_vm_config(vm_config, ovmf_variant)
+        .build_tables()
+        .context("failed to generate expected ACPI tables")?;
+    Ok(TdxRtmr0AcpiHashes {
+        loader: measure_sha384(&tables.loader),
+        rsdp: measure_sha384(&tables.rsdp),
+        tables: measure_sha384(&tables.tables),
+    })
+}
+
+fn select_mrtd(measurement: &TdxOsImageMeasurement, vm_config: &VmConfig) -> Result<Vec<u8>> {
+    let machine = machine_from_vm_config(vm_config, measurement.tdvf.ovmf_variant);
     let opts = machine
         .versioned_options()
         .context("failed to resolve QEMU measurement options")?;

dstack/dstack-types/src/lib.rs

@@ -1350,8 +1350,9 @@ pub struct VmConfig {
     ///
     /// Its presence does not select lite verification: `tdx_attestation_variant`
     /// alone does. A `Legacy` boot is verified through the image download even
-    /// when this document is attached, because only that path verifies the ACPI
-    /// tables.
+    /// when this document is attached, because the two paths disagree on what
+    /// `os_image_hash` means and honoring the document would move a boot the
+    /// app pinned to `Legacy` onto the weaker image-identity check.
     #[serde(default, skip_serializing_if = "Option::is_none")]
     pub tdx_measurement: Option<TdxOsImageMeasurementDocument>,
     /// GCP TDX no-image-download measurement material. Present for GCP

dstack/verifier/README.md

@@ -253,10 +253,36 @@ The verifier performs the following verification steps:
    result as `app_info.os_image_hash_verified` (self-contained for all platforms
    except the TDX legacy full-image path, which reports `false`).
 
-`details.acpi_tables_verified` is `true` only for the full-image TDX path, where the verifier recomputes ACPI table contents and checks the resulting RTMRs against the quote. It is `false` for TDX lite, which uses the quote's named ACPI DATA digests without validating table contents, and for non-TDX platforms where ACPI table verification is not applicable.
+`details.acpi_tables_verified` is `true` for both TDX paths, which recompute the ACPI table contents and check them against the quote. It is `false` only for non-TDX platforms, where ACPI table verification is not applicable.
 
 All verification steps must pass for the verification to be considered valid.
 
+### TDX ACPI table verification
+
+RTMR0 covers three ACPI blobs QEMU hands to OVMF (`acpi-loader`, `acpi-rsdp`,
+`acpi-tables`); `acpi-tables` carries the DSDT, which is AML the guest kernel
+executes. Both TDX paths regenerate those blobs from the VM shape declared in
+`vm_config` (vCPU count, RAM size, PCI topology, QEMU version) and require the
+recomputed digests to equal the ones the quote's event log reports, before
+rebuilding the expected RTMR0 from the recomputed values.
+
+Verification fails closed in both directions:
+
+- **digest mismatch** — the tables are not the ones this VM shape produces.
+- **cannot generate** — the shape is one the ACPI generator does not model
+  (`swtpm = true`, or a QEMU older than 8.0). There is nothing to compare
+  against, so the attestation is rejected rather than accepted as unverified.
+
+The second case is deliberate. `swtpm` and `qemu_version` are host-declared
+fields that no other measurement independently constrains, so accepting an
+unverifiable shape would let a host opt out of the check by declaring one.
+CVMs using the TPM key provider (`swtpm = true`) therefore cannot be verified
+on either TDX path, which is the pre-existing behavior of the full-image path.
+
+QEMU versions newer than the newest ACPI profile the verifier models are
+generated with that profile, so a QEMU upgrade that leaves the ACPI ABI alone
+keeps verifying; one that changes it surfaces as a digest mismatch.
+
 ### Identifying the deployment
 
 Beyond pass/fail, the result carries a few descriptive fields so a relying party can apply its own policy:

dstack/verifier/fixtures/tdx-lite.README.md

@@ -3,8 +3,8 @@
 This fixture was captured from the local meta-dstack e2e stack using TDX
 `tdx_attestation_variant = "lite"`. It covers the KMS/verifier path that
 verifies the OS image from `vm_config.tdx_measurement` (`sha256sum.txt` bytes
-plus `measurement.tdx.cbor` bytes), without downloading the image and without
-running the QEMU ACPI table helper.
+plus `measurement.tdx.cbor` bytes), without downloading the image. The ACPI
+tables are regenerated in-process from the VM shape, so no QEMU is involved.
 
 Files:
 
@@ -61,6 +61,7 @@ dstack-verifier --config verifier-no-download.toml \
   --verify verifier/fixtures/tdx-lite-attestation.json
 ```
 
-Expected result: `Valid: true`, with quote, event log, and OS image hash all
-verified, and `ACPI tables verified: false` because lite mode does not validate
-ACPI table contents.
+Expected result: `Valid: true`, with quote, event log, OS image hash, and ACPI
+tables all verified. The ACPI digests are regenerated in-process from the
+fixture's VM shape (2 vCPUs, 2 GiB, QEMU 8.2.2) and must equal the ones the
+captured CVM reported.