The Files security lattice in Kotlin (labels, clearance) #76

2026-09-04T18:53:27Z

paulhitt commented

2026-09-04 18:53:27 +00:00

(Migrated from gitlab.com)

Label and Clearance: the two-dimensional lattice Files is built on, and the
ten-byte encoding that is authenticated data for every construction using it.

The encoding vectors were computed independently, not read off this
implementation. A label that encodes differently on two platforms does not warn
— it produces a decryption failure, or plaintext that quietly belongs to the
wrong sensitivity. A vector taken from the code under test would pin whatever
the code happens to do.

Two dimensions, and the tests are shaped around the failure that READS AS
WORKING: an implementation comparing classification and forgetting compartments
behaves correctly on every test built from levels alone, right up until
somebody sees a compartment they are not in. Domination needs a superset of
areas, not an overlap; two labels can be incomparable in both directions.

Bit 63 is the sign bit of a Long. Building the mask with an Int shift loses
it, and the compartment that vanishes is the one nobody notices until somebody
sees a file they are not cleared for. Pinned, along with the all-ones case where
a sign-extension mistake still produces plausible-looking bytes.

A finding, and a divergence I deliberately did NOT create. Files
implements the simple security property (no read up) and NOT the ★-property (no
write down) — on either client. iOS gates ensureLabelKey and use on
clearance.permits and nothing else, so Kotlin's mayWrite calls the same
check, with a comment saying why and a test asserting the current behaviour that
will fail loudly the day it changes.

Implementing it on Android alone would mean a file that saves on one phone and
is refused on the other, with neither person able to tell which rule they had
met — worse than the gap, because an apparent bug gets worked around. Filed as
android#15 / ios#65 with the trade written out: no-write-down is the half a
lattice actually exists for, and it is also the half that is awkward enough to
need a stated downgrade path rather than a bare refusal. It interacts with
sharing a file into a chat — a write to a place with no label at all — so it
needs an answer before that ships.

16 tests. App builds, every JVM suite green.

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

`Label` and `Clearance`: the two-dimensional lattice Files is built on, and the ten-byte encoding that is authenticated data for every construction using it. The encoding vectors were computed independently, not read off this implementation. A label that encodes differently on two platforms does not warn — it produces a decryption failure, or plaintext that quietly belongs to the wrong sensitivity. A vector taken from the code under test would pin whatever the code happens to do. Two dimensions, and the tests are shaped around the failure that READS AS WORKING: an implementation comparing classification and forgetting compartments behaves correctly on every test built from levels alone, right up until somebody sees a compartment they are not in. Domination needs a superset of areas, not an overlap; two labels can be incomparable in both directions. Bit 63 is the sign bit of a Long. Building the mask with an Int shift loses it, and the compartment that vanishes is the one nobody notices until somebody sees a file they are not cleared for. Pinned, along with the all-ones case where a sign-extension mistake still produces plausible-looking bytes. **A finding, and a divergence I deliberately did NOT create.** Files implements the simple security property (no read up) and NOT the ★-property (no write down) — on either client. iOS gates `ensureLabelKey` and `use` on `clearance.permits` and nothing else, so Kotlin's `mayWrite` calls the same check, with a comment saying why and a test asserting the current behaviour that will fail loudly the day it changes. Implementing it on Android alone would mean a file that saves on one phone and is refused on the other, with neither person able to tell which rule they had met — worse than the gap, because an apparent bug gets worked around. Filed as android#15 / ios#65 with the trade written out: no-write-down is the half a lattice actually exists for, and it is also the half that is awkward enough to need a stated downgrade path rather than a bare refusal. It interacts with sharing a file into a chat — a write to a place with no label at all — so it needs an answer before that ships. 16 tests. App builds, every JVM suite green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

paulhitt commented

2026-09-04 18:53:27 +00:00

(Migrated from gitlab.com)

assigned to @paulhitt

paulhitt (Migrated from gitlab.com) changed target branch from feat/wallet-screen to main

2026-09-04 20:49:48 +00:00

paulhitt commented

2026-09-04 20:49:50 +00:00

(Migrated from gitlab.com)

mentioned in commit 9c107b7c8d

mentioned in commit 9c107b7c8d70a6920f774bcdf213f8fdbe95dff3

paulhitt (Migrated from gitlab.com) merged commit 9c107b7c8d into main

2026-09-04 20:49:50 +00:00

paulhitt commented

2026-09-09 19:01:29 +00:00

(Migrated from gitlab.com)

changed the description

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: extant2000/flamenet-messenger-android#76