Expose the security lattice to the interop driver (relay#49) #94

Merged
paulhitt merged 1 commits from test/label-lattice-interop into main 2026-09-05 10:40:23 +00:00
paulhitt commented 2026-09-05 10:39:19 +00:00 (Migrated from gitlab.com)

relay#49 requires that labels and security levels be kept as Messenger and
Files converge. Both engines have implemented §1's lattice independently
since the Files apps shipped, each pins its own vectors, and nothing has ever
compared the two.

The ten-byte encoding is authenticated data for every construction that
uses a label
, so a platform disagreement does not warn. It produces a
decryption failure, or — worse — plaintext that quietly belongs to the wrong
sensitivity. Each side passing its own vectors is necessary and not
sufficient; two engines can pass their own and still disagree.

label_encode reports the mask as a STRING. Bit 63 makes it a negative Long,
and a JSON number would arrive on the other side as a double and lose the low
bits — turning the one compartment most likely to be mis-shifted into the one
this check cannot see.

The matching harness stage is flamenet-e2e!28. Proven by breaking it rather
than by watching it pass: dropping compartments.containsAll(...) from
dominates — the classic "compares the level and forgets the areas" bug —
turned exactly four checks red, all of them compartment cases, each reporting
iOS and Android disagreeing. That bug behaves correctly on every case built
from levels alone, which is why it needs two engines to catch.

Co-Authored-By: Claude Opus 5 noreply@anthropic.com

relay#49 requires that labels and security levels be kept as Messenger and Files converge. Both engines have implemented §1's lattice independently since the Files apps shipped, each pins its own vectors, and nothing has ever compared the two. **The ten-byte encoding is authenticated data for every construction that uses a label**, so a platform disagreement does not warn. It produces a decryption failure, or — worse — plaintext that quietly belongs to the wrong sensitivity. Each side passing its own vectors is necessary and not sufficient; two engines can pass their own and still disagree. `label_encode` reports the mask as a STRING. Bit 63 makes it a negative Long, and a JSON number would arrive on the other side as a double and lose the low bits — turning the one compartment most likely to be mis-shifted into the one this check cannot see. The matching harness stage is flamenet-e2e!28. Proven by breaking it rather than by watching it pass: dropping `compartments.containsAll(...)` from `dominates` — the classic "compares the level and forgets the areas" bug — turned exactly four checks red, all of them compartment cases, each reporting iOS and Android disagreeing. That bug behaves correctly on every case built from levels alone, which is why it needs two engines to catch. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
paulhitt commented 2026-09-05 10:39:19 +00:00 (Migrated from gitlab.com)

assigned to @paulhitt

assigned to @paulhitt
paulhitt (Migrated from gitlab.com) scheduled this pull request to auto merge when all checks succeed 2026-09-05 10:39:53 +00:00
paulhitt commented 2026-09-05 10:40:24 +00:00 (Migrated from gitlab.com)

mentioned in commit de968ac1aa

mentioned in commit de968ac1aa6d6e66cb569f34dcacf7fb61b44f3d
paulhitt (Migrated from gitlab.com) merged commit de968ac1aa into main 2026-09-05 10:40:24 +00:00
paulhitt commented 2026-09-09 19:01:17 +00:00 (Migrated from gitlab.com)

changed the description

changed the description
Sign in to join this conversation.