Skip to content

nish:secret: let a Secret be a field of a class that owns its wipe (lift NL2430) #668

Closed

Description

@amritk

Follow-up to #430, whose tracking run is #626.

Why

#430 moved every TLS and QUIC key holder onto volatile wipes at each end of life (#639, #652, #653, #664, #665). Two findings stay Open, narrowed because of one rule: a Secret may not be a field (NL2430, reject_secret_field).

  • TLS-1 (docs/security/tls.md). An open connection's secrets sit in TlsServer/TlsRecordServer fields as plain u8[]:

    • the traffic secrets kept for KeyUpdate;
    • the exporter and resumption secrets;
    • the caller's ephemeral key until the ServerHello is written.

    They are wiped at every end, but the checker does not stop code from reading, comparing, logging or forgetting to wipe them.

  • QUIC-1 (docs/security/quic.md). A QuicKeys from quicKeys/quicKeysUpdate is a plain class. A caller that keeps it or drops it without quicKeysWipe leaves the keys in the arena, and nothing refuses that.

Today the guarantees nish:secret gives a local stop at the field boundary:

  • no template, builtin, ===, condition, index or member;
  • wiped or returned on every path.

A field-held Secret would extend them to the state a connection keeps between calls.

What lifting NL2430 has to answer

The path-by-path rule ("a Secret leaves the function that made it returned or wiped", NL2439–NL2446) is lexical. A field outlives every lexical scope, so the rule needs an owner that is not a scope. Each of these is a decision, not a detail:

  1. Who wipes, and when it is proven. A class holding a Secret field needs a wipe obligation the checker can discharge. Candidates:

    • (a) The holder must be bound with using, so its dispose runs at scope end. This reuses the existing using machinery, and the holder's lifetime becomes lexical again.
    • (b) The class declares a wipe()/release() method that must wipe every Secret field, and the holder object itself becomes linear under NL2439–NL2446: made, then released or returned on every path. That is a much larger analysis.
    • (c) A runtime-only rule: arena/scope teardown wipes Secret fields. That gives no static proof, and frees outside an arena are not covered.
  2. Aliasing of the holder. A second reference to the holder (const a = conn, an array of holders, a Map value, a closure capture, a task argument) is a second name for the key. The NL2512 alias walk would have to cover holders as well as raw bytes.

  3. Every way in (CLAUDE.md, "A checker rule covers every way in"):

    Each shape needs its own negative case. These are exactly the shapes that reached soundness holes in feat(checker): Mutex<T>, a lock that owns its data, in nish/threads #562 and feat(checker): Channel<T> of scalars, closed when its senders return, in nish/threads #566 after review rounds had passed them.

  4. Field reads. A field Secret read inside expose/exposeWith must not move it out (this.k stays owned), and assigning over a held field needs an NL2442-style "wipe first" rule.

  5. Struct copies and wipe(record). wipe already takes a record of integers. Decide whether a record containing a Secret may be copied at all.

Downsides and costs

  • Soundness risk. This is the highest-risk kind of checker change in the repo. The current rule is small and easy to audit, while an object-lifetime rule has many entry points (see 2 and 3). Expect several adversarial review rounds and many reject_secret_* negatives.
  • The proof can be weaker than today's runtime wipe. Under option (a), a connection that lives across calls in a pool slot (TlsTcpServer, QuicConnection slots) cannot be using-bound, so the slot design may need restructuring or an escape hatch. An escape hatch would bring back the hole this issue is meant to close.
  • Rolling freeze. src/ cannot use the construct until the next release. That does not matter for std/, but the self-host compiler cannot dogfood it soon.
  • Migration churn. Moving the TLS/QUIC holders to Secret fields touches the same files fix(tls): wipe every key a TLS connection holds when it ends #652, fix(quic): wipe a connection's packet keys and AES schedules when a level, generation or connection ends #653 and feat(crypto)!: TLS and QUIC one-shot key derivations take and answer Secret #665 just stabilised:
    • their read-back tests and -O2 counts move;
    • the goldens move;
    • the security records are rewritten again.
  • Language-stability surface. Lifting a restriction is not a break, but the new obligations (which using binding, which release) become rules users must learn. They need a docs/LANGUAGE.md rule, a cookbook entry and a guide page.
  • The benefit is a compile-time guarantee, not new wiping. The bytes in TLS-1 and QUIC-1 are already volatile-wiped at every end, and pinned by -O2 and read-back tests. What this adds is that the checker refuses misuse and forgotten wipes.

Acceptance (sketch)

  • A docs/LANGUAGE.md "Secrets" rule replaces NL2430 with the chosen ownership model. It comes with a golden .ll, a native round trip, negatives for each way in (constructor move, this escape, holder alias, using declarators, field overwrite, field read outside expose), and a cookbook and guide entry.
  • TlsServer/TlsRecordServer's traffic, exporter and resumption secrets and QuicKeys hold Secret fields, with no expected.out change and with -O2 and read-back pins kept.
  • TLS-1 and QUIC-1 are closed in their records, and Move the QUIC and TLS key-holding structs onto nish:secret #430 is closed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions