diff --git a/docs/security/security-model.md b/docs/security/security-model.md index 8dbe14685..4f48fe824 100644 --- a/docs/security/security-model.md +++ b/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 diff --git a/dstack/dstack-mr/src/tdx.rs b/dstack/dstack-mr/src/tdx.rs index 5eb8f774d..71e112ba4 100644 --- a/dstack/dstack-mr/src/tdx.rs +++ b/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> { - 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 { + 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> { + let machine = machine_from_vm_config(vm_config, measurement.tdvf.ovmf_variant); let opts = machine .versioned_options() .context("failed to resolve QEMU measurement options")?; diff --git a/dstack/dstack-types/src/lib.rs b/dstack/dstack-types/src/lib.rs index a1a6e80e8..d43baf895 100644 --- a/dstack/dstack-types/src/lib.rs +++ b/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, /// GCP TDX no-image-download measurement material. Present for GCP diff --git a/dstack/verifier/README.md b/dstack/verifier/README.md index ce229a53f..fd3117032 100644 --- a/dstack/verifier/README.md +++ b/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: diff --git a/dstack/verifier/fixtures/tdx-lite.README.md b/dstack/verifier/fixtures/tdx-lite.README.md index 01b977e92..1eb215bcd 100644 --- a/dstack/verifier/fixtures/tdx-lite.README.md +++ b/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. diff --git a/dstack/verifier/src/verification.rs b/dstack/verifier/src/verification.rs index 883a79ba1..f01b61617 100644 --- a/dstack/verifier/src/verification.rs +++ b/dstack/verifier/src/verification.rs @@ -584,6 +584,31 @@ impl CvmVerifier { }) } + /// Compare recomputed ACPI digests against the ones the guest reported. + /// + /// RTMR0 alone would already fail on a mismatch, but only with an opaque + /// "MRs do not match": name the offending table here so an operator can + /// tell a tampered table apart from an unexpected VM shape. + fn assert_tdx_acpi_hashes_match( + expected: &TdxRtmr0AcpiHashes, + reported: &TdxRtmr0AcpiHashes, + ) -> Result<()> { + for (name, expected, reported) in [ + (TDX_ACPI_LOADER_EVENT, &expected.loader, &reported.loader), + (TDX_ACPI_RSDP_EVENT, &expected.rsdp, &reported.rsdp), + (TDX_ACPI_TABLES_EVENT, &expected.tables, &reported.tables), + ] { + if expected != reported { + bail!( + "TDX lite {name} digest mismatch: expected {}, reported {}", + hex::encode(expected), + hex::encode(reported) + ); + } + } + Ok(()) + } + /// Helper method to ensure image is downloaded and return image paths async fn ensure_image_downloaded(&self, vm_config: &VmConfig) -> Result { let hex_os_image_hash = hex::encode(&vm_config.os_image_hash); @@ -779,16 +804,14 @@ impl CvmVerifier { // so a new variant fails the build here instead of taking one. // // A `tdx_measurement` document must not pull a `Legacy` boot onto - // the lite path. The paths are not interchangeable: the legacy path - // recomputes the ACPI tables from `vm_config` and reports - // `acpi_tables_verified`, while the lite path takes the RTMR0 ACPI - // digests from the event log as given (see - // `tdx_acpi_hashes_from_event_log`) and never checks the table - // contents. Images attach the document whenever they have it, - // independent of the scheme, so honoring it here would drop ACPI - // table verification for a boot that resolved to `Legacy` precisely - // because the app asked for it (`requirements.tdx_measure_acpi_tables`, - // enforced guest-side in `dstack-util`'s system_setup). + // the lite path. Both paths now verify the ACPI tables, but they + // disagree on what `os_image_hash` means: legacy requires it to be + // the image digest and recomputes every MR from the downloaded + // image, while lite treats it as `sha256(sha256sum.txt)` and trusts + // the attached document for the image-static material. Images + // attach the document whenever they have it, independent of the + // scheme, so honoring it here would silently move a boot the app + // pinned to `Legacy` onto weaker image-identity checks. // // `Lite` without a document is rejected by the lite path itself, // rather than degraded to a download. @@ -969,7 +992,7 @@ impl CvmVerifier { vm_config: &VmConfig, attestation: &VerifiedAttestation, _debug: bool, - _details: &mut VerificationDetails, + details: &mut VerificationDetails, ) -> Result<()> { let Some(report) = &attestation.report.tdx_report() else { bail!("No TDX report"); @@ -1016,12 +1039,26 @@ impl CvmVerifier { // Compute expected measurements. TDX lite keeps the unified image hash // and carries split measurement material; verify it without - // downloading the image or running QEMU-derived ACPI table generators. - // The guest labels the three RTMR0 ACPI DATA events as acpi-loader, - // acpi-rsdp, and acpi-tables before exposing the event log, so the - // verifier does not guess based on event order. - let acpi_hashes = Self::tdx_acpi_hashes_from_event_log(event_log) + // downloading the image. The guest labels the three RTMR0 ACPI DATA + // events as acpi-loader, acpi-rsdp, and acpi-tables before exposing the + // event log, so the verifier does not guess based on event order. + let reported_acpi_hashes = Self::tdx_acpi_hashes_from_event_log(event_log) .context("TDX lite attestation is missing named RTMR0 ACPI DATA digests")?; + // Recompute the digests from the declared VM shape instead of trusting + // the reported ones, and treat both failure modes as fatal: a mismatch + // means the tables are not the ones this shape produces, and a shape + // the generator cannot model (`swtpm`, a QEMU older than any profile) + // leaves nothing to compare against. Downgrading either case to "pass, + // but unverified" would make the check optional at the host's + // discretion, because `swtpm` and `qemu_version` are host-declared + // fields that no other measurement independently constrains. + let acpi_hashes = + dstack_mr::tdx::expected_rtmr0_acpi_hashes(vm_config, measurement.tdvf.ovmf_variant) + .context("failed to recompute expected TDX lite ACPI table digests")?; + Self::assert_tdx_acpi_hashes_match(&acpi_hashes, &reported_acpi_hashes)?; + details.acpi_tables_verified = true; + // RTMR0 below is rebuilt from the recomputed digests, so the expected + // value depends on nothing the host reported about the tables. let mrs = dstack_mr::tdx::tdx_measurements_from_measurement_document( document, vm_config, @@ -2180,8 +2217,11 @@ mod tests { ); } + /// The fixture was captured from a real CVM, so its RTMR0 ACPI digests are + /// whatever QEMU actually produced. Reproducing them without the image + /// proves the generator agrees with hardware, not just with itself. #[tokio::test] - async fn verifies_tdx_lite_fixture_without_acpi_table_verification() { + async fn verifies_tdx_lite_fixture_without_image_download() { let request: VerificationRequest = serde_json::from_str(include_str!("../fixtures/tdx-lite-attestation.json")) .expect("TDX lite verifier fixture parses"); @@ -2199,7 +2239,7 @@ mod tests { assert!(response.details.quote_verified); assert!(response.details.event_log_verified); assert!(response.details.os_image_hash_verified); - assert!(!response.details.acpi_tables_verified); + assert!(response.details.acpi_tables_verified); assert_eq!( response.details.tee_variant, Some(ra_tls::attestation::TeeVariant::DstackTdx) @@ -2209,4 +2249,55 @@ mod tests { "TDX lite verification must not download or cache OS images" ); } + + /// The captured VM ran 2 vCPUs; a VM shape that disagrees with the quote + /// must not reproduce its ACPI digests, which is what makes the recomputed + /// digests worth comparing in the first place. + #[test] + fn tdx_lite_acpi_hashes_depend_on_the_reported_vm_shape() { + let fixture: serde_json::Value = + serde_json::from_str(include_str!("../fixtures/tdx-lite-getquote.json")) + .expect("TDX lite getquote fixture parses"); + let mut vm_config: VmConfig = serde_json::from_str( + fixture["vm_config"] + .as_str() + .expect("vm_config is a string"), + ) + .expect("fixture vm_config parses"); + let event_log: Vec = serde_json::from_str( + fixture["event_log"] + .as_str() + .expect("event_log is a string"), + ) + .expect("fixture event log parses"); + let ovmf_variant = vm_config.ovmf_variant.unwrap_or_default(); + + let reported = CvmVerifier::tdx_acpi_hashes_from_event_log(&event_log) + .expect("fixture carries named ACPI digests"); + let expected = dstack_mr::tdx::expected_rtmr0_acpi_hashes(&vm_config, ovmf_variant) + .expect("ACPI tables are generated for the fixture VM shape"); + CvmVerifier::assert_tdx_acpi_hashes_match(&expected, &reported) + .expect("recomputed digests match the captured CVM"); + + vm_config.cpu_count += 1; + let expected = dstack_mr::tdx::expected_rtmr0_acpi_hashes(&vm_config, ovmf_variant) + .expect("ACPI tables are generated for the altered VM shape"); + CvmVerifier::assert_tdx_acpi_hashes_match(&expected, &reported) + .expect_err("an extra vCPU must change the ACPI tables"); + } + + #[test] + fn tdx_lite_acpi_hash_mismatch_names_the_table() { + let expected = TdxRtmr0AcpiHashes { + loader: vec![1; 48], + rsdp: vec![2; 48], + tables: vec![3; 48], + }; + let mut reported = expected.clone(); + reported.tables = vec![4; 48]; + let err = CvmVerifier::assert_tdx_acpi_hashes_match(&expected, &reported) + .expect_err("mismatched tables digest is rejected"); + assert!(err.to_string().contains(TDX_ACPI_TABLES_EVENT), "{err:#}"); + assert!(CvmVerifier::assert_tdx_acpi_hashes_match(&expected, &expected).is_ok()); + } }