extant2000/flamenet-messenger-android
1
0
Fork 0
Code Issues 7 Pull Requests Actions Packages Projects Releases Wiki Activity

The Files security lattice in Kotlin (labels, clearance)

Browse Source 
`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>
This commit is contained in:
Paul Hitt
2026-09-04 14:53:26 -04:00
co-authored by Claude Opus 5
parent d915001dcc
commit 6a0dce6d4e
3 changed files with 298 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
engine/src/main/kotlin/io/flamenet/e2e/Label.kt
+101
View File
@@ -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<Int> = 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)
}
engine/src/test/kotlin/io/flamenet/e2e/LabelTest.kt
+196
View File
@@ -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<IllegalArgumentException> { Label(0, setOf(64)) }
assertFailsWith<IllegalArgumentException> { 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")
}
}