From 6a0dce6d4e5e87cfa8f4be456f3ab7c8d7c27c93 Mon Sep 17 00:00:00 2001 From: Paul Hitt Date: Fri, 4 Sep 2026 14:53:26 -0400 Subject: [PATCH] The Files security lattice in Kotlin (labels, clearance) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 --- PARITY.md | 2 +- .../src/main/kotlin/io/flamenet/e2e/Label.kt | 101 +++++++++ .../test/kotlin/io/flamenet/e2e/LabelTest.kt | 196 ++++++++++++++++++ 3 files changed, 298 insertions(+), 1 deletion(-) create mode 100644 engine/src/main/kotlin/io/flamenet/e2e/Label.kt create mode 100644 engine/src/test/kotlin/io/flamenet/e2e/LabelTest.kt diff --git a/PARITY.md b/PARITY.md index 84c9ebe..c113e40 100644 --- a/PARITY.md +++ b/PARITY.md @@ -337,7 +337,7 @@ the messenger rather than staying separate apps. | Feature | Android | |---|:--:| | Local vault: add, organise, delete | ⚪ | -| Bell–LaPadula labels and clearance | ⚪ | +| Bell–LaPadula labels and clearance | 🟡 lattice, encoding and clearance in Kotlin, pinned to independently-computed vectors; the ★-property is unenforced on **both** clients — android#15 | | Share a file into a chat or group | ⚪ | | Wallet engine: BIP-39, Base58, SLIP-0010 | ✅ pinned to the published vectors | | Wallet engine: address derivation and signing | ✅ BIP-44 path, Base58 address, and the engine's own RFC 8032 signs — no API-33 floor | diff --git a/engine/src/main/kotlin/io/flamenet/e2e/Label.kt b/engine/src/main/kotlin/io/flamenet/e2e/Label.kt new file mode 100644 index 0000000..2068b07 --- /dev/null +++ b/engine/src/main/kotlin/io/flamenet/e2e/Label.kt @@ -0,0 +1,101 @@ +package io.flamenet.e2e + +/** + * The security lattice. Mirrors §1 of the published Files specification. + * + * 🔴 **The ten-byte encoding is authenticated data for every construction that + * uses it**, so a label that encodes differently on two platforms does not + * produce a warning — it produces a decryption failure, or worse, plaintext + * that quietly belongs to the wrong sensitivity. That is why [bytes] is pinned + * to a vector rather than left to look obviously right. + * + * ⚠️ **Two dimensions, and both are required.** A classification alone is a + * ladder: anything high enough reads anything lower. Compartments cut across + * it — "Secret, and only if you are in this area" — and the interesting failure + * is an implementation that checks the level and forgets the areas, which reads + * as working right up until somebody sees a compartment they are not in. + */ +data class Label( + val classification: Short, + /** Bit positions 0..63. */ + val compartments: Set = emptySet(), +) { + init { + require(compartments.all { it in 0..63 }) { "compartment bits must be 0..63" } + } + + val mask: Long + get() = compartments.fold(0L) { acc, bit -> acc or (1L shl bit) } + + /** + * `this ⊒ other`: at least as high, AND a superset of areas. + * + * 🔴 Both, always. Dropping the compartment half turns the lattice back + * into a ladder and silently widens every read. + */ + fun dominates(other: Label): Boolean = + classification >= other.classification && compartments.containsAll(other.compartments) + + /** + * `int16be classification || uint64be compartment mask`. + * + * ⚠️ Big-endian, and stated because the JVM's own `ByteBuffer` default + * happens to agree while Kotlin's shifts do not care — writing this with + * `toByte()` on an unshifted value would produce little-endian bytes that + * still look plausible in a debugger and decrypt nothing. + */ + fun bytes(): ByteArray { + val out = ByteArray(10) + out[0] = ((classification.toInt() shr 8) and 0xff).toByte() + out[1] = (classification.toInt() and 0xff).toByte() + val m = mask + for (i in 0 until 8) { + out[2 + i] = ((m ushr (56 - i * 8)) and 0xff).toByte() + } + return out + } + + companion object { + /** The label everything dominates: unclassified, no areas. */ + val bottom = Label(0) + } +} + +/** + * What one person is allowed to reach. + * + * 🔴 **Both bounds, always.** A label must sit INSIDE the range, not merely + * below the top of it. The minimum is what stops somebody cleared for sensitive + * work from also holding the unclassified pile — which sounds like a + * convenience to remove until it is the reason an audit can say who could have + * seen what. + */ +data class Clearance(val maximum: Label, val minimum: Label = Label.bottom) { + + fun permits(label: Label): Boolean = + maximum.dominates(label) && label.dominates(minimum) + + /** + * 🔴 **No read up.** Bell–LaPadula's simple security property: you cannot + * read what is above you. This is the one people expect. + */ + fun mayRead(label: Label): Boolean = permits(label) + + /** + * Whether a write to [label] is allowed. + * + * 🔴 **The SAME check as reading, and that is a deliberate match with iOS + * rather than an oversight.** `FilesSession.ensureLabelKey` and `use` both + * gate on `clearance.permits`, so the range is the whole rule on both + * platforms. + * + * ⚠️ **Bell–LaPadula's ★-property is therefore NOT enforced.** The model + * says somebody cleared to read sensitive material must not write *below* + * their clearance, because they would carry what they read down with them. + * Neither client implements that. Adding it on Android alone would mean a + * file that saves on one phone and is refused on the other, with no way for + * either person to tell which rule they had met — a worse outcome than the + * gap. Filed for both so it is decided once: android#15 / ios#65. + */ + fun mayWrite(label: Label): Boolean = permits(label) +} diff --git a/engine/src/test/kotlin/io/flamenet/e2e/LabelTest.kt b/engine/src/test/kotlin/io/flamenet/e2e/LabelTest.kt new file mode 100644 index 0000000..838bcd8 --- /dev/null +++ b/engine/src/test/kotlin/io/flamenet/e2e/LabelTest.kt @@ -0,0 +1,196 @@ +package io.flamenet.e2e + +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +/** + * The security lattice, and the two Bell–LaPadula rules it exists to enforce. + * + * 🔴 **The encoding vectors were computed independently, not read off this + * implementation.** The ten bytes are authenticated data for every construction + * that uses a label, so an encoding that differs between 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. + */ +class LabelTest { + + private fun hex(bytes: ByteArray) = bytes.joinToString("") { "%02x".format(it) } + + // ---- The encoding ---------------------------------------------------- + + /** `int16be classification || uint64be compartment mask`. */ + @Test + fun `the ten-byte encoding matches the specification`() { + assertEquals("00000000000000000000", hex(Label(0).bytes())) + assertEquals("00010000000000000000", hex(Label(1).bytes())) + assertEquals("00038000000000000001", hex(Label(3, setOf(0, 63)).bytes())) + assertEquals("01000000000000000100", hex(Label(256, setOf(8)).bytes())) + } + + /** + * ⚠️ A negative classification and a full compartment mask together — the + * case where a sign-extension mistake or an `Int` in place of a `Long` + * shows up. Both halves are all-ones, so a wrong shift produces something + * that still looks plausible. + */ + @Test + fun `the extremes encode without sign-extension damage`() { + assertEquals("ffffffffffffffffffff", hex(Label(-1, (0..63).toSet()).bytes())) + } + + /** + * 🔴 Bit 63 is the sign bit of a Long. Building the mask with an `Int` + * shift, or reading it back as one, loses it — and the compartment that + * vanishes is the one nobody notices until somebody sees a file they are + * not cleared for. + */ + @Test + fun `the top compartment bit survives`() { + assertEquals("00008000000000000000", hex(Label(0, setOf(63)).bytes())) + assertTrue(Label(0, setOf(63)).mask != 0L) + } + + @Test + fun `the encoding is always ten bytes`() { + assertEquals(10, Label(0).bytes().size) + assertEquals(10, Label(-1, (0..63).toSet()).bytes().size) + } + + @Test + fun `a compartment outside the range is refused`() { + assertFailsWith { Label(0, setOf(64)) } + assertFailsWith { Label(0, setOf(-1)) } + } + + // ---- Domination ------------------------------------------------------ + + @Test + fun `a higher classification dominates a lower one`() { + assertTrue(Label(3).dominates(Label(1))) + assertFalse(Label(1).dominates(Label(3))) + assertTrue(Label(2).dominates(Label(2))) + } + + /** + * 🔴 **The failure that reads as working.** An implementation that compares + * the classification and forgets the compartments behaves correctly on + * every test built from levels alone — right up until somebody sees a + * compartment they are not in. + */ + @Test + fun `a higher level does NOT dominate a compartment it is not in`() { + val topSecretNoAreas = Label(9) + val secretInArea = Label(5, setOf(2)) + assertFalse( + topSecretNoAreas.dominates(secretInArea), + "a higher classification reached into a compartment it does not hold", + ) + } + + @Test + fun `domination needs a superset of areas, not an overlap`() { + val holder = Label(5, setOf(1, 2)) + assertTrue(holder.dominates(Label(5, setOf(1)))) + assertTrue(holder.dominates(Label(5, setOf(1, 2)))) + assertFalse(holder.dominates(Label(5, setOf(1, 3))), + "an overlapping but incomplete set was treated as domination") + } + + /** Two labels can be incomparable — neither dominates the other. */ + @Test + fun `disjoint compartments are incomparable in both directions`() { + val a = Label(5, setOf(1)) + val b = Label(5, setOf(2)) + assertFalse(a.dominates(b)) + assertFalse(b.dominates(a)) + } + + @Test + fun `bottom is dominated by everything`() { + assertTrue(Label(0).dominates(Label.bottom)) + assertTrue(Label(9, setOf(3)).dominates(Label.bottom)) + } + + // ---- Clearance: no read up ------------------------------------------- + + @Test + fun `a clearance reads what it dominates`() { + val cleared = Clearance(maximum = Label(5, setOf(1, 2))) + assertTrue(cleared.mayRead(Label(3, setOf(1)))) + assertTrue(cleared.mayRead(Label(5, setOf(1, 2)))) + } + + @Test + fun `a clearance cannot read above itself`() { + val cleared = Clearance(maximum = Label(5)) + assertFalse(cleared.mayRead(Label(6))) + assertFalse(cleared.mayRead(Label(5, setOf(1))), + "a compartment outside the clearance was readable") + } + + /** + * 🔴 **The minimum is a real bound, not decoration.** A label must sit + * INSIDE the range. Somebody cleared for sensitive work is deliberately not + * also holding the unclassified pile — which sounds like a convenience to + * remove until it is the reason an audit can say who could have seen what. + */ + @Test + fun `a clearance with a floor cannot read below it`() { + val cleared = Clearance(maximum = Label(5), minimum = Label(2)) + assertTrue(cleared.mayRead(Label(3))) + assertFalse(cleared.mayRead(Label(1)), "a label below the floor was readable") + } + + // ---- Writing --------------------------------------------------------- + + /** + * 🔴 **Writing is gated by the same range check as reading, and the + * ★-property is NOT enforced — on either platform.** + * + * Bell–LaPadula says somebody cleared to read sensitive material must not + * write *below* their clearance, because they would carry what they read + * down with them. iOS gates `ensureLabelKey` and `use` on + * `clearance.permits` and nothing else, so this matches it deliberately. + * + * Implementing the rule on Android alone would produce 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 itself. Filed as android#15 / + * ios#65 so it is decided once, for both. + * + * ⚠️ This asserts the CURRENT behaviour, including the part that is a gap. + * It should fail loudly on the day somebody implements the ★-property, + * which is the point of writing the absence down rather than leaving it + * implicit. + */ + @Test + fun `writing uses the same range check as reading, star-property not enforced`() { + val cleared = Clearance(maximum = Label(5)) + assertTrue(cleared.mayWrite(Label(5))) + assertTrue( + cleared.mayWrite(Label(1)), + "the star-property is now enforced — see android#15, and update the " + + "iOS side and this test together", + ) + assertFalse(cleared.mayWrite(Label(8))) + assertFalse(cleared.mayRead(Label(8))) + } + + @Test + fun `a floor bounds writing as well as reading`() { + val cleared = Clearance(maximum = Label(5), minimum = Label(2)) + assertTrue(cleared.mayWrite(Label(3))) + assertFalse(cleared.mayWrite(Label(1))) + } + + @Test + fun `a compartment outside the clearance cannot be written either`() { + val cleared = Clearance(maximum = Label(5, setOf(1))) + assertTrue(cleared.mayWrite(Label(5, setOf(1)))) + assertFalse(cleared.mayWrite(Label(5, setOf(1, 2))), + "a compartment outside the clearance was writable") + } +}