Skip to content
aien-devPublic

About

Security-critical network code rewritten in Omega, so decades-old bug classes (out-of-bounds access, integer overflow, unbounded reads) cannot happen silently. First project: server-side Tailnet Lock for self-hosted Tailscale control servers.

Resources

Contributing

Security policy

Stars

0 stars

Watchers

0 watching

Forks

Repository files navigation

omnet

Security-critical network code, rewritten in Omega.

Most serious vulnerabilities in network software over the last several decades come from a short list of bug classes: out-of-bounds reads and writes, integer overflow, unbounded reads and loops, use-after-free, and check-then-use races. omnet rewrites security-critical parts of network infrastructure in a language where the first group cannot happen silently. Its design rules target the rest.

The first project is Tailnet Lock for self-hosted Tailscale (Headscale) control servers. Tailnet Lock (TKA) lets the devices of a tailnet, not the control server, decide which devices may join. The stock Tailscale client already implements the device side. The open-source control server headscale does not implement the server side (headscale#1307). omnet builds that server-side logic in Omega.

What the language rules out, and what it does not

Facts below are from the Omega language reference, docs/one_layer/OMEGESE.md §9, at the pinned commit in omega.pin.

Bug class Omega behaviour
Out-of-bounds array access Every index that is not a constant is checked when it runs: trap 3. Constant indices outside the array are refused at compile time. Kernel I/O checks its buffer range before the call.
Signed integer overflow Signed add sub mul neg div shl trap 1 when the exact result does not fit.
Lossy conversion A conversion to a type that cannot hold the value traps 5. There are no implicit conversions.
Bad shifts, division by zero A shift outside 0 .. width-1 traps 7; division by zero traps 2.
Unbounded loops Every loop has a bound (default 1,000,000 passes); passing it traps 4.
Heap corruption, use-after-free There is no heap allocator and no exposed pointer. Arrays have a fixed length that travels with the name. Local arrays are freed under compile-time ownership checks.
Stack exhaustion A call or local array that would overrun the fixed 8 MiB stack traps 6 before writing.

An unsized view T * / edit T * parameter is a pointer plus a count. Every index into it is checked at run time and the count travels with it, so the bounds rule above holds for slices as well (OM-2 guarantee matrix lives in the Omega repository, at the pinned commit). A trap stops the program. That turns memory corruption into a crash, so a reachable trap is still a denial-of-service bug.

Bounded by the code, with a test that shows it:

  • Store record sizes and running totals are charged with checked arithmetic and held under a 65536 record cap and a 33554432 byte cap; an over-capacity write is refused and the registry stays readable (registry capacity guard test).
  • A file path is used to open a descriptor, and the work then continues on the descriptor, never on a path checked earlier (design rule 2). Rename, short-write and crash paths are exercised by fault tests.

Still open, and handled by review:

  • Logic and protocol errors, including wrong authorization decisions.
  • Timing side channels. omnet code is not constant-time-audited; the secret comparison bounds how many bytes are read, not how long it takes.
  • Unsigned arithmetic wraps by definition. Checked arithmetic applies only where a module uses it.

Reduced but not eliminated:

  • Resource exhaustion at the service level: too many clients or too much stored state.

Design rules for omnet code

  1. Bounded input. Every read has an explicit capacity, and every message has a maximum size that is checked before it is parsed.
  2. No check-then-use on names. Act on an opened descriptor, never on a path checked earlier.
  3. Fail closed. Parse errors and signature failures reject. Compatibility behavior must match the pinned protocol: unknown signed AUM kinds advance the hash chain as no-ops, as Tailscale specifies; they never bypass authorization.
  4. Least privilege. A component that parses untrusted input runs without the privileges of the component that acts on the result.
  5. Two referees. Each algorithm is checked against published test vectors and against an independent implementation used only as a test oracle (never shipped). Every test harness has a mutant check that proves it can fail.

Layout

Path Content
om/<unit>/<unit>.om Omega library: functions only, no globals, no main
om/<unit>/test/ Program-mode test driver, vectors, run.sh
cmd/tkad/ Native Omega local daemon, RPC handlers, recovery and real-socket tests
tools/build-tkad.sh Builds the daemon with the pinned compiler
integration/headscale/ Pinned Headscale v0.29.6 adapter patch, build script and trust contract
integration/e2e/ Unmodified Tailscale v1.102.0 client builds and isolated lifecycle harness
docs/design/ Design documents
tools/omc.sh Builds the pinned seed-born Omega compiler and verifies its digest
tools/test.sh Runs library and daemon suites

Build and test

Requirements: Linux on ARM64 (the Omega compiler emits AArch64 Linux programs), git, POSIX sh, Python 3, and Go >=1.26.5 for the TKA differential oracle. Omega holds all TKA logic; the optional Headscale adapter is Go glue and uses Go1.27.3.

tools/test.sh      # builds the pinned compiler on first use, then runs every unit's tests

Status

The Omega daemon implements all eight TKA RPCs, node registry/map operations, durable snapshots, and validated restart recovery over a private Unix socket. Its local adapter is trusted and must run as the same UID; the daemon does not authenticate remote Tailscale clients.

The current profile supports one tailnet, 64 nodes, 128 authority updates and 64-KiB JSON messages. The Headscale adapter and stock-client control-plane lifecycle have passed isolated end-to-end verification, including unsigned-peer filtering, authenticated rotation, authority-key removal, persistence, owner authorization, outage rejection and disablement. This is not deployed tailnet protection, data-plane qualification or a production security audit. Build with tools/build-tkad.sh; see cmd/tkad/README.md and integration/headscale/README.md before running.

See docs/design/tailnet-lock.md for the implementation limits, verification plan, and remaining stages.

License

Apache-2.0. See LICENSE.

About

Security-critical network code rewritten in Omega, so decades-old bug classes (out-of-bounds access, integer overflow, unbounded reads) cannot happen silently. First project: server-side Tailnet Lock for self-hosted Tailscale control servers.

Resources

Contributing

Security policy

Stars

0 stars

Watchers

0 watching

Forks

Releases

Packages

Used by

Contributors

Languages