amadan

carlos / platform Public

infra: a termination queue per region, and box records that storage will not let anyone rewrite

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude 3a4ce1c43ecf233dca9ad8ed5bc935d8d0681630 parent abe7fc2
6 files changed, +209 −0
  • docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md +45 −0
  • infra/modules/deployment-buckets/main.tf +52 −0
  • infra/modules/deployment-buckets/variables.tf +6 −0
  • infra/modules/region-host/README.md +24 −0
  • infra/modules/region-host/main.tf +77 −0
  • infra/modules/region-host/outputs.tf +5 −0
diff --git a/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md b/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
index 3b1aa8c9d..18587034b 100644
--- a/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
+++ b/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md
@@ -879,3 +879,48 @@ None. Rev 4.2's three were ruled as H7, H8 and H9 (2026-10-04).
| Finding | Disposition |
|---|---|
| A5-1 P1: step 1 waits for the replicator's handle, closed only in step 4 | accepted: step 1 allows only the box's own replicator descriptors; step 4 closes it and runs the unrestricted check; tested with a live replicator (§5.8), K2 |
+
+## 18. Notes from plan 1a (2026-10-05)
+
+Plan `docs/superpowers/plans/2026-10-05-region-ha-1a-foundations.md` builds
+the parts of this spec that need no claim. It keeps every property above
+and changes three mechanisms:
+
+1. **Exact content by hash, not by S3 version id (§5.6, §5.1).** The store
+ abstraction has no version-id read and the box role has no
+ `s3:GetObjectVersion`. Objects are immutable, their key contains their
+ SHA-256, the manifest records it, and a reader verifies it. A bind
+ names its record by `record_sha256` in place of `record_version_id`.
+2. **The identity signature (§5.1).** The record carries IMDS's
+ base64 RSA-SHA256 signature (`/latest/dynamic/instance-identity/signature`),
+ verified with the regional certificate, in place of the PKCS7 form.
+ Same document, same signer, no new dependency.
+3. **`snapshot` is a periodic full publish, not a sealed archive (§5.6).**
+ `hostfiles.SyncDir` stages every difference between the directory and
+ the manifest. Run on the snapshot interval it gives the `snapshot`
+ setting; run every ten minutes it is the continuous setting's repair
+ scan; run before stop evidence it is the release flush. The manifest
+ therefore has no `base` or `base_seq`, and restore reads one manifest
+ and the objects it names.
+
+Two corrections to the spec, found while planning:
+
+- **§5.4's alert for two unstamped entries is dropped.** Static sites and
+ public address routes run on every box, so every box publishes them as
+ `home`, unstamped: that is normal, and the edge cannot tell them from
+ relocatable hosts. The edge reports only two boxes at the same positive
+ stamp. Plan 1b decides whether the publisher marks relocatable entries
+ so the edge can alert on those alone.
+- **§5.1's region check has two halves.** `boxid.Verify` proves which
+ region a box is in. Whoever uses that compares it with the region it
+ expects: `eligibleBoxes` takes the placement's AWS region and refuses a
+ box whose signed region differs, and `termfence.Verify` compares the
+ observation's region with the signed one. Plan 1b must supply the
+ expected region from something better than a majority vote of the
+ unsigned edges files.
+- Build tags (Task 6): the descriptor-based directory code is `//go:build unix`, not `linux`, so the CLI's macOS build uses it too; Windows gets a stub that publishes nothing.
+
+Two limits to lift in plan 1b: a file over 64 MiB is recorded in the
+manifest as skipped and is not published (the store takes a whole body in
+memory), and the third termination-evidence source (Auto Scaling activity
+history) is not built until spec 4 verifies it.
diff --git a/infra/modules/deployment-buckets/main.tf b/infra/modules/deployment-buckets/main.tf
index b6fcbb7b9..c2d7b532c 100644
--- a/infra/modules/deployment-buckets/main.tf
+++ b/infra/modules/deployment-buckets/main.tf
@@ -59,3 +59,55 @@ resource "aws_s3_bucket_server_side_encryption_configuration" "data" {
apply_server_side_encryption_by_default { sse_algorithm = "AES256" }
}
}
+
+# --- Box records (region HA spec 1 §5.1) -----------------------------------
+# control/boxes/<id>.json binds a box's name to one AWS instance, and
+# control/boxes/<id>.bind.json is an operator's word for a legacy label.
+# Both are written once and never changed. Storage enforces that, so no
+# bug or stolen box credential can rebind a name to another machine.
+#
+# EVERY statement here names control/boxes/ and nothing wider. A broad Deny
+# on this bucket has broken lease releases before.
+
+resource "aws_s3_bucket_policy" "deployment_box_records" {
+ bucket = aws_s3_bucket.deployment.id
+ policy = jsonencode({
+ Version = "2012-10-17"
+ Statement = [
+ {
+ # A record or bind may be created, never replaced. The qualifier
+ # leaves multipart preparation alone and still covers its completion.
+ Sid = "BoxRecordsAreCreateOnly"
+ Effect = "Deny"
+ Principal = "*"
+ Action = "s3:PutObject"
+ Resource = "${aws_s3_bucket.deployment.arn}/control/boxes/*"
+ Condition = {
+ Null = { "s3:if-none-match" = "true" }
+ Bool = { "s3:ObjectCreationOperation" = "true" }
+ }
+ },
+ {
+ Sid = "BoxRecordsAreNeverDeleted"
+ Effect = "Deny"
+ Principal = "*"
+ Action = ["s3:DeleteObject", "s3:DeleteObjectVersion"]
+ Resource = "${aws_s3_bucket.deployment.arn}/control/boxes/*"
+ },
+ {
+ # With no operators named, the list is one ARN nobody has, so the
+ # Deny covers everyone.
+ Sid = "OnlyOperatorsWriteBinds"
+ Effect = "Deny"
+ Principal = "*"
+ Action = "s3:PutObject"
+ Resource = "${aws_s3_bucket.deployment.arn}/control/boxes/*.bind.json"
+ Condition = {
+ ArnNotLike = {
+ "aws:PrincipalArn" = length(var.operator_role_arns) > 0 ? var.operator_role_arns : ["arn:aws:iam::000000000000:role/nobody"]
+ }
+ }
+ },
+ ]
+ })
+}
diff --git a/infra/modules/deployment-buckets/variables.tf b/infra/modules/deployment-buckets/variables.tf
index eba25373b..9b2ffb0ba 100644
--- a/infra/modules/deployment-buckets/variables.tf
+++ b/infra/modules/deployment-buckets/variables.tf
@@ -7,3 +7,9 @@ variable "data_bucket_name" {
description = "Name of the regional data bucket (parked databases, WAL streams, leases, blobs)."
type = string
}
+
+variable "operator_role_arns" {
+ description = "IAM role ARNs of human operators. Only these may write a box bind (control/boxes/*.bind.json). Empty means nobody can: the safe default until operators are named."
+ type = list(string)
+ default = []
+}
diff --git a/infra/modules/region-host/README.md b/infra/modules/region-host/README.md
index b10c3a8c0..084a978b2 100644
--- a/infra/modules/region-host/README.md
+++ b/infra/modules/region-host/README.md
@@ -111,3 +111,27 @@ curl -sI --resolve <host>:443:<eip> https://<host>/ | grep -i x-carlos-version
Use `--resolve` against the box's own EIP rather than trusting DNS: a stale
answer from a resolver has produced more than one false "verified" report.
+
+## Termination evidence
+
+The module creates a queue, `<iam_name>-terminations`, that receives an
+event whenever an EC2 instance in this account and region reaches
+`terminated`. Region HA reads it to prove a dead box is gone before its
+instances run elsewhere. Only the module's own EventBridge rule can write
+to the queue, and the box role can only read and delete from it.
+
+After the first apply, check that nobody but the rule can write to it.
+From an administrator's session:
+
+ aws sqs send-message --queue-url <termination_queue_url> --message-body '{"forged":true}'
+
+must fail with `AccessDenied`. Then terminate a throwaway instance in the
+region and confirm its event arrives.
+
+The root volume is deleted when the instance is terminated. Region HA
+depends on that: a terminated box must leave no disk behind.
+
+Open item for region HA plan 1b: the box role's `ec2:DescribeInstances`
+is unconditioned, because the infrastructure inventory reads every
+region. The HA spec asks for an `ec2:Region` condition on the call the
+placer makes. Decide there whether that is a second, narrower statement.
diff --git a/infra/modules/region-host/main.tf b/infra/modules/region-host/main.tf
index 14b7724a6..563611373 100644
--- a/infra/modules/region-host/main.tf
+++ b/infra/modules/region-host/main.tf
@@ -473,6 +473,9 @@ resource "aws_instance" "host" {
volume_size = var.root_volume_size
volume_type = "gp3"
encrypted = true
+ # A terminated box must leave no disk behind: termination is the proof
+ # that its instances may run elsewhere (region HA spec 1 §5.9).
+ delete_on_termination = true
}
tags = { Name = var.name }
# The AMI data source floats (most_recent): without this, a newer
@@ -669,3 +672,77 @@ resource "aws_iam_role_policy" "host_store" {
]
})
}
+
+# --- Termination evidence (region HA spec 1 §5.9) ---------------------------
+# EC2 tells EventBridge when an instance in this account and region reaches
+# "terminated"; the rule forwards that to a queue the region's boxes read.
+# Delivery is best-effort on AWS's side: the queue keeps what arrived, and a
+# box that finds nothing here still asks EC2 directly.
+
+resource "aws_sqs_queue" "terminations" {
+ name = "${var.iam_name}-terminations"
+ message_retention_seconds = 1209600 # 14 days, the maximum
+ sqs_managed_sse_enabled = true
+}
+
+resource "aws_cloudwatch_event_rule" "terminations" {
+ name = "${var.iam_name}-terminations"
+ description = "EC2 instances reaching terminated, for region HA failover."
+ event_pattern = jsonencode({
+ source = ["aws.ec2"]
+ "detail-type" = ["EC2 Instance State-change Notification"]
+ detail = { state = ["terminated"] }
+ })
+}
+
+resource "aws_cloudwatch_event_target" "terminations" {
+ rule = aws_cloudwatch_event_rule.terminations.name
+ arn = aws_sqs_queue.terminations.arn
+}
+
+# Only this rule may put a message on the queue. A message is evidence, so
+# who can write one matters as much as who can read one.
+#
+# The Allow alone is not enough: a principal in this account with its own
+# sqs:SendMessage grant (an admin role, a wildcard policy) could still post
+# a forged event, because an identity policy and a queue policy add up.
+# The Deny closes that. It matches every send whose source is not this
+# rule, including one with no source at all, which is what a direct
+# SendMessage from a role looks like.
+resource "aws_sqs_queue_policy" "terminations" {
+ queue_url = aws_sqs_queue.terminations.id
+ policy = jsonencode({
+ Version = "2012-10-17"
+ Statement = [
+ {
+ Sid = "TheTerminationRuleMaySend"
+ Effect = "Allow"
+ Principal = { Service = "events.amazonaws.com" }
+ Action = "sqs:SendMessage"
+ Resource = aws_sqs_queue.terminations.arn
+ Condition = { ArnEquals = { "aws:SourceArn" = aws_cloudwatch_event_rule.terminations.arn } }
+ },
+ {
+ Sid = "NobodyElseMaySend"
+ Effect = "Deny"
+ Principal = "*"
+ Action = "sqs:SendMessage"
+ Resource = aws_sqs_queue.terminations.arn
+ Condition = { ArnNotEquals = { "aws:SourceArn" = aws_cloudwatch_event_rule.terminations.arn } }
+ },
+ ]
+ })
+}
+
+resource "aws_iam_role_policy" "host_terminations" {
+ name = "${var.iam_name}-terminations"
+ role = aws_iam_role.host.id
+ policy = jsonencode({
+ Version = "2012-10-17"
+ Statement = [{
+ Effect = "Allow"
+ Action = ["sqs:ReceiveMessage", "sqs:DeleteMessage", "sqs:GetQueueAttributes"]
+ Resource = aws_sqs_queue.terminations.arn
+ }]
+ })
+}
diff --git a/infra/modules/region-host/outputs.tf b/infra/modules/region-host/outputs.tf
index f7cde057e..3ddaabd82 100644
--- a/infra/modules/region-host/outputs.tf
+++ b/infra/modules/region-host/outputs.tf
@@ -37,3 +37,8 @@ output "vpc_cidr" {
description = "CIDR of the VPC the host lives in — the value for CARLOS_RELAY_DENY_CIDRS on a box that runs the relay."
value = data.aws_vpc.host.cidr_block
}
+
+output "termination_queue_url" {
+ description = "The queue that receives this region's EC2 terminated events."
+ value = aws_sqs_queue.terminations.id
+}