Security: exhaustive defense against scalable offense

Language models changed the economics of attack. An attacker with a model can read a million lines of code looking for one hole, while a defender has to hold every line. Attacks live in the complexity reviewers skip, and there is always more complexity than review. This page describes what kola does about that asymmetry and what it does not promise.

Make the surface a list

Writing more careful code does not close the gap, because review does not scale the way automated vulnerability search now does. kola's central security decision is to make the security-relevant surface of a program finite, enumerable and machine-readable, so that a defender (a person, or the same kind of model the attacker uses) can check all of it instead of sampling it. Exhaustive defense beats scalable offense only when the surface is a list rather than a codebase. In kola it is a list:

• Memory unsafety has no source construct. There is no unsafe, no FFI (foreign function interface: a way to call C code directly), no raw pointer, no extern and no inline assembly. What remains outside kola's checks is the compiler with its runtime and the hardware legs: C or assembly symbols named by an hw clause on a standard-library or package function. That set is enumerable: kola audit lists every leg, kola test --native runs each one against the function's kola body, a leg of a ct fn is disassembled and refused if it contains a conditional or indirect jump, and --no-hw builds without any of them.

• The ability to reach the world is the budget lines of package manifests. A package declares which capabilities it may take from the root set. kola audit fails when code exceeds the budget, and an unknown capability name is an error rather than an ignored typo. A pack with [caps] allowed = [] that is handed nothing cannot reach the network, the filesystem or the clock, by the type system rather than by policy.

• Behaviour is the effect rows on public signatures (Effects and capabilities). Reading a module's signatures tells you what it can do; there is nowhere else for authority or a side effect to hide.

• Trust in input is the untrusted marker. A parameter carrying wire, file, stdin or IPC bytes is marked untrusted, and no contract may depend on it. The section below explains why.

• Every run-time trap site is known to the compiler. kola report checks lists, per function, what was proven at compile time and what is still checked at run time. kola report reachable walks the same list from a program's entry points, across modules, and names what the walk could not follow.

• Randomness carries its provenance in the type. A value an adversary must not guess is an Entropy[[u8; N]], drawn from the OS on every call. The constructor that test vectors need, Entropy::of, is refused by kola audit on any path that does not start in a test. kola report secrets finds a compile-time constant reaching a Secret-typed position, which is to say a credential baked into the image.

kola query attack-surface emits the whole surface of a compilation unit as one JSON object, built from the compiler's own facts rather than from text search: every function that is handed a capability (granted capabilities, tokens derived from them and linear handles such as &Conn or &Dir, followed transitively through structs that carry them), every function that takes byte input while holding no authority, every function value crossing a boundary, every return that escapes a region, and every type that carries a capability.

A list like this is only useful if it is complete, and nobody runs a completeness claim written in prose. So the claim is a test: the compiler's suite synthesizes a probe function for every reserved capability and handle type, runs the enumeration, and checks that each one appears in the right class, with negative controls so that listing everything cannot pass. A new capability type joins the surface or the test fails naming it. The general lesson applies beyond this tool: wherever a security claim matters, make something execute it.

Remove the raw material

The bug classes automated hunters harvest in C cannot be expressed in kola: use-after-free (using memory after it was released), out-of-bounds access (reading or writing past the end of a buffer), double free (releasing the same memory twice) and silent integer overflow. Nothing in kola is undefined behaviour, the C notion of an operation whose result the language does not specify and the compiler may assume never happens (see the table in Why kola?). This matters especially for generated code. Plausible but subtly wrong is a statistical generator's natural failure mode, and in C that class becomes exploit material. In kola it becomes a deterministic trap: a bug that would have been remote code execution becomes a loud stop.

A domain block narrows how loud. A trap inside one tears down that block's region and runs its recover arm instead of killing the process, so a hostile request dies and the server keeps running. Recovery turns "the process dies" into "the request dies and someone has to fix it". A trap is still a bug, and kola audit counts every domain so that fault paths cannot be papered over quietly.

There is also no ambient authority to escalate into. A parser typed fn scan[r](p: &r [u8]) -> Verdict !{} cannot send what it parses anywhere, even if its body were written maliciously: it holds no capability, and its effect row proves it is pure. The working discipline for untrusted input follows from that. Code that processes bytes read through a capability is pure data processing, with no effects, up to the point where the input is validated. The standard library's protocol code is written this way.

A contract is a promise to a caller, and wire bytes have no caller

The most instructive hole kola has closed was in its own standard library, and it was not a memory bug. A transport function carried req packet.len >= 32, an ordinary precondition, where packet was a UDP payload straight off the wire. A crafted 20-byte packet would therefore trap, and on a freestanding build (one running with no operating system, as router firmware does) a trap halts the whole router. That is a remote denial of service, available before any authentication, from one packet. Every guarantee was working as designed, because contracts are enforced and a violated one is supposed to stop the program.

The fix rests on one sentence: a contract is a claim about the caller, and attacker-supplied bytes have no caller. Marking a parameter untrusted says exactly that, and the checker then refuses any contract that depends on it:

pub fn parse(untrusted pkt: &[u8]) -> u16 !{}
    req pkt.len >= 4
{
    0
}

The compiler answers error[card §8]: `req` depends on untrusted input `pkt` and tells you to check at run time and return Result or Option. Done that way, the length check is ordinary code, and it also gives the prover the fact it needs:

use std::encoding::bytes;

enum Frame { Ping, Data(u16) }

pub fn parse(untrusted pkt: &[u8]) -> Option[Frame] !{} {
    if pkt.len < 4 { return None; }
    let kind = bytes::rd16(pkt, 0);
    let len = bytes::rd16(pkt, 2);
    if kind == 1 { return Some(Frame::Ping); }
    if kind == 2 && widen[usize](len) + 4 == pkt.len { return Some(Frame::Data(len)); }
    None
}

test short_packet_is_refused_not_trapped {
    assert parse(&b"\x00\x01") == None;
    assert parse(&b"\x00\x01\x00\x00") == Some(Frame::Ping);
}

kola report checks on this file shows both rd16 preconditions as proven at their call sites. What makes the class hard to see by eye is that the dangerous condition usually sits beside a legitimate one in the same clause: a genuine caller obligation and an attacker-controlled length on one req line. kola report tainted-reqs finds candidates in existing code. The untrusted refusal at kola check looks only at the function that carries the marker; a contract three calls down in a codec is visible to kola report reachable, which walks the closure from the entry points.

Together with Secret[T] (data you must not reveal) and ct fn (code whose timing must not reveal), untrusted completes a data-trust axis expressed in types and checked by the compiler.

Contain what you don't control

A dependency gets only the capabilities its API is actually handed, and its manifest budget is enforced by the compiler and fails closed: a missing budget section means nothing is allowed. The audit works from the checker's effect facts, not from a text search.

Read the budget precisely. allowed says what a pack may take from the root set. Authority that a pack receives as an ordinary parameter is its caller's authority, so the audit prints it separately on a reaches: line: linear handles, granted directory and window tokens, and fn references whose effect row carries io or block. The budget is what the pack can mint; the reaches: line is what it was trusted with. A reviewer needs both. Listing Sys in a budget grants only Sys, not everything it contains. The practical consequence: a dependency update that suddenly wants network access fails the build until the top-level manifest grants it, and the review is a one-line diff. Packages are inert data until compiled; there are no install-time scripts.

Getting the code is a separate question. kola pack push signs a package, the registry stores and serves the signature, and kola pack fetch verifies it, pinning the publisher's key per package name on first use: the first key seen for a package is remembered, and a later release signed by a different key is refused. The trust anchor is the publisher; the registry is only a transport. An unsigned package from an https registry is a hard failure, with --allow-unsigned as the visible escape. kola security check <packdir> compares every dependency, and what it resolved to, against the registry's published advisories. The full package story is in Packages.

Every failure replays

All nondeterminism (time, randomness, I/O order, thread scheduling) flows through capabilities, so a security-relevant trap replays bit for bit from a seed under kola test --sim --seed N. A successful attack reduces to a seed and an input, and becomes a regression test.

The claims are attacked on purpose

The security model is falsifiable, and it has been falsified in places, deliberately. Adversarial review rounds set a model the task of breaking the guarantees. The first round found memory-safety breaks that existed only in the native backend while the interpreter trapped correctly, plus gaps in capability handling and in the audit; a later round on the fixed code found holes in the checker itself. Every finding was fixed with a regression test shown to fail without the fix. The structural lesson became architecture: the decision to drop a check now has exactly one site, the verified IR, and every backend reads it from there, so two backends cannot disagree about which checks were removed (IR-0). A passed round covers the attacks that were tried and no others, which is why the rounds continue.

Two working rules support this. A defect is not fixed until there is a test that fails when the fix is reverted. And a check that skips itself, or reports success for something it never ran, is treated as worse than no check, because it absorbs the attention that would have noticed the gap.

What the language cannot defend

• Wrong specifications. If a contract models the protocol or the hardware incorrectly, every proof built on it is confidently wrong. The mitigations are methodological: independent oracles, published test vectors, differential testing.

• Defects on both sides of a differential. Comparing two executors cannot find a bug they share, and a simulated test cannot settle a claim about a real socket or real hardware.

• Side channels beyond timing. A side channel leaks a secret through something other than the program's output, such as how long it takes or how much power the chip draws. Timing is addressed for cryptography by the compiler-checked constant-time subset (Constant time). Leaks through the CPU's speculative execution (work it does ahead of time and then discards) and through power consumption are out of scope.

• Hostile publishers. Budgets contain a hostile package; they do not make it absent. Who publishes is a social problem, which publisher pinning makes visible rather than solves.

• Progress. Every check is about traps. A loop that never advances passes kola report checks and hangs at run time, which an attacker who controls the input may be able to arrange.