Verify TDX lite ACPI tables against the declared VM shape - #1051

Depends on #1052 for the "QEMU newer than the newest profile" case; correct without it, just less forgiving of a QEMU upgrade.

Problem

RTMR0 covers three blobs QEMU hands to OVMF: acpi-loader, acpi-rsdp, acpi-tables. The full-image TDX path regenerates them and compares the resulting RTMR0 against the quote. The lite path cannot download the image, so it did something weaker (verify_os_image_hash_for_dstack_tdx_lite): it pulled those three digests out of the guest's event log and fed them straight back into the expected RTMR0 it rebuilds.

That is self-consistent but not a check. An untrusted host that pushes modified ACPI tables through fw_cfg gets OVMF to measure them faithfully, the guest reports the resulting digests faithfully, and the verifier rebuilds an expected RTMR0 from those same digests — so it matches by construction. acpi-tables carries the DSDT, i.e. AML the guest kernel executes, plus a table-loader command stream that tells OVMF where to patch guest memory. The rest of RTMR0 (TD HOB, CFV constants, SecureBoot variables, boot events) is pinned by measurement.tdx.cbor and vm_config; these three entries were the hole, and docs/security/security-model.md had a section explaining why it was left open.

The tables could not go into measurement.tdx.cbor: they depend on the deployment topology (vCPU count, RAM size, NIC/GPU/NVSwitch count, hugepages, QEMU version), which is unknown at image build time. Precomputing them host-side and shipping them in vm_config would be circular — the host would be handing the verifier the answer.

Fix

#1050 removed the reason the lite path skipped this: ACPI generation is now pure Rust, in-process, and needs no image bytes at all — only the VM shape, every field of which vm_config already carries. So the verifier derives the expected digests itself.

• dstack_mr::tdx::expected_rtmr0_acpi_hashes(vm_config, ovmf_variant) regenerates the three blobs and returns their SHA-384s, reusing the Machine construction that MRTD candidate selection already does (extracted as machine_from_vm_config).
• The lite path recomputes the digests, requires them to equal the reported ones, and rebuilds RTMR0 from the recomputed values — so the expected RTMR0 depends on nothing the host said about the tables. On mismatch it names the offending table instead of reporting a bare "MRs do not match".

The expected values stay derived from low-dimensional inputs the host cannot lie about for free: the same vm_config fields also drive the TD HOB measurement in RTMR0 and the kernel measurement in RTMR1, so misreporting the topology to fit forged tables breaks the other measurements.

Why mandatory, and why both failure modes are fatal

The first version of this PR put the check behind a config gate and reported the outcome in acpi_tables_verified. That does not close the hole, for a reason worth spelling out: swtpm and qemu_version are host-declared vm_config fields that no other measurement independently constrains. swtpm = true makes the generator bail; a bogus version makes it generate for the wrong profile. So under any design where "could not generate" or "did not match" still yields is_valid = true, an attacker ships forged ACPI tables and declares swtpm = true to land in the unverified branch. The check would be optional at the attacker's discretion, and nothing in-tree consumes acpi_tables_verified today (KMS boot_info does not carry it).

So there is no knob and no soft outcome:

• digest mismatch → verification fails, naming the table.
• shape the generator cannot model (swtpm = true, QEMU older than 8.0) → verification fails; there is nothing to compare against.

Consequence to be explicit about: CVMs using the TPM key provider (swtpm = true, KeyProviderKind::Tpm) can no longer be verified on the lite path. They already could not be verified on the full-image path — Machine::build_tables() has rejected swtpm since refactor(attestation): reject swtpm measurement — so this makes the two paths agree rather than introducing a new gap. Supporting swtpm in qemu-acpi (TPM2 table, the PPI AML, and a second fixture matrix) is a separate piece of work.

Verification

The lite fixture (verifier/fixtures/tdx-lite-attestation.json) was captured from a real CVM, so its RTMR0 ACPI digests are whatever QEMU 8.2.2 actually produced on that host. Recomputing them in-process reproduces them exactly — the generator agrees with hardware, not just with itself:

$ dstack-verifier --config v.toml --verify verifier/fixtures/tdx-lite-attestation.json
is_valid=true  acpi_tables_verified=true

Tests:

• verifies_tdx_lite_fixture_without_image_download — the real fixture passes and now reports acpi_tables_verified (previously asserted false).
• tdx_lite_acpi_hashes_depend_on_the_reported_vm_shape — recomputed digests match the captured CVM, and adding one vCPU makes them stop matching, so the comparison has teeth.
• tdx_lite_acpi_hash_mismatch_names_the_table — a mismatch names acpi-tables.

cargo test -p dstack-verifier -p dstack-mr -p dstack-kms --all-features passes; cargo fmt / cargo clippy clean.

Docs updated rather than left stale: docs/security/security-model.md's "Why TDX lite mode does not validate ACPI table contents" is replaced by the fail-closed rationale (the BadAML sandbox stays documented as defense in depth), plus the verifier README and the lite fixture README.