Hashing and cryptography

The hash and crypto operations hash values, encrypt and decrypt them, hash and check passwords, sign and check messages, and check tokens and one-time codes. Each job has one construction, chosen to be safe, so you never choose an algorithm.

A clinic seals each clinical note to its own record, hashes its staff's passwords, checks the webhooks its payment provider sends with the secret they share, and signs the receipts it issues. The keys are settings, each given as a call's key: and read nowhere else:

config {    notes_key: EncryptionKey    payments_webhook_secret: SigningKey    receipt_key: PrivateKey}

type ClinicalNote = Text {    max_length: 4000}type NoteId = Text {}type SealedNote = Bytes {}type StaffPassword = Password {    min_length: 12    max_length: 128}type WebhookBody = Text {    max_length: 100000}type WebhookSignature = Bytes {}type Receipt = Text {    max_length: 2000}type ReceiptSignature = Bytes {}type Genuine = Bool {}type NoteUnreadable = Failure {    kind: FailureKind.invalid_value}/// A clinical note sealed to its own record, so it can't be moved to/// another.action seal_note(note: ClinicalNote, record: NoteId) -> SealedNote {    return SealedNote(crypto.encrypt(note, key: config.notes_key, context: record))}/// A sealed note's text: another record's id, an altered note or another/// key can't open it.function open_note(sealed_note: SealedNote, record: NoteId) fails NoteUnreadable -> ClinicalNote {    var note_bytes: Bytes = attempt crypto.decrypt(        sealed_note,        key: config.notes_key,        context: record    ) {        unreadable: NoteUnreadable    }    var note_text: Text = attempt encoding.from_utf8(note_bytes) {        malformed: NoteUnreadable    }    return attempt ClinicalNote(note_text) {        max_length: NoteUnreadable    }}/// The hash a member of staff's password is stored as.action stored_password(staff_password: StaffPassword) -> PasswordHash {    return crypto.hash_password(staff_password)}/// Whether a password signs in; `correct_outdated` asks for a fresh hash.function sign_in_check(staff_password: StaffPassword, stored_hash: PasswordHash) -> PasswordCheck {    return crypto.verify_password(staff_password, stored_hash)}/// The signature on a webhook the clinic sends to the payment provider.function webhook_signature(body: WebhookBody) -> WebhookSignature {    return WebhookSignature(crypto.hmac(body, key: config.payments_webhook_secret))}/// Whether a webhook came from the payment provider, which shares the/// secret.function from_provider(body: WebhookBody, provider_signature: WebhookSignature) -> Genuine {    return Genuine(        crypto.verify_hmac(body, provider_signature, key: config.payments_webhook_secret)    )}/// A receipt's signature, which anyone with the clinic's public key can/// check.function receipt_signature(receipt: Receipt) -> ReceiptSignature {    return ReceiptSignature(crypto.sign(receipt, key: config.receipt_key))}/// The clinic's public key, which it publishes so anyone can check its/// receipts.function clinic_public_key() -> PublicKey {    return crypto.public_key(key: config.receipt_key)}/// Whether a receipt was signed with the private half of `issuer_key`.function receipt_from(    receipt: Receipt,    claimed_signature: ReceiptSignature,    issuer_key: PublicKey) -> Genuine {    return Genuine(crypto.verify_signature(receipt, claimed_signature, issuer_key))}

A test run makes its own throwaway keys, and its nonces and salts come from the test's seed, as random's values do. The older hash is the same password at 4 MiB and 3 passes, and the signature is RFC 8032's second test vector, the message r under its key:

test "a sealed note opens only for its own record" {    var sealed_copy: SealedNote = seal_note("Allergic to penicillin.", "note-1")    var read_back: ClinicalNote = attempt open_note(sealed_copy, "note-1")    assert read_back == "Allergic to penicillin."    assert open_note(sealed_copy, "note-2") fails NoteUnreadable    assert seal_note("Allergic to penicillin.", "note-1") != sealed_copy}test "a password signs in, and an older hash asks for a fresh one" {    var stored_hash: PasswordHash = stored_password("correct horse battery staple")    assert sign_in_check("correct horse battery staple", stored_hash) == PasswordCheck.correct    assert sign_in_check("correct horse battery stapler", stored_hash) == PasswordCheck.wrong    assert sign_in_check(        "correct horse battery staple",        "$argon2id$v=19$m=4096,t=3,p=1$AAECAwQFBgcICQoLDA0ODw$VTsSHiMxkq48zEo8LUSymjr7JjaRSgsxGX2Z8HQE9Cw"    ) == PasswordCheck.correct_outdated}test "a webhook is checked against its signature" {    var body: WebhookBody = "{\"paid\": true}"    assert from_provider(body, webhook_signature(body))    assert not from_provider("{\"paid\": false}", webhook_signature(body))}test "a receipt's signature checks with its issuer's public key" {    var rfc_signature_bytes: Bytes = attempt encoding.from_hex(        "92a009a9f0d4cab8720e820b5f642540a2b27b5416503f8fb3762223ebdb69da085ac1e43e15996e458f3613d0f11d8c387b2eaeb4302aeeb00d291612bb0c00"    ) {        malformed: NoteUnreadable    }    var rfc_signature: ReceiptSignature = ReceiptSignature(rfc_signature_bytes)    assert receipt_from("r", rfc_signature, "PUAXw-hDiVqStwqnTRt-vJyYLM8uxJaMwM1V8Sr0Zgw")    assert not receipt_from("R", rfc_signature, "PUAXw-hDiVqStwqnTRt-vJyYLM8uxJaMwM1V8Sr0Zgw")    assert text.length(encoding.to_hex(receipt_signature("r"))) == 128}test "what the clinic signs checks with the key it publishes" {    var paid_signature: ReceiptSignature = receipt_signature("Paid in full.")    assert receipt_from("Paid in full.", paid_signature, clinic_public_key())    assert not receipt_from("Paid in part.", paid_signature, clinic_public_key())}

One construction for each job

A release that changes a construction keeps reading the old format, by the sealed value's version byte or the password hash's PHC string, and correct_outdated tells your app to hash a password again when its owner signs in. Sign-in and identity leaves checking a password to your application, which is why it needs these operations.

Keys are settings that code never reads

Code never reads a secret (Secrets), and a key is no exception. A key is an opaque value, held in a setting, or as data:

• an EncryptionKey setting (32 random bytes) for encrypt and decrypt;
• a SigningKey setting (Signing keys) for hmac;
• a PrivateKey setting (an Ed25519 key's 32 bytes) for sign and public_key.

You write each key by name, key: config.<name>, and nowhere else. That makes a crypto operation's key: one of the places the compiler owns, alongside those Secrets lists. A key given by position, or read anywhere else, is still configuration.secret_flow, whose message names the one place the key goes. A key: given anything but a setting or a key held as data, such as a parameter or text, is type.mismatch.

Reading a key anywhere but a key: is configuration.secret_flow, even to take a fingerprint of it:

type KeyFingerprint = Bytes {}config {    notes_key: EncryptionKey}/// A fingerprint of the notes key, to tell in a log which key is in use.function key_fingerprint() -> KeyFingerprint {    return KeyFingerprint(hash.sha256(config.notes_key))}

  |9 |     return KeyFingerprint(hash.sha256(config.notes_key))  |                                       ^^^^^^^^^^^^^^^^ a key, read here

An EncryptionKey rotates as a SigningKey does, through a NAME_PREVIOUS setting. A PrivateKey reads no _PREVIOUS: whoever checks a signature holds the public key, so rotating one is the verifiers' job.

An EncryptionKey or PrivateKey setting's environment variable holds its 32 bytes as unpadded Base64url, 43 characters. Anything else is refused at startup, by the check before the app starts (Checking values before the app starts). hmac and verify_hmac use a SigningKey's text bytes directly as the HMAC key, so an outside system that shares the secret can check what your app signs.

A key is never a value

EncryptionKey, PrivateKey and SigningKey are built-in secret types. A key has no text and no JSON form (for json.write and json.read): the secret rule wins over the contract's "never". Code never builds a key from a value it can see, and building a key type from a value is type.constructor_input.

A setting holds most keys, but a key can also be held as data, one per device or person. crypto.new_key(as: EncryptionKey) makes one in an action: 32 bytes from the host's generator, the same whichever key type as: names. It is opaque, so it does two things. It is stored in a field of a key type, which keeps it sealed, or it is given as a crypto call's key:, straight from a record's field, a var holding it or a name a match binds it to. It may wait in a var on the way to either:

application {    connections: {        main: {            driver: Driver.postgres            url: config.database_url        }    }    field_encryption_key: config.field_encryption_key}

/// A clinician's tablet, with a key of its own.entity Tablet {    id: Uuid    device_key: EncryptionKey    policy: {        create: [Access.public]        read: [Access.public]    }}

use field/entities { Tablet }/// Enrols a tablet, making its key, which is stored sealed.action enrol_device() -> Tablet {    return Tablet.create {        set: {            device_key: crypto.new_key(as: EncryptionKey)        }    }}

use field/entities { Tablet }use field/types { PatientNote, SealedNote }/// A note sealed with the device's own key.action seal_for_device(tablet: Tablet, note: PatientNote) -> SealedNote {    return SealedNote(crypto.encrypt(note, key: tablet.device_key, context: "note"))}

use field/entities { Tablet }use field/types { OpenedNote, SealedNote }use field/failures { NotForThisDevice }use field/actions { enrol_device, open_for_device }test "a note opens for its own device and no other" {    var clinic_tablet: Tablet = enrol_device()    var ward_tablet: Tablet = enrol_device()    var sealed_note: SealedNote = seal_for_device(clinic_tablet, "Allergic to penicillin.")    var note_read: OpenedNote = attempt open_for_device(clinic_tablet, sealed_note)    assert note_read == encoding.to_utf8("Allergic to penicillin.")    assert open_for_device(ward_tablet, sealed_note) fails NotForThisDevice}

Anywhere else is type.key_as_value: returned, passed to code of your own, compared with anything but none, read as text or bytes, or put in another value. A key's bytes come from the host's secret randomness, which a recording's tape never holds, and leave the runtime only sealed, so neither a recording nor a replay holds one. A key held as data has no previous key: it rotates by being replaced.

Each executor gives the operation one opaque key value, which prints as <key>. It comes from the source the plan decides for the call: the setting, a key-type field or a var. Only the runtime turns it into the key it holds.

The sealed format

crypto.encrypt writes version 1 of the sealed format: a version byte, an algorithm byte (1, for XChaCha20-Poly1305), the key's identity (4 bytes), the 24-byte random nonce, the ciphertext and its 16-byte tag. The associated data is the first six bytes and the call's context: as UTF-8, so the header, the context and the ciphertext are all authenticated.

The key's identity is the first four bytes of HMAC-SHA-256 of a fixed label under the key, which says nothing about the key. decrypt tries each of the current and the previous key whose identity the value carries, current first. Anything else is unreadable, never saying which: a value too short, another version or algorithm, an altered byte, or another context or key. An empty value seals and opens.

Password hashes

crypto.hash_password uses OWASP's first choice of Argon2id parameters: 19,456 KiB, 2 passes, 1 lane, version 19, a 16-byte salt from the invocation's random bytes and a 32-byte hash. It writes the reference PHC string ($argon2id$v=19$m=19456,t=2,p=1$<salt>$<hash>, in standard Base64 without padding). A hash checks correct_outdated when its memory, passes, lanes or hash length differs from the release's.

A PasswordHash reads only Argon2id at version 19, in its one spelling, with bounded costs: at most 2 GiB (RFC 9106's costliest recommendation), 16 passes and 16 lanes, a salt of 8 to 64 bytes and a hash of 16 to 64. So a hash from outside can't make a sign-in allocate without bound. verify_password reads the hash again and gives wrong for anything else, never a fault. A PasswordHash is stored as its PHC string and never leaves the server (type.password_hash_exposed).

PasswordCheck is a standard enum, written and stored as its variant's name.

Signatures

A PublicKey is an Ed25519 key's 32 bytes as unpadded Base64url, the same spelling as a PrivateKey setting's, and its construction checks the spelling. Signing is pure Ed25519, with no prehash and no context. verify_signature verifies strictly, by RFC 8032's checks, refusing small-order keys and non-canonical signatures. So a key that isn't a point on the curve, or a signature of another length, gives false.

verify_hmac takes the same time whichever key matches: it computes the MACs of both keys whatever the first gives, and compares each in constant time.

Keys and nonces in tests

A test run makes 32 random bytes, as Base64url, for each EncryptionKey and PrivateKey, as it makes a signing key's, while a nonce and a salt come from the test's seed. A deployable takes both from the host's generator, so no key and nonce repeat.

Digests

A digest is Bytes, and encoding writes it as text: encoding.to_hex for an ETag or a content key.

There is no MD5 or SHA-1, since both are broken. An outside system that still asks for one is reached through a package (External services). That includes TOTP, whose RFC 6238 default is HMAC-SHA-1 and whose per-person secret is a TotpSecret, kept sealed (How a secret is kept).

Encrypted fields

notes: ClinicalNote { encrypted: true } on an entity stores the field sealed with the application's field_encryption_key:, in the sealed format above, and decrypts it on load. The field is kept out of unique rules, indexes, filters, ordering, search and logs, as the table on Built-in services says of field encryption. Each value is sealed under a key derived from the setting for this one use, and bound to its column and its record's id. There is one key for the application, never one per person (Encrypted fields, which also says how it rotates, and what losing it costs).

encrypt, decrypt, hash_password, verify_password, hmac, verify_hmac, sign, verify_signature, public_key and new_key are built, each checked against its standard's known answers and built for WebAssembly. None reads randomness itself, and the cipher, Argon2 and Ed25519 wipe their own copies of a key when dropped. Encrypted fields are built.