MTK security decides who is acting, what a program may call, which records and fields a caller may touch, and where each result may go. The host grants services, the application declares its data rules in source, and the runtime carries protection through every computed value to every output.
Worked example
An HR assistant that cannot leak payroll
Corbin Freight runs its HR application on MTK for 2,300 employees. Dana Brooks manages the Great Plains region and reads the records of her 140 reports, but salaries belong to the four-person payroll team. Dana also uses an assistant agent that writes her a weekly team summary through an outside model endpoint. Payroll and tax fields must never reach that endpoint.
01
Dana signs in through Corbin's OIDC issuer. The workforce auth domain lists the sign-in methods it accepts and admits invited accounts only. The host holds the trusted issuers and their keys, so no application can hand itself an identity.
Her request for the region's employee records runs the trove's access block. Any member of the tenant reads names. Salary has its own property block: payroll reads it, and so does the employee on their own row. Dana's 140 rows come back with salary replaced by a fixed marker that carries no length or hint of the value.
Dana delegates the weekly summary to the assistant. Each hop of a delegation is one chain link that names the actor, the subject it acts for, the grant, the scope and the time window. The agent's reach is the intersection of Dana's grants, the delegation's scope and the agent's own grants, so it cannot read salary either.
04
The agent's first version opened the encrypted tax ID column and put it in the prompt. Opening an encrypted column yields a secret, and an outbound request refuses a secret. That version never compiled.
private chest summarize(text name, secret text taxId) {
chest[] headers = []
secret buffer prompt = t.buffer.fromText(`Summarize {name}, tax id {taxId}`)
return t.net.http.post("model", "/v1/summaries", headers, prompt)
# refuses: argument 4 holds a secret, and t.net.http.post refuses one there
}
05
The fixed agent sends name, title and office. Before dispatch the receiver compares the request's label with the model endpoint's ceiling, which is internal. A prompt derived from a restricted payroll field fails that comparison, and no byte of the request leaves.
What happened
Dana got her summary every Monday. The compiler refused the version that put a tax ID into a model prompt, and the destination check refuses any prompt labeled above the endpoint's ceiling. Outbound provenance and the security history record the agent as the actor and Dana as the subject it acted for.
Four checks on every action
Every read, write and output passes four checks. Each one starts from denial and needs its own grant, so passing one check carries no weight at the next.
The effective access is the intersection of the host's grant, the workload's grant, the caller's grants, the data policy and the protection rules. A role is a named set of grants, never a rank. Tenant membership, an administrator role, encryption and possession of a key each add nothing to a person's clearance.
Identity: who is acting, proven by a verified sign-in and the full delegation chain.
Authority: which libraries, stores and data operations the host and the application grant.
Protection: which labels, disclosure rules and value qualifiers travel with the data.
Destination: whether this exact receiver may get this output now.
Host grants and narrowing
A grant is the fixed list of libraries and services a running program may call. The host builds it at launch from two inputs: what the compiled code reaches, and what the operator lends. It never changes while the program runs.
Each host declares a default, the donor grant, and an operator narrows it in one of two ways. An admitting document names exactly the rows the deployment gets. A revoking document names the rows it loses. Neither can add a library the host never declared, and a narrowed folder must sit inside a declared one.
The two forms differ when a release adds a library. Under admit the new library stays absent until someone names it. Under revoke it arrives with the release. An air-gapped deployment admits. Each host declares which form it takes and refuses a document of the other form, and a document with both fields refuses.
A store slot binds a symbolic slot in the program to one table, on two axes. access covers rows: none, read, write or readWrite. database is a set of tokens for the typed companion, such as query for index reads and feed for change feeds. A slot that reads rows has said nothing about acknowledging a feed, which moves state another consumer reads.
Chest
Narrow a script grant
This invocation record revokes three libraries from the donor grant before main.tri runs. A revocation only removes access. If the script reaches t.math, the launch stops before main and names the library and the call that reached it.
chest grant = {
text[] revoke = ["t.math", "t.runtime", "t.text"]
u16 schemaVersion = 1
}
text operand = "main.tri"
Chest
Grant a store slot
The HR program reads employee rows and runs declared index queries. It cannot write a row, acknowledge a feed or maintain an index. A slot the program declares and the lend leaves unbound grants nothing and denies the call that tries it.
# _grant/grant.draft
u16 schemaVersion = 1
chest[] entryStoreSlots = [
{
u16 schemaVersion = 1
text name = "employee"
text table = "hr/employee"
text access = "read"
text[] database = ["query"]
}
]
Shell
Print the grant a program needs
tricli --reach summary.tri compiles the program and prints the smallest grant that covers it, without running it. The fixed summary program reaches t.buffer and t.net.http and nothing else, so a reviewer can compare the lend with what the code uses.
A library config is a library's own policy inside its grant row. The host writes the binding half: which folders, programs and credentials exist. The operator can only narrow it, and each library defines what narrowing means for its fields.
For t.proc, a narrower config keeps a subset of programs, may only add required leading arguments, and only lowers ceilings. For t.io, each anchor keeps its name and may only lose access. For t.log, the threshold only moves toward fewer levels. For the two security libraries, credential names and each credential's uses only shrink.
Chest
Limit child programs and their environment
The config admits git with status or log as the leading argument, sets the child's entire environment, and caps children, argument count and argument bytes. A prefix admits whatever follows it, so log -p passes too. An empty allowedPrograms list denies every spawn, and a secret in an argument or environment row refuses at compile.
chest config = {
u16 schemaVersion = 2
chest[] allowedPrograms = [
{ u16 schemaVersion = 1, text name = "git",
chest[] arguments = [
{ text[] prefix = ["status"] },
{ text[] prefix = ["log"] }
],
chest[] environment = [
{ text key = "HOME", text value = "/var/lib/myapp/home" },
{ text key = "PATH", text value = "/usr/bin" }
] }
]
u32 maxChildren = 4
u32 maxArgs = 16
u32 maxArgBytes = 4096
}
Chest
Give file access through a named anchor
The program sees one anchor, exports, and only reads from it. It names files relative to that anchor, and the host decides which directory the name means. Each ceiling bounds one dimension: bytes per read, bytes per write, list size and tree depth.
The program may seal and open under payroll-export and compare against payroll-webhook, and nothing else. A handle for an unlisted name refuses as denied. Each use is algorithm-specific, and reading a public key is a separate use from signing with it.
{
u16 schemaVersion = 1
text id = "t.security.secret"
chest? config = {
u16 schemaVersion = 1
chest[] credentials = [
{ text name = "payroll-export", text[] uses = ["open", "seal"] },
{ text name = "payroll-webhook", text[] uses = ["compare"] }
]
}
chest[] storeSlots = []
}
Keys, secrets and sealing
A key reaches a program as resource<t.security.crypto.key>, a handle that holds no key bytes. A handle cannot be printed, interpolated, stored in a record or written to a log. Process-held keys are aead, ed25519, hmacSha256 and p256, 32 bytes each, erased at the handle's last use. RSA keys, named secrets and recipient keys stay with their custodian, and the program spends only their granted uses.
secret qualifies a value that every output refuses at compile. Anything computed from a secret is secret. == and ordering refuse, because a byte-by-byte comparison leaks how much of a guess matched; t.buffer.constantTimeEqual and t.security.secret.compare answer in constant time. A secret written into source as a literal refuses outside a test unit, and so does any literal holding a private-key block.
A secret lives in a zeroing allocation and is wiped at its last use. A debugger snapshot and a fault document show secret(<length>), even under reveal. A secret can be stored only into an encrypted column.
expose() is the one step from a secret to plain data. In a development profile it is free. In a release profile the lend must name every function that calls it. Each call writes an audit row that reaches durable storage before the value moves. If the audit row cannot be written, the call faults and the value stays where it was.
sensitive is one level below secret, for values such as a session token or an email address. Logs, standard output, child-process arguments and lock keys refuse it. Responses, troves and comparisons accept it.
The secret qualifier tracks explicit flow: a branch on a secret compiles. Classification labels, described below, also carry the decisions a branch makes.
Trident
Use a granted key
The snippet assumes an aead sealing key, a separate Ed25519 signing key, and the aad, plaintext and message values. seal draws its own 24-byte nonce and returns XChaCha20-Poly1305 ciphertext with a 16-byte tag. open authenticates before it returns anything, and its result stays secret.
Corbin's payroll provider signs its webhook calls with a shared secret. The custodian holds that secret and answers only whether the presented bytes match. The program never sees the stored value or a digest of it.
Each line marked refuses stops the build with a message that names the sink and the fix. The comparison fix is t.buffer.constantTimeEqual(presented, stored), which returns a plain bool. The literal refuses because a key in source is a key in every clone of the repository.
private void audit(secret text salary) {
t.log.info(salary) # refuses: t.log.info refuses a secret
text copy = salary # refuses: copy is not declared secret
}
private bool same(secret buffer presented, secret buffer stored) {
return presented == stored # refuses: use t.buffer.constantTimeEqual
}
private void connect() {
secret text apiKey = "sk-4f2a9c" # refuses: a secret takes no source literal
}
Trident
Encrypt columns in the writing runtime
The writing runtime encrypts bankAccount before the value leaves the process, so the store, its log and its backups hold ciphertext. taxId is encrypted to the auditor recipient. Its blind token backs the unique index and reveals which rows share a tax ID, nothing more. Reading either column yields ciphertext, and open() yields a secret.
# _db/troves/employeeFile.tri
trove employeeFile {
sensitive = true
ref employee? employee = null
text bankAccount = "" with { encrypted, pii = true }
text taxId = "" with { encrypted = { to = auditor, blind = true } }
unique index byTaxId = taxId
}
Identity domains
An auth domain declares one group of accounts and how they sign in. Its declaration lives in the server's _auth folder. Issuers, audiences and claim maps live in the application's configuration, and secrets and trust ceilings live in the host's.
Sign-in runs a fixed sequence: protocol verification, stable subject, account link, account status, tenant membership, assurance policy and an authority fence. Only the complete sequence mints auth<workforce>, a proof that lasts for one delivery and has no literal, decoder or stored form. subject<workforce> is the durable reference a row keeps.
Each method proves what its protocol proves. OIDC uses the authorization code flow with PKCE S256, exact issuer and audience, and a nonce. A passkey checks a single-use challenge, origin, relying-party id and user verification. SSH keys verify through MerSSH, and a fingerprint alone grants nothing. A workload identity needs a trusted issuer and pins its credential and deployment generations.
Accounts link by exact issuer and case-sensitive subject; email and display names never merge accounts. Assurance is a set of established facts with no numeric ladder, and factors from different sessions never pool into a stronger one.
Host-owned trust
The host holds issuer keys, verifier configuration and trust state. A request never chooses its verifier, trust root, algorithm or key-fetch address.
Sessions
The session capability rotates after sign-in and after any change of authority. A reused refresh token cannot produce two live sessions.
Development sign-in
A development-class host admits synthetic accounts from declared seeds, with authorization and audit intact. A release-class launch rejects that source.
Trident
Require a verified member at the entry
The member fact comes from verified claim mapping, never from a request field. Once an application declares an auth domain, every external entry states public admission or a named policy. An entry that states neither refuses at compile.
handle rename(const ctx, text name)
require (ctx.auth.member, "workforce member") {
member.update(ctx.auth.account, { displayName = name })
}
on auth(workforce, const authNotice notice) {
# Enforcement and terminal cleanup already belong to the mechanism.
}
Trident
Store a password as a verifier
A pwhash is a salted Argon2id verifier with no ==, no order and no conversion to text. The presented password is a resource of the request being handled, so no document, row, log or recording ever holds it. A login under outdated parameters re-hashes in place.
trove account {
text<length=[1,32]> name = ""
server pwhash? passwordHash = null
unique index byName = name
}
# login: the handler of an endpoint whose `password` row is withheld
resource<t.net.http.serve.presented> pw = t.net.http.serve.presented("password")
bool ok = t.security.crypto.passwordCompare(account.passwordHash, pw)
if (ok && t.security.crypto.passwordStale(account.passwordHash)) {
account.passwordHash = t.security.crypto.passwordHash(pw)
}
Record and property access
A trove's access block holds pure predicates for read, insert, update and delete. A missing predicate denies its operation. Relation leaves such as tenant.payroll(who.subject) read declared tenant relations, never a boolean the caller supplies.
A property block narrows one field. A field with no property root takes the trove's root, and a stated root intersects it, so a property can only be stricter than its row. Reading salary never implies editing it.
An update passes the access check on the old row and on the final merged row. A caller cannot make itself the owner to pass. A denied field write fails the whole mutation.
A query discloses only its authorized projection. Counts, sort keys, aggregates, joins, page boundaries and unique-key conflicts keep the protection of every field they touch. A forbidden row and an absent row look the same to an ordinary reader, so probing for hidden records learns nothing.
Read is not write
An owner can read their own salary and still cannot change it. Editing needs the trove's HR rule and the property's payroll rule together.
Insert-only ingestion
An intake service can hold insert access with no read access. Its ability to publish output is a separate grant.
Caches and cursors
Cached reads, cursors and feeds recheck before each page or delivery. A narrowed grant blocks the old generation at once, even while new data loads.
Classification
A security domain declares ordered levels and independent compartments once. organization.label(restricted, legal) is a label with level restricted and compartment legal. A label is ordinary data and grants nothing by itself.
Label A dominates label B when both use the same domain instance, A's level is at least B's, and A holds every compartment of B. Joining two labels takes the higher level and the union of compartments. A reader cleared for restricted with finance cannot read a field labeled restricted with legal.
A trove sets a protection floor, a row's protectionBy column may raise it, and a property may raise it again. The effective label of a field is the join of all three. Changing a row's classification takes its own audited permission and never happens through an ordinary field write.
A person's clearance bounds what they read. The value's own protection bounds where it may be written. A cleared reader can write public data from public inputs, and reading restricted data never licenses a later public write.
Trident
Define levels and label sensitive fields
Every row starts at public. summary is at least internal, and contactIdentity is restricted in the legal compartment. Only compliance can read or update contactIdentity, and that property rule and the label check both apply.
The compiler proves static restrictions, and the runtime carries protection on every value it computes. Authors calculate with money, text and records as usual and never label an intermediate by hand.
Control decisions carry protection too. A comparison, branch, loop bound, array index or early return joins the labels of what it observed into the call's observation watermark. Every later effect in that call carries the watermark, even a constant message, so a restricted value cannot decide whether a public log line appears.
Every protected effect names an admitted destination. The destination must dominate every source label and satisfy every disclosure clause. The host rejects a governed launch when a reachable output lacks a complete protection contract. It never falls back to a plain file or another provider.
Encryption never lowers a label. Ciphertext keeps its classification and disclosure clauses, so restricted data stays out of a lower-cleared cache, backup or replica whatever the transport.
HTTP responses, peers, consoles and outside services: exact receiver, purpose and label ceiling, checked on every delivery.
Files: a protected scope the host lends; no raw export strips a label.
Child processes, model requests, agents and tools: the provider and its retention terms are the destination. Running on the same machine grants no clearance.
Rendering and devices: scene inputs join their labels; frames, captures and audio are outputs.
Logs, metrics, traces, recordings and debugger views: projection happens before retention, and the secret and sensitive rules still apply.
Caches, backups, replicas and migrations: labels follow the bytes, and the host's placement ceiling covers every copy.
Trident
A log refuses a sensitive value
sensitive keeps tokens and personal data out of logs and standard output. The same value still compares and can reach a response or a trove. Writing one to a log on purpose takes its expose() or its pseudonym.
private bool signedIn(sensitive text sessionToken, sensitive text stored) {
sensitive text line = `session {sessionToken} opened`
t.log.info(line) # refuses: a log takes no sensitive value
return sessionToken == stored
}
Release decisions
A release lowers protection for one exact artifact, one destination and one policy generation. There is no downgrade mode. A release declaration lives in the server's _security folder. It names the source domains, the protection the output receives, a pure transformation, the destination family, the approval rule and the reason.
The request binds the source artifact, the transformed artifact, both protections and the exact destination. Approval refers to the digest of that complete request. Change one byte of the report, the transformation, the policy or the receiver, and the approval no longer applies.
A rule that needs two approvers needs two distinct live subjects with two distinct real actors, so delegation cannot manufacture a second approver. The receipt reaches durable confirmation before any byte leaves, and it cannot be copied to cover another payload, destination or session. Only the selected output loses the approved protection; the rest of the call stays protected.
sourceArtifact and transformedArtifact: SHA-256 digests of the data before and after the release transformation.
transformationIdentity: the digest of the pure transformation that produced the output.
sourceProtection and proposedProtection: the protection the data carries and the protection the output receives.
destination: the exact receiver, as a descriptor rather than a family.
declarationIdentity and imageIdentity: digests of the release declaration and of the policy image in force.
authorityDependencies: the grants and approvals the decision rests on, so revoking one revokes the release.
reason and correlationId: why the release happened, and the id that ties it to the audit trail.
Delegation
An agent acts under its own account, or for a person through explicit delegation. Its reach is the intersection of the person's grants, the delegation's scope, the agent's own grants, the application policy and the host limits. Redelegation is denied unless a grant names it.
The chain keeps every hop. A rule that requires a human examines the whole chain, so an agent acting for Dana stays agent-originated. A person who assumes an agent's account stays the actual actor.
Owning an agent gives no permission. Jobs store a grant reference, never a live session, and reauthorize at each attempt and each effect.
Live assumption lets a help-desk actor act as a user for a stated purpose, tenant and time limit. Access is the intersection of the user's authority and the actor's own help-desk grant. The user's MFA, device proof and keys never transfer, and an assumed session cannot create credentials, change roles, delegate or nest another assumption.
rolePreview
A synthetic subject with a declared role, over isolated fixtures. Writes and outside effects stay simulated.
subjectPreview
An authorized snapshot of a real user's data, with no live credentials and no production output routes.
liveRead
Reads and presentation as the user, under a purpose-bound grant. No mutation through any helper, trigger or job.
liveAct
Named effects as the user, within both the user's authority and the actor's grant. Every effect records the real actor.
Revocation and audit
Revocation orders against effects. A generation check and the effect it guards share one admission interval, so nothing admitted after a revocation's fence takes effect. Narrowing invalidates cached reads, cursors, queues, watches and pending output at once.
A delivery that read protected data keeps the authority it read under. If that authority changes, the runtime aborts the delivery before its next protected effect or output. Security time and revocation keep running while a debugger pauses the program.
A protected change and its security receipt commit in one Store transaction. If the audit row cannot prepare, the change does not happen. The security trove is append-only for every application and runtime caller, and sealed checkpoints anchor to an outside witness.
Isolation between protection domains
One application can serve several protection scopes. The host chooses the deployment boundary, and the policy stays in the application's source.
When restricted plaintext must never enter a lower-trust process, put the two in separate processes or on separate hardware. Two application instances in one heap share one boundary.
These controls govern data and effects inside the admitted executable and its providers. Protection from a hostile kernel, a modified executable, timing side channels or physical access comes from the process, scheduling and hardware boundaries the deployment supplies. Labels cannot manufacture those boundaries.
Property rules in one deployment
Row and property access, disclosure clauses and checked outputs, with no ranked domain. Fits an HR or billing application.
Mixed labels in one deployment
The host, engine, memory, store and providers are admitted for the highest label they process. Each delivery checks its own labels and clauses.
Separate deployments per scope
The same application runs in distinct domain instances with distinct stores. No session, cache or subject spelling bridges them; exchange takes a sender release, a receiver import and an explicit level mapping.
Preview and development
Preview runs in an isolated domain instance with synthetic entitlements. A development grant cannot open production snapshots, and replay never mints a live release.