Secrecy

A program can give away a password it never prints. Writing ^ in front of a type marks a value as secret, and the compiler then refuses to build code that would leak it - and keeps refusing all the way through optimization.

What this is for

Say you check a password by comparing it one character at a time, and stop at the first character that does not match. That is the obvious way to write it, and it is correct - it never prints the password, never logs it, and returns nothing but yes or no.

It still gives the password away. An attacker who can time the check learns something from every attempt: a guess starting with the right character takes a hair longer to reject than one starting with the wrong character, because the comparison got one step further before giving up. Guess the first character - only one of them is measurably slower. Keep it, and guess the second. A password that would take longer than the universe to brute-force all at once falls in a few thousand tries, one character at a time.

Timing is not the only such channel. Three things about a running program are observable without reading its memory:

• Which way it branched. Taking one path rather than another takes a different amount of time, and leaves different traces in the processor.
• Which memory it touched. Reading table[secret] pulls exactly that entry into the cache. An attacker sharing the machine can often work out which one.
• How long an instruction took. Some instructions - division especially - finish faster or slower depending on the values fed to them.

The standard defence is to write the code so none of those depend on the secret: compare every character whether or not an earlier one already failed, and combine the results arithmetically instead of branching. This is called constant-time code, and it is notoriously easy to get wrong.

Why the compiler has to be involved

Even when you get it right by hand, the compiler can undo it. An optimizer's whole job is to notice that work is unnecessary and remove it - and branch-free code that carefully does the same work every time looks exactly like work worth eliminating. A shortcut you deliberately avoided writing gets helpfully added back, and nothing warns you. The source is still constant-time; the binary is not.

So the guarantee cannot live in a coding convention or a library. It has to be something the compiler itself knows about and is obliged to preserve. That is what ^ is.

# `^u64` is a secret. the compiler tracks where it flows.
#[oblivious]
fun ct_diff(a: ^u64, b: ^u64) ^u64 {
    ret a ^ b;                 # one xor, always the same work
}

fun verify(given: ^u64, secret: ^u64) bool {
    if (given == secret) { ret true; }   # refused - see below
    ret (ct_diff(given, secret):>u64) == 0;
}

That branch does not compile:

error: secret value used as a branch condition
  --> ./src/root.mach:16:5
   |
16 |     if (given == secret) { ret true; }
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: a secret may not steer control flow; branching on it leaks
     through timing. compute branch-free, or `:>T` to a public value when
     disclosure is intended

Three things are worth drawing out of that. The mistake is caught when you compile, not by an audit or a timing measurement after the fact. Secrecy is part of the type, so it travels with the value through every function it is passed to - you cannot lose track of which variable holds the sensitive one. And disclosure is possible but never accidental: :>T is the one way to turn a secret back into an ordinary value, so every deliberate release is a visible mark in the source that a reviewer can search for.

The rest of this page is the precise version of all that.

The secrecy lattice

There are two secrecy levels in a two-point lattice: public is the bottom, secret the top. ^ lifts a type to secret and binds to the type immediately to its right, so it nests with * and [N] in any order: ^u32, *^u8, ^*u8, [N]^u8, ^MyRec. Doubling collapses: ^^T is ^T.

A public value coerces up to secret wherever a secret is expected, with no syntax. The reverse never happens implicitly.

fun up(p: u32) ^u32 { ret p; }      # public u32 flows into a secret slot

A literal is public by construction and stays public through that coercion: its value sits in the instruction stream, so classifying it as secret would protect nothing. That does not weaken the join below - a value computed with a secret is secret however its other operand is spelled - so v << 3 on a secret v still yields a secret, while the constant 3 is not mistaken for a secret shift count.

Join

Any operation with a secret operand yields a secret result. Taint joins across arithmetic, bitwise, shift, and comparison operators, and through a value read out of a secret container.

fun mix(a: ^u32, b: u32) ^u32 { ret a + b; }    # ^u32 + u32 -> ^u32

rec Key { d: ^[32]u8; }
fun first(k: Key) ^u8 { ret k.d[0]; }            # element of a secret array is ^u8

Taking the address of a ^T value with ? gives the public pointer *^T - the address is public, the pointee secret - and dereferencing it with @ recovers the secret ^T.

Gates

A secret may not reach a position the leakage model observes. Each is a compile error decided by operand type:

• a secret branch or loop condition (if, for)
• a secret left operand of a short-circuiting && / || - it is the branch the operator keys on; a secret right operand only taints the result
• a secret memory index (table[i] with i secret)
• a secret memory address - an access through a secret pointer, whether by @p, p[i], or the auto-deref in p.x
• a secret operand of the always-variable-latency / or %

fun leak(a: ^u32, t: *u8, p: ^*u8) u8 {
    if (a) { ret 1; }       # error: secret value used as a branch condition
    ret t[a];               # error: secret value used as a memory index
    ret @p;                 # error: secret value used as a memory address
}

The index and the address are the two halves of one effective address, so both are gated. Only a secret pointer is an address: a ^[N]T or ^Rec is a secret value living at a public address, and a *^T is a public address to secret storage.

Three more gates decide against the target's constant-time capabilities rather than the source alone, so they are reported at lowering: a secret operand of a floating-point operation (always variable-latency, gated on every target); a secret operand of an integer multiply on a target without a trusted data-independent-timing mode, conservatively every ISA today; and a secret variable shift count on a target without a barrel shifter. A secret passed to a variadic pack is also rejected, including one wrapped inside an aggregate.

Asking about secrecy at comptime

$is_secret(T) folds true when T is ^-qualified at the outermost level. It is a type predicate like $is_record / $is_union / $is_pointer: comptime-only, valid as a $if / $or gate condition, and answered per instantiation inside a generic. The full reference is in Intrinsics.

It exists because secrecy was otherwise invisible to a library. Every other predicate asks about the shape under the ^ and so answers false for every secret, which makes $is_record(^u64) and $is_record(u64) the same answer - a reflection walk could only ever meet a secret field as a fallthrough it had to refuse. $is_secret is the positive question, and it is what lets a derive decide rather than refuse: a formatter redacts a secret field, a hash refuses one (a data-dependent fold is a leak in the shape of a digest), and an equality picks the constant-time comparison instead of the early-out whose timing is the secret.

rec Session { id: u64; key: ^[32]u8; }

$each f in $fields(Session) {
    $if ($is_secret(f.type)) { }            # redact: no read of `key` is emitted
    $or { render(s.[f]); }
}

Outermost only, the same line the rest of the family draws. ^*u8 is secret - the pointer is the secret, which is the shape the welded-storage rules exist for. *^u8 is not: it is a public address to secret storage, and $is_secret($pointee_of(f.type)) asks about the pointee. [N]^u8 is not, and neither is a record with a secret field - the field is, and that is where a walk meets the question.

There is deliberately no transitive "contains a secret anywhere" query: the per-field question is the one a walk actually has, and answering the transitive one in its place would make the common case wrong.

Downgrade with :>T

:>T is the only way to remove ^. It produces a new public value of type T and never reinterprets storage in place. The destination type T must always be named explicitly.

fun publish(a: ^u32) u32 { ret a:>u32; }

:>T peels exactly the outer qualifier, so it can never launder a welded pointee - *^T stays *^T. :: and :~ may neither add nor drop ^.

Welded-storage pointers

Secrecy is fixed at declaration and is non-launderable, which makes the public/secret aliasing leak unconstructable with no alias analysis at all:

• a ^T is stored only through a *^T, never a *T
• a secret-welded pointer cannot be erased to the untyped ptr
• a uni's overlapping variants must agree on secrecy

fun erase(p: *^u8) ptr { ret p; }     # error: cannot erase a secret pointer to ptr
uni Bad { a: ^u32; b: u32; }          # error: variants disagree on secrecy

The union rule is a property of the union type, not of the syntax that declared it, so it holds for an inline uni { ... } and at every instance of a generic union. At the declaration a variant typed by a generic parameter says nothing about secrecy, so the check happens where each instance is formed.

uni U[T] { a: T; b: u32; }
rec Box[T] { u: U[T]; }

var s: U[^u32];                       # error: this instantiation makes the variants disagree
var b: Box[^u32];                     # same error: the instance need not be spelled

Welding extends to nested aggregates: a *Pair whose x field is ^u64 has a welded field, so ?p.x yields a *^u64 and inherits the refusal.

#[oblivious] - the codegen contract

The flow typing constrains the source; #[oblivious] carries the obligation through codegen. Inside a function carrying it, the backend must not introduce a secret-dependent branch or select a variable-latency instruction on a secret operand.

#[oblivious]
fun ct_select(mask: ^u32, a: ^u32, b: ^u32) ^u32 { ret (a & mask) | (b & ~mask); }

A function instance that computes on a secret must carry it; one that only moves, stores, or declassifies secrets is transparent and stays annotation-free. The check runs per monomorphized instance.

A secret-taint bit is threaded from sema's flow typing through IR and MIR to the emitted instruction stream, preserved across every value replacement, inline clone, instruction selection, and register-allocator copy. The one place taint stops is the declassify barrier a :>T cast lowers to. Secret-free code carries no taint and compiles byte-identically. A translation validator then re-derives the taint over the lowered MIR as a monotone dataflow fixpoint and independently re-checks the leakage conditions. The stages after that MIR are trusted, not re-checked: see Where the check runs.

Inline assembly inside an oblivious function

Inline asm inside such a function is validated, not rejected. The block is parsed into instructions and walked for the same three leaks the compiler checks everywhere else. Taint enters through the block's {name} bindings, whose secrecy is stamped from the local's declared type. What the walk cannot model, it refuses:

That last row is a per-target asymmetry worth stating precisely. A branch whose condition is a register operand is visible to the walk and is checked: aarch64's cbz / cbnz, and every riscv64 branch, which compares two registers - RISC-V has no flags register at all. A branch whose condition rides the flags register cannot be checked, because a cmp of a secret before it would be invisible, so those are refused.

#[oblivious] remains a per-function contract. A call out to a non-oblivious function is not validated - that is the boundary the decorator draws, not a hole in it.

The zeroizing-write guarantee

Wiping a secret is only useful if the wipe survives to run. That guarantee exists, but it is not provided by #[oblivious], and it is scoped more broadly than the decorator is. A store into secret storage is tainted at lowering, keyed on the storage rather than on any decorator:

# no decorator: the wipe is protected anyway
fun clear(p: *^u8, n: usize) {
    var i: usize = 0;
    for (i < n) { p[i] = 0; i = i + 1; }
}

What it covers. Memory reached through a pointer that escapes the function - the shape a zeroize helper has. Such a store cannot be promoted out of memory, and the taint is present for any future pass to read.

What it does not cover. A value the compiler keeps in a register. Writing to a promoted local is not a memory write, so wiping one is not preserved:

var x: ^u8 = k;
x = 0;          # NOT guaranteed: `x` may never have been in memory

Adding #[oblivious] does not change this. To wipe reliably, write through a pointer whose target is memory the compiler cannot promote away.

Trusted base

The only secret-to-public crossings are the explicit :>T cast and inline asm blocks. Everything else is enforced. A proof is always relative to a leakage model, and its fidelity to real silicon is empirical.

The contract is only offered where mach emits the instructions that execute. A target whose back half hands a module to a downstream compiler instead - the SPIR-V backend - rejects #[oblivious]: neither that translation nor the device's timing behaviour is covered by the leakage model. Compile constant-time code for a machine target, and pass such a target only public data.

Assurance

What holds today: the type system checks that the source respects the leakage model, #[oblivious] carries the obligation through codegen, and the translation validator independently re-checks the lowered MIR. All three are static. Two host-executed measurements sit under them, and each only means anything on the machine it runs on, which is why both are unit tests rather than build checks.

The timing harness is a tool, not a gate

mach.lang.ct.probe is a dudect-style harness in the compiler's tree. mach test runs it at deliberately tiny sample counts and prints its table. It asserts nothing about the numbers, not a threshold and not positivity, because even "a mean is positive" proved to be a property of the host's clock resolution rather than of the harness (mach#3092). The run can only fail if the harness itself crashes. No property of a measured time gates anything, here or anywhere else in the suite.

That is deliberate and it is not a gap. A dudect score is a statistic over wall-clock time on hardware nobody controls, so any threshold over it has a false-failure rate that belongs to the machine rather than to the code. A required check that can fail nondeterministically is worse than no check: it teaches a reader to re-run a red constant-time result until it turns green. An earlier form of this harness did assert on such thresholds, and failed a release gate on x86_64-darwin and then passed a re-run of the identical commit (mach#3070).

So the claims below are measurements, taken deliberately, not properties the test suite enforces. They are re-taken by raising the counts in mach.lang.ct.probe and reading the printed table, on a quiet machine, by a person who then reads the numbers. Performance and timing work belongs in mach-bench, which is built for it, rather than in a correctness suite that must be deterministic.

What such a measurement can establish is bounded. It works by refutation, because that is all a timing measurement can do: a clean score is consistent with a leak the instrument cannot see. So each mode carries a planted leak that must be detected, and a constant-time reference that must not separate the way the planted one does. Read the separation between the two class means, never |t|. Welch's statistic divides by the sample variance, and concurrent load inflates the variance without moving the means, so |t| collapses under load while the leak is plainly still there. Measured at load average 27, six consecutive runs of one binary gave |t| between 7.51 and 11.24 against a threshold of 10, while the mean ratio never fell below 3.4.

A third probe leaks nothing at all and says whether a run counts. Any separation it shows is the machine rather than the code, so a run in which it is not flat has no discriminating power, and its verdict means nothing in either direction. A flat null is necessary and not sufficient: it must also be sampled at a comparable cost to the probe it is bounding, or a quiet control at one magnitude certifies nothing about noise at another.

The x86-64 flags table is measured, not inferred

The inline-asm model #[oblivious] rests on classifies eighteen x86-64 instructions by which ones define ZF and CF, which merely write them, and which read them. That table is re-derived on x86-64 hosts by mach.lang.target.isa.x64.probe, which runs each instruction twice with RFLAGS preset all-set and all-clear and compares what the CPU did against the transcription. Defining the flags is the only fact that clears a taint, so a row that drifts from the silicon is a permission rather than a refusal.

Three rows are exempt and classified by reasoning instead. popfq, iretq and syscall pass the writer probe cleanly and are still not definers, because their flags come from the stack, the interrupt frame, or an existing value masked through IA32_FMASK. Where a value came from is structural rather than measurable. A host that is not x86-64 declines the probe by name.

What a timing harness can and cannot assure

The leakage model has three channels, and no single sampling regime covers them (mach#2363):

The two harness modes need opposite sampling and neither substitutes for the other. Latency mode times a large batch of calls per sample, which is what lifts a running-time difference above clock resolution. That same batching hides an address-trace leak: every call in a batch is handed the same input, so after the first call both input classes are reading a warm cache line and the single cache miss carrying the signal is averaged away. Measured on one function, a secret-indexed read over a table larger than the last-level cache, latency mode scored |t| of about 1 to 15 across runs, straddling its own threshold so it neither confirmed nor denied, while address mode, at one call per sample, scored in the hundreds. Two consequences worth stating plainly:

• A clean latency-mode number for a table lookup is not evidence of address-trace safety. It is the wrong instrument for that channel.
• An address-trace leak is only measurable when the table exceeds the last-level cache. A cache-resident table leaks its index just as truly and no timing harness will see it. For small tables the property rests entirely on the secret-index gate and on reading the emitted code.

Where the check runs

The constant-time contract is checked at the IR level. The validator runs over the lowered, target-independent MIR before width legalization, instruction selection, register allocation, spilling, frame insertion, and encoding, and trusts those stages to be timing-preserving. What it refuses, it refuses closed: an operation it does not know, an out-of-range register reference, and inline assembly without a complete effect declaration are rejected, never defaulted to public.

A proof over the final allocated machine program, after selection, allocation, spills and frame insertion, over physical registers and flags, is planned additive work (mach#3591) and not something this version claims. Where mach does not own the later stages at all, as with a whole-module emitter such as SPIR-V, the contract is refused rather than assumed.