pravo id and pravo protect

Quick reference

Protection is off by default. A state with protection off is unchanged: format 1, with the layout that every version of pravo reads. These commands turn protection on for one state, show where it stands and keep it in line with the list of readers. What sealing protects says what the seal covers and what it leaves open.

A state has three formats.

pravo protect init --encrypt takes a state from format 1 to format 3. A pravo that does not know format 3 refuses the state with state at LOCATION was written by a newer pravo (format 3).

Subcommands

Flags

Exit codes

The readers file

.pravo/access/readers.txt in the repository lists who may read the state, one line for each reader:

NAME ssh-ed25519 BASE64 x25519:BASE64URL

Whoever can merge a change to this file decides who may read. Writers take the list from the checked-out repository and never from the state, so a person who can only write to the bucket cannot add themselves. Commit the file.

pravo looks for the file in --access-dir, then in $PRAVO_ACCESS_DIR, then in .pravo/access of the root, then in the same place in each parent directory up to the directory that holds .git. Outside a repository it looks in the root only.

A command that writes a sealed state compares the file with the readers recorded in the state. If they differ, it stops with exit code 5 and .pravo/access/readers.txt and the state differ (dan added, fay removed). Run pravo protect rewrap. A command that only reads prints the same text as a warning on standard error. A missing file stops a command that writes the state with exit code 5, and an invalid one with exit code 6. The protect commands exit with 6 for both: protect check, init and rewrap have no verdict without a valid file. protect status prints file not found or file is invalid: and exits 0.

A state that is not sealed in a repository that has a readers file is refused in the same way. A command that writes stops with exit code 5 and the repository lists readers in .pravo/access/readers.txt, but the state is not sealed: it has not been sealed yet, or its meta.json was changed. Run pravo protect status; to seal it, pravo protect init --encrypt; if the state is not meant to be sealed, remove the readers file. A state that does not exist yet is refused before anything is created: the command stops with exit code 5 and the repository lists readers in .pravo/access/readers.txt, but the state does not exist yet. Create it sealed with: pravo protect init --encrypt. A command that only reads prints the text as a warning, and creates no state. A file that is found counts whether or not it can be read. protect check, protect init, protect status and the id commands are not stopped. A root in a repository whose readers file is meant for other roots names another access directory with --access-dir or $PRAVO_ACCESS_DIR, and is then not expected to be sealed.

The identity

An identity is a name, a signing key and a reader key. The reader key opens the sealed state. The signing key is part of the line in the readers file and is not used while the state has no roles.

The identity directory is not ~/.pravo, which is the provider cache and may be deleted.

pravo finds the identity in this order: --identity NAME, $PRAVO_IDENTITY, then the files of the identity directory. When there are several files, it uses the one named like the user. If none is, it uses the one file whose reader key has a lock in the current group of the state, which meta.json lists. For protect init, which has no locks yet, the reader key is one of the readers file. The reader key of an identity file is public: choosing reads no passphrase, and only the chosen identity is asked for its passphrase. If no file or more than one matches, the command stops with no identity found: ... holds several identities (ada dan) and none is named like you, and names the files that match when there are several. Name one with --identity. The same choice is made for the state of another root that pravo.#RemoteOutputs reads, by the locks in that state's meta.json. pravo looks only when the state is sealed, so a state with protection off never asks for a passphrase.

A passphrase is asked for on the terminal without echo. Without a terminal it is read from $PRAVO_PASSPHRASE or $PRAVO_IDENTITY_PASSPHRASE, and a command with neither stops with the identity ada is sealed with a passphrase and stdin is not a terminal; set PRAVO_PASSPHRASE. pravo removes PRAVO_IDENTITY, PRAVO_PASSPHRASE and PRAVO_IDENTITY_PASSPHRASE from its environment once it has read them, and provider processes are started without them. pravo mcp never asks on a terminal: the identity of a server comes from the environment it was started in.

The recovery recipient

A recovery recipient is one more reader of a sealed state whose key nobody holds whole. The key is made when the recovery is set, split into N shares by Shamir secret sharing, and forgotten. Any K of the shares rebuild it, and fewer give nothing. Every group of the state carries a lock for its public key, so that K holders of shares can open the state when every reader has lost their key.

A command that is interrupted after it set the recovery in the state keeps the shares and writes the recovery file, and says so: the lock is there, and the shares are the only way in. Shares of a key that the state does not hold are removed. With --json, rewrap and recover write the files first and report a recovery object: action (set, replaced, from_file or removed), k, n, key, file and, for new shares, shares.

