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

New Issue

2026-09-04T18:52:47Z

paulhitt commented

2026-09-04 18:52:47 +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:42 +00:00

(Migrated from gitlab.com)

Recommendation, reached while building the sharing path (android!53)

Do not implement the ★-property. Stop describing Files as Bell–LaPadula.

The sharing path forced the question, because sending a file into a chat is a write to a place with no label at all. Here is what I found.

The codebase had already answered it

Attachment.FILE in the engine carries this, and has since before the lattice existed:

🔴 The label is a MARKING, not a permission. The content key is in the same envelope, so whoever can read the message can read the file — the bubble shows the classification so it can be filed the same way here, and must never imply this device was cleared for it.

That is the whole answer, written on the wire format. It was never connected to the ★-property question, but it settles it: the content key travels with the file by design. Not as an oversight — that is what makes sending work at all.

Why the ★-property cannot be enforced here

Strict Bell–LaPadula would forbid sending any classified file into a chat, since a chat is effectively unclassified. That is not a stricter version of this product; it is a different product with no sharing in it.

More fundamentally: there is no trusted computing base. When the rows lived in Postgres, session_dominates(...) was an RLS predicate and the database itself refused. There is no database now. The person holds every key, on a device they control, running a client they could modify. A client-side refusal is a suggestion — and a suggestion dressed as a control is worse than no control, because it is the one people plan around.

What Files does provide, stated honestly

Cryptographic read separation. No label key, no plaintext. Real, and enforced by mathematics rather than by a check. This is the simple security property and it genuinely holds.
A classification that travels. The number survives the trip and the recipient's phone files the document at it. Real, and useful.
Not mandatory access control. Nothing can refuse.

What this changes

Neither client implements the ★-property. Kotlin's Clearance.mayWrite stays permits, matching iOS, with the test that asserts the gap so it fails loudly if anyone implements it on one side only.
🔴 The claim has to go wherever it is made. "We implement Bell–LaPadula" is not true of either client, and this is the same category as the positioning rule about "we can't read your messages" — an overclaim about a security property is the kind that gets noticed by exactly the people it was meant to impress. I have not swept for the phrase outside the code; that is worth doing.
The downgrade is made legible instead. PickFileToSendSheet on both platforms now says, before the tap: whoever you send this to will be able to open it; the classification travels so it's filed the same way on their phone; it doesn't stop them reading it.

If you want the property anyway

It is buildable in one place — writes within the vault, where a folder has a label and the software is on both ends of the operation. But it would be a rule that holds inside the vault and evaporates the moment anything is shared, which is arguably worse to explain than not having it. My recommendation is not to.

⚠️ Proceeding on this reading so the sharing path could land. Say the word and I will reverse it — the test in LabelTest is written to make that a small change on both sides at once.

Same recommendation for ios#65.

## Recommendation, reached while building the sharing path (android!53) **Do not implement the ★-property. Stop describing Files as Bell–LaPadula.** The sharing path forced the question, because sending a file into a chat is a write to a place with no label at all. Here is what I found. ### The codebase had already answered it `Attachment.FILE` in the engine carries this, and has since before the lattice existed: > 🔴 The label is a MARKING, not a permission. The content key is in the same envelope, so whoever can read the message can read the file — the bubble shows the classification so it can be filed the same way here, and must never imply this device was cleared for it. That is the whole answer, written on the wire format. It was never connected to the ★-property question, but it settles it: **the content key travels with the file by design.** Not as an oversight — that is what makes sending work at all. ### Why the ★-property cannot be enforced here Strict Bell–LaPadula would forbid sending any classified file into a chat, since a chat is effectively unclassified. That is not a stricter version of this product; it is a different product with no sharing in it. More fundamentally: **there is no trusted computing base.** When the rows lived in Postgres, `session_dominates(...)` was an RLS predicate and the database itself refused. There is no database now. The person holds every key, on a device they control, running a client they could modify. A client-side refusal is a suggestion — and **a suggestion dressed as a control is worse than no control**, because it is the one people plan around. ### What Files does provide, stated honestly - **Cryptographic read separation.** No label key, no plaintext. Real, and enforced by mathematics rather than by a check. This is the simple security property and it genuinely holds. - **A classification that travels.** The number survives the trip and the recipient's phone files the document at it. Real, and useful. - **Not mandatory access control.** Nothing can refuse. ### What this changes 1. **Neither client implements the ★-property.** Kotlin's `Clearance.mayWrite` stays `permits`, matching iOS, with the test that asserts the gap so it fails loudly if anyone implements it on one side only. 2. 🔴 **The claim has to go wherever it is made.** "We implement Bell–LaPadula" is not true of either client, and this is the same category as the positioning rule about "we can't read your messages" — an overclaim about a security property is the kind that gets noticed by exactly the people it was meant to impress. I have not swept for the phrase outside the code; that is worth doing. 3. **The downgrade is made legible instead.** `PickFileToSendSheet` on both platforms now says, before the tap: whoever you send this to will be able to open it; the classification travels so it's filed the same way on their phone; it doesn't stop them reading it. ### If you want the property anyway It is buildable in one place — writes *within* the vault, where a folder has a label and the software is on both ends of the operation. But it would be a rule that holds inside the vault and evaporates the moment anything is shared, which is arguably worse to explain than not having it. My recommendation is not to. ⚠️ Proceeding on this reading so the sharing path could land. Say the word and I will reverse it — the test in `LabelTest` is written to make that a small change on both sides at once. Same recommendation for ios#65.

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: extant2000/flamenet-messenger-android#15