Files: the ★-property (no write down) is not enforced on either client #65

New Issue

2026-09-04T18:52:48Z

paulhitt commented

2026-09-04 18:52:48 +00:00

(Migrated from gitlab.com)

Files implements the simple security property — no read up — and not the ★-property — no write down. Neither client does. Found while porting the lattice to Kotlin; Android deliberately matches iOS rather than fixing it on one side.

What is enforced today

Clearance.permits(label) = maximum.dominates(label) && label.dominates(minimum). iOS gates both FilesSession.ensureLabelKey and FilesSession.use on it; the Kotlin Clearance.mayWrite calls the same check, with a comment saying why and a test asserting the current behaviour so it fails loudly the day this changes.

So: a person cleared to Secret cannot read Top Secret, and cannot read a compartment they are not in. Both correct.

What is not

Bell–LaPadula's ★-property says somebody cleared to read sensitive material must not write below their clearance — they would be carrying what they read down with them, deliberately or not. Today a person cleared to Secret can save a file into the unclassified area, and nothing stops them putting Secret content in it.

🔴 This is the rule the model exists for. No-read-up stops somebody reaching material above them, which most people expect and most systems get right. No-write-down stops the material leaking downward through a person who is allowed to see it, which is the actual threat a lattice is built to contain, and it is the half that is missing.

Why it was not just implemented

⚠️ A rule enforced on one client and not the other is worse than the gap. A file that saves on an iPhone and is refused on an Android handset — with neither person able to tell which rule they had met — turns a security property into an apparent bug, and the usual response to an apparent bug is to work around it.

The trade, which is real

The ★-property is genuinely awkward for people, and that is not a reason to skip it — it is a reason to design the explanation:

Somebody cleared high cannot save anything into a low area, including material that genuinely belongs there. Strict Bell–LaPadula has no exception; real systems add trusted downgrade, which is a whole mechanism with its own audit trail.
The refusal reads as a bug to anybody who has not met the model. A destination greyed out with no explanation teaches people the app is broken; "you can read above this, so you cannot write here" teaches them the rule. Whichever way this goes, the wording is most of the work.
It interacts with sharing a file into a chat — that is a write, to a place with no label at all. It needs an answer before that path ships on Android.

Options

Implement it strictly. Truest to the model, most likely to be worked around.
Implement it with a stated downgrade, one explicit action that records what was moved and by whom. More work; the only version that survives contact with people doing a job.
Leave it, and say so on /metadata and the Files screen. Cheapest, and honest only if it is actually written down — an unenforced half of a named model is a claim being made by the name.

My reading is (3) now and (2) when Files has real users, because (1) produces a workaround culture and a lattice people route around protects nothing. But "we implement Bell–LaPadula" should not be said anywhere until this is settled, and I have not checked whether it already is.

⚠️ Both clients or neither. Same reasoning as android#13 / ios#63.

Files implements the **simple security property** — no read up — and not the **★-property** — no write down. Neither client does. Found while porting the lattice to Kotlin; Android deliberately matches iOS rather than fixing it on one side. ## What is enforced today `Clearance.permits(label)` = `maximum.dominates(label) && label.dominates(minimum)`. iOS gates both `FilesSession.ensureLabelKey` and `FilesSession.use` on it; the Kotlin `Clearance.mayWrite` calls the same check, with a comment saying why and a test asserting the current behaviour so it fails loudly the day this changes. So: a person cleared to Secret cannot read Top Secret, and cannot read a compartment they are not in. Both correct. ## What is not Bell–LaPadula's ★-property says somebody cleared to read sensitive material must not write **below** their clearance — they would be carrying what they read down with them, deliberately or not. Today a person cleared to Secret can save a file into the unclassified area, and nothing stops them putting Secret content in it. 🔴 **This is the rule the model exists for.** No-read-up stops somebody reaching material above them, which most people expect and most systems get right. No-write-down stops the material *leaking downward through a person who is allowed to see it*, which is the actual threat a lattice is built to contain, and it is the half that is missing. ## Why it was not just implemented ⚠️ A rule enforced on one client and not the other is worse than the gap. A file that saves on an iPhone and is refused on an Android handset — with neither person able to tell which rule they had met — turns a security property into an apparent bug, and the usual response to an apparent bug is to work around it. ## The trade, which is real The ★-property is genuinely awkward for people, and that is not a reason to skip it — it is a reason to design the explanation: - Somebody cleared high **cannot save anything into a low area**, including material that genuinely belongs there. Strict Bell–LaPadula has no exception; real systems add trusted downgrade, which is a whole mechanism with its own audit trail. - The refusal reads as a bug to anybody who has not met the model. A destination greyed out with no explanation teaches people the app is broken; "you can read above this, so you cannot write here" teaches them the rule. Whichever way this goes, the *wording* is most of the work. - It interacts with **sharing a file into a chat** — that is a write, to a place with no label at all. It needs an answer before that path ships on Android. ## Options 1. **Implement it strictly.** Truest to the model, most likely to be worked around. 2. **Implement it with a stated downgrade**, one explicit action that records what was moved and by whom. More work; the only version that survives contact with people doing a job. 3. **Leave it, and say so on `/metadata` and the Files screen.** Cheapest, and honest only if it is actually written down — an unenforced half of a named model is a claim being made by the name. My reading is (3) now and (2) when Files has real users, because (1) produces a workaround culture and a lattice people route around protects nothing. But "we implement Bell–LaPadula" should not be said anywhere until this is settled, and I have not checked whether it already is. ⚠️ Both clients or neither. Same reasoning as android#13 / ios#63.

paulhitt commented

2026-09-04 19:33:43 +00:00

(Migrated from gitlab.com)

See the full reasoning on android#15. Short version: do not implement the ★-property, and stop describing Files as Bell–LaPadula. The content key travels in the same envelope as the file by design, so no client-side refusal is a control — and a suggestion dressed as one is worse than nothing. The engine's own Attachment.FILE comment had already settled this: the label is a MARKING, not a permission. What Files really provides is cryptographic read separation plus a classification that travels; the sharing sheet now says exactly that before the tap.

See the full reasoning on android#15. Short version: **do not implement the ★-property, and stop describing Files as Bell–LaPadula.** The content key travels in the same envelope as the file by design, so no client-side refusal is a control — and a suggestion dressed as one is worse than nothing. The engine's own `Attachment.FILE` comment had already settled this: *the label is a MARKING, not a permission*. What Files really provides is cryptographic read separation plus a classification that travels; the sharing sheet now says exactly that before the tap.

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: extant2000/flamenet-messenger-ios#65