Nothing opens the lock of the recovery key until the shares are used, so the lock carries a keyed check under the data key of its group. A reader, and so every command that writes the state, sees a box that someone with no data key changed: the command stops with exit code 5, protect status says which groups, and protect rewrap makes the lock again. The check shows that the box is the one a reader made. It does not show that the shares open it, so rehearse once: copy the bucket, and run protect recover against the copy with K shares.

Two commands that change the recovery at once do not both succeed. The one that finds the recovery changed since it read the state writes nothing, removes the shares it wrote and exits with code 3; the other one's shares are the ones that open the state.

A share file holds one line, pravo-share-1, the id of the key, the index, K/N, the share and a short check that catches a mistyped or damaged line, after two lines of comment.

A command that writes a sealed state compares the recovery file with the state, as it compares the readers file, and stops with exit code 5 when they disagree:

A recovery file that does not load stops a command that writes with exit code 6. A command that only reads prints the same text as a warning.

Setting a recovery is a decision about trust. K holders of shares can read the state together, and nothing delays them: there is no signature and no waiting time until roles exist. A recovery key that was used has been rebuilt on one machine, so replace it afterwards. The shares of a replaced key open nothing that is sealed from then on: replacing or removing the recovery makes a new data key, as removing a reader does, so a holder of old shares who kept a copy of the bucket opens what was in it and nothing written after. A reader may not hold the recovery key: rewrap refuses a readers file that lists it.

id new

pravo id new makes a reader key and a signing key, writes the identity to NAME in the identity directory, and prints the line for the readers file. It asks for a passphrase twice, at least 8 characters. It touches no state, and anyone can run it at any time.

Identity ada created
  signing  ssh-ed25519 SHA256:<fingerprint>  new key, kept in the identity file
  reader   x25519:<key>  sealed with a passphrase in people/ada/id/ada

Give whoever keeps .pravo/access/readers.txt this line, and nothing else:

  ada ssh-ed25519 <ssh-key> x25519:<key>

The line is public and safe to paste into a chat or a pull request. Give it to whoever keeps the readers file.

An identity is never overwritten. pravo id new --name ada for a name that exists stops with identity ada already exists at PATH and exit code 1, before it asks for a passphrase.

--ssh FILE uses an ssh-ed25519 public key as the signing key, so that there is no new signing key to manage. pravo reads FILE.pub, or FILE if that is itself a public key, and never reads a private key. Keys of other types are refused.

For a CI job

A job has no person to type a passphrase. --ci makes an identity with no passphrase and writes it to the file named by --out, with mode 0600. It writes nothing to the identity directory. --out is required with --ci and refused without it. An existing file is not overwritten.

Identity deploy-bot created for a job. It has no passphrase: protect the file.
  private  deploy-bot.identity   (store it as the CI secret PRAVO_IDENTITY, then delete this file)
  public   deploy-bot ssh-ed25519 <ssh-key> x25519:<key>

--ci requires --name, and id new --ci without it stops with exit code 1. A default taken from the operating system user would be the name of a person, and a name is used once in the readers file, so give each job a name of its own.

Store the contents of the file as the secret PRAVO_IDENTITY of the job, then delete the file. Use one identity for each job, and never a person's identity in a job. Add the public line to the readers file and run pravo protect rewrap. The identity is the authority of the job in pravo and is not its cloud credential.

id show

pravo id show prints the signing key, the reader key and the line for the readers file. It reads the public part of the file and does not ask for the passphrase.

Identity ada (people/ada/id/ada)
  signing  ssh-ed25519 SHA256:<fingerprint>  new key, kept in the identity file
  reader   x25519:<key>  sealed with a passphrase

Give whoever keeps .pravo/access/readers.txt this line, and nothing else:

  ada ssh-ed25519 <ssh-key> x25519:<key>

With --json, id new and id show print one document with name, path, signing (alg, fingerprint, source), reader and line.

protect check

pravo protect check reads the store and says whether it can be sealed. It writes nothing to the state. It tests the store harder than the probe that every command makes (S3-compatible stores): eight writers replace one object at once and exactly one must win, and a key that has just been written must be in the listing. It then lists what is running now.

package ws

$settings: state: {
	backend:    "s3"
	bucket:     "northwind-state"
	prefix:     "prod"
	region:     "eu-west-1"
	endpoint:   "http://127.0.0.1:9000"
	path_style: true
}

