Security records

These are the types for what security code keeps and checks: digests, signatures and sealed values, a password policy, passkeys and certificates.

Hash, Hmac and EncryptedValue

These three hold the bytes hash.sha256, crypto.hmac and crypto.encrypt give, as types of their own, so a digest can't be passed where a signature is expected. An EncryptedValue is ciphertext, so it may be stored and sent; only crypto.decrypt, with the key, reads what it holds.

Each is built on Bytes. The operations still give Bytes, and building each type from its own call is proved while compiling, so Hash(hash.sha256(x)) needs no attempt arm. Any other bytes are checked as they are built, so Hmac(hash.sha256(x)) and bytes from anywhere else need one. crypto.decrypt takes an EncryptedValue as the Bytes it is.

Each type checks its bytes, and bytes that don't fit break format:

• A Hash is a SHA-256 digest's 32 bytes.
• An Hmac is an HMAC-SHA-256 tag's 32 bytes.
• An EncryptedValue is the sealed format: its version (1) and its algorithm (1, XChaCha20-Poly1305), then room for its key identity, nonce and tag, so at least 46 bytes, with no most. Whether a sealed value opens is for crypto.decrypt to say, with the key.

Their text carries no algorithm tag. Each type has one algorithm (Hashing and cryptography makes no algorithm choices), and a sealed value carries its own in its second byte. Their canonical text and their JSON are the Base64 of the bytes, standard alphabet, padded, in one spelling, which is how every Bytes value is sent. So a field that was Bytes {} becomes a Hash with no change on the wire. To write a digest as hexadecimal, as for an ETag, use encoding.to_hex. Each is stored as bytea, shown to people as its Base64, and not ordered.

Every Bytes value compares in constant time, not only these three: == looks at every byte of two values of one length, whatever the first difference, inside records and lists too, and the canonical order a set keeps does the same. So comparing a received signature with the one expected says nothing of where they differ.

A clinic keeps what it needs to recognise a partner's API key, signs the webhooks it sends, and keeps each referral letter sealed to its record:

config {    letters_key: EncryptionKey    outbound_webhook_secret: SigningKey}

type ReferralText = Text {    max_length: 4000}type ReferralId = Text {}type PartnerKeyDigest = Hash {}type OutboundSignature = Hmac {}type KeyRecognised = Bool {}type ReferralUnreadable = Failure {    kind: FailureKind.invalid_value}/// What is kept of a partner's API key: its SHA-256, which signs no one/// in.function partner_key_digest(partner_key: ApiKey) -> PartnerKeyDigest {    return PartnerKeyDigest(hash.sha256(partner_key))}/// Whether a key a partner sends is the one it was issued; the digests/// compare in constant time.function partner_key_recognised(    offered_key: ApiKey,    kept_digest: PartnerKeyDigest) -> KeyRecognised {    return KeyRecognised(partner_key_digest(offered_key) == kept_digest)}/// The signature on a webhook the clinic sends.function outbound_signature(outgoing_body: ReferralText) -> OutboundSignature {    return OutboundSignature(crypto.hmac(outgoing_body, key: config.outbound_webhook_secret))}/// A referral letter sealed to its own record, which may be stored and/// sent as it is.action sealed_referral(referral_letter: ReferralText, referral: ReferralId) -> EncryptedValue {    return EncryptedValue(        crypto.encrypt(referral_letter, key: config.letters_key, context: referral)    )}/// A sealed referral's text, for its own record only.function opened_referral(    kept_letter: EncryptedValue,    referral: ReferralId) fails ReferralUnreadable -> ReferralText {    var letter_bytes: Bytes = attempt crypto.decrypt(        kept_letter,        key: config.letters_key,        context: referral    ) {        unreadable: ReferralUnreadable    }    var letter_text: Text = attempt encoding.from_utf8(letter_bytes) {        malformed: ReferralUnreadable    }    return attempt ReferralText(letter_text) {        max_length: ReferralUnreadable    }}

The digest of abc is FIPS 180-4's own example:

test "a partner's key is recognised by its digest" {    var kept_digest: PartnerKeyDigest = partner_key_digest("example_key_0123456789abcdef")    assert partner_key_recognised("example_key_0123456789abcdef", kept_digest)    assert not partner_key_recognised("example_key_0123456789abcdeX", kept_digest)    assert text.from(partner_key_digest("abc")) == "ungWv48Bz+pBQUDeXa4iI7ADYaOWF3qctBD/YfIAFa0="}test "a sealed referral opens only for its own record" {    var kept_letter: EncryptedValue = sealed_referral("Please see Ms Okafor.", "referral-7")    var read_back: ReferralText = attempt opened_referral(kept_letter, "referral-7")    assert read_back == "Please see Ms Okafor."    assert opened_referral(kept_letter, "referral-8") fails ReferralUnreadable}

PasswordPolicy

A PasswordPolicy holds the rules your app sets for a password, as NIST SP 800-63B describes them: the fewest and most characters, and whether a new password is checked against a list of breached ones. It has no composition rules, no expiry and no hints, which NIST says not to impose.

• min_length is from NIST's 8 (15 where a password is the only factor) to a Password's 256.
• max_length is from NIST's "at least 64" to 256.
• The fewest is never more than the most. This is proved on a literal, and checked as JSON is read.
• check_breached records whether your app checks a new password against a list of breached ones. NIST says a new password SHALL be compared against such a list, but Jadpo has no list and no operation for it.

It is sent as an object of its parts, stored in a column per part, and shown as its lengths, 15–64.

WebAuthnCredential

A WebAuthnCredential is a passkey as the server keeps it (Passkeys): its credential ID, its public key, its signature counter, its transports, whether it may be and is backed up, the name the person gave it, and when it was made and last used. It never holds a biometric.

It is sent with its parts' names, its bytes as Base64 and its count as any Int is sent, stored in a column per part, and shown by its name. Each Bytes part is bounded by its length.

The webauthn-rs column names the part of webauthn-rs's stored passkey that each part matches: webauthn-rs is the reference the runtime's passkey ceremonies are held to. What webauthn-rs keeps besides is the same for every passkey Jadpo registers, so it isn't held:

• user_verified is true and registration_policy is required, since a passkey is always verified;
• extensions is RegisteredExtensions::none();
• attestation is never requested, so attestation is ParsedAttestation::default() and attestation_format is None.

Checking a passkey's answer reads a stored credential's key, counter, user_verified, registration_policy and backup flags, and its transports when it lists the credentials allowed, never its extensions, so leaving them out changes nothing.

Certificate

A Certificate is an X.509 certificate (RFC 5280), read from its PEM (RFC 7468). Use it to read a certificate a partner sends, pin it by its fingerprint and check its dates. Its parts are:

• subject and issuer, each a distinguished name as RFC 4514 writes it;
• serial_number;
• not_before and not_after, the first and last instants it is valid at;
• fingerprint, the SHA-256 of its DER, as a Hash;
• der, the DER itself, so a program can pass it on.

There is no common-name part; read the subject instead.

Each part is read from what the certificate's issuer signed, so code reads the parts and never sets them. An object literal of a Certificate is type.constructor_input, and because values never change, nothing sets a part later.

Nothing here checks a certificate's signature, its chain, its extensions or whether it was revoked. A certificate isn't secret. A key's PEM is never a certificate, and reading one fails malformed.

A clinic receives lab results from a partner, which sends the certificate it signs them with. The clinic pins that certificate by its fingerprint and checks it is in date:

type PartnerPem = Text {    max_length: 100000}type CertificateRefused = Failure {    kind: FailureKind.invalid_value}type CheckedAt = Instant {}type CertificateHolds = Bool {}/// The certificate a partner sent, read from its PEM.function partner_certificate(sent_pem: PartnerPem) fails CertificateRefused -> Certificate {    return attempt text.parse(sent_pem, as: Certificate) {        malformed: CertificateRefused    }}/// Whether a certificate is the one pinned for the partner: its SHA-256/// fingerprint, compared in constant time.function is_pinned(presented: Certificate, pinned_fingerprint: Hash) -> CertificateHolds {    return CertificateHolds(presented.fingerprint == pinned_fingerprint)}/// Whether a certificate is in date: its first and last instants are both/// included.function in_date(presented: Certificate, checked_at: CheckedAt) -> CertificateHolds {    return CertificateHolds(        presented.not_before <= checked_at and checked_at <= presented.not_after    )}

test "a partner's certificate is read, pinned and dated" {    var lab_certificate: Certificate = attempt partner_certificate(        "-----BEGIN CERTIFICATE-----\nMIIBljCCAUigAwIBAgIIHy49TFtqeYgwBQYDK2VwMEgxCzAJBgNVBAYTAkdCMRww\nGgYDVQQKDBNKYWRwbyBUZXN0LCBTaWduaW5nMRswGQYDVQQDDBJqYWRwby10ZXN0\nLmV4YW1wbGUwHhcNMjYxMDAxMDAwMDAwWhcNMzYxMDAxMDAwMDAwWjBIMQswCQYD\nVQQGEwJHQjEcMBoGA1UECgwTSmFkcG8gVGVzdCwgU2lnbmluZzEbMBkGA1UEAwwS\namFkcG8tdGVzdC5leGFtcGxlMCowBQYDK2VwAyEAAJyTOxfkgCmTOYhl/AXEMRpT\n07QqDzpBZIRCSESxhYejUDBOMB0GA1UdDgQWBBTH4Arltue6aEupl+oqXRoIZos6\nLTAfBgNVHSMEGDAWgBTH4Arltue6aEupl+oqXRoIZos6LTAMBgNVHRMBAf8EAjAA\nMAUGAytlcANBAHkV9ilHQ5TVpSZyPobRcjo9bERYbugOAsKXD4ZJjCRPqpyK+aDc\n+FxV2FFnXI2UQxnYsieWNSclooiCSIuDmwA=\n-----END CERTIFICATE-----\n"    )    assert lab_certificate.subject == "CN=jadpo-test.example,O=Jadpo Test\\, Signing,C=GB"    assert lab_certificate.issuer == lab_certificate.subject    assert lab_certificate.serial_number == "1f2e3d4c5b6a7988"    var pinned: Hash = lab_certificate.fingerprint    assert text.from(pinned) == "18Ma3EAjFJeXynaXWJODAHbnCHr90gDsttEzYJqXWg0="    assert is_pinned(lab_certificate, pinned)    assert in_date(lab_certificate, "2026-10-18T09:00:00Z")    assert in_date(lab_certificate, "2036-10-01T00:00:00Z")    assert not in_date(lab_certificate, "2036-10-01T00:00:01Z")    assert partner_certificate(        "-----BEGIN PUBLIC KEY-----\nMCowBQYDK2VwAyEAGb9ECWmEzf6FQbrBZ9w7lshQhqowtrbLDFw4rXAxZuE=\n-----END PUBLIC KEY-----\n"    ) fails CertificateRefused}

Building a certificate from parts chosen in code is refused, since nothing would have signed them:

type CertificateDer = Bytes {}type IssuedAt = Instant {}/// A certificate made up in code, its parts chosen rather than signed.function made_up(    chosen_der: CertificateDer,    chosen_digest: Hash,    issued_at: IssuedAt) -> Certificate {    return Certificate {        subject: "CN=bank.example"        issuer: "CN=Trusted Root"        serial_number: "01"        not_before: issued_at        not_after: issued_at        fingerprint: chosen_digest        der: chosen_der    }}

error: `Certificate` isn't built from its parts --> main.jadpo:11:12   |11 |     return Certificate {   |            ^^^^^^^^^^^ parts set in code  reason: A `Certificate`'s subject, issuer, serial number, validity and fingerprint are read from the DER its issuer signed, so code reads them and never sets them.  next: Read the `Certificate` from its PEM with `text.parse(..., as: Certificate)`, or from JSON with `json.read` (agent)  rule: type.constructor_input  help: https://jadpo.dev/docs/errors/type.constructor_inputcheck failed: 1 error, 1 file

How a certificate is read

• Its text and its JSON are its PEM, in RFC 7468's strict form: one CERTIFICATE block, its DER in standard Base64 lines of 64 characters, the last line 1 to 64, each line ending in a line feed. It is read with line feeds, or with a carriage return and a line feed throughout, and the last line's ending is optional. Nothing else is read: text before or after the block, headers, white space, a second block and any other label, TRUSTED CERTIFICATE and every key's included, are each malformed. Its JSON is that text, as for every type with a canonical text, not its DER in Base64. It is stored in a column per part.
• Only DER is read, at most 64 KiB, whether it is inside a PEM or read from bytes by crypto.read_certificate: each length definite and in its fewest octets, no tag number of 31 or more, each INTEGER in its fewest octets, a BOOLEAN all ones or all zeros, a BIT STRING's unused bits zero, each arc of an OBJECT IDENTIFIER in its fewest octets, no universal type constructed but a SEQUENCE or a SET, each time in RFC 5280's form (YYMMDDHHMMSSZ, YYYYMMDDHHMMSSZ), and nothing after the certificate. The algorithm outside what was signed must be the one inside (RFC 5280 §4.1.1.2), each compared as its DER.
• The serial number is positive and at most 20 octets, its sign octet included (RFC 5280 §4.1.2.2), so a negative or a zero one is malformed. It is written in lowercase hexadecimal, two digits an octet, without the sign octet and with no separators: 8210cfb0d240e3594463e0bb63828b00 for ISRG Root X1.
• Names are written as RFC 4514 writes them: the relative names last first, joined by ,, and the attributes of one joined by +. The nine types RFC 4514 §3 names go by their short names (CN, L, ST, O, OU, C, STREET, DC, UID), and any other type by its dotted OID. A value of a known string kind (UTF8String, PrintableString, IA5String, NumericString, VisibleString, BMPString, UniversalString) is written as its text, escaped as §2.4 says and with every control character as \ and its hexadecimal, so a name shows on one line. A TeletexString, any other kind and any type without a short name is written as # and the hexadecimal of its DER. A string that isn't its kind's, such as UTF-8 that isn't valid, makes the certificate malformed.
• Validity is two instants, both included (RFC 5280 §4.1.2.5). 99991231235959Z, which RFC 5280 writes for a certificate with no well-defined expiry, is past the latest instant Jadpo holds, so a time in the last hours of 9999 reads as that latest instant. A certificate whose last instant is before its first is read, and is valid at no instant.
• It is shown by its subject, or by its serial number when the subject is empty: RFC 5280 lets a certificate whose names are all in its extensions have an empty subject. It is not ordered, and == compares every part, the bytes in constant time.