Sessions and namespaces

A session is a person’s or agent’s working environment on the box: one beamlet VM in one budget, with a namespace and capabilities the steward built for it. A namespace is the session’s own map from path prefixes to capabilities; it is built before the session starts, nothing in it is inherited, and there is no global file tree behind it. This page covers logging in over SSH, what a session is, vault sessions, namespaces and binds, and approve@, the one terminal where a person grants authority.

Purpose

A session is the unit a person works in and the unit Redoubt keeps apart. Alice’s session and Bob’s are different VMs in different budgets, and each reaches only what its namespace and handles name. So the questions this page answers are the ones a person asks first: how do I get in, what can my session reach and why, how do I work with data that must not leak, and where do I say yes when something asks for more.

How to use it

Log in with your own SSH key. The user name picks the session:

$ ssh alice@box            # an ordinary session: Alice's unlabelled data
$ ssh alice+tax@box        # a vault session carrying Alice's `tax` label
$ ssh alice.work@box       # a second ordinary session beside the first: Alice's context `work`
$ ssh alice+tax.work@box   # the context `work` of the `tax` vault, another context again
$ ssh approve@box          # the approval terminal: only the steward talks here

At the prompt, the session’s namespace is a table you can print:

/home/alice (1)> ns()
/boot          bootfsd
/home/alice
/net
/dev/cons
steward
budget
bootfsd
erofsd:system
/home/alice (2)> File.ls!("/home/alice")
["notes.txt", "src"]
/home/alice (3)> File.read("/home/bob/notes.txt")
{:error, :enoent}

A line with a / is a path the session reaches, with the handle’s name beside it when the same handle was also handed by name (/boot is bootfsd); a line without one is a named handle: the steward’s grant to this session, the session’s own budget, and the system volume beamlet loads its modules from.

bind/2 makes a connection the session already holds appear at another prefix. It creates no authority, only a name:

/home/alice (4)> {home, _rest} = ns_lookup("/home/alice")
/home/alice (5)> bind("/h", home)
:ok
/home/alice (6)> File.ls!("/h/src")                  # the same files as /home/alice/src

Leaving the session with exit ends it: the steward destroys the session’s budget, and every process in it ends with it. Closing the SSH terminal instead detaches it, and the next login of the same context reattaches it; a context is one session at a time, so a second ssh alice.work@box while the first is open takes it over (contexts).

What it can and cannot do

Logging in

Status: built · tested: bench:steward-ssh-two-principals, bench:steward-login-refused, bench:steward-context-login, bench:userland-boot

sshd (the SSH server) accepts a connection, and sshd and the steward authenticate the person with the principal’s login key. In M1 (sessions over SSH, kept apart) the principals and their keys come from the boot manifest (init). A login key is the person’s own: it stays on their machine or security key and never lives in keyd (the key server). sshd refuses authentication with any public key keyd holds, so a hijacked session that can sign with keyd cannot log in as anyone (sshd).

The steward then starts the session: it carves a budget for it under the principal’s budget, builds its namespace from the principal’s capabilities, and launches a beamlet VM in it (the steward). Each principal has one fixed sub-budget per label set, and sessions are carved from the one that matches their labels, so a flood of sessions in one label set cannot starve another.

Contexts

Status: built · tested: bench:steward-context-login, host:redoubt-sshd::the_login_grammar, host:redoubt-sshd::only_a_pty_channel_s_end_of_input_closes_the_terminal, host:redoubt-steward::context_free_holds_one_session_per_name, bench:steward-session-ends, bench:steward-context-labels, bench:sshd-restart-detaches, host:redoubt-consrelay::an_attach_cuts_to_a_line_says_what_was_dropped_and_replays, host:redoubt-consrelay::the_vm_s_size_is_the_channel_s_and_an_attach_redraws, bench:steward-context-cap, bench:steward-context-idle, bench:shell-contexts, bench:steward-restart-context, bench:steward-login-timing

A context is a named session of one principal in one label set. The SSH user name is principal[+label][.context], in that order only: alice is Alice’s default context, alice.work her context work, alice+tax.work the context work of her tax vault. Each part is 1 to 64 bytes of lower-case ASCII letters, digits, _ and -, starting with a letter, with no case folding; . is the separator, not :, which scp, sftp and rsync read as the start of a path. Contexts are not declared: a login names one, and the first login makes it.

• Its identity is (principal, label set, name). alice.work and alice+tax.work are two contexts, each carved from its own label set’s sub-budget, so a context never crosses from one label set to another.
• One session at a time (the steward). A second login naming a context reaches its session rather than making another; while that session is still starting, the login is refused. Once the session has ended, the name is free again.
• Closing SSH detaches. Closing the terminal of a session with a pty (an interactive ssh) leaves the context’s VM running; what it writes meanwhile is kept, the newest 64 KiB (consrelay). The next ssh alice.work@box reattaches: [context work: reattached], a line saying how many bytes were dropped if any were, then the kept output; the relay answers the VM’s waiting resize with the new terminal’s size. exit at the prompt ends the context. If sshd itself restarts, every attached context is detached the same way. Without a pty (ssh alice@box < file) the end of the input is the end of the file the shell reads, as before, not a closed terminal.
• A second terminal takes over. A login to a context attached elsewhere takes it: the old terminal is told [context work taken over from ADDRESS at up 2h13m] and closed (one that has stopped reading may be closed untold), and the new one is told where it was taken from (R80 (one channel per context)).
• No enumeration. A key that is not the principal’s, a principal or a label set the manifest does not give, and a name outside the grammar all get the same refusal, so its content says nothing about which names exist. Its timing is not made equal: inside the steward’s one call, an unknown principal or label set, or a name outside the grammar, is refused before any of its machines runs, and a wrong key for a known principal runs the blame and session machines before the key check refuses it; nothing is counted. Measured at the client, the three kinds’ median refusals lie within a millisecond of each other, inside their spread (the steward).
• Reserved names take no suffix. approve is the approval terminal’s name: no principal takes it, and approve+x and approve.x are not logins.
• A cap per label set (R82 (the context cap)). A principal has at most a set number of live contexts in each label set, attached or detached, the console’s session counted where it runs: by default what the label set’s share of the principal’s budget holds, or fewer if the manifest says so. A login that would make one more is refused like any other refusal; nothing running is ended to make room. In the image alice has two SSH contexts beside the console, three in her vault, and bob two; agent is the image’s principal for a sponsor-run agent, sponsored by alice: its session is a lease of hers, carved from her unlabelled share (so it counts among her contexts there), with a home of its own and no labels and no network scope (agents).
• Idle contexts end (R83 (idle contexts end)). A context left detached for its principal’s idle bound, by default a day, ends with everything in it. An attached context never does, and each attach starts the count again.
• From the prompt. contexts() lists the session’s label set’s contexts, detach() closes the terminal and leaves the context running, and end_context(name) ends one (the shell). Another label set’s contexts are never shown, and its names are unknown.
• A steward restart ends them. Contexts end with the steward; after it restarts, a login makes a new context, however it is named (the steward).

A session is a VM in a budget

Status: built · tested: bench:steward-ssh-two-principals, bench:steward-session-ends, bench:steward-sub-budget-flood

One session is one beamlet VM, in one budget of class user, under the principal’s budget (budgets). What that gives:

• Everything the session does is paid for there. Every page, process and share of the CPU it uses is charged to the session’s budget or to a budget carved from it (R6 (charging)). A session cannot spend Bob’s pages. Its VM’s two schedulers are threads of its one process: on several harts they run at once, and the kernel charges each hart’s run to the session’s budget, so the session’s share is its weight’s however many harts it uses (beamlet).
• Every call it makes says who it is. The kernel stamps each message with the budget’s account (the principal it bills to) and label set; the session cannot choose either (R14 (unforgeable sender)). Servers admit and check calls by that (account, label set).
• Ending it ends everything in it. Logout, a lost connection, or the steward ending the session destroys its budget. Every process in it ends, every handle stamped with it dies wherever copies went, and nothing outside it is touched (R10 (destruction)).
• One VM is one trust domain. Everything typed at the prompt, every script and every Erlang process in the VM runs with the session’s full authority. Code that must have less (an agent, an untrusted parser) runs in a VM or native program of its own, in a budget of its own (agents, native programs).

There is no root and no sudo. “Admin” means holding specific capabilities over shared things, and a session holds only what its principal was granted.

Vault sessions

Status: built · partly tested: a vault session’s own reads and writes wait for its namespace to reach the VM; the label check they meet at walfsd is attacked on its own · tested: bench:steward-vault-session, bench:steward-vault-launch, bench:steward-sub-budget-flood, bench:walfsd-label-check, host:redoubt-steward-server::a_vault_login_carves_from_the_vault_s_sub_budget_and_has_no_network

A vault session carries one of its principal’s labels: ssh alice+tax@box starts a session whose budget has Alice’s tax label. A budget’s labels are fixed when it is created and only grow downward (I6 (labels only grow downward)), so nothing started inside a vault session can shed the label. A program the session launches runs in a budget carved from the session’s with the same labels, which are the only ones the kernel lets a session’s child carry: it writes its standard output and error to pipes of the session’s, which the session draws on its own channel, and to nothing unlabelled (native programs). It holds no console of its own: the M1 (sessions over SSH, kept apart) residual, a launched program reading and writing the session’s console past the shell, is closed.

What the label changes, per the label rule of the servers (labels):

• It can read unlabelled data and data carrying tax: reading needs the caller’s labels to include the object’s.
• It can write only data carrying exactly tax: writing needs the labels to be equal. So it can read Alice’s home volume and cannot write a byte to it.
• It cannot send to an unlabelled process at all (R1 (flow)), and servers that are sinks refuse it: ipd (the TCP/IP server) refuses every labelled caller, so a vault session has no network, and its gen_tcp connect is {error, eacces}, the refusal’s name (beamlet).

What it shows on the SSH channel reaches only Alice, who owns the label; sshd keeps each channel’s labels, and a labelled channel is its owner’s terminal only, with no forwarding, no subsystems (so no file transfer: file transfer) and no exec. Data leaves the label only by declassification: a request to the steward, approved by the label’s owner at approve@ (the steward).

Namespaces

Status: built · partly tested: on the box the cases show which connections the steward made and in which budget, and a session’s paths are walked once its namespace reaches the VM; the binding table, slot by slot, is host-tested · tested: bench:steward-ssh-two-principals, bench:steward-vault-session, bench:steward-home-quota, host:redoubt-steward-server::a_login_runs_the_session_batch_and_answers_the_session, host:redoubt-steward-server::a_vault_login_carves_from_the_vault_s_sub_budget_and_has_no_network

A namespace is a table inside the process: path prefixes, each naming a capability (a 9P connection) the process holds. The launcher writes it into the child’s startup block before the child starts (processes); for a session, the launcher is the steward. There is no mount call and no kernel mount table: the kernel knows handles, never paths.

flowchart LR
    subgraph S["Alice's session: one beamlet VM"]
        direction TB
        subgraph NS["namespace: prefix to connection"]
            h["/home/alice"]
            c["/dev/cons"]
            b["/boot"]
            n["/net"]
        end
        subgraph NH["named handles"]
            st["steward"]
            bu["budget: the session's own budget"]
            sy["erofsd:system"]
        end
    end
    h --> FS["walfsd, Alice's home volume"]
    c --> SH["sshd, this SSH channel"]
    b --> BF["bootfsd, read-only"]
    n --> IP["ipd, a scope of hosts and ports"]
    st --> ST["the steward, this session's grant"]
    sy --> SY["erofsd, the system volume, read-only"]

Figure: a session’s namespace. Each entry is a connection the session holds; a path reaches only what an entry names, so /home/bob/notes.txt, which no entry is a prefix of, is enoent.

What follows from a table of capabilities:

• A path resolves by its longest matching prefix, and the rest of the path is walked on that connection. /dev/cons/x goes to the console’s connection with x left over.
• Nothing is inherited. A path whose prefix names nothing the session holds is :enoent, not a permission error: there is nothing there to refuse.
• Above the entries is a directory the namespace answers itself. / or /home, above an entry and inside none, lists the next name of each entry below it, and nothing in it can be removed or written (:eacces); making it is :eexist, as it is there, so File.mkdir_p passes through it; /home/bob, beside /home/alice, is still :enoent.
• .. never climbs out. Paths are cleaned lexically before lookup, in the client and again in the server, so /../../etc is /etc on the same connection.
• Different prefixes are usually different servers. /home/alice and a vault’s volume are two connections, so a rename between them is a copy and a remove, never atomic (files).
• A home holds its principal’s quota, whatever its sessions. Every session of Alice’s, her console session and her named contexts among them, is minted through the one connection the steward carved at her home with her home_quota, so together they hold at most that many bytes; a write past it is :enospc, and Bob’s home on the same volume keeps its own (home quotas and vaults). A vault has no quota of its own: it is its labelled volume, bounded by its room.
• A copy of a connection is the same connection. All holders of a handle share one badge and one set of open files, so a launcher never passes its own connection to a child: it asks the server for a fresh one with new_connection, and disconnects it when the child’s exit notice arrives (the serving library).

Binds. bind/2 puts a connection the session already holds at another prefix. It needs no server and creates no authority. A namespace is the session’s own: binding in it changes nothing for any other process, and a child sees only the table its launcher wrote for it (files and binds).

What a session is told

Status: built · partly tested: a plain session and a vault session read theirs on the machine; a named context’s is host-tested only · tested: bench:shell-commands, host:beamlet-redoubt::a_sessions_identity_is_read_from_its_arguments, host:beamlet-redoubt::the_platform_tells_a_session_its_identity, host:beamlet-vm::the_identity_is_the_platforms_and_without_a_system_is_not_supported, host:redoubt-steward-server::a_sessions_arguments_name_its_principal_labels_context_and_home, host:redoubt-steward-server::a_sessions_launch_is_told_its_context

A session’s VM learns what it is from its launch arguments, which the launcher writes into its startup block, as the steward does for every session it launches (the steward): principal=NAME; label=NAME:ID, one for each label of its set, in the set’s order; context=NAME for a named context, none for the principal’s default one or the console’s session; and home=/PATH, the path the session’s namespace binds the principal’s home at, for a vault session as for a plain one, none for a principal with no home or for a vault session in a confined boot, whose home slot binds nothing (the steward). beamlet reads them once at its start and gives them to Elixir as redoubt:identity/0 (beamlet); beside them a session is launched with the named handle notices, the receive right of the endpoint the steward tells it a lease’s end on, and a shared server’s restart, which the shell serves from its start, re-binding the slot the restart named through the steward (Redoubt.Shell.Notices; the steward, failure and restart); a VM started without principal= is no session and gets not_found, and one whose home= is not a clean absolute path, or comes twice, is told nothing either. They are fixed for the VM’s life, and they are information, not authority: the label set the kernel stamps is redoubt:labels/0, and what the session can reach is its handles, whatever the arguments say; the shell starts in the home named, and can only because the namespace reaches it (the shell). A session that could rewrite them would lie only to itself.

How a program reads its namespace

For native programs the namespace table exists in code: redoubt-rt (the native runtime) parses the startup block and resolves paths against it (libs/rt/src/startup.rs, libs/rt/src/path.rs).

• The block names the handles process_start installed (slots 1 to n, at most MAX_START_HANDLES, 128), namespace entries (a handle and a clean absolute path), named handles (a handle and a name) and the arguments. Paths are unique, names are unique, and a block that breaks any rule is refused whole: the parent may be hostile.
• resolve returns the entry with the longest matching prefix and what is left of the path; a prefix matches only at a / boundary, so /dev/consx does not match /dev/cons. A relative path resolves to nothing.
• clean resolves . and .. lexically and never climbs above the root: ../../etc/passwd is etc/passwd. A name longer than 255 bytes or holding a NUL, and a path deeper than 64 components, are refused.
• A named handle’s name is lower-case ASCII letters, digits and _:+-, starting with a letter, at most 64 bytes (walfsd:data, alice+secrets).
• A program started with an empty namespace fails cleanly: the echo client exits with its error code, and the echo server with NO_ENDPOINT, instead of reaching anything.

approve@

Status: built · partly tested: a labelled agent’s request and a note; a declassification waits for the steward’s declassification and push · tested: bench:steward-approve-box, bench:steward-screen-inert, bench:steward-pending-cap

ssh approve@box is the approval terminal. When an agent asks its sponsor for more authority, or a session asks for a declassification, the request goes to the steward, and the requester’s own terminal only shows that an approval is waiting. The person answers at approve@, where only the steward talks to the terminal, so the requester can never draw on the screen the person decides from (the steward).

• The person’s own key. approve@ authenticates with the person’s own SSH key, which never lives in keyd. A session’s network capabilities never include the box’s own addresses, so a hijacked session cannot reach approve@ over loopback.
• What is shown is rendered by the steward from the structured request: who asks (its kind, such as agent or session, and its steward-given name, agent-7), what, where, for how long, and the label consequences. Every field is printable ASCII, escaped and length-capped. A labelled requester’s free text is never shown; an unlabelled requester’s is quoted and marked untrusted.
• What is approved is bound: each request has a random 64-bit id and a hash of its exact content, and approving confirms both: approve ID HASH, the hash in full or as the eight-character code the screen shows beside it, which the steward expands only from the last screen it wrote on that channel (sshd). An approval grants no more than the approver holds. The requester’s own sessions print [an approval is waiting] and nothing of the request.

In M3 (agents, approvals and the attack suite) approve@ is served by the same sshd as every other channel. That is a stated residual: a bug in the SSH code reached from any channel could control the approval screen, and a network flood can delay approvals (sshd). The design protects the approval channel from the requester; it does not protect the person’s judgment, and an approval that grants more than the person intended is a wall the design names, not one it closes (agents).

Why

Sessions are budgets because budgets are what the kernel enforces. The kernel knows nothing about people. It knows budgets, which pay for everything and whose destruction revokes everything, and label sets, which it checks on every message. Making a session a budget with a label set means the separation between Alice and Bob is the kernel’s, and ending a session is one call that cannot leave anything behind.

Namespaces instead of a file tree. A global file tree with permission bits asks every server to decide, per path, who may do what, and a mistake anywhere is a leak everywhere. A namespace of capabilities asks one question once, at launch: what does this process get. A path that is not in the table does not exist for that process, so there is nothing to probe, and a child can be given a narrower table than its parent by writing fewer entries. Plan 9 showed that per-process namespaces make a usable system; Redoubt adds that every entry is a capability.

Approval out of band. If an approval could happen in the requester’s own terminal, a hijacked session could draw a fake prompt, or answer it. Putting approvals behind a separate login, with the person’s own key, rendered only by the steward, makes the channel something the requester cannot touch. The human is still a wall that can be talked into things; the design says so rather than hide it.