Store            s3://northwind-state/prod  (eu-west-1)
Conditional      create-only ok · replace ok · delete ok
                 8 concurrent replaces: 1 winner · listing sees a new key at once
State            0 records · format 1
Readers file     not found (looked in .pravo/access)
Running          0 transactions · 0 locks held
Machines         no writer in the last 30 days
exit=6

A state in a local directory is refused: its compare-and-swap is a lock of one user, so two users of one directory would not be excluded. --allow-local accepts a directory that only you use. A state that is already sealed prints Already sealed. Use pravo protect status.

protect init

pravo protect init --encrypt seals the state. It needs the readers file and an identity that is on it, because sealing to a list that you are not on would lock you out: the command stops with exit code 5 otherwise. A state that does not exist yet is created sealed, with no records.

It shows what it will do and asks Proceed? [y/N]. --yes answers it. Without a terminal and without --yes it refuses to ask. Nothing is written before the answer. The command does not run while a transaction is running or a lock is held. Run it while nobody plans or applies.

1. Every record is written once as the object rec/SHA256, and resources/ADDRESS.json becomes a pointer to it. A record is never overwritten again.
2. The attributes and the private data of each record are encrypted with one data key, which is locked for each reader.
3. outputs.json, the values of the stored plans, the values in the command lines of transactions and the text of the errors of transactions that failed are sealed the same way. The words of a command and the names of its flags stay readable, and so does a positional argument. The value of a flag that takes one is sealed, written --flag value or --flag=value, unless it is a flag with a public value such as --limit, --ttl, --only, --out, --policy or --chdir. A word after a flag that takes no value is a positional argument. A secret belongs in -t.
4. The state is set to format 3, and meta.json holds the locks.

--recovery K/N also sets a recovery recipient: a lock for a key that is split into N shares, any K of which rebuild it. The shares are written to recovery-shares/ before the state is touched, so that a seal that fails leaves no recovery lock that nobody can open, and the public key is written to .pravo/access/recovery.txt when the seal is done. The prompt lists it as one more step. The recovery recipient says what to do with the files.

A run that is interrupted leaves the state in the middle of sealing, and an earlier pravo cannot open it. A kill leaves it where it was. An interrupt (Ctrl-C) finishes the records that are being sealed, starts no other and ends with interrupted after N records were sealed in this run. Run the command again to finish: it skips the records it has done. pravo protect status says migrating until then, and commands that write the state refuse with a seal is in progress; run pravo protect init --encrypt to finish. Commit the readers file when the command ends.

ada ssh-ed25519 <ssh-key> x25519:<key>
dan ssh-ed25519 <ssh-key> x25519:<key>

Readers  .pravo/access/readers.txt  (ada dan)
This will:
  1  write 2 records as immutable objects  rec/<sha256>
  2  encrypt their attributes and private data to 2 readers (ada dan)
  3  seal outputs.json, stored-plan values and the values in transaction command lines the same way
  4  set the state to format 3. Earlier versions of pravo will refuse it
store check passed
2 records sealed in <time> s
outputs sealed · recipients written to meta.json

The state is sealed to ada dan.

Commit the readers file. Writers read the list from git:
  .pravo/access/readers.txt
No recovery recipient. If every reader loses their key, the state cannot be read.
Add one with: pravo protect rewrap --recovery 3/5

A state that is already sealed prints Already sealed (format 3). Use pravo protect rewrap to change the readers. and writes nothing. Without --recovery there is no recovery recipient, and the command prints No recovery recipient. with the consequence and the line that adds one, pravo protect rewrap --recovery 3/5.

protect status

pravo protect status is the command to run when you are unsure. It opens the state with your identity, checks every record against its name and every pointer against its record, and prints one screen. It writes nothing.

Sealed       on · format 3 · 2 readers (ada dan) · recovery none
Store        s3://northwind-state/prod
Readers      .pravo/access/readers.txt matches the store
You          ada · reader key x25519:<key>
Roles        off
Unsettled    none

With --json, status prints one document: state (none for a state that does not exist yet, off, immutable, migrating or sealed), format (absent when there is no state), store, records, checked, unsettled, untrusted, readers (the names the state is sealed to), readers_file (found, valid, matches, path, added, removed), recovery (k, n, key, locked, and file: match, differs, missing or invalid, present only when the state has a recovery) and you for a sealed state, and expects_sealed: true when the repository lists readers and the state is not sealed, which includes a state that does not exist yet. A job that wants a verdict before it plans runs pravo protect status --json | jq -e '.format == 3'.

A record that does not match its name, a pointer that disagrees with its record, or a sealed value that does not open where it is, prints Untrusted: and the object, and the command exits 7.

protect rewrap

pravo protect rewrap compares the readers file with the readers the state is sealed to, and changes the state to match. It needs an identity that is a reader, and the readers file. It does not need the readers to agree to anything, and it rewrites meta.json only. If another command changes meta.json while it runs, rewrap reads it again and repeats; if it keeps changing, rewrap stops and asks you to run it again. A state with nothing to change prints The store already matches the readers file.

Adding a reader. The new reader makes an identity and sends the line it prints. A reader adds the line to the file, commits it and runs rewrap. The data keys are locked for the new reader in every group, so that the new reader can open what is already there. No record is rewritten.

Removing a reader. A reader who is removed loses their lock in every group, and the state gets a new data key. Records are sealed under it as they are next written. Until then they stay under the old key. --all seals every record, the outputs, the stored plans and the sealed text of the errors of transactions again under the new key at once. A copy of the state that was made before the removal still opens with the removed reader's key, and the reader has read what they read. Replace the secrets they could read where they live.

--all needs the state at rest: run it while nobody plans or applies. It seals again and deletes the records that are sealed in another group and that no pointer names. It does not remove the old groups from meta.json, and the last record of a resource that was destroyed or removed with state rm stays in rec/, sealed under the group it was written in. pravo protect gc removes both. What sealing protects lists what stays in the bucket.

The recovery. --recovery K/N sets the recovery recipient of the state, or replaces it: a new key is made, split into N shares and written to recovery-shares/, the public key goes to .pravo/access/recovery.txt, and every group gets a lock for it. A replaced key loses its lock in every group and the state gets a new data key, so its shares open nothing that is written afterwards; a copy of the bucket made before still opens with them, so collect and destroy them. --remove-recovery takes the recovery out of the state and deletes the file; commit the deletion. Both ask first, unless --yes is given. --remove-recovery also deletes a recovery file when the state has no recovery. Without either flag, a recovery file that names a key that the state does not have is set in the state with no new shares, and a recovery lock that is missing from a group is made again. --all and a replacement of the recovery run as two steps when the recovery key opens the state; protect recover does that for you.

protect recover

pravo protect recover --share FILE --share FILE … opens a state with the shares of its recovery key when no reader can, and makes the readers of the state the readers in the readers file. It is the way back when every reader has lost their key.

1. Make an identity: pravo id new --name NAME.
2. Write its line to the readers file in place of the lines of the readers who are lost.
3. Collect K share files from their holders, and run pravo protect recover --share a.txt --share b.txt.

The command rebuilds the recovery key in memory, checks it against the public key in meta.json, shows what it will do and asks Proceed? [y/N]. It then opens the state with that key, locks the data keys for the new readers, removes the old ones and makes a new data key, as rewrap does, and writes meta.json. Commit the readers file. It does not read the readers file for a verdict first: a state is recovered when no identity can open it.

Recovery key rebuilt from 2 shares.
Readers  .pravo/access/readers.txt  (eve)
This will:
  1  lock the data keys for eve
  2  remove ada dan, and make a new data key
meta.json updated
New data keys for 1 reader group. Records are sealed again as they are next written.
The recovery key was rebuilt on this machine. Replace it: pravo protect rewrap --recovery K/N

--all seals every record, the outputs and the stored plans again under the new key, and does not run while a command is running or a lock is held. --recovery K/N also replaces the recovery key, in a second step after the records are sealed again, and writes the new shares; without it the old recovery stays and the command says to replace it. A recovery key that was rebuilt has been seen in one place.

protect gc

pravo protect gc deletes what a state of format 2 or 3 keeps and nothing reads. A state of format 1 keeps one object for each resource, and the command says that it has nothing to collect. It works in two parts, and a state that is not sealed has the first only.

Records. A write never overwrites a record. The bucket therefore keeps every revision of every record, the record of a resource that was destroyed or removed with pravo state rm, and the record that a write left when it failed. In format 2 these hold their attributes in the clear. A record that no pointer names is garbage once it is older than the grace, 24 hours or --older-than, and two collections have found it so. The age is the newest of the times updated_at, refreshed_at and applied_at in the record, which are readable without a key. A record that shows none of them is kept, and so is an object in rec/ that does not match its name: the command lists it and does not touch it. A record that a pointer names is never deleted.

Nothing names a record from the time a writer has made it until the writer replaces the pointer. Two things protect that interval. The grace covers a writer that is stopped between the two writes, as long as the record carries the time it was written at. It is never shorter than 65 seconds: twice the 30 seconds that a command goes on sealing in the group it opened with after a rewrap, and five more. The age is read from the record, so it is the clock of the machine that wrote the record against the clock of the machine that collects: gc needs the clocks of the machines that write to agree to within the grace. Give --older-than more than the skew of the clocks you have.

Some writers copy a record with the times it already had: pravo protect rewrap --all, pravo protect init and pravo state push and pull write every record, old times included, and the pointers after. The grace says nothing of such a record, so a collection is in two phases. A collection that finds an old record unnamed marks it in the object gc/marks.json and deletes nothing. A collection at least 15 minutes later deletes the records that are still unnamed and that it marked, and drops the marks of the ones that a pointer names or that are gone. A writer that finishes inside 15 minutes is therefore never caught between its record and its pointer. The 15 minutes are judged by clocks as well: a mark holds the time of the machine that wrote it, and the collection that decides compares it with its own clock. A machine whose clock is ahead of the one that marked shortens the interval by the difference, and a collection from machines whose clocks differ by a large part of 15 minutes can delete a record whose writer is still between its record and its pointer. Run gc from one machine, or keep the clocks of the machines that run it, as well as of those that write, close to each other. The first collection of a state prints Marked 3 records that no pointer names. A collection at least 15m later deletes the ones that are still unnamed. and a collection inside the 15 minutes keeps what it marked. A copy of the state does not carry the marks, and --dry-run reads them and writes nothing, so it does not create them either.

The command lists the pointers again right before it deletes, and deletes a record only if it still holds the bytes it judged, so a record that was named or replaced meanwhile stays. This part needs no key, and it does not need the state at rest. It can run while commands run, and two collections that run at the same time lose no mark that matters.

Groups. rewrap leaves the old groups in meta.json, with a lock for each reader that is left, and a command opens one lock for each group. The data key of a reader who was removed still opens whatever is sealed in the group they were in. gc drops a group, other than the current one, when nothing is sealed in it: no record that a pointer names, no record that the first part spared, not outputs.json, no object of a stored plan, and no sealed text of the error of a transaction that failed. Run pravo protect rewrap --all first, so that everything is under the current group, and give a command that opened the state before the rewrap time to finish: while the last change of the readers is younger than 65 seconds, gc keeps every group and says so, because such a command still seals in the old group and a record sealed in a group that meta.json does not list any more stops the state from opening. A stored plan that an apply uses is left by rewrap --all, and keeps its group until the apply is done and rewrap --all runs again. A group with something in it is kept, and the command says what. A dropped group is gone from meta.json and the history gets the entry gc. A removed reader then holds a key that opens nothing that is left. A copy of the bucket made before still opens with it, and so does a version of meta.json that a bucket which keeps old versions of its objects holds: the deleted records stay there too until the lifecycle rules of the bucket remove them.

This part needs an identity that is a reader, the readers file (a command that writes a sealed state compares it with the state, as above) and the state at rest: no transaction is running and no lock is held. With no identity, or one that is not a reader, gc collects the records, says Groups were not looked at and exits with 0. With a command running it collects the records and exits with 4. With a readers file that is missing, invalid or different from the state it collects the records and exits with 5 or 6, as any command that writes a sealed state does. --dry-run writes nothing, so it warns of the same readers file and exits with 0; a lock that is held still gives 4.

The example waits for those 65 seconds, because the state was sealed just before.

No record is garbage: a pointer names every record.
No group needs to be dropped: the state has only its current group.

With --json, gc prints one document: format, dry_run, older_than_seconds, settle_seconds (15 minutes, 900), records (listed, named, unnamed, young, unknown_age, marked, settling, deleted, bytes and foreign) and, for a sealed state, groups (examined, dropped, kept with id, records, unnamed_records, outputs, plans and summaries, and skipped with the reason when the groups were not looked at).

A stored plan that an apply holds a claim on is left as it is. --all counts these plans and prints 2 stored plans in use were not sealed again; run pravo protect rewrap --all when they are done. With --json the count is plans_skipped.

See also

• Seal the state to a list of readers walks through it.
• What sealing protects lists what the seal covers and what it leaves open.
• State format describes the files of each format.
• Exit codes lists code 7.
• Global flags, environment and exit codes lists the variables.