From 4a45ee74966a79f3d5927ae45b262390d2f809df Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 21 Sep 2026 15:24:22 +0000 Subject: [PATCH 01/88] App Attest step 1: CBOR (RFC 8949), COSE_Key EC2 (RFC 9052) and WebAuthn authenticator-data decoders in .dag, claimed over a real Apple-issued attestation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first of the pure byte decoders the App Attest verifier needs (extdeps.apple.app_attest attestation_verification_from_implementation has no supplier on main). Three extdeps modules, each cited: extdeps.standards.rfc_8949 (strict CBOR: definite-length only, floats and reserved additional info refuse, integers beyond 2^53 refuse before the multiply, nesting bounded, unique text-key member read), extdeps.standards.rfc_9052 (COSE_Key EC2 P-256 ES256 -> SEC 1 point), extdeps.standards.webauthn_authenticator_data (the §6.1 layout, whole and 37-octet prefix). The fixture is a real attestation object and assertion Apple issued to a development build (veehaitch/devicecheck-appattest ios-14.4.yaml at cb26211f), transcribed as octets with its published facts; over it the decoders establish Apple's steps 4, 5, 6, 7 and 8 from real bytes. One upstream fact the sample surfaced: Apple's assertion authenticatorData is 37 octets with the AT flag set and nothing following, so assertions are read as the prefix, never the full layout. Co-Authored-By: Claude Opus 5 (1M context) --- .../apple/app_attest_sample_ios_14_4.dag | 197 +++++++++ dag/extdeps/standards/rfc_8949.dag | 374 ++++++++++++++++++ dag/extdeps/standards/rfc_9052.dag | 167 ++++++++ .../standards/webauthn_authenticator_data.dag | 210 ++++++++++ .../app_attest_sample_decode_witness_test.dag | 199 ++++++++++ dag/test/claim/cbor_rfc8949_witness_test.dag | 254 ++++++++++++ dag/test/claim/cose_rfc9052_witness_test.dag | 121 ++++++ 7 files changed, 1522 insertions(+) create mode 100644 dag/extdeps/apple/app_attest_sample_ios_14_4.dag create mode 100644 dag/extdeps/standards/rfc_8949.dag create mode 100644 dag/extdeps/standards/rfc_9052.dag create mode 100644 dag/extdeps/standards/webauthn_authenticator_data.dag create mode 100644 dag/test/claim/app_attest_sample_decode_witness_test.dag create mode 100644 dag/test/claim/cbor_rfc8949_witness_test.dag create mode 100644 dag/test/claim/cose_rfc9052_witness_test.dag diff --git a/dag/extdeps/apple/app_attest_sample_ios_14_4.dag b/dag/extdeps/apple/app_attest_sample_ios_14_4.dag new file mode 100644 index 00000000000..f3f337781a0 --- /dev/null +++ b/dag/extdeps/apple/app_attest_sample_ios_14_4.dag @@ -0,0 +1,197 @@ +module extdeps.apple.app_attest_sample_ios_14_4 + +import std.types { Int, List, NonEmptyStr } +import std.integer { UInt8 } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// ONE REAL ATTESTATION OBJECT AND ONE REAL ASSERTION, issued by Apple's App Attest service to a +// development build on iOS 14.4 on 2021-01-23, published with their expected facts in the test +// corpus of veehaitch/devicecheck-appattest (Apache-2.0), file src/test/resources/ios-14.4.yaml at +// commit cb26211f63c1e2e7949deafe2efdf352daca27fa. Apple publishes no attestation vector, so this +// corpus is the external authority for "what Apple's service actually emits"; every expected +// value here is transcribed from that file, none is derived by this repository. +// +// What the object establishes and the witnesses over it check: fmt "apple-appattest"; x5c of two +// DER certificates (leaf P-256 signed ecdsa-with-SHA256 by Apple App Attestation CA 1, whose key +// is P-384 and which the P-384 root signs with ecdsa-with-SHA384); a 3703-octet receipt; a +// 164-octet authData with the AT flag, the development AAGUID, counter 0, a 32-octet credentialId +// equal to the key id, and a COSE EC2 P-256 credential key whose SEC 1 point hashes to the key id. +// +// THE OCTETS ARE THE CORPUS'S attestationBase64 AND assertionBase64 DECODED, transcribed as octet +// rows rather than carried as base64 because a witness that base64-decodes 7 KB in the interpreter +// spends ~3.7M eval steps on the transport encoding before it reaches the fact under claim. +// SHA-256 of the attestation octets: 9472e19c33e28e8cca9b1bc3a0417f6690ac0425d23b36be0a3f1d115ddda9d1; +// of the assertion octets: 345ffb1c9d2369cb9b6f20b70a81d0dea4effa5219f68be200e47ab942832f83. +// +// ONE FACT THE SAMPLE ESTABLISHES THAT APPLE'S PAGE DOES NOT STATE: the assertion's +// authenticatorData is 37 octets with the flags octet 0x40 -- the WebAuthn AT bit set with no +// attested credential data following. Apple's assertion procedure reads only rpIdHash and the +// counter, so an assertion is decoded as the 37-octet prefix +// (extdeps.standards.webauthn_authenticator_data decode_authenticator_data_prefix), never as a +// full WebAuthn structure, which would refuse it as truncated. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/veehaitch/devicecheck-appattest/blob/cb26211f63c1e2e7949deafe2efdf352daca27fa/src/test/resources/ios-14.4.yaml" + } +} + +data sample_team_identifier: NonEmptyStr = "6MURL8TA57" +data sample_bundle_identifier: NonEmptyStr = "de.vincent-haupert.apple-appattest-poc" + +// keyIdBase64, standard base64 of the 32-octet key id. +data sample_key_id_b64: NonEmptyStr = "YmbJO4x5nEHUvncp9zdWuVZjNBEMgJn3cdSToAXQe3M=" + +// clientDataBase64 ("wurzelpfropf") and clientDataHashSha256Base64: the app attested over +// SHA-256 of these client data bytes. +data sample_client_data_b64: NonEmptyStr = "d3VyemVscGZyb3Bm" +data sample_client_data_hash_b64: NonEmptyStr = "i+ZcylFa0JfJU5Z9GNY12G3XihQu09B3UmvtEca+xns=" + +// The assertion's authenticatorData is 37 octets with counter 1; its challenge was "wurzel". +data sample_assertion_counter: Int = 1 +data sample_assertion_challenge_b64: NonEmptyStr = "d3VyemVs" + +// The attestation object, 5274 octets. +data sample_attestation_octets: List = [ + 163, 99, 102, 109, 116, 111, 97, 112, 112, 108, 101, 45, 97, 112, 112, 97, 116, 116, 101, 115, 116, 103, 97, 116, 116, 83, 116, 109, 116, 162, 99, 120, 53, 99, 130, 89, 2, 249, 48, 130, + 2, 245, 48, 130, 2, 123, 160, 3, 2, 1, 2, 2, 6, 1, 119, 47, 41, 247, 72, 48, 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 2, 48, 79, 49, 35, 48, 33, 6, 3, 85, + 4, 3, 12, 26, 65, 112, 112, 108, 101, 32, 65, 112, 112, 32, 65, 116, 116, 101, 115, 116, 97, 116, 105, 111, 110, 32, 67, 65, 32, 49, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, + 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 19, 48, 17, 6, 3, 85, 4, 8, 12, 10, 67, 97, 108, 105, 102, 111, 114, 110, 105, 97, 48, 30, 23, 13, 50, 49, 48, 49, + 50, 50, 49, 50, 49, 51, 51, 53, 90, 23, 13, 50, 49, 48, 49, 50, 53, 49, 50, 49, 51, 51, 53, 90, 48, 129, 145, 49, 73, 48, 71, 6, 3, 85, 4, 3, 12, 64, 54, 50, + 54, 54, 99, 57, 51, 98, 56, 99, 55, 57, 57, 99, 52, 49, 100, 52, 98, 101, 55, 55, 50, 57, 102, 55, 51, 55, 53, 54, 98, 57, 53, 54, 54, 51, 51, 52, 49, 49, 48, 99, + 56, 48, 57, 57, 102, 55, 55, 49, 100, 52, 57, 51, 97, 48, 48, 53, 100, 48, 55, 98, 55, 51, 49, 26, 48, 24, 6, 3, 85, 4, 11, 12, 17, 65, 65, 65, 32, 67, 101, 114, + 116, 105, 102, 105, 99, 97, 116, 105, 111, 110, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 19, 48, 17, 6, 3, 85, 4, 8, + 12, 10, 67, 97, 108, 105, 102, 111, 114, 110, 105, 97, 48, 89, 48, 19, 6, 7, 42, 134, 72, 206, 61, 2, 1, 6, 8, 42, 134, 72, 206, 61, 3, 1, 7, 3, 66, 0, 4, 136, + 192, 52, 161, 144, 170, 125, 188, 90, 6, 21, 1, 198, 84, 40, 3, 148, 37, 130, 25, 139, 63, 28, 197, 70, 115, 202, 59, 154, 210, 11, 65, 82, 130, 103, 165, 79, 95, 219, 160, 70, + 159, 175, 180, 107, 182, 153, 10, 57, 107, 240, 79, 148, 164, 157, 67, 32, 200, 28, 122, 178, 64, 163, 152, 163, 129, 255, 48, 129, 252, 48, 12, 6, 3, 85, 29, 19, 1, 1, 255, 4, + 2, 48, 0, 48, 14, 6, 3, 85, 29, 15, 1, 1, 255, 4, 4, 3, 2, 4, 240, 48, 129, 139, 6, 9, 42, 134, 72, 134, 247, 99, 100, 8, 5, 4, 126, 48, 124, 164, 3, 2, + 1, 10, 191, 137, 48, 3, 2, 1, 1, 191, 137, 49, 3, 2, 1, 0, 191, 137, 50, 3, 2, 1, 0, 191, 137, 51, 3, 2, 1, 1, 191, 137, 52, 51, 4, 49, 54, 77, 85, 82, + 76, 56, 84, 65, 53, 55, 46, 100, 101, 46, 118, 105, 110, 99, 101, 110, 116, 45, 104, 97, 117, 112, 101, 114, 116, 46, 97, 112, 112, 108, 101, 45, 97, 112, 112, 97, 116, 116, 101, 115, + 116, 45, 112, 111, 99, 165, 6, 4, 4, 32, 115, 107, 115, 191, 137, 54, 3, 2, 1, 5, 191, 137, 55, 3, 2, 1, 0, 191, 137, 57, 3, 2, 1, 0, 191, 137, 58, 3, 2, 1, + 0, 48, 25, 6, 9, 42, 134, 72, 134, 247, 99, 100, 8, 7, 4, 12, 48, 10, 191, 138, 120, 6, 4, 4, 49, 52, 46, 52, 48, 51, 6, 9, 42, 134, 72, 134, 247, 99, 100, 8, + 2, 4, 38, 48, 36, 161, 34, 4, 32, 152, 154, 61, 37, 24, 161, 124, 37, 156, 239, 85, 20, 212, 92, 230, 205, 210, 53, 31, 99, 216, 160, 41, 1, 151, 36, 66, 71, 158, 194, 68, + 62, 48, 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 2, 3, 104, 0, 48, 101, 2, 48, 104, 19, 165, 122, 19, 56, 8, 97, 237, 114, 120, 87, 245, 187, 117, 90, 232, 118, 136, 155, + 101, 84, 11, 67, 111, 179, 225, 221, 195, 209, 196, 231, 150, 166, 30, 238, 199, 185, 209, 95, 235, 4, 206, 69, 72, 17, 12, 192, 2, 49, 0, 221, 56, 195, 19, 229, 122, 82, 254, 67, + 43, 133, 71, 122, 164, 241, 150, 120, 10, 198, 83, 28, 92, 179, 74, 81, 60, 107, 66, 157, 227, 59, 216, 157, 47, 62, 181, 162, 40, 16, 63, 70, 194, 181, 34, 247, 164, 230, 128, 89, + 2, 71, 48, 130, 2, 67, 48, 130, 1, 200, 160, 3, 2, 1, 2, 2, 16, 9, 186, 197, 225, 188, 64, 26, 217, 212, 83, 149, 188, 56, 26, 8, 84, 48, 10, 6, 8, 42, 134, 72, + 206, 61, 4, 3, 3, 48, 82, 49, 38, 48, 36, 6, 3, 85, 4, 3, 12, 29, 65, 112, 112, 108, 101, 32, 65, 112, 112, 32, 65, 116, 116, 101, 115, 116, 97, 116, 105, 111, 110, 32, + 82, 111, 111, 116, 32, 67, 65, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 19, 48, 17, 6, 3, 85, 4, 8, 12, 10, 67, + 97, 108, 105, 102, 111, 114, 110, 105, 97, 48, 30, 23, 13, 50, 48, 48, 51, 49, 56, 49, 56, 51, 57, 53, 53, 90, 23, 13, 51, 48, 48, 51, 49, 51, 48, 48, 48, 48, 48, 48, + 90, 48, 79, 49, 35, 48, 33, 6, 3, 85, 4, 3, 12, 26, 65, 112, 112, 108, 101, 32, 65, 112, 112, 32, 65, 116, 116, 101, 115, 116, 97, 116, 105, 111, 110, 32, 67, 65, 32, 49, + 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 19, 48, 17, 6, 3, 85, 4, 8, 12, 10, 67, 97, 108, 105, 102, 111, 114, 110, + 105, 97, 48, 118, 48, 16, 6, 7, 42, 134, 72, 206, 61, 2, 1, 6, 5, 43, 129, 4, 0, 34, 3, 98, 0, 4, 174, 91, 55, 160, 119, 77, 121, 178, 53, 143, 64, 231, 209, 242, + 38, 38, 241, 194, 95, 239, 23, 128, 45, 234, 179, 130, 106, 89, 135, 79, 248, 210, 173, 21, 37, 120, 154, 162, 102, 4, 25, 18, 72, 182, 60, 185, 103, 6, 158, 152, 211, 99, 189, 94, + 55, 15, 191, 160, 142, 50, 158, 128, 115, 169, 133, 231, 116, 110, 163, 89, 162, 246, 111, 41, 219, 50, 175, 69, 94, 33, 22, 88, 213, 103, 175, 158, 38, 126, 178, 97, 77, 194, 26, 102, + 206, 153, 163, 102, 48, 100, 48, 18, 6, 3, 85, 29, 19, 1, 1, 255, 4, 8, 48, 6, 1, 1, 255, 2, 1, 0, 48, 31, 6, 3, 85, 29, 35, 4, 24, 48, 22, 128, 20, 172, + 145, 16, 83, 51, 189, 190, 104, 65, 255, 167, 12, 169, 229, 250, 234, 229, 229, 138, 161, 48, 29, 6, 3, 85, 29, 14, 4, 22, 4, 20, 62, 227, 93, 28, 4, 25, 169, 201, 180, 49, + 248, 132, 116, 214, 225, 225, 87, 114, 227, 155, 48, 14, 6, 3, 85, 29, 15, 1, 1, 255, 4, 4, 3, 2, 1, 6, 48, 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 3, 3, 105, + 0, 48, 102, 2, 49, 0, 187, 190, 136, 141, 115, 141, 5, 2, 207, 188, 253, 102, 109, 9, 87, 80, 53, 188, 214, 135, 44, 63, 132, 48, 73, 38, 41, 237, 209, 249, 20, 232, 121, 153, + 28, 154, 232, 181, 174, 248, 211, 168, 84, 51, 247, 182, 13, 6, 2, 49, 0, 171, 56, 237, 208, 204, 129, 237, 0, 164, 82, 195, 186, 68, 249, 147, 99, 101, 83, 254, 204, 41, 127, 46, + 180, 223, 159, 94, 190, 90, 74, 202, 182, 153, 92, 75, 130, 13, 249, 4, 56, 111, 120, 7, 187, 88, 148, 57, 183, 103, 114, 101, 99, 101, 105, 112, 116, 89, 14, 119, 48, 128, 6, 9, + 42, 134, 72, 134, 247, 13, 1, 7, 2, 160, 128, 48, 128, 2, 1, 1, 49, 15, 48, 13, 6, 9, 96, 134, 72, 1, 101, 3, 4, 2, 1, 5, 0, 48, 128, 6, 9, 42, 134, 72, + 134, 247, 13, 1, 7, 1, 160, 128, 36, 128, 4, 130, 3, 232, 49, 130, 4, 51, 48, 57, 2, 1, 2, 2, 1, 1, 4, 49, 54, 77, 85, 82, 76, 56, 84, 65, 53, 55, 46, 100, + 101, 46, 118, 105, 110, 99, 101, 110, 116, 45, 104, 97, 117, 112, 101, 114, 116, 46, 97, 112, 112, 108, 101, 45, 97, 112, 112, 97, 116, 116, 101, 115, 116, 45, 112, 111, 99, 48, 130, 3, + 3, 2, 1, 3, 2, 1, 1, 4, 130, 2, 249, 48, 130, 2, 245, 48, 130, 2, 123, 160, 3, 2, 1, 2, 2, 6, 1, 119, 47, 41, 247, 72, 48, 10, 6, 8, 42, 134, 72, 206, + 61, 4, 3, 2, 48, 79, 49, 35, 48, 33, 6, 3, 85, 4, 3, 12, 26, 65, 112, 112, 108, 101, 32, 65, 112, 112, 32, 65, 116, 116, 101, 115, 116, 97, 116, 105, 111, 110, 32, 67, + 65, 32, 49, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 19, 48, 17, 6, 3, 85, 4, 8, 12, 10, 67, 97, 108, 105, 102, + 111, 114, 110, 105, 97, 48, 30, 23, 13, 50, 49, 48, 49, 50, 50, 49, 50, 49, 51, 51, 53, 90, 23, 13, 50, 49, 48, 49, 50, 53, 49, 50, 49, 51, 51, 53, 90, 48, 129, 145, + 49, 73, 48, 71, 6, 3, 85, 4, 3, 12, 64, 54, 50, 54, 54, 99, 57, 51, 98, 56, 99, 55, 57, 57, 99, 52, 49, 100, 52, 98, 101, 55, 55, 50, 57, 102, 55, 51, 55, 53, + 54, 98, 57, 53, 54, 54, 51, 51, 52, 49, 49, 48, 99, 56, 48, 57, 57, 102, 55, 55, 49, 100, 52, 57, 51, 97, 48, 48, 53, 100, 48, 55, 98, 55, 51, 49, 26, 48, 24, 6, + 3, 85, 4, 11, 12, 17, 65, 65, 65, 32, 67, 101, 114, 116, 105, 102, 105, 99, 97, 116, 105, 111, 110, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, + 73, 110, 99, 46, 49, 19, 48, 17, 6, 3, 85, 4, 8, 12, 10, 67, 97, 108, 105, 102, 111, 114, 110, 105, 97, 48, 89, 48, 19, 6, 7, 42, 134, 72, 206, 61, 2, 1, 6, 8, + 42, 134, 72, 206, 61, 3, 1, 7, 3, 66, 0, 4, 136, 192, 52, 161, 144, 170, 125, 188, 90, 6, 21, 1, 198, 84, 40, 3, 148, 37, 130, 25, 139, 63, 28, 197, 70, 115, 202, 59, + 154, 210, 11, 65, 82, 130, 103, 165, 79, 95, 219, 160, 70, 159, 175, 180, 107, 182, 153, 10, 57, 107, 240, 79, 148, 164, 157, 67, 32, 200, 28, 122, 178, 64, 163, 152, 163, 129, 255, 48, + 129, 252, 48, 12, 6, 3, 85, 29, 19, 1, 1, 255, 4, 2, 48, 0, 48, 14, 6, 3, 85, 29, 15, 1, 1, 255, 4, 4, 3, 2, 4, 240, 48, 129, 139, 6, 9, 42, 134, 72, + 134, 247, 99, 100, 8, 5, 4, 126, 48, 124, 164, 3, 2, 1, 10, 191, 137, 48, 3, 2, 1, 1, 191, 137, 49, 3, 2, 1, 0, 191, 137, 50, 3, 2, 1, 0, 191, 137, 51, 3, + 2, 1, 1, 191, 137, 52, 51, 4, 49, 54, 77, 85, 82, 76, 56, 84, 65, 53, 55, 46, 100, 101, 46, 118, 105, 110, 99, 101, 110, 116, 45, 104, 97, 117, 112, 101, 114, 116, 46, 97, + 112, 112, 108, 101, 45, 97, 112, 112, 97, 116, 116, 101, 115, 116, 45, 112, 111, 99, 165, 6, 4, 4, 32, 115, 107, 115, 191, 137, 54, 3, 2, 1, 5, 191, 137, 55, 3, 2, 1, 0, + 191, 137, 57, 3, 2, 1, 0, 191, 137, 58, 3, 2, 1, 0, 48, 25, 6, 9, 42, 134, 72, 134, 247, 99, 100, 8, 7, 4, 12, 48, 10, 191, 138, 120, 6, 4, 4, 49, 52, 46, + 52, 48, 51, 6, 9, 42, 134, 72, 134, 247, 99, 100, 8, 2, 4, 38, 48, 36, 161, 34, 4, 32, 152, 154, 61, 37, 24, 161, 124, 37, 156, 239, 85, 20, 212, 92, 230, 205, 210, 53, + 31, 99, 216, 160, 41, 1, 151, 36, 66, 71, 158, 194, 68, 62, 48, 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 2, 3, 104, 0, 48, 101, 2, 48, 104, 19, 165, 122, 19, 56, 8, + 97, 237, 114, 120, 87, 245, 187, 117, 90, 232, 118, 136, 155, 101, 84, 11, 67, 111, 179, 225, 221, 195, 209, 196, 231, 150, 166, 30, 238, 199, 185, 209, 95, 235, 4, 206, 69, 72, 17, 12, + 192, 2, 49, 0, 221, 56, 195, 19, 229, 122, 82, 254, 67, 43, 133, 71, 122, 164, 241, 150, 120, 10, 198, 83, 28, 92, 179, 74, 81, 60, 107, 66, 157, 227, 59, 216, 157, 47, 62, 181, + 162, 40, 16, 63, 70, 194, 181, 34, 247, 164, 230, 128, 48, 40, 2, 1, 4, 2, 1, 1, 4, 32, 139, 230, 92, 202, 81, 90, 208, 151, 201, 83, 150, 125, 24, 214, 53, 216, 109, 215, + 138, 20, 46, 211, 208, 119, 82, 107, 237, 17, 198, 190, 198, 123, 48, 96, 2, 1, 5, 2, 1, 1, 4, 88, 97, 80, 53, 83, 57, 85, 102, 121, 48, 57, 50, 99, 75, 108, 97, 82, + 89, 107, 107, 117, 84, 118, 81, 65, 84, 120, 47, 82, 51, 66, 57, 83, 119, 113, 72, 114, 54, 75, 54, 70, 88, 97, 65, 87, 115, 122, 114, 84, 43, 50, 120, 107, 65, 103, 75, 77, + 69, 102, 108, 50, 54, 80, 88, 90, 112, 110, 86, 89, 97, 89, 122, 51, 114, 74, 105, 51, 100, 73, 65, 113, 69, 90, 101, 117, 98, 81, 61, 61, 48, 14, 2, 1, 6, 2, 1, 1, + 4, 6, 65, 84, 84, 69, 83, 84, 48, 15, 2, 1, 7, 2, 4, 79, 1, 1, 4, 7, 115, 97, 110, 100, 98, 111, 120, 48, 32, 2, 1, 12, 2, 1, 1, 4, 24, 50, 48, 50, + 49, 45, 48, 49, 45, 50, 51, 84, 49, 50, 58, 49, 51, 58, 51, 53, 46, 56, 48, 49, 90, 48, 32, 2, 1, 21, 2, 1, 1, 4, 24, 50, 48, 50, 49, 45, 48, 52, 45, 50, + 51, 84, 49, 50, 58, 49, 51, 58, 51, 53, 46, 56, 48, 49, 90, 0, 0, 0, 0, 0, 0, 160, 128, 48, 130, 3, 173, 48, 130, 3, 84, 160, 3, 2, 1, 2, 2, 16, 89, 51, + 86, 173, 229, 89, 130, 207, 68, 66, 55, 172, 223, 69, 27, 83, 48, 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 2, 48, 124, 49, 48, 48, 46, 6, 3, 85, 4, 3, 12, 39, 65, + 112, 112, 108, 101, 32, 65, 112, 112, 108, 105, 99, 97, 116, 105, 111, 110, 32, 73, 110, 116, 101, 103, 114, 97, 116, 105, 111, 110, 32, 67, 65, 32, 53, 32, 45, 32, 71, 49, 49, 38, + 48, 36, 6, 3, 85, 4, 11, 12, 29, 65, 112, 112, 108, 101, 32, 67, 101, 114, 116, 105, 102, 105, 99, 97, 116, 105, 111, 110, 32, 65, 117, 116, 104, 111, 114, 105, 116, 121, 49, 19, + 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 11, 48, 9, 6, 3, 85, 4, 6, 19, 2, 85, 83, 48, 30, 23, 13, 50, 48, 48, 53, + 49, 57, 49, 55, 52, 55, 51, 49, 90, 23, 13, 50, 49, 48, 54, 49, 56, 49, 55, 52, 55, 51, 49, 90, 48, 90, 49, 54, 48, 52, 6, 3, 85, 4, 3, 12, 45, 65, 112, 112, + 108, 105, 99, 97, 116, 105, 111, 110, 32, 65, 116, 116, 101, 115, 116, 97, 116, 105, 111, 110, 32, 70, 114, 97, 117, 100, 32, 82, 101, 99, 101, 105, 112, 116, 32, 83, 105, 103, 110, 105, + 110, 103, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 11, 48, 9, 6, 3, 85, 4, 6, 19, 2, 85, 83, 48, 89, 48, 19, + 6, 7, 42, 134, 72, 206, 61, 2, 1, 6, 8, 42, 134, 72, 206, 61, 3, 1, 7, 3, 66, 0, 4, 127, 233, 21, 52, 108, 195, 138, 123, 152, 60, 147, 209, 208, 67, 95, 216, 171, + 218, 86, 112, 4, 211, 44, 88, 134, 101, 81, 149, 122, 180, 120, 247, 203, 42, 248, 186, 69, 247, 250, 120, 234, 198, 44, 73, 228, 249, 205, 192, 132, 181, 3, 20, 241, 2, 51, 218, 155, + 118, 250, 68, 42, 43, 184, 114, 163, 130, 1, 216, 48, 130, 1, 212, 48, 12, 6, 3, 85, 29, 19, 1, 1, 255, 4, 2, 48, 0, 48, 31, 6, 3, 85, 29, 35, 4, 24, 48, 22, + 128, 20, 217, 23, 254, 75, 103, 144, 56, 75, 146, 244, 219, 206, 213, 87, 128, 20, 11, 143, 61, 201, 48, 67, 6, 8, 43, 6, 1, 5, 5, 7, 1, 1, 4, 55, 48, 53, 48, 51, + 6, 8, 43, 6, 1, 5, 5, 7, 48, 1, 134, 39, 104, 116, 116, 112, 58, 47, 47, 111, 99, 115, 112, 46, 97, 112, 112, 108, 101, 46, 99, 111, 109, 47, 111, 99, 115, 112, 48, 51, + 45, 97, 97, 105, 99, 97, 53, 103, 49, 48, 49, 48, 130, 1, 28, 6, 3, 85, 29, 32, 4, 130, 1, 19, 48, 130, 1, 15, 48, 130, 1, 11, 6, 9, 42, 134, 72, 134, 247, 99, + 100, 5, 1, 48, 129, 253, 48, 129, 195, 6, 8, 43, 6, 1, 5, 5, 7, 2, 2, 48, 129, 182, 12, 129, 179, 82, 101, 108, 105, 97, 110, 99, 101, 32, 111, 110, 32, 116, 104, 105, + 115, 32, 99, 101, 114, 116, 105, 102, 105, 99, 97, 116, 101, 32, 98, 121, 32, 97, 110, 121, 32, 112, 97, 114, 116, 121, 32, 97, 115, 115, 117, 109, 101, 115, 32, 97, 99, 99, 101, 112, + 116, 97, 110, 99, 101, 32, 111, 102, 32, 116, 104, 101, 32, 116, 104, 101, 110, 32, 97, 112, 112, 108, 105, 99, 97, 98, 108, 101, 32, 115, 116, 97, 110, 100, 97, 114, 100, 32, 116, 101, + 114, 109, 115, 32, 97, 110, 100, 32, 99, 111, 110, 100, 105, 116, 105, 111, 110, 115, 32, 111, 102, 32, 117, 115, 101, 44, 32, 99, 101, 114, 116, 105, 102, 105, 99, 97, 116, 101, 32, 112, + 111, 108, 105, 99, 121, 32, 97, 110, 100, 32, 99, 101, 114, 116, 105, 102, 105, 99, 97, 116, 105, 111, 110, 32, 112, 114, 97, 99, 116, 105, 99, 101, 32, 115, 116, 97, 116, 101, 109, 101, + 110, 116, 115, 46, 48, 53, 6, 8, 43, 6, 1, 5, 5, 7, 2, 1, 22, 41, 104, 116, 116, 112, 58, 47, 47, 119, 119, 119, 46, 97, 112, 112, 108, 101, 46, 99, 111, 109, 47, 99, + 101, 114, 116, 105, 102, 105, 99, 97, 116, 101, 97, 117, 116, 104, 111, 114, 105, 116, 121, 48, 29, 6, 3, 85, 29, 14, 4, 22, 4, 20, 105, 30, 199, 15, 71, 236, 227, 141, 221, 117, + 55, 68, 243, 233, 225, 90, 108, 16, 86, 37, 48, 14, 6, 3, 85, 29, 15, 1, 1, 255, 4, 4, 3, 2, 7, 128, 48, 15, 6, 9, 42, 134, 72, 134, 247, 99, 100, 12, 15, 4, + 2, 5, 0, 48, 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 2, 3, 71, 0, 48, 68, 2, 32, 37, 24, 22, 92, 94, 41, 156, 89, 246, 133, 57, 173, 93, 219, 153, 246, 55, 62, + 246, 14, 205, 8, 69, 169, 253, 119, 26, 214, 36, 45, 44, 34, 2, 32, 93, 42, 155, 42, 95, 171, 163, 99, 129, 101, 141, 24, 64, 247, 175, 72, 11, 215, 107, 161, 148, 216, 52, 32, + 135, 244, 214, 147, 91, 181, 27, 174, 48, 130, 2, 249, 48, 130, 2, 127, 160, 3, 2, 1, 2, 2, 16, 86, 251, 131, 212, 43, 255, 141, 195, 55, 153, 35, 181, 90, 174, 110, 189, 48, + 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 3, 48, 103, 49, 27, 48, 25, 6, 3, 85, 4, 3, 12, 18, 65, 112, 112, 108, 101, 32, 82, 111, 111, 116, 32, 67, 65, 32, 45, 32, + 71, 51, 49, 38, 48, 36, 6, 3, 85, 4, 11, 12, 29, 65, 112, 112, 108, 101, 32, 67, 101, 114, 116, 105, 102, 105, 99, 97, 116, 105, 111, 110, 32, 65, 117, 116, 104, 111, 114, 105, + 116, 121, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 11, 48, 9, 6, 3, 85, 4, 6, 19, 2, 85, 83, 48, 30, 23, 13, + 49, 57, 48, 51, 50, 50, 49, 55, 53, 51, 51, 51, 90, 23, 13, 51, 52, 48, 51, 50, 50, 48, 48, 48, 48, 48, 48, 90, 48, 124, 49, 48, 48, 46, 6, 3, 85, 4, 3, 12, + 39, 65, 112, 112, 108, 101, 32, 65, 112, 112, 108, 105, 99, 97, 116, 105, 111, 110, 32, 73, 110, 116, 101, 103, 114, 97, 116, 105, 111, 110, 32, 67, 65, 32, 53, 32, 45, 32, 71, 49, + 49, 38, 48, 36, 6, 3, 85, 4, 11, 12, 29, 65, 112, 112, 108, 101, 32, 67, 101, 114, 116, 105, 102, 105, 99, 97, 116, 105, 111, 110, 32, 65, 117, 116, 104, 111, 114, 105, 116, 121, + 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 11, 48, 9, 6, 3, 85, 4, 6, 19, 2, 85, 83, 48, 89, 48, 19, 6, 7, + 42, 134, 72, 206, 61, 2, 1, 6, 8, 42, 134, 72, 206, 61, 3, 1, 7, 3, 66, 0, 4, 146, 206, 99, 189, 125, 134, 177, 171, 40, 10, 59, 28, 225, 175, 251, 4, 148, 128, 145, + 172, 246, 49, 223, 166, 203, 40, 53, 111, 68, 75, 225, 33, 229, 87, 221, 18, 141, 141, 186, 130, 124, 149, 190, 73, 250, 190, 51, 202, 174, 205, 4, 25, 241, 47, 67, 37, 250, 244, 190, + 179, 203, 131, 126, 186, 163, 129, 247, 48, 129, 244, 48, 15, 6, 3, 85, 29, 19, 1, 1, 255, 4, 5, 48, 3, 1, 1, 255, 48, 31, 6, 3, 85, 29, 35, 4, 24, 48, 22, 128, + 20, 187, 176, 222, 161, 88, 51, 136, 154, 164, 138, 153, 222, 190, 189, 235, 175, 218, 203, 36, 171, 48, 70, 6, 8, 43, 6, 1, 5, 5, 7, 1, 1, 4, 58, 48, 56, 48, 54, 6, + 8, 43, 6, 1, 5, 5, 7, 48, 1, 134, 42, 104, 116, 116, 112, 58, 47, 47, 111, 99, 115, 112, 46, 97, 112, 112, 108, 101, 46, 99, 111, 109, 47, 111, 99, 115, 112, 48, 51, 45, + 97, 112, 112, 108, 101, 114, 111, 111, 116, 99, 97, 103, 51, 48, 55, 6, 3, 85, 29, 31, 4, 48, 48, 46, 48, 44, 160, 42, 160, 40, 134, 38, 104, 116, 116, 112, 58, 47, 47, 99, + 114, 108, 46, 97, 112, 112, 108, 101, 46, 99, 111, 109, 47, 97, 112, 112, 108, 101, 114, 111, 111, 116, 99, 97, 103, 51, 46, 99, 114, 108, 48, 29, 6, 3, 85, 29, 14, 4, 22, 4, + 20, 217, 23, 254, 75, 103, 144, 56, 75, 146, 244, 219, 206, 213, 87, 128, 20, 11, 143, 61, 201, 48, 14, 6, 3, 85, 29, 15, 1, 1, 255, 4, 4, 3, 2, 1, 6, 48, 16, 6, + 10, 42, 134, 72, 134, 247, 99, 100, 6, 2, 3, 4, 2, 5, 0, 48, 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 3, 3, 104, 0, 48, 101, 2, 49, 0, 141, 111, 166, 159, 161, + 224, 228, 236, 91, 78, 115, 138, 146, 127, 61, 120, 83, 152, 143, 244, 218, 31, 88, 30, 195, 117, 74, 254, 56, 168, 76, 42, 131, 26, 26, 170, 13, 166, 100, 109, 225, 185, 147, 232, 209, + 85, 76, 237, 2, 48, 103, 59, 44, 180, 225, 232, 55, 7, 119, 203, 213, 236, 118, 168, 26, 58, 85, 59, 63, 53, 106, 200, 197, 230, 146, 176, 225, 97, 190, 128, 73, 105, 228, 95, 43, + 169, 108, 225, 17, 2, 170, 204, 97, 217, 56, 183, 115, 74, 48, 130, 2, 67, 48, 130, 1, 201, 160, 3, 2, 1, 2, 2, 8, 45, 197, 252, 136, 210, 197, 75, 149, 48, 10, 6, 8, + 42, 134, 72, 206, 61, 4, 3, 3, 48, 103, 49, 27, 48, 25, 6, 3, 85, 4, 3, 12, 18, 65, 112, 112, 108, 101, 32, 82, 111, 111, 116, 32, 67, 65, 32, 45, 32, 71, 51, 49, + 38, 48, 36, 6, 3, 85, 4, 11, 12, 29, 65, 112, 112, 108, 101, 32, 67, 101, 114, 116, 105, 102, 105, 99, 97, 116, 105, 111, 110, 32, 65, 117, 116, 104, 111, 114, 105, 116, 121, 49, + 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 11, 48, 9, 6, 3, 85, 4, 6, 19, 2, 85, 83, 48, 30, 23, 13, 49, 52, 48, + 52, 51, 48, 49, 56, 49, 57, 48, 54, 90, 23, 13, 51, 57, 48, 52, 51, 48, 49, 56, 49, 57, 48, 54, 90, 48, 103, 49, 27, 48, 25, 6, 3, 85, 4, 3, 12, 18, 65, 112, + 112, 108, 101, 32, 82, 111, 111, 116, 32, 67, 65, 32, 45, 32, 71, 51, 49, 38, 48, 36, 6, 3, 85, 4, 11, 12, 29, 65, 112, 112, 108, 101, 32, 67, 101, 114, 116, 105, 102, 105, + 99, 97, 116, 105, 111, 110, 32, 65, 117, 116, 104, 111, 114, 105, 116, 121, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, 110, 99, 46, 49, 11, 48, + 9, 6, 3, 85, 4, 6, 19, 2, 85, 83, 48, 118, 48, 16, 6, 7, 42, 134, 72, 206, 61, 2, 1, 6, 5, 43, 129, 4, 0, 34, 3, 98, 0, 4, 152, 233, 47, 61, 64, 114, + 164, 237, 147, 34, 114, 129, 19, 28, 221, 16, 149, 241, 197, 163, 78, 113, 220, 20, 22, 217, 14, 229, 166, 5, 42, 119, 100, 123, 95, 78, 56, 211, 187, 28, 68, 181, 127, 245, 31, 182, + 50, 98, 93, 201, 233, 132, 91, 79, 48, 79, 17, 90, 0, 253, 88, 88, 12, 165, 245, 15, 44, 77, 7, 71, 19, 117, 218, 151, 151, 151, 111, 49, 92, 237, 43, 157, 123, 32, 59, 216, + 185, 84, 217, 94, 153, 164, 58, 81, 10, 49, 163, 66, 48, 64, 48, 29, 6, 3, 85, 29, 14, 4, 22, 4, 20, 187, 176, 222, 161, 88, 51, 136, 154, 164, 138, 153, 222, 190, 189, 235, + 175, 218, 203, 36, 171, 48, 15, 6, 3, 85, 29, 19, 1, 1, 255, 4, 5, 48, 3, 1, 1, 255, 48, 14, 6, 3, 85, 29, 15, 1, 1, 255, 4, 4, 3, 2, 1, 6, 48, 10, + 6, 8, 42, 134, 72, 206, 61, 4, 3, 3, 3, 104, 0, 48, 101, 2, 49, 0, 131, 233, 193, 196, 22, 94, 26, 93, 52, 24, 217, 237, 239, 244, 108, 14, 0, 70, 75, 184, 223, 178, + 70, 17, 197, 15, 253, 230, 122, 140, 161, 166, 107, 206, 194, 3, 212, 156, 245, 147, 198, 116, 184, 106, 223, 170, 35, 21, 2, 48, 109, 102, 138, 16, 202, 212, 13, 212, 79, 205, 141, 67, + 62, 180, 138, 99, 165, 51, 110, 227, 109, 218, 23, 183, 100, 31, 200, 83, 38, 249, 136, 98, 116, 57, 11, 23, 91, 203, 81, 168, 12, 232, 24, 3, 231, 162, 178, 40, 0, 0, 49, 129, + 252, 48, 129, 249, 2, 1, 1, 48, 129, 144, 48, 124, 49, 48, 48, 46, 6, 3, 85, 4, 3, 12, 39, 65, 112, 112, 108, 101, 32, 65, 112, 112, 108, 105, 99, 97, 116, 105, 111, 110, + 32, 73, 110, 116, 101, 103, 114, 97, 116, 105, 111, 110, 32, 67, 65, 32, 53, 32, 45, 32, 71, 49, 49, 38, 48, 36, 6, 3, 85, 4, 11, 12, 29, 65, 112, 112, 108, 101, 32, 67, + 101, 114, 116, 105, 102, 105, 99, 97, 116, 105, 111, 110, 32, 65, 117, 116, 104, 111, 114, 105, 116, 121, 49, 19, 48, 17, 6, 3, 85, 4, 10, 12, 10, 65, 112, 112, 108, 101, 32, 73, + 110, 99, 46, 49, 11, 48, 9, 6, 3, 85, 4, 6, 19, 2, 85, 83, 2, 16, 89, 51, 86, 173, 229, 89, 130, 207, 68, 66, 55, 172, 223, 69, 27, 83, 48, 13, 6, 9, 96, 134, + 72, 1, 101, 3, 4, 2, 1, 5, 0, 48, 10, 6, 8, 42, 134, 72, 206, 61, 4, 3, 2, 4, 70, 48, 68, 2, 32, 85, 215, 139, 86, 161, 56, 105, 109, 232, 34, 243, 35, 208, + 117, 16, 1, 182, 41, 209, 199, 248, 50, 215, 165, 123, 0, 110, 197, 36, 250, 179, 40, 2, 32, 1, 128, 38, 36, 186, 26, 236, 3, 238, 66, 111, 63, 54, 41, 85, 29, 175, 89, 208, + 169, 228, 32, 252, 130, 61, 246, 84, 150, 133, 188, 226, 180, 0, 0, 0, 0, 0, 0, 104, 97, 117, 116, 104, 68, 97, 116, 97, 88, 164, 69, 101, 18, 234, 126, 38, 148, 118, 171, 147, + 225, 183, 151, 22, 133, 89, 47, 247, 63, 137, 74, 192, 236, 47, 213, 72, 8, 160, 139, 251, 108, 143, 64, 0, 0, 0, 0, 97, 112, 112, 97, 116, 116, 101, 115, 116, 100, 101, 118, 101, + 108, 111, 112, 0, 32, 98, 102, 201, 59, 140, 121, 156, 65, 212, 190, 119, 41, 247, 55, 86, 185, 86, 99, 52, 17, 12, 128, 153, 247, 113, 212, 147, 160, 5, 208, 123, 115, 165, 1, 2, + 3, 38, 32, 1, 33, 88, 32, 136, 192, 52, 161, 144, 170, 125, 188, 90, 6, 21, 1, 198, 84, 40, 3, 148, 37, 130, 25, 139, 63, 28, 197, 70, 115, 202, 59, 154, 210, 11, 65, 34, + 88, 32, 82, 130, 103, 165, 79, 95, 219, 160, 70, 159, 175, 180, 107, 182, 153, 10, 57, 107, 240, 79, 148, 164, 157, 67, 32, 200, 28, 122, 178, 64, 163, 152, +] + +// The assertion object, 140 octets. +data sample_assertion_octets: List = [ + 162, 105, 115, 105, 103, 110, 97, 116, 117, 114, 101, 88, 70, 48, 68, 2, 32, 73, 232, 20, 255, 65, 30, 188, 245, 66, 178, 243, 134, 50, 55, 116, 67, 201, 214, 3, 244, 165, 80, 216, + 20, 209, 43, 236, 117, 139, 199, 179, 168, 2, 32, 24, 206, 193, 177, 150, 210, 184, 94, 147, 142, 98, 186, 198, 211, 133, 122, 76, 149, 202, 55, 252, 106, 65, 175, 167, 154, 133, 68, 105, + 189, 45, 60, 113, 97, 117, 116, 104, 101, 110, 116, 105, 99, 97, 116, 111, 114, 68, 97, 116, 97, 88, 37, 69, 101, 18, 234, 126, 38, 148, 118, 171, 147, 225, 183, 151, 22, 133, 89, 47, + 247, 63, 137, 74, 192, 236, 47, 213, 72, 8, 160, 139, 251, 108, 143, 64, 0, 0, 0, 1, +] diff --git a/dag/extdeps/standards/rfc_8949.dag b/dag/extdeps/standards/rfc_8949.dag new file mode 100644 index 00000000000..7baeb413a95 --- /dev/null +++ b/dag/extdeps/standards/rfc_8949.dag @@ -0,0 +1,374 @@ +module extdeps.standards.rfc_8949 + +import std.types { Int, String, List } +import std.logic { Bool } +import std.integer { UInt8 } +import std.encoding { utf8_decode_octets } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// RFC 8949, Concise Binary Object Representation (CBOR), STD 94. Cited sections: §3 (the data item +// and its initial byte: major type in the high three bits, additional information in the low +// five), §3.1 (major types 0..7), §3.2 (indefinite-length items), §3.3 (floating-point and simple +// values), §3.4 (tagged items), Appendix A (the examples the witnesses decode), Appendix C (the +// well-formedness pseudocode this decoder is the fold of). +data rfc_8949_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.rfc-editor.org/rfc/rfc8949#section-3" + } +} + +data extdeps_external_authority_anchor: ExternalAuthority = rfc_8949_external_authority_anchor + +// ── What this module decodes, and what it refuses by design ───────────────────────────────── +// The consumer is a verifier over attacker-reachable bytes (extdeps.apple.app_attest: the +// attestation object and the assertion are CBOR), so the decoder is STRICT and its refusals are +// typed and located. Three things a general CBOR reader admits are refused here on purpose: +// +// * indefinite-length strings, arrays and maps (§3.2): the consumers' upstreams emit +// definite-length items, and an unbounded item has no place in a bounded fold; +// * floating-point values (§3.3, major type 7 with additional information 25..27): nothing +// verified here is a float, and admitting one would mean modeling IEEE 754 decoding for a value +// no consumer reads. Major type 7 with 0..24 is a simple value and IS decoded; +// * the reserved additional-information values 28..30 (§3, Table 3). +// +// Integers above 2^53 are refused too: Int is the substrate's integer and a value it cannot carry +// exactly is not decoded into a plausible neighbour. Every refusal names the offset it fired at. + +type CborValue + = CborUnsigned { value: Int } + | CborNegative { value: Int } + | CborByteString { octets: List } + | CborTextString { text: String } + | CborArray { items: List } + | CborMap { entries: List } + | CborTagged { tag: Int, item: CborValue } + | CborSimple { value: Int } + +type CborEntry { + key: CborValue + value: CborValue +} + +type CborRefusal + = CborTruncated { at: Int, needed: Int, available: Int } + | CborIndefiniteLengthRefused { at: Int, major: Int } + | CborFloatRefused { at: Int, info: Int } + | CborReservedAdditionalInfo { at: Int, info: Int } + | CborIntegerBeyondExact { at: Int } + | CborTextNotUtf8 { at: Int } + | CborTrailingOctets { consumed: Int, total: Int } + | CborDepthExceeded { at: Int, limit: Int } + +type CborDecode + = CborDecoded { value: CborValue, next: Int } + | CborRefused { cause: CborRefusal } + +// Nesting is bounded so the fold is: an attestation object nests four deep (map > map > array > +// bytes), an assertion two. A document deeper than this is refused, not descended. +data cbor_nesting_limit: Int = 16 + +// 2^53: the largest magnitude Int carries exactly. +data cbor_exact_integer_bound: Int = 9007199254740992 + +fn cbor_octet_at(octets: List, at: Int) -> Int? { + match octets |> get(at) { + null => none + o => Present { value: o } + } +} + +// The argument (§3): the low five bits select the value directly (0..23) or say how many +// following octets carry it big-endian (24 -> 1, 25 -> 2, 26 -> 4, 27 -> 8). +type CborHead + = CborHeadRead { major: Int, argument: Int, next: Int } + | CborHeadIndefinite { major: Int, next: Int } + | CborHeadRefused { cause: CborRefusal } + +fn cbor_argument_octet_count(info: Int) -> Int { + if info == 24 { 1 } else if info == 25 { 2 } else if info == 26 { 4 } else { 8 } +} + +// Accumulates big-endian while the next octet keeps the value under the exact bound; `none` is +// "beyond exact", decided BEFORE the multiply so a 64-bit host Int is never asked to overflow. +fn cbor_big_endian_value(octets: List, at: Int, n: Int, acc: Int) -> Int? { + if n <= 0 { Present { value: acc } } else { + match cbor_octet_at(octets: octets, at: at) { + Absent => Present { value: acc } + Present { value: o } => + if acc >= cbor_exact_integer_bound / 256 { none } + else { cbor_big_endian_value(octets: octets, at: at + 1, n: n - 1, acc: acc * 256 + o) } + } + } +} + +fn cbor_read_head(octets: List, at: Int) -> CborHead { + match cbor_octet_at(octets: octets, at: at) { + Absent => CborHeadRefused { cause: CborTruncated { at: at, needed: 1, available: 0 } } + Present { value: initial } => { + let major = initial / 32 + let info = initial % 32 + if info < 24 { + CborHeadRead { major: major, argument: info, next: at + 1 } + } else if info == 31 { + CborHeadIndefinite { major: major, next: at + 1 } + } else if info > 27 { + CborHeadRefused { cause: CborReservedAdditionalInfo { at: at, info: info } } + } else if major == 7 && info > 24 { + CborHeadRefused { cause: CborFloatRefused { at: at, info: info } } + } else { + let n = cbor_argument_octet_count(info: info) + let available = count(octets) - (at + 1) + if available < n { + CborHeadRefused { cause: CborTruncated { at: at + 1, needed: n, available: available } } + } else { + match cbor_big_endian_value(octets: octets, at: at + 1, n: n, acc: 0) { + Absent => CborHeadRefused { cause: CborIntegerBeyondExact { at: at } } + Present { value: v } => CborHeadRead { major: major, argument: v, next: at + 1 + n } + } + } + } + } + } +} + +fn cbor_slice(octets: List, at: Int, n: Int) -> List { + octets |> skip(at) |> take(n) +} + +fn cbor_text_of_octets(octets: List) -> String? { + match utf8_decode_octets(octets: octets) { + Absent => none + Present { value: cps } => Present { value: fold(cps, init: "", f: (acc, cp) => acc + from_code_point(cp: cp)) } + } +} + +type CborItemsAcc + = CborItemsOk { items: List, next: Int } + | CborItemsRefused { cause: CborRefusal } + +fn cbor_decode_items(octets: List, at: Int, remaining: Int, depth: Int, acc: List) -> CborItemsAcc { + if remaining <= 0 { CborItemsOk { items: acc, next: at } } else { + match cbor_decode_item(octets: octets, at: at, depth: depth) { + CborRefused { cause: c } => CborItemsRefused { cause: c } + CborDecoded { value: v, next: n } => cbor_decode_items(octets: octets, at: n, remaining: remaining - 1, depth: depth, acc: acc |> list_push(v)) + } + } +} + +type CborEntriesAcc + = CborEntriesOk { entries: List, next: Int } + | CborEntriesRefused { cause: CborRefusal } + +fn cbor_decode_entries(octets: List, at: Int, remaining: Int, depth: Int, acc: List) -> CborEntriesAcc { + if remaining <= 0 { CborEntriesOk { entries: acc, next: at } } else { + match cbor_decode_item(octets: octets, at: at, depth: depth) { + CborRefused { cause: c } => CborEntriesRefused { cause: c } + CborDecoded { value: k, next: n1 } => + match cbor_decode_item(octets: octets, at: n1, depth: depth) { + CborRefused { cause: c } => CborEntriesRefused { cause: c } + CborDecoded { value: v, next: n2 } => + cbor_decode_entries(octets: octets, at: n2, remaining: remaining - 1, depth: depth, acc: acc |> list_push(CborEntry { key: k, value: v })) + } + } + } +} + +fn cbor_decode_string_payload(octets: List, at: Int, n: Int) -> CborRefusal? { + let available = count(octets) - at + if available < n { Present { value: CborTruncated { at: at, needed: n, available: available } } } else { none } +} + +// ONE ITEM AT ONE OFFSET (Appendix C well-formedness, as a fold). `depth` counts the arrays, maps +// and tags this item sits inside; it is the structural descent the nesting limit bounds. +fn cbor_decode_item(octets: List, at: Int, depth: Int) -> CborDecode { + if depth > cbor_nesting_limit { + CborRefused { cause: CborDepthExceeded { at: at, limit: cbor_nesting_limit } } + } else { + match cbor_read_head(octets: octets, at: at) { + CborHeadRefused { cause: c } => CborRefused { cause: c } + CborHeadIndefinite { major: m, next: _ } => CborRefused { cause: CborIndefiniteLengthRefused { at: at, major: m } } + CborHeadRead { major: major, argument: arg, next: next } => + if major == 0 { CborDecoded { value: CborUnsigned { value: arg }, next: next } } + else if major == 1 { CborDecoded { value: CborNegative { value: 0 - 1 - arg }, next: next } } + else if major == 2 { + match cbor_decode_string_payload(octets: octets, at: next, n: arg) { + Present { value: c } => CborRefused { cause: c } + Absent => CborDecoded { value: CborByteString { octets: cbor_slice(octets: octets, at: next, n: arg) }, next: next + arg } + } + } + else if major == 3 { + match cbor_decode_string_payload(octets: octets, at: next, n: arg) { + Present { value: c } => CborRefused { cause: c } + Absent => + match cbor_text_of_octets(octets: cbor_slice(octets: octets, at: next, n: arg)) { + Absent => CborRefused { cause: CborTextNotUtf8 { at: next } } + Present { value: t } => CborDecoded { value: CborTextString { text: t }, next: next + arg } + } + } + } + else if major == 4 { + match cbor_decode_items(octets: octets, at: next, remaining: arg, depth: depth + 1, acc: []) { + CborItemsRefused { cause: c } => CborRefused { cause: c } + CborItemsOk { items: items, next: n } => CborDecoded { value: CborArray { items: items }, next: n } + } + } + else if major == 5 { + match cbor_decode_entries(octets: octets, at: next, remaining: arg, depth: depth + 1, acc: []) { + CborEntriesRefused { cause: c } => CborRefused { cause: c } + CborEntriesOk { entries: entries, next: n } => CborDecoded { value: CborMap { entries: entries }, next: n } + } + } + else if major == 6 { + match cbor_decode_item(octets: octets, at: next, depth: depth + 1) { + CborRefused { cause: c } => CborRefused { cause: c } + CborDecoded { value: v, next: n } => CborDecoded { value: CborTagged { tag: arg, item: v }, next: n } + } + } + else { CborDecoded { value: CborSimple { value: arg }, next: next } } + } + } +} + +// ── The document ───────────────────────────────────────────────────────────────────────────── +// One data item that consumes every octet. Trailing octets are refused (§4.1: a CBOR data item is +// exactly one encoded item; what follows it is another item or garbage, and this decoder is not +// asked to decode a sequence). +type CborDocument + = CborDocumentDecoded { value: CborValue } + | CborDocumentRefused { cause: CborRefusal } + +fn cbor_decode_document(octets: List) -> CborDocument { + match cbor_decode_item(octets: octets, at: 0, depth: 0) { + CborRefused { cause: c } => CborDocumentRefused { cause: c } + CborDecoded { value: v, next: n } => + if n != count(octets) { CborDocumentRefused { cause: CborTrailingOctets { consumed: n, total: count(octets) } } } + else { CborDocumentDecoded { value: v } } + } +} + +// ── Reading a map by text key ──────────────────────────────────────────────────────────────── +// The consumers' maps are keyed by text ("fmt", "attStmt", "authData", "x5c", "receipt", +// "signature", "authenticatorData"). A member is read by its unique text key: a key that occurs +// twice is refused, as extdeps.languages.json.parse json_object_unique_member refuses it, because +// two readers of a duplicate-keyed map can disagree about what was sent (§5.6). +type CborMemberLookup + = CborMemberFound { value: CborValue } + | CborMemberAbsent { key: String } + | CborMemberDuplicated { key: String } + | CborMemberNotAMap + +fn cbor_entries_named(entries: List, key: String) -> List { + fold(entries, init: [], f: (acc, e) => match e.key { + CborTextString { text: t } => if t == key { acc |> list_push(e.value) } else { acc } + _ => acc + }) +} + +fn cbor_map_unique_text_member(v: CborValue, key: String) -> CborMemberLookup { + match v { + CborMap { entries: entries } => { + let hits = cbor_entries_named(entries: entries, key: key) + if count(hits) == 0 { CborMemberAbsent { key: key } } + else if count(hits) > 1 { CborMemberDuplicated { key: key } } + else { + match hits |> get(0) { + null => CborMemberAbsent { key: key } + h => CborMemberFound { value: h } + } + } + } + _ => CborMemberNotAMap + } +} + +fn cbor_byte_string_octets(v: CborValue) -> List? { + match v { + CborByteString { octets: o } => Present { value: o } + _ => none + } +} + +fn cbor_text_string_value(v: CborValue) -> String? { + match v { + CborTextString { text: t } => Present { value: t } + _ => none + } +} + +fn cbor_array_items(v: CborValue) -> List? { + match v { + CborArray { items: i } => Present { value: i } + _ => none + } +} + +fn cbor_unsigned_value(v: CborValue) -> Int? { + match v { + CborUnsigned { value: n } => Present { value: n } + _ => none + } +} + +// Structural equality for witnesses and consumers that compare a decoded item to an expected one. +fn cbor_values_equal(a: CborValue, b: CborValue) -> Bool { + match a { + CborUnsigned { value: x } => match b { + CborUnsigned { value: y } => x == y + _ => false + } + CborNegative { value: x } => match b { + CborNegative { value: y } => x == y + _ => false + } + CborByteString { octets: x } => match b { + CborByteString { octets: y } => x == y + _ => false + } + CborTextString { text: x } => match b { + CborTextString { text: y } => x == y + _ => false + } + CborSimple { value: x } => match b { + CborSimple { value: y } => x == y + _ => false + } + CborTagged { tag: tx, item: ix } => match b { + CborTagged { tag: ty, item: iy } => tx == ty && cbor_values_equal(a: ix, b: iy) + _ => false + } + CborArray { items: xs } => match b { + CborArray { items: ys } => count(xs) == count(ys) && cbor_lists_equal(xs: xs, ys: ys, i: 0) + _ => false + } + CborMap { entries: xs } => match b { + CborMap { entries: ys } => count(xs) == count(ys) && cbor_entries_equal(xs: xs, ys: ys, i: 0) + _ => false + } + } +} + +fn cbor_lists_equal(xs: List, ys: List, i: Int) -> Bool { + if i >= count(xs) { true } else { + match xs |> get(i) { + null => false + x => match ys |> get(i) { + null => false + y => cbor_values_equal(a: x, b: y) && cbor_lists_equal(xs: xs, ys: ys, i: i + 1) + } + } + } +} + +fn cbor_entries_equal(xs: List, ys: List, i: Int) -> Bool { + if i >= count(xs) { true } else { + match xs |> get(i) { + null => false + x => match ys |> get(i) { + null => false + y => cbor_values_equal(a: x.key, b: y.key) && cbor_values_equal(a: x.value, b: y.value) && cbor_entries_equal(xs: xs, ys: ys, i: i + 1) + } + } + } +} diff --git a/dag/extdeps/standards/rfc_9052.dag b/dag/extdeps/standards/rfc_9052.dag new file mode 100644 index 00000000000..32959ffa92e --- /dev/null +++ b/dag/extdeps/standards/rfc_9052.dag @@ -0,0 +1,167 @@ +module extdeps.standards.rfc_9052 + +import std.types { Int, List } +import std.logic { Bool } +import std.integer { UInt8 } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import extdeps.standards.rfc_8949 { CborValue, CborUnsigned, CborNegative, CborByteString, CborMap, CborEntry } + +// RFC 9052, CBOR Object Signing and Encryption (COSE): Structures and Process, §7 (Key Objects): +// a COSE_Key is a CBOR map keyed by integer labels. The labels and the EC2 parameters are registered +// in RFC 9053 §7.1.1 (kty 2 = EC2; crv -1, x -2, y -3) and the IANA COSE registries: kty label 1, +// alg label 3, P-256 is crv 1, ES256 is alg -7. This module reads exactly the EC2 P-256 key shape +// WebAuthn's attestedCredentialData carries for an App Attest credential. +data rfc_9052_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.rfc-editor.org/rfc/rfc9052#section-7" + } +} + +data extdeps_external_authority_anchor: ExternalAuthority = rfc_9052_external_authority_anchor + +data cose_key_label_kty: Int = 1 +data cose_key_label_alg: Int = 3 +data cose_ec2_label_crv: Int = 0 - 1 +data cose_ec2_label_x: Int = 0 - 2 +data cose_ec2_label_y: Int = 0 - 3 +data cose_kty_ec2: Int = 2 +data cose_crv_p256: Int = 1 +data cose_alg_es256: Int = 0 - 7 +data cose_p256_coordinate_octets: Int = 32 + +// Each label is an integer key; a map may carry a label at most once (RFC 9052 §7: "keys in the +// map MUST be unique"), so a duplicated label is refused rather than first- or last-wins. +type CoseLabelLookup + = CoseLabelFound { value: CborValue } + | CoseLabelAbsent { label: Int } + | CoseLabelDuplicated { label: Int } + | CoseKeyNotAMap + +fn cose_label_matches(k: CborValue, label: Int) -> Bool { + match k { + CborUnsigned { value: v } => v == label + CborNegative { value: v } => v == label + _ => false + } +} + +fn cose_entries_labelled(entries: List, label: Int) -> List { + fold(entries, init: [], f: (acc, e) => if cose_label_matches(k: e.key, label: label) { acc |> list_push(e.value) } else { acc }) +} + +fn cose_key_label(key: CborValue, label: Int) -> CoseLabelLookup { + match key { + CborMap { entries: entries } => { + let hits = cose_entries_labelled(entries: entries, label: label) + if count(hits) == 0 { CoseLabelAbsent { label: label } } + else if count(hits) > 1 { CoseLabelDuplicated { label: label } } + else { + match hits |> get(0) { + null => CoseLabelAbsent { label: label } + h => CoseLabelFound { value: h } + } + } + } + _ => CoseKeyNotAMap + } +} + +fn cose_integer_of(v: CborValue) -> Int? { + match v { + CborUnsigned { value: n } => Present { value: n } + CborNegative { value: n } => Present { value: n } + _ => none + } +} + +type CoseKeyRefusal + = CoseKeyLabelRefused { lookup: CoseLabelLookup } + | CoseKeyTypeUnexpected { kty: Int } + | CoseKeyCurveUnexpected { crv: Int } + | CoseKeyAlgorithmUnexpected { alg: Int } + | CoseKeyCoordinateMalformed { label: Int, octets: Int } + | CoseKeyLabelNotAnInteger { label: Int } + +// The one key shape read here: EC2 over P-256 with ES256, x and y each exactly 32 octets. The +// output is the SEC 1 uncompressed point 0x04 || x || y, which is extdeps.crypto.signature's +// Sec1Uncompressed encoding and the input extdeps.crypto.nist_p256 p256_ecdsa_verify_octets takes. +type CoseEc2P256Key + = CoseEc2P256KeyRead { sec1_uncompressed: List } + | CoseEc2P256KeyRefused { cause: CoseKeyRefusal } + +fn cose_required_integer(key: CborValue, label: Int) -> CoseKeyRefusal? { + match cose_key_label(key: key, label: label) { + CoseLabelFound { value: v } => + match cose_integer_of(v: v) { + Present { value: _ } => none + Absent => Present { value: CoseKeyLabelNotAnInteger { label: label } } + } + other => Present { value: CoseKeyLabelRefused { lookup: other } } + } +} + +fn cose_integer_at(key: CborValue, label: Int) -> Int { + match cose_key_label(key: key, label: label) { + CoseLabelFound { value: v } => + match cose_integer_of(v: v) { + Present { value: n } => n + Absent => 0 + } + _ => 0 + } +} + +type CoseCoordinate + = CoseCoordinateRead { octets: List } + | CoseCoordinateRefused { cause: CoseKeyRefusal } + +fn cose_coordinate(key: CborValue, label: Int) -> CoseCoordinate { + match cose_key_label(key: key, label: label) { + CoseLabelFound { value: v } => + match v { + CborByteString { octets: o } => + if count(o) == cose_p256_coordinate_octets { CoseCoordinateRead { octets: o } } + else { CoseCoordinateRefused { cause: CoseKeyCoordinateMalformed { label: label, octets: count(o) } } } + _ => CoseCoordinateRefused { cause: CoseKeyCoordinateMalformed { label: label, octets: 0 } } + } + other => CoseCoordinateRefused { cause: CoseKeyLabelRefused { lookup: other } } + } +} + +fn cose_first_refusal(rs: List) -> CoseKeyRefusal? { + fold(rs, init: none, f: (acc, r) => match acc { + Present { value: a } => Present { value: a } + Absent => r + }) +} + +fn cose_ec2_p256_key(key: CborValue) -> CoseEc2P256Key { + match cose_first_refusal(rs: [ + cose_required_integer(key: key, label: cose_key_label_kty), + cose_required_integer(key: key, label: cose_key_label_alg), + cose_required_integer(key: key, label: cose_ec2_label_crv), + ]) { + Present { value: c } => CoseEc2P256KeyRefused { cause: c } + Absent => { + let kty = cose_integer_at(key: key, label: cose_key_label_kty) + let alg = cose_integer_at(key: key, label: cose_key_label_alg) + let crv = cose_integer_at(key: key, label: cose_ec2_label_crv) + if kty != cose_kty_ec2 { CoseEc2P256KeyRefused { cause: CoseKeyTypeUnexpected { kty: kty } } } + else if alg != cose_alg_es256 { CoseEc2P256KeyRefused { cause: CoseKeyAlgorithmUnexpected { alg: alg } } } + else if crv != cose_crv_p256 { CoseEc2P256KeyRefused { cause: CoseKeyCurveUnexpected { crv: crv } } } + else { + match cose_coordinate(key: key, label: cose_ec2_label_x) { + CoseCoordinateRefused { cause: c } => CoseEc2P256KeyRefused { cause: c } + CoseCoordinateRead { octets: x } => + match cose_coordinate(key: key, label: cose_ec2_label_y) { + CoseCoordinateRefused { cause: c } => CoseEc2P256KeyRefused { cause: c } + CoseCoordinateRead { octets: y } => + CoseEc2P256KeyRead { sec1_uncompressed: concat(concat([4], x), y) } + } + } + } + } + } +} diff --git a/dag/extdeps/standards/webauthn_authenticator_data.dag b/dag/extdeps/standards/webauthn_authenticator_data.dag new file mode 100644 index 00000000000..d6a4729fa67 --- /dev/null +++ b/dag/extdeps/standards/webauthn_authenticator_data.dag @@ -0,0 +1,210 @@ +module extdeps.standards.webauthn_authenticator_data + +import std.types { Int, List } +import std.logic { Bool } +import std.integer { UInt8 } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import extdeps.standards.rfc_8949 { CborValue, CborDecode, CborDecoded, CborRefused, CborRefusal, cbor_decode_item } + +// W3C Web Authentication: An API for accessing Public Key Credentials, Level 3, §6.1 Authenticator +// Data. The byte layout an authenticator emits and a relying party parses: +// +// rpIdHash 32 octets SHA-256 of the RP ID +// flags 1 octet bit 0 UP, bit 2 UV, bit 3 BE, bit 4 BS, bit 6 AT, bit 7 ED +// signCount 4 octets big-endian +// attestedCredentialData variable present iff AT: aaguid (16) || credentialIdLength (2, BE) +// || credentialId || credentialPublicKey (COSE_Key, CBOR) +// extensions variable present iff ED: a CBOR map +// +// Apple App Attest emits this structure in both its objects (extdeps.apple.app_attest): the +// attestation's authData carries AT with the App Attest AAGUID and the credential key; an +// assertion's authenticatorData is the 37-octet prefix alone -- WITH THE AT BIT SET AND NOTHING +// FOLLOWING (extdeps.apple.app_attest_sample_ios_14_4), so an assertion is read by +// decode_authenticator_data_prefix and would be refused as truncated by the full decoder. Apple's +// verification steps 5..8 read rpIdHash, signCount, aaguid and credentialId from here. +data webauthn_authenticator_data_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.w3.org/TR/webauthn-3/#sctn-authenticator-data" + } +} + +data extdeps_external_authority_anchor: ExternalAuthority = webauthn_authenticator_data_external_authority_anchor + +data authenticator_data_rp_id_hash_octets: Int = 32 +data authenticator_data_prefix_octets: Int = 37 +data authenticator_data_aaguid_octets: Int = 16 + +type AuthenticatorFlags { + user_present: Bool + user_verified: Bool + backup_eligible: Bool + backup_state: Bool + attested_credential_data_included: Bool + extension_data_included: Bool +} + +fn flag_bit_set(flags: Int, bit: Int) -> Bool { + let shifted = if bit == 0 { flags } else if bit == 2 { flags / 4 } else if bit == 3 { flags / 8 } else if bit == 4 { flags / 16 } else if bit == 6 { flags / 64 } else { flags / 128 } + shifted % 2 == 1 +} + +fn authenticator_flags_of(octet: Int) -> AuthenticatorFlags { + AuthenticatorFlags { + user_present: flag_bit_set(flags: octet, bit: 0), + user_verified: flag_bit_set(flags: octet, bit: 2), + backup_eligible: flag_bit_set(flags: octet, bit: 3), + backup_state: flag_bit_set(flags: octet, bit: 4), + attested_credential_data_included: flag_bit_set(flags: octet, bit: 6), + extension_data_included: flag_bit_set(flags: octet, bit: 7), + } +} + +type AttestedCredentialData { + aaguid: List + credential_id: List + credential_public_key: CborValue +} + +type AuthenticatorData { + rp_id_hash: List + flags: AuthenticatorFlags + sign_count: Int + attested_credential: AttestedCredentialData? + extensions: CborValue? +} + +type AuthenticatorDataRefusal + = AuthenticatorDataTruncated { at: Int, needed: Int, available: Int } + | AuthenticatorDataCredentialKeyRefused { cause: CborRefusal } + | AuthenticatorDataExtensionsRefused { cause: CborRefusal } + | AuthenticatorDataTrailingOctets { consumed: Int, total: Int } + +type AuthenticatorDataDecode + = AuthenticatorDataDecoded { data: AuthenticatorData } + | AuthenticatorDataRefused { cause: AuthenticatorDataRefusal } + +fn octet_or_zero(octets: List, at: Int) -> Int { + match octets |> get(at) { + null => 0 + o => o + } +} + +fn big_endian_at(octets: List, at: Int, n: Int, acc: Int) -> Int { + if n <= 0 { acc } else { big_endian_at(octets: octets, at: at + 1, n: n - 1, acc: acc * 256 + octet_or_zero(octets: octets, at: at)) } +} + +fn slice(octets: List, at: Int, n: Int) -> List { + octets |> skip(at) |> take(n) +} + +fn truncated_if_short(octets: List, at: Int, needed: Int) -> AuthenticatorDataRefusal? { + let available = count(octets) - at + if available < needed { Present { value: AuthenticatorDataTruncated { at: at, needed: needed, available: available } } } else { none } +} + +type AttestedCredentialRead + = AttestedCredentialRead { credential: AttestedCredentialData, next: Int } + | AttestedCredentialRefused { cause: AuthenticatorDataRefusal } + +// aaguid || credentialIdLength || credentialId || credentialPublicKey, from `at`. The COSE key is +// one CBOR item whose end the CBOR decoder reports, which is what lets extensions follow it. +fn read_attested_credential(octets: List, at: Int) -> AttestedCredentialRead { + match truncated_if_short(octets: octets, at: at, needed: authenticator_data_aaguid_octets + 2) { + Present { value: r } => AttestedCredentialRefused { cause: r } + Absent => { + let aaguid = slice(octets: octets, at: at, n: authenticator_data_aaguid_octets) + let id_len = big_endian_at(octets: octets, at: at + authenticator_data_aaguid_octets, n: 2, acc: 0) + let id_at = at + authenticator_data_aaguid_octets + 2 + match truncated_if_short(octets: octets, at: id_at, needed: id_len) { + Present { value: r } => AttestedCredentialRefused { cause: r } + Absent => + match cbor_decode_item(octets: octets, at: id_at + id_len, depth: 0) { + CborRefused { cause: c } => AttestedCredentialRefused { cause: AuthenticatorDataCredentialKeyRefused { cause: c } } + CborDecoded { value: key, next: n } => AttestedCredentialRead { + credential: AttestedCredentialData { aaguid: aaguid, credential_id: slice(octets: octets, at: id_at, n: id_len), credential_public_key: key }, + next: n, + } + } + } + } + } +} + +type ExtensionsRead + = ExtensionsRead { extensions: CborValue?, next: Int } + | ExtensionsRefused { cause: AuthenticatorDataRefusal } + +fn read_extensions(octets: List, at: Int, included: Bool) -> ExtensionsRead { + if !included { ExtensionsRead { extensions: none, next: at } } else { + match cbor_decode_item(octets: octets, at: at, depth: 0) { + CborRefused { cause: c } => ExtensionsRefused { cause: AuthenticatorDataExtensionsRefused { cause: c } } + CborDecoded { value: v, next: n } => ExtensionsRead { extensions: Present { value: v }, next: n } + } + } +} + +fn authenticator_data_finish(octets: List, rp_id_hash: List, flags: AuthenticatorFlags, sign_count: Int, credential: AttestedCredentialData?, at: Int) -> AuthenticatorDataDecode { + match read_extensions(octets: octets, at: at, included: flags.extension_data_included) { + ExtensionsRefused { cause: r } => AuthenticatorDataRefused { cause: r } + ExtensionsRead { extensions: ext, next: n } => + if n != count(octets) { AuthenticatorDataRefused { cause: AuthenticatorDataTrailingOctets { consumed: n, total: count(octets) } } } + else { + AuthenticatorDataDecoded { data: AuthenticatorData { rp_id_hash: rp_id_hash, flags: flags, sign_count: sign_count, attested_credential: credential, extensions: ext } } + } + } +} + +// THE WHOLE STRUCTURE, consuming every octet: what the flags say is present must be present and +// nothing else may follow. For the assertion reading see decode_authenticator_data_prefix. +fn decode_authenticator_data(octets: List) -> AuthenticatorDataDecode { + match truncated_if_short(octets: octets, at: 0, needed: authenticator_data_prefix_octets) { + Present { value: r } => AuthenticatorDataRefused { cause: r } + Absent => { + let rp_id_hash = slice(octets: octets, at: 0, n: authenticator_data_rp_id_hash_octets) + let flags = authenticator_flags_of(octet: octet_or_zero(octets: octets, at: 32)) + let sign_count = big_endian_at(octets: octets, at: 33, n: 4, acc: 0) + if flags.attested_credential_data_included { + match read_attested_credential(octets: octets, at: authenticator_data_prefix_octets) { + AttestedCredentialRefused { cause: r } => AuthenticatorDataRefused { cause: r } + AttestedCredentialRead { credential: c, next: n } => + authenticator_data_finish(octets: octets, rp_id_hash: rp_id_hash, flags: flags, sign_count: sign_count, credential: Present { value: c }, at: n) + } + } else { + authenticator_data_finish(octets: octets, rp_id_hash: rp_id_hash, flags: flags, sign_count: sign_count, credential: none, at: authenticator_data_prefix_octets) + } + } + } +} + +// ── The 37-octet prefix alone ──────────────────────────────────────────────────────────────── +// rpIdHash || flags || signCount, and nothing else: exactly 37 octets, the flags carried but not +// interpreted as a promise of what follows. This is the assertion reading; a longer input is +// refused as trailing rather than parsed, because the caller asked for the prefix form. +type AuthenticatorDataPrefix { + rp_id_hash: List + flags: AuthenticatorFlags + sign_count: Int +} + +type AuthenticatorDataPrefixDecode + = AuthenticatorDataPrefixDecoded { prefix: AuthenticatorDataPrefix } + | AuthenticatorDataPrefixRefused { cause: AuthenticatorDataRefusal } + +fn decode_authenticator_data_prefix(octets: List) -> AuthenticatorDataPrefixDecode { + match truncated_if_short(octets: octets, at: 0, needed: authenticator_data_prefix_octets) { + Present { value: r } => AuthenticatorDataPrefixRefused { cause: r } + Absent => + if count(octets) != authenticator_data_prefix_octets { + AuthenticatorDataPrefixRefused { cause: AuthenticatorDataTrailingOctets { consumed: authenticator_data_prefix_octets, total: count(octets) } } + } else { + AuthenticatorDataPrefixDecoded { prefix: AuthenticatorDataPrefix { + rp_id_hash: slice(octets: octets, at: 0, n: authenticator_data_rp_id_hash_octets), + flags: authenticator_flags_of(octet: octet_or_zero(octets: octets, at: 32)), + sign_count: big_endian_at(octets: octets, at: 33, n: 4, acc: 0), + } } + } + } +} diff --git a/dag/test/claim/app_attest_sample_decode_witness_test.dag b/dag/test/claim/app_attest_sample_decode_witness_test.dag new file mode 100644 index 00000000000..45ed1f39e37 --- /dev/null +++ b/dag/test/claim/app_attest_sample_decode_witness_test.dag @@ -0,0 +1,199 @@ +module test.claim.app_attest_sample_decode_witness_test + +import std.logic { Bool } +import std.types { Int, String, List, NonEmptyStr } +import std.integer { UInt8 } +import std.encoding { base64_decode, Standard } +import std.bytes { bytes_octets, utf8_encode_bytes } +import extdeps.crypto.sha2 { sha256 } +import extdeps.standards.rfc_8949 { + CborValue, CborTextString, CborByteString, CborArray, CborMap, CborSimple, + CborDocumentDecoded, CborDocumentRefused, cbor_decode_document, + CborMemberFound, cbor_map_unique_text_member, cbor_byte_string_octets, cbor_text_string_value, cbor_array_items, +} +import extdeps.standards.rfc_9052 { CoseEc2P256KeyRead, CoseEc2P256KeyRefused, cose_ec2_p256_key } +import extdeps.standards.webauthn_authenticator_data { + AuthenticatorData, AuthenticatorDataDecoded, AuthenticatorDataRefused, decode_authenticator_data, + AuthenticatorDataTruncated, AuthenticatorDataTrailingOctets, + AuthenticatorDataPrefixDecoded, AuthenticatorDataPrefixRefused, decode_authenticator_data_prefix, +} +import extdeps.apple.app_attest { app_attest_app_id, AppIdPrefix } +import extdeps.apple.app_attest_sample_ios_14_4 { + sample_attestation_octets, sample_assertion_octets, sample_key_id_b64, sample_team_identifier, sample_bundle_identifier, + sample_assertion_counter, +} + +// THE INHABITANCE CLAIMS for the three decoders (DESIGN §3, the pairing obligation): the RFC 8949 +// Appendix A vectors, the COSE label reads and the authenticator-data layout are each claimed over +// designed bytes elsewhere; here the SAME folds run over an object Apple's service actually +// issued, and what they read is compared to the facts the corpus publishes beside it. Deleting +// any of the three decoders reds these; a decoder that agrees with its own fixtures but not with +// Apple's bytes reds these too. + +fn octets_or_empty(b64: String) -> List { + match base64_decode(s: b64, variant: Standard) { + Present { value: o } => o + Absent => [] + } +} + +fn sample_ascii(s: String) -> List { + bytes_octets(b: utf8_encode_bytes(s: s)) +} + +fn sample_attestation() -> CborValue { + match cbor_decode_document(octets: sample_attestation_octets) { + CborDocumentDecoded { value: v } => v + CborDocumentRefused { cause: _ } => CborSimple { value: 23 } + } +} + +fn member_octets(v: CborValue, key: String) -> List { + match cbor_map_unique_text_member(v: v, key: key) { + CborMemberFound { value: m } => + match cbor_byte_string_octets(v: m) { + Present { value: o } => o + Absent => [] + } + _ => [] + } +} + +fn member_value(v: CborValue, key: String) -> CborValue { + match cbor_map_unique_text_member(v: v, key: key) { + CborMemberFound { value: m } => m + _ => CborSimple { value: 23 } + } +} + +// The object is CBOR { fmt: "apple-appattest", attStmt: { x5c: [leaf, ca], receipt }, authData } +// (extdeps.apple.app_attest, "Validation, in Apple's order"). The two certificate lengths and the +// receipt length are the corpus's bytes as decoded, so a decoder that mis-sizes a byte string +// cannot agree with all three. +test fn the_sample_attestation_decodes_to_apples_shape() -> Bool { + let att = sample_attestation() + let fmt = match cbor_text_string_value(v: member_value(v: att, key: "fmt")) { + Present { value: t } => t + Absent => "" + } + let stmt = member_value(v: att, key: "attStmt") + let x5c = match cbor_array_items(v: member_value(v: stmt, key: "x5c")) { + Present { value: items } => items + Absent => [] + } + let leaf_len = match x5c |> get(0) { + null => 0 + c => count(match cbor_byte_string_octets(v: c) { + Present { value: o } => o + Absent => [] + }) + } + let ca_len = match x5c |> get(1) { + null => 0 + c => count(match cbor_byte_string_octets(v: c) { + Present { value: o } => o + Absent => [] + }) + } + fmt == "apple-appattest" && count(x5c) == 2 && leaf_len == 761 && ca_len == 583 + && count(member_octets(v: stmt, key: "receipt")) == 3703 + && count(member_octets(v: att, key: "authData")) == 164 +} + +fn sample_auth_data() -> AuthenticatorData? { + match decode_authenticator_data(octets: member_octets(v: sample_attestation(), key: "authData")) { + AuthenticatorDataDecoded { data: d } => Present { value: d } + AuthenticatorDataRefused { cause: _ } => none + } +} + +// Apple's steps 6, 7 and 8 read from real authData: counter 0, the development AAGUID +// ("appattestdevelop", extdeps.apple.app_attest AppAttestEnvironment), credentialId equal to the +// key id. The AT flag is set and no extensions follow. +test fn the_sample_auth_data_carries_apples_facts() -> Bool { + match sample_auth_data() { + Absent => false + Present { value: d } => + match d.attested_credential { + Absent => false + Present { value: c } => + d.flags.attested_credential_data_included && !d.flags.extension_data_included + && d.sign_count == 0 + && c.aaguid == sample_ascii(s: "appattestdevelop") + && c.credential_id == octets_or_empty(b64: sample_key_id_b64) + && match d.extensions { + Absent => true + Present { value: _ } => false + } + } + } +} + +// Apple's step 5 on real bytes: rpIdHash equals SHA-256 of ".", built by +// app_attest_app_id. This is the one claim that joins extdeps.crypto.sha2 to the sample. +test fn the_sample_rp_id_hash_is_sha256_of_the_app_id() -> Bool { + match sample_auth_data() { + Absent => false + Present { value: d } => + d.rp_id_hash == sha256(message: sample_ascii(s: app_attest_app_id(prefix: sample_team_identifier as AppIdPrefix, bundle_id: sample_bundle_identifier) as String)) + } +} + +// Apple's step 4 on real bytes: the credential public key, read as a COSE EC2 P-256 key and +// rendered as the SEC 1 uncompressed point, hashes to the key id. +test fn the_sample_credential_key_hashes_to_the_key_id() -> Bool { + match sample_auth_data() { + Absent => false + Present { value: d } => + match d.attested_credential { + Absent => false + Present { value: c } => + match cose_ec2_p256_key(key: c.credential_public_key) { + CoseEc2P256KeyRefused { cause: _ } => false + CoseEc2P256KeyRead { sec1_uncompressed: pt } => + count(pt) == 65 && sha256(message: pt) == octets_or_empty(b64: sample_key_id_b64) + } + } + } +} + +// The assertion is CBOR { signature, authenticatorData }: a 37-octet authenticatorData with +// counter 1 and a DER ECDSA signature. Its flags octet is 0x40 -- the AT bit with no attested +// credential data behind it -- so it decodes as the prefix and the full WebAuthn decoder REFUSES +// it; both arms are claimed so the prefix reader cannot be quietly replaced by the full one. +test fn the_sample_assertion_decodes_as_a_prefix_with_counter_one() -> Bool { + match cbor_decode_document(octets: sample_assertion_octets) { + CborDocumentRefused { cause: _ } => false + CborDocumentDecoded { value: v } => { + let ad = member_octets(v: v, key: "authenticatorData") + match decode_authenticator_data_prefix(octets: ad) { + AuthenticatorDataPrefixRefused { cause: _ } => false + AuthenticatorDataPrefixDecoded { prefix: p } => + count(ad) == 37 && p.sign_count == sample_assertion_counter + && p.flags.attested_credential_data_included + && count(member_octets(v: v, key: "signature")) == 70 + && match decode_authenticator_data(octets: ad) { + AuthenticatorDataDecoded { data: _ } => false + AuthenticatorDataRefused { cause: AuthenticatorDataTruncated { at: 37, needed: 18, available: 0 } } => true + AuthenticatorDataRefused { cause: _ } => false + } + } + } + } +} + +// CONTROL: the same real authData with its last octet dropped refuses as truncated inside the +// COSE key, and with one octet appended refuses as trailing. Both name the offset. +test fn the_sample_auth_data_reds_when_cut_or_extended() -> Bool { + let ad = member_octets(v: sample_attestation(), key: "authData") + let cut = ad |> take(163) + let extended = ad |> list_push(0) + match decode_authenticator_data(octets: cut) { + AuthenticatorDataDecoded { data: _ } => false + AuthenticatorDataRefused { cause: _ } => + match decode_authenticator_data(octets: extended) { + AuthenticatorDataRefused { cause: AuthenticatorDataTrailingOctets { consumed: 164, total: 165 } } => true + _ => false + } + } +} diff --git a/dag/test/claim/cbor_rfc8949_witness_test.dag b/dag/test/claim/cbor_rfc8949_witness_test.dag new file mode 100644 index 00000000000..a80209ba3f7 --- /dev/null +++ b/dag/test/claim/cbor_rfc8949_witness_test.dag @@ -0,0 +1,254 @@ +module test.claim.cbor_rfc8949_witness_test + +import std.logic { Bool } +import std.types { Int, String, List } +import std.integer { UInt8 } +import extdeps.standards.rfc_8949 { + CborValue, CborUnsigned, CborNegative, CborByteString, CborTextString, CborArray, CborMap, CborTagged, CborSimple, CborEntry, + CborDocument, CborDocumentDecoded, CborDocumentRefused, + CborRefusal, CborTruncated, CborIndefiniteLengthRefused, CborFloatRefused, CborReservedAdditionalInfo, CborIntegerBeyondExact, + CborTextNotUtf8, CborTrailingOctets, CborDepthExceeded, + cbor_decode_document, cbor_values_equal, + CborMemberLookup, CborMemberFound, CborMemberAbsent, CborMemberDuplicated, CborMemberNotAMap, cbor_map_unique_text_member, + cbor_nesting_limit, +} + +// Every accepted vector below is a row of RFC 8949 Appendix A (Examples of Encoded CBOR Data +// Items); the refused ones are the same appendix's indefinite-length and floating-point rows, +// plus truncations and a trailing octet the appendix does not list because they are not items. + +fn cbor_decodes_to(octets: List, expected: CborValue) -> Bool { + match cbor_decode_document(octets: octets) { + CborDocumentDecoded { value: v } => cbor_values_equal(a: v, b: expected) + CborDocumentRefused { cause: _ } => false + } +} + +fn cbor_refuses(octets: List) -> CborRefusal? { + match cbor_decode_document(octets: octets) { + CborDocumentDecoded { value: _ } => none + CborDocumentRefused { cause: c } => Present { value: c } + } +} + +// 0x00 -> 0; 0x17 -> 23: the argument carried in the initial byte. +test fn appendix_a_small_unsigned_decode() -> Bool { + cbor_decodes_to(octets: [0], expected: CborUnsigned { value: 0 }) && cbor_decodes_to(octets: [23], expected: CborUnsigned { value: 23 }) +} + +// 0x1818 -> 24 (one following octet); 0x1903e8 -> 1000 (two); 0x1a000f4240 -> 1000000 (four); +// 0x1b000000e8d4a51000 -> 1000000000000 (eight). +test fn appendix_a_widened_unsigned_decode() -> Bool { + cbor_decodes_to(octets: [24, 24], expected: CborUnsigned { value: 24 }) + && cbor_decodes_to(octets: [25, 3, 232], expected: CborUnsigned { value: 1000 }) + && cbor_decodes_to(octets: [26, 0, 15, 66, 64], expected: CborUnsigned { value: 1000000 }) + && cbor_decodes_to(octets: [27, 0, 0, 0, 232, 212, 165, 16, 0], expected: CborUnsigned { value: 1000000000000 }) +} + +// 0x20 -> -1; 0x3863 -> -100; 0x3903e7 -> -1000. +test fn appendix_a_negative_decode() -> Bool { + cbor_decodes_to(octets: [32], expected: CborNegative { value: 0 - 1 }) + && cbor_decodes_to(octets: [56, 99], expected: CborNegative { value: 0 - 100 }) + && cbor_decodes_to(octets: [57, 3, 231], expected: CborNegative { value: 0 - 1000 }) +} + +// 0x40 -> h''; 0x4401020304 -> h'01020304'. +test fn appendix_a_byte_string_decode() -> Bool { + cbor_decodes_to(octets: [64], expected: CborByteString { octets: [] }) + && cbor_decodes_to(octets: [68, 1, 2, 3, 4], expected: CborByteString { octets: [1, 2, 3, 4] }) +} + +// 0x60 -> ""; 0x6161 -> "a"; 0x6449455446 -> "IETF"; 0x62c3bc -> "ü" (two-octet UTF-8); +// 0x63e6b0b4 -> "水" (three-octet); 0x64f0908591 -> "𐅑" (four-octet). +test fn appendix_a_text_string_decode() -> Bool { + cbor_decodes_to(octets: [96], expected: CborTextString { text: "" }) + && cbor_decodes_to(octets: [97, 97], expected: CborTextString { text: "a" }) + && cbor_decodes_to(octets: [100, 73, 69, 84, 70], expected: CborTextString { text: "IETF" }) + && cbor_decodes_to(octets: [98, 195, 188], expected: CborTextString { text: "ü" }) + && cbor_decodes_to(octets: [99, 230, 176, 180], expected: CborTextString { text: "水" }) + && cbor_decodes_to(octets: [100, 240, 144, 133, 145], expected: CborTextString { text: "𐅑" }) +} + +// 0x80 -> []; 0x83010203 -> [1, 2, 3]; 0x8301820203820405 -> [1, [2, 3], [4, 5]]. +test fn appendix_a_array_decode() -> Bool { + cbor_decodes_to(octets: [128], expected: CborArray { items: [] }) + && cbor_decodes_to(octets: [131, 1, 2, 3], expected: CborArray { items: [CborUnsigned { value: 1 }, CborUnsigned { value: 2 }, CborUnsigned { value: 3 }] }) + && cbor_decodes_to( + octets: [131, 1, 130, 2, 3, 130, 4, 5], + expected: CborArray { items: [ + CborUnsigned { value: 1 }, + CborArray { items: [CborUnsigned { value: 2 }, CborUnsigned { value: 3 }] }, + CborArray { items: [CborUnsigned { value: 4 }, CborUnsigned { value: 5 }] }, + ] }, + ) +} + +// 0xa0 -> {}; 0xa201020304 -> {1: 2, 3: 4}; 0xa26161016162820203 -> {"a": 1, "b": [2, 3]}. +test fn appendix_a_map_decode() -> Bool { + cbor_decodes_to(octets: [160], expected: CborMap { entries: [] }) + && cbor_decodes_to( + octets: [162, 1, 2, 3, 4], + expected: CborMap { entries: [ + CborEntry { key: CborUnsigned { value: 1 }, value: CborUnsigned { value: 2 } }, + CborEntry { key: CborUnsigned { value: 3 }, value: CborUnsigned { value: 4 } }, + ] }, + ) + && cbor_decodes_to( + octets: [162, 97, 97, 1, 97, 98, 130, 2, 3], + expected: CborMap { entries: [ + CborEntry { key: CborTextString { text: "a" }, value: CborUnsigned { value: 1 } }, + CborEntry { key: CborTextString { text: "b" }, value: CborArray { items: [CborUnsigned { value: 2 }, CborUnsigned { value: 3 }] } }, + ] }, + ) +} + +// 0xc11a514b67b0 -> 1(1363896240): a tagged unsigned. +test fn appendix_a_tagged_decode() -> Bool { + cbor_decodes_to(octets: [193, 26, 81, 75, 103, 176], expected: CborTagged { tag: 1, item: CborUnsigned { value: 1363896240 } }) +} + +// 0xf4 -> false (simple 20); 0xf5 -> true (21); 0xf6 -> null (22); 0xf7 -> undefined (23); +// 0xf0 -> simple(16); 0xf8ff -> simple(255). +test fn appendix_a_simple_decode() -> Bool { + cbor_decodes_to(octets: [244], expected: CborSimple { value: 20 }) + && cbor_decodes_to(octets: [245], expected: CborSimple { value: 21 }) + && cbor_decodes_to(octets: [246], expected: CborSimple { value: 22 }) + && cbor_decodes_to(octets: [247], expected: CborSimple { value: 23 }) + && cbor_decodes_to(octets: [240], expected: CborSimple { value: 16 }) + && cbor_decodes_to(octets: [248, 255], expected: CborSimple { value: 255 }) +} + +// 0x9fff -> [_ ] (indefinite array); 0x5f42010243030405ff (indefinite byte string); +// 0xbf6161016162820203ff (indefinite map): each refuses AT ITS HEAD, naming the major type. +test fn indefinite_length_items_refuse() -> Bool { + match cbor_refuses(octets: [159, 255]) { + Present { value: CborIndefiniteLengthRefused { at: 0, major: 4 } } => + match cbor_refuses(octets: [95, 66, 1, 2, 67, 3, 4, 5, 255]) { + Present { value: CborIndefiniteLengthRefused { at: 0, major: 2 } } => + match cbor_refuses(octets: [191, 97, 97, 1, 97, 98, 130, 2, 3, 255]) { + Present { value: CborIndefiniteLengthRefused { at: 0, major: 5 } } => true + _ => false + } + _ => false + } + _ => false + } +} + +// 0xf93c00 -> 1.0 (half); 0xfa47c35000 -> 100000.0 (single); 0xfb3ff199999999999a -> 1.1 (double). +test fn floating_point_items_refuse() -> Bool { + match cbor_refuses(octets: [249, 60, 0]) { + Present { value: CborFloatRefused { at: 0, info: 25 } } => + match cbor_refuses(octets: [250, 71, 195, 80, 0]) { + Present { value: CborFloatRefused { at: 0, info: 26 } } => + match cbor_refuses(octets: [251, 63, 241, 153, 153, 153, 153, 153, 154]) { + Present { value: CborFloatRefused { at: 0, info: 27 } } => true + _ => false + } + _ => false + } + _ => false + } +} + +// Additional information 28 (0x1c) is reserved (§3, Table 3). +test fn reserved_additional_info_refuses() -> Bool { + match cbor_refuses(octets: [28]) { + Present { value: CborReservedAdditionalInfo { at: 0, info: 28 } } => true + _ => false + } +} + +// The truncations: an empty document; a two-octet argument with one octet present; a byte string +// declaring four octets over three; an array declaring three items over two. +test fn truncated_items_refuse_with_the_offset() -> Bool { + match cbor_refuses(octets: []) { + Present { value: CborTruncated { at: 0, needed: 1, available: 0 } } => + match cbor_refuses(octets: [25, 3]) { + Present { value: CborTruncated { at: 1, needed: 2, available: 1 } } => + match cbor_refuses(octets: [68, 1, 2, 3]) { + Present { value: CborTruncated { at: 1, needed: 4, available: 3 } } => + match cbor_refuses(octets: [131, 1, 2]) { + Present { value: CborTruncated { at: 3, needed: 1, available: 0 } } => true + _ => false + } + _ => false + } + _ => false + } + _ => false + } +} + +// One item followed by another octet is not one document. +test fn trailing_octets_refuse() -> Bool { + match cbor_refuses(octets: [1, 2]) { + Present { value: CborTrailingOctets { consumed: 1, total: 2 } } => true + _ => false + } +} + +// 0x1bffffffffffffffff -> 18446744073709551615, the largest uint64: beyond Int's exact range. +test fn integers_beyond_exact_range_refuse() -> Bool { + match cbor_refuses(octets: [27, 255, 255, 255, 255, 255, 255, 255, 255]) { + Present { value: CborIntegerBeyondExact { at: 0 } } => true + _ => false + } +} + +// A text string whose payload is not UTF-8 (a lone continuation octet) refuses at the payload. +test fn text_string_not_utf8_refuses() -> Bool { + match cbor_refuses(octets: [97, 128]) { + Present { value: CborTextNotUtf8 { at: 1 } } => true + _ => false + } +} + +fn nested_arrays(n: Int, acc: List) -> List { + if n <= 0 { acc |> list_push(128) } else { nested_arrays(n: n - 1, acc: acc |> list_push(129)) } +} + +// One level past the nesting limit refuses; exactly at the limit decodes. The two arms bracket the +// bound so a limit that is not enforced reds the first and a limit off by one reds the second. +test fn nesting_past_the_limit_refuses_and_at_the_limit_decodes() -> Bool { + let past = cbor_refuses(octets: nested_arrays(n: cbor_nesting_limit + 1, acc: [])) + let at = cbor_refuses(octets: nested_arrays(n: cbor_nesting_limit, acc: [])) + match past { + Present { value: CborDepthExceeded { at: _, limit: _ } } => + match at { + Absent => true + _ => false + } + _ => false + } +} + +fn text_keyed_map(octets: List) -> CborValue { + match cbor_decode_document(octets: octets) { + CborDocumentDecoded { value: v } => v + CborDocumentRefused { cause: _ } => CborSimple { value: 23 } + } +} + +// {"a": 1, "b": [2, 3]}: "a" is found, "c" is absent; {"a": 1, "a": 2} is duplicated; an array is +// not a map. +test fn unique_text_member_lookup_discriminates() -> Bool { + let m = text_keyed_map(octets: [162, 97, 97, 1, 97, 98, 130, 2, 3]) + let dup = text_keyed_map(octets: [162, 97, 97, 1, 97, 97, 2]) + match cbor_map_unique_text_member(v: m, key: "a") { + CborMemberFound { value: CborUnsigned { value: 1 } } => + match cbor_map_unique_text_member(v: m, key: "c") { + CborMemberAbsent { key: "c" } => + match cbor_map_unique_text_member(v: dup, key: "a") { + CborMemberDuplicated { key: "a" } => + match cbor_map_unique_text_member(v: CborArray { items: [] }, key: "a") { + CborMemberNotAMap => true + _ => false + } + _ => false + } + _ => false + } + _ => false + } +} diff --git a/dag/test/claim/cose_rfc9052_witness_test.dag b/dag/test/claim/cose_rfc9052_witness_test.dag new file mode 100644 index 00000000000..60c1e20cf9d --- /dev/null +++ b/dag/test/claim/cose_rfc9052_witness_test.dag @@ -0,0 +1,121 @@ +module test.claim.cose_rfc9052_witness_test + +import std.logic { Bool } +import std.types { Int, List } +import std.integer { UInt8 } +import extdeps.standards.rfc_8949 { CborValue, CborUnsigned, CborNegative, CborByteString, CborMap, CborArray, CborEntry } +import extdeps.standards.rfc_9052 { + CoseEc2P256KeyRead, CoseEc2P256KeyRefused, cose_ec2_p256_key, + CoseKeyTypeUnexpected, CoseKeyCurveUnexpected, CoseKeyAlgorithmUnexpected, CoseKeyCoordinateMalformed, CoseKeyLabelRefused, CoseKeyLabelNotAnInteger, + CoseLabelAbsent, CoseLabelDuplicated, CoseKeyNotAMap, +} + +// DESIGNED COSE_Key maps, each one label away from the EC2 P-256 ES256 shape the reader admits. +// The real-producer inhabitance is test.claim.app_attest_sample_decode_witness_test +// the_sample_credential_key_hashes_to_the_key_id, over Apple's bytes. + +fn coordinate(n: Int, fill: Int, acc: List) -> List { + if n <= 0 { acc } else { coordinate(n: n - 1, fill: fill, acc: acc |> list_push(fill)) } +} + +fn label(n: Int) -> CborValue { + if n < 0 { CborNegative { value: n } } else { CborUnsigned { value: n } } +} + +fn cose_entry(k: Int, v: CborValue) -> CborEntry { + CborEntry { key: label(n: k), value: v } +} + +fn ec2_key(kty: Int, alg: Int, crv: Int, x: List, y: List) -> CborValue { + CborMap { entries: [ + cose_entry(k: 1, v: label(n: kty)), + cose_entry(k: 3, v: label(n: alg)), + cose_entry(k: 0 - 1, v: label(n: crv)), + cose_entry(k: 0 - 2, v: CborByteString { octets: x }), + cose_entry(k: 0 - 3, v: CborByteString { octets: y }), + ] } +} + +fn cose_well_formed() -> CborValue { + ec2_key(kty: 2, alg: 0 - 7, crv: 1, x: coordinate(n: 32, fill: 1, acc: []), y: coordinate(n: 32, fill: 2, acc: [])) +} + +// The admitted shape renders 0x04 || x || y, 65 octets, x first. +test fn a_well_formed_ec2_p256_key_renders_the_sec1_point() -> Bool { + match cose_ec2_p256_key(key: cose_well_formed()) { + CoseEc2P256KeyRefused { cause: _ } => false + CoseEc2P256KeyRead { sec1_uncompressed: pt } => + count(pt) == 65 + && match pt |> get(0) { + null => false + o => o == 4 + } + && match pt |> get(1) { + null => false + o => o == 1 + } + && match pt |> get(33) { + null => false + o => o == 2 + } + } +} + +// kty 1 (OKP) is not EC2; crv 2 (P-384) is not P-256; alg -35 (ES384) is not ES256. Each refusal +// names the value it saw, and the checks fire in that order. +test fn a_wrong_type_curve_or_algorithm_refuses_by_name() -> Bool { + let x = coordinate(n: 32, fill: 1, acc: []) + let y = coordinate(n: 32, fill: 2, acc: []) + match cose_ec2_p256_key(key: ec2_key(kty: 1, alg: 0 - 7, crv: 1, x: x, y: y)) { + CoseEc2P256KeyRefused { cause: CoseKeyTypeUnexpected { kty: 1 } } => + match cose_ec2_p256_key(key: ec2_key(kty: 2, alg: 0 - 7, crv: 2, x: x, y: y)) { + CoseEc2P256KeyRefused { cause: CoseKeyCurveUnexpected { crv: 2 } } => + match cose_ec2_p256_key(key: ec2_key(kty: 2, alg: 0 - 35, crv: 1, x: x, y: y)) { + CoseEc2P256KeyRefused { cause: CoseKeyAlgorithmUnexpected { alg: a } } => a == 0 - 35 + _ => false + } + _ => false + } + _ => false + } +} + +// A 31-octet x refuses naming label -2 and 31; a y that is not a byte string refuses with 0. +test fn a_malformed_coordinate_refuses_with_its_label() -> Bool { + match cose_ec2_p256_key(key: ec2_key(kty: 2, alg: 0 - 7, crv: 1, x: coordinate(n: 31, fill: 1, acc: []), y: coordinate(n: 32, fill: 2, acc: []))) { + CoseEc2P256KeyRefused { cause: CoseKeyCoordinateMalformed { label: lx, octets: 31 } } => + lx == 0 - 2 && match cose_ec2_p256_key(key: CborMap { entries: [ + cose_entry(k: 1, v: label(n: 2)), cose_entry(k: 3, v: label(n: 0 - 7)), cose_entry(k: 0 - 1, v: label(n: 1)), + cose_entry(k: 0 - 2, v: CborByteString { octets: coordinate(n: 32, fill: 1, acc: []) }), + cose_entry(k: 0 - 3, v: label(n: 5)), + ] }) { + CoseEc2P256KeyRefused { cause: CoseKeyCoordinateMalformed { label: ly, octets: 0 } } => ly == 0 - 3 + _ => false + } + _ => false + } +} + +// A missing kty, a kty given twice, a kty that is a byte string, and a key that is an array. +test fn label_lookup_refusals_are_carried() -> Bool { + let x = CborByteString { octets: coordinate(n: 32, fill: 1, acc: []) } + let missing = CborMap { entries: [cose_entry(k: 3, v: label(n: 0 - 7)), cose_entry(k: 0 - 1, v: label(n: 1)), cose_entry(k: 0 - 2, v: x), cose_entry(k: 0 - 3, v: x)] } + let twice = CborMap { entries: [cose_entry(k: 1, v: label(n: 2)), cose_entry(k: 1, v: label(n: 2)), cose_entry(k: 3, v: label(n: 0 - 7)), cose_entry(k: 0 - 1, v: label(n: 1)), cose_entry(k: 0 - 2, v: x), cose_entry(k: 0 - 3, v: x)] } + let not_int = CborMap { entries: [cose_entry(k: 1, v: x), cose_entry(k: 3, v: label(n: 0 - 7)), cose_entry(k: 0 - 1, v: label(n: 1)), cose_entry(k: 0 - 2, v: x), cose_entry(k: 0 - 3, v: x)] } + match cose_ec2_p256_key(key: missing) { + CoseEc2P256KeyRefused { cause: CoseKeyLabelRefused { lookup: CoseLabelAbsent { label: 1 } } } => + match cose_ec2_p256_key(key: twice) { + CoseEc2P256KeyRefused { cause: CoseKeyLabelRefused { lookup: CoseLabelDuplicated { label: 1 } } } => + match cose_ec2_p256_key(key: not_int) { + CoseEc2P256KeyRefused { cause: CoseKeyLabelNotAnInteger { label: 1 } } => + match cose_ec2_p256_key(key: CborArray { items: [] }) { + CoseEc2P256KeyRefused { cause: CoseKeyLabelRefused { lookup: CoseKeyNotAMap } } => true + _ => false + } + _ => false + } + _ => false + } + _ => false + } +} From a5530e9dae272f3c93356131a4fd6dac456a2433 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 21 Sep 2026 15:45:19 +0000 Subject: [PATCH 02/88] App Attest step 2: DER (X.690), X.509 (RFC 5280), PEM (RFC 7468) readers in .dag and the pinned Apple App Attestation Root CA, claimed over the sample's real certificate chain extdeps.standards.x690_der reads the DER profile and refuses BER's freedoms by name: indefinite lengths, non-minimal long-form lengths, high tag numbers, unused BIT STRING bits, non-minimal or negative INTEGERs. extdeps.standards.rfc_5280 reads Certificate/TBSCertificate/ AlgorithmIdentifier/Validity/SubjectPublicKeyInfo/Extension, refuses an outer signature algorithm that disagrees with the signed one, looks extensions up uniquely, and renders ECDSA-Sig-Value as fixed-width r||s for the curve verifiers. extdeps.standards.rfc_7468 reads one PEM block. extdeps.apple.app_attest gains the root CA pinned byte for byte from apple.com. Over the sample chain the readers establish, from real bytes: Apple's steps 2 and 3 (the leaf's nonce extension equals SHA-256(authData || clientDataHash)); the leaf's SPKI point IS the credential key the authData carries; leaf -> CA 1 -> pinned root join by DER Name equality; CA 1 and the root are secp384r1 / ecdsa-with-SHA384, so the chain step needs P-384. Co-Authored-By: Claude Opus 5 (1M context) --- dag/extdeps/apple/app_attest.dag | 36 +- dag/extdeps/standards/rfc_5280.dag | 477 +++++++++++++++++++ dag/extdeps/standards/rfc_7468.dag | 59 +++ dag/extdeps/standards/x690_der.dag | 361 ++++++++++++++ dag/test/claim/x509_rfc5280_witness_test.dag | 335 +++++++++++++ 5 files changed, 1267 insertions(+), 1 deletion(-) create mode 100644 dag/extdeps/standards/rfc_5280.dag create mode 100644 dag/extdeps/standards/rfc_7468.dag create mode 100644 dag/extdeps/standards/x690_der.dag create mode 100644 dag/test/claim/x509_rfc5280_witness_test.dag diff --git a/dag/extdeps/apple/app_attest.dag b/dag/extdeps/apple/app_attest.dag index 47823cd66cf..3034319a00e 100644 --- a/dag/extdeps/apple/app_attest.dag +++ b/dag/extdeps/apple/app_attest.dag @@ -1,6 +1,6 @@ module extdeps.apple.app_attest -import std.types { NonEmptyStr, String, Int } +import std.types { NonEmptyStr, String, Int, List } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } @@ -68,6 +68,40 @@ type AttestationRefusal data app_attest_nonce_extension_oid: NonEmptyStr = "1.2.840.113635.100.8.2" + +// ── The trust anchor ───────────────────────────────────────────────────────────────────────── +// Apple App Attestation Root CA, published at apple.com/certificateauthority as PEM and pinned +// here byte for byte: CN=Apple App Attestation Root CA, O=Apple Inc., ST=California; serial +// 0bf3be0ef1cdd2e0fb8c6e721f621798; secp384r1 key; ecdsa-with-SHA384 self-signature; valid +// 2020-03-18 to 2045-03-15; SHA-256 of the DER +// 1cb9823ba28ba6ad2d33a006941de2ae4f513ef1d4e831b9f7e0fa7b6242c932. Step 1 of the validation +// chains x5c to THIS certificate and no other; a rotation is a new pinned row, never a fetch. +data apple_app_attestation_root_ca_pem_lines: List = [ + "-----BEGIN CERTIFICATE-----", + "MIICITCCAaegAwIBAgIQC/O+DvHN0uD7jG5yH2IXmDAKBggqhkjOPQQDAzBSMSYw", + "JAYDVQQDDB1BcHBsZSBBcHAgQXR0ZXN0YXRpb24gUm9vdCBDQTETMBEGA1UECgwK", + "QXBwbGUgSW5jLjETMBEGA1UECAwKQ2FsaWZvcm5pYTAeFw0yMDAzMTgxODMyNTNa", + "Fw00NTAzMTUwMDAwMDBaMFIxJjAkBgNVBAMMHUFwcGxlIEFwcCBBdHRlc3RhdGlv", + "biBSb290IENBMRMwEQYDVQQKDApBcHBsZSBJbmMuMRMwEQYDVQQIDApDYWxpZm9y", + "bmlhMHYwEAYHKoZIzj0CAQYFK4EEACIDYgAERTHhmLW07ATaFQIEVwTtT4dyctdh", + "NbJhFs/Ii2FdCgAHGbpphY3+d8qjuDngIN3WVhQUBHAoMeQ/cLiP1sOUtgjqK9au", + "Yen1mMEvRq9Sk3Jm5X8U62H+xTD3FE9TgS41o0IwQDAPBgNVHRMBAf8EBTADAQH/", + "MB0GA1UdDgQWBBSskRBTM72+aEH/pwyp5frq5eWKoTAOBgNVHQ8BAf8EBAMCAQYw", + "CgYIKoZIzj0EAwMDaAAwZQIwQgFGnByvsiVbpTKwSga0kP0e8EeDS4+sQmTvb7vn", + "53O5+FRXgeLhpJ06ysC5PrOyAjEAp5U4xDgEgllF7En3VcE3iexZZtKeYnpqtijV", + "oyFraWVIyd/dganmrduC1bmTBGwD", + "-----END CERTIFICATE-----", +] + +fn apple_app_attestation_root_ca_pem() -> String { + join(apple_app_attestation_root_ca_pem_lines, "\n") +} + +// The credential certificate's nonce extension value is DER: SEQUENCE { [1] EXPLICIT OCTET +// STRING nonce } (Apple, step 3: "the single octet string ... under the sequence"), so the +// extension's OCTET STRING carries a SEQUENCE carrying a context tag carrying the 32 octets. +data app_attest_nonce_extension_context_tag: Int = 1 + // THE APP ID IS ".". Apple: the prefix is USUALLY the 10-character team // identifier, and is read from the app's Identifier entry in the developer account -- so it is its // own fact, not a second name for the team id, and the verifier is configured with it directly. diff --git a/dag/extdeps/standards/rfc_5280.dag b/dag/extdeps/standards/rfc_5280.dag new file mode 100644 index 00000000000..e9b32f076a3 --- /dev/null +++ b/dag/extdeps/standards/rfc_5280.dag @@ -0,0 +1,477 @@ +module extdeps.standards.rfc_5280 + +import std.types { Int, String, List } +import std.logic { Bool } +import std.integer { UInt8 } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import extdeps.standards.x690_der { + DerElement, DerRefusal, DerRead, DerElementRead, DerRefused, DerContextSpecific, DerUniversal, + der_read_document, DerDocumentRead, DerDocumentRefused, + der_children, DerChildrenRead, DerChildrenRefused, der_child_at, der_expect, der_expect_sequence, der_expect_universal, + der_value, der_tlv, der_unsigned_integer, DerUnsignedRead, DerUnsignedRefused, + der_object_identifier, DerOidRead, DerOidRefused, der_bit_string_octets, DerBitsRead, DerBitsRefused, + der_boolean, DerBoolRead, DerBoolRefused, + der_tag_integer, der_tag_bit_string, der_tag_octet_string, der_tag_object_identifier, der_tag_boolean, der_tag_utc_time, der_tag_generalized_time, der_tag_sequence, + DerTagUnexpected, DerElementAbsent, +} + +// RFC 5280, Internet X.509 PKI Certificate and CRL Profile, §4.1 (the Certificate, TBSCertificate, +// AlgorithmIdentifier, Validity, SubjectPublicKeyInfo and Extension structures) and §4.1.2.5 (Time +// as UTCTime or GeneralizedTime); RFC 5480 §2 for the EC SubjectPublicKeyInfo (id-ecPublicKey with +// a namedCurve parameter) and RFC 5758 §3.2 for the ECDSA signature algorithm identifiers. The +// signature value is ECDSA-Sig-Value (RFC 5480 §2 / SEC 1): SEQUENCE { r INTEGER, s INTEGER }. +// +// This reader decodes the structure and hands out its facts; it does not validate a path. Chain +// verification (issuer/subject join, validity against a clock, signature under the issuer's key) +// is the consumer's fold, because which anchors are trusted and which clock is authoritative are +// the consumer's facts, not the profile's. +data rfc_5280_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.rfc-editor.org/rfc/rfc5280#section-4.1" + } +} + +data extdeps_external_authority_anchor: ExternalAuthority = rfc_5280_external_authority_anchor + +// Object identifiers, dotted as the registries spell them. +data oid_id_ec_public_key: String = "1.2.840.10045.2.1" +data oid_prime256v1: String = "1.2.840.10045.3.1.7" +data oid_secp384r1: String = "1.3.132.0.34" +data oid_ecdsa_with_sha256: String = "1.2.840.10045.4.3.2" +data oid_ecdsa_with_sha384: String = "1.2.840.10045.4.3.3" + +type X509Extension { + oid: String + critical: Bool + value: List +} + +// Names are kept as their DER (the whole Name TLV): the profile's issuer/subject join is byte +// equality of encoded Names under DER (§7.1 permits comparison by exact encoding match first), +// and no consumer here reads a Name's attributes. +type X509Certificate { + tbs_octets: List + serial: List + tbs_signature_algorithm: String + issuer_octets: List + not_before: String + not_after: String + subject_octets: List + spki_algorithm: String + spki_named_curve: String? + spki_public_key: List + extensions: List + signature_algorithm: String + signature_octets: List +} + +type X509Refusal + = X509DerRefused { cause: DerRefusal } + | X509SignatureAlgorithmMismatch { tbs: String, outer: String } + | X509TimeTagUnexpected { at: Int, tag: Int } + | X509ExtensionMalformed { at: Int } + +type X509Decode + = X509Decoded { certificate: X509Certificate } + | X509Refused { cause: X509Refusal } + +fn x509_der(c: DerRefusal) -> X509Decode { + X509Refused { cause: X509DerRefused { cause: c } } +} + +// AlgorithmIdentifier ::= SEQUENCE { algorithm OID, parameters ANY OPTIONAL }. +type AlgorithmIdentifier + = AlgorithmIdentifierRead { algorithm: String, parameters_oid: String? } + | AlgorithmIdentifierRefused { cause: DerRefusal } + +fn read_algorithm_identifier(octets: List, e: DerElement) -> AlgorithmIdentifier { + match der_children(octets: octets, parent: e) { + DerChildrenRefused { cause: c } => AlgorithmIdentifierRefused { cause: c } + DerChildrenRead { elements: kids } => + match der_child_at(children: kids, i: 0, at: e.value_at) { + DerRefused { cause: c } => AlgorithmIdentifierRefused { cause: c } + DerElementRead { element: alg } => + match der_object_identifier(octets: octets, e: alg) { + DerOidRefused { cause: c } => AlgorithmIdentifierRefused { cause: c } + DerOidRead { dotted: oid } => + match kids |> get(1) { + null => AlgorithmIdentifierRead { algorithm: oid, parameters_oid: none } + p => + if p.tag_number == der_tag_object_identifier { + match der_object_identifier(octets: octets, e: p) { + DerOidRefused { cause: c } => AlgorithmIdentifierRefused { cause: c } + DerOidRead { dotted: curve } => AlgorithmIdentifierRead { algorithm: oid, parameters_oid: Present { value: curve } } + } + } else { + AlgorithmIdentifierRead { algorithm: oid, parameters_oid: none } + } + } + } + } + } +} + +fn ascii_of(octets: List) -> String { + fold(octets, init: "", f: (acc, o) => acc + from_code_point(cp: o)) +} + +// Time ::= CHOICE { utcTime UTCTime, generalTime GeneralizedTime }: the contents are kept as the +// ASCII the certificate carries ("210122121335Z" or "20300313000000Z"); interpretation against a +// clock is the consumer's. +type X509Time + = X509TimeRead { text: String } + | X509TimeRefused { cause: X509Refusal } + +fn read_time(octets: List, e: DerElement) -> X509Time { + if e.tag_number == der_tag_utc_time || e.tag_number == der_tag_generalized_time { + X509TimeRead { text: ascii_of(octets: der_value(octets: octets, e: e)) } + } else { + X509TimeRefused { cause: X509TimeTagUnexpected { at: e.header_at, tag: e.tag_number } } + } +} + +type X509Validity + = X509ValidityRead { not_before: String, not_after: String } + | X509ValidityRefused { cause: X509Refusal } + +fn read_validity(octets: List, e: DerElement) -> X509Validity { + match der_children(octets: octets, parent: e) { + DerChildrenRefused { cause: c } => X509ValidityRefused { cause: X509DerRefused { cause: c } } + DerChildrenRead { elements: kids } => + match der_child_at(children: kids, i: 0, at: e.value_at) { + DerRefused { cause: c } => X509ValidityRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: nb } => + match der_child_at(children: kids, i: 1, at: e.value_at) { + DerRefused { cause: c } => X509ValidityRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: na } => + match read_time(octets: octets, e: nb) { + X509TimeRefused { cause: c } => X509ValidityRefused { cause: c } + X509TimeRead { text: b } => + match read_time(octets: octets, e: na) { + X509TimeRefused { cause: c } => X509ValidityRefused { cause: c } + X509TimeRead { text: a } => X509ValidityRead { not_before: b, not_after: a } + } + } + } + } + } +} + +// Extension ::= SEQUENCE { extnID OID, critical BOOLEAN DEFAULT FALSE, extnValue OCTET STRING }. +type X509ExtensionRead + = X509ExtensionOk { extension: X509Extension } + | X509ExtensionRefused { cause: X509Refusal } + +fn read_extension(octets: List, e: DerElement) -> X509ExtensionRead { + match der_children(octets: octets, parent: e) { + DerChildrenRefused { cause: c } => X509ExtensionRefused { cause: X509DerRefused { cause: c } } + DerChildrenRead { elements: kids } => + match der_child_at(children: kids, i: 0, at: e.value_at) { + DerRefused { cause: c } => X509ExtensionRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: id } => + match der_object_identifier(octets: octets, e: id) { + DerOidRefused { cause: c } => X509ExtensionRefused { cause: X509DerRefused { cause: c } } + DerOidRead { dotted: oid } => + if count(kids) == 2 { + match der_child_at(children: kids, i: 1, at: e.value_at) { + DerRefused { cause: c } => X509ExtensionRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: v } => + if v.tag_number != der_tag_octet_string { X509ExtensionRefused { cause: X509ExtensionMalformed { at: e.header_at } } } + else { X509ExtensionOk { extension: X509Extension { oid: oid, critical: false, value: der_value(octets: octets, e: v) } } } + } + } else if count(kids) == 3 { + match der_child_at(children: kids, i: 1, at: e.value_at) { + DerRefused { cause: c } => X509ExtensionRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: crit } => + match der_boolean(octets: octets, e: crit) { + DerBoolRefused { cause: c } => X509ExtensionRefused { cause: X509DerRefused { cause: c } } + DerBoolRead { value: critical } => + match der_child_at(children: kids, i: 2, at: e.value_at) { + DerRefused { cause: c } => X509ExtensionRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: v } => + if v.tag_number != der_tag_octet_string { X509ExtensionRefused { cause: X509ExtensionMalformed { at: e.header_at } } } + else { X509ExtensionOk { extension: X509Extension { oid: oid, critical: critical, value: der_value(octets: octets, e: v) } } } + } + } + } + } else { + X509ExtensionRefused { cause: X509ExtensionMalformed { at: e.header_at } } + } + } + } + } +} + +type X509Extensions + = X509ExtensionsRead { extensions: List } + | X509ExtensionsRefused { cause: X509Refusal } + +fn read_extensions_list(octets: List, kids: List, i: Int, acc: List) -> X509Extensions { + if i >= count(kids) { X509ExtensionsRead { extensions: acc } } else { + match kids |> get(i) { + null => X509ExtensionsRead { extensions: acc } + e => + match read_extension(octets: octets, e: e) { + X509ExtensionRefused { cause: c } => X509ExtensionsRefused { cause: c } + X509ExtensionOk { extension: x } => read_extensions_list(octets: octets, kids: kids, i: i + 1, acc: acc |> list_push(x)) + } + } + } +} + +// extensions [3] EXPLICIT Extensions: the context tag wraps one SEQUENCE OF Extension. +fn read_tbs_extensions(octets: List, wrapper: DerElement) -> X509Extensions { + match der_expect_sequence(octets: octets, at: wrapper.value_at) { + DerRefused { cause: c } => X509ExtensionsRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: seq } => + match der_children(octets: octets, parent: seq) { + DerChildrenRefused { cause: c } => X509ExtensionsRefused { cause: X509DerRefused { cause: c } } + DerChildrenRead { elements: kids } => read_extensions_list(octets: octets, kids: kids, i: 0, acc: []) + } + } +} + +// The TBSCertificate fields after the optional [0] version: the index of serialNumber depends on +// whether version is present. +fn tbs_first_index(kids: List) -> Int { + match kids |> get(0) { + null => 0 + e => match e.tag_class { + DerContextSpecific => if e.tag_number == 0 { 1 } else { 0 } + _ => 0 + } + } +} + +// [3] extensions, wherever it sits after subjectPublicKeyInfo ([1] and [2] unique ids may precede it). +fn tbs_extensions_element(kids: List, from: Int) -> DerElement? { + fold(kids |> skip(from), init: none, f: (acc, e) => match acc { + Present { value: found } => Present { value: found } + Absent => match e.tag_class { + DerContextSpecific => if e.tag_number == 3 { Present { value: e } } else { none } + _ => none + } + }) +} + +type SubjectPublicKeyInfo + = SpkiRead { algorithm: String, named_curve: String?, public_key: List } + | SpkiRefused { cause: DerRefusal } + +fn read_spki(octets: List, e: DerElement) -> SubjectPublicKeyInfo { + match der_children(octets: octets, parent: e) { + DerChildrenRefused { cause: c } => SpkiRefused { cause: c } + DerChildrenRead { elements: kids } => + match der_child_at(children: kids, i: 0, at: e.value_at) { + DerRefused { cause: c } => SpkiRefused { cause: c } + DerElementRead { element: alg } => + match read_algorithm_identifier(octets: octets, e: alg) { + AlgorithmIdentifierRefused { cause: c } => SpkiRefused { cause: c } + AlgorithmIdentifierRead { algorithm: a, parameters_oid: curve } => + match der_child_at(children: kids, i: 1, at: e.value_at) { + DerRefused { cause: c } => SpkiRefused { cause: c } + DerElementRead { element: bits } => + match der_bit_string_octets(octets: octets, e: bits) { + DerBitsRefused { cause: c } => SpkiRefused { cause: c } + DerBitsRead { octets: key } => SpkiRead { algorithm: a, named_curve: curve, public_key: key } + } + } + } + } + } +} + +fn tbs_child(kids: List, i: Int, at: Int) -> DerRead { + der_child_at(children: kids, i: i, at: at) +} + +type TbsRead + = TbsOk { certificate_without_signature: X509Certificate } + | TbsRefused { cause: X509Refusal } + +fn read_tbs(octets: List, tbs: DerElement) -> TbsRead { + match der_children(octets: octets, parent: tbs) { + DerChildrenRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + DerChildrenRead { elements: kids } => { + let i0 = tbs_first_index(kids: kids) + match tbs_child(kids: kids, i: i0, at: tbs.value_at) { + DerRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: serial_e } => + match der_unsigned_integer(octets: octets, e: serial_e) { + DerUnsignedRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + DerUnsignedRead { magnitude: serial } => + match tbs_child(kids: kids, i: i0 + 1, at: tbs.value_at) { + DerRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: sig_alg_e } => + match read_algorithm_identifier(octets: octets, e: sig_alg_e) { + AlgorithmIdentifierRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + AlgorithmIdentifierRead { algorithm: tbs_alg, parameters_oid: _ } => + match tbs_child(kids: kids, i: i0 + 2, at: tbs.value_at) { + DerRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: issuer_e } => + match tbs_child(kids: kids, i: i0 + 3, at: tbs.value_at) { + DerRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: validity_e } => + match read_validity(octets: octets, e: validity_e) { + X509ValidityRefused { cause: c } => TbsRefused { cause: c } + X509ValidityRead { not_before: nb, not_after: na } => + match tbs_child(kids: kids, i: i0 + 4, at: tbs.value_at) { + DerRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: subject_e } => + match tbs_child(kids: kids, i: i0 + 5, at: tbs.value_at) { + DerRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + DerElementRead { element: spki_e } => + match read_spki(octets: octets, e: spki_e) { + SpkiRefused { cause: c } => TbsRefused { cause: X509DerRefused { cause: c } } + SpkiRead { algorithm: spki_alg, named_curve: curve, public_key: key } => + match tbs_extensions_element(kids: kids, from: i0 + 6) { + Absent => TbsOk { certificate_without_signature: X509Certificate { + tbs_octets: der_tlv(octets: octets, e: tbs), serial: serial, tbs_signature_algorithm: tbs_alg, + issuer_octets: der_tlv(octets: octets, e: issuer_e), not_before: nb, not_after: na, + subject_octets: der_tlv(octets: octets, e: subject_e), spki_algorithm: spki_alg, spki_named_curve: curve, spki_public_key: key, + extensions: [], signature_algorithm: "", signature_octets: [], + } } + Present { value: ext_e } => + match read_tbs_extensions(octets: octets, wrapper: ext_e) { + X509ExtensionsRefused { cause: c } => TbsRefused { cause: c } + X509ExtensionsRead { extensions: exts } => TbsOk { certificate_without_signature: X509Certificate { + tbs_octets: der_tlv(octets: octets, e: tbs), serial: serial, tbs_signature_algorithm: tbs_alg, + issuer_octets: der_tlv(octets: octets, e: issuer_e), not_before: nb, not_after: na, + subject_octets: der_tlv(octets: octets, e: subject_e), spki_algorithm: spki_alg, spki_named_curve: curve, spki_public_key: key, + extensions: exts, signature_algorithm: "", signature_octets: [], + } } + } + } + } + } + } + } + } + } + } + } + } + } + } + } +} + +// Certificate ::= SEQUENCE { tbsCertificate, signatureAlgorithm, signatureValue BIT STRING }. The +// outer signatureAlgorithm must equal the TBS's (§4.1.1.2), which is what keeps an attacker from +// naming a weaker algorithm outside the signed bytes. +fn decode_certificate(octets: List) -> X509Decode { + match der_read_document(octets: octets) { + DerDocumentRefused { cause: c } => x509_der(c: c) + DerDocumentRead { element: outer } => + if outer.tag_number != der_tag_sequence { x509_der(c: DerTagUnexpected { at: 0, expected: der_tag_sequence, found: outer.tag_number }) } + else { + match der_children(octets: octets, parent: outer) { + DerChildrenRefused { cause: c } => x509_der(c: c) + DerChildrenRead { elements: kids } => + match der_child_at(children: kids, i: 0, at: outer.value_at) { + DerRefused { cause: c } => x509_der(c: c) + DerElementRead { element: tbs } => + match der_child_at(children: kids, i: 1, at: outer.value_at) { + DerRefused { cause: c } => x509_der(c: c) + DerElementRead { element: alg_e } => + match der_child_at(children: kids, i: 2, at: outer.value_at) { + DerRefused { cause: c } => x509_der(c: c) + DerElementRead { element: sig_e } => + match read_tbs(octets: octets, tbs: tbs) { + TbsRefused { cause: c } => X509Refused { cause: c } + TbsOk { certificate_without_signature: cert } => + match read_algorithm_identifier(octets: octets, e: alg_e) { + AlgorithmIdentifierRefused { cause: c } => x509_der(c: c) + AlgorithmIdentifierRead { algorithm: outer_alg, parameters_oid: _ } => + if outer_alg != cert.tbs_signature_algorithm { X509Refused { cause: X509SignatureAlgorithmMismatch { tbs: cert.tbs_signature_algorithm, outer: outer_alg } } } + else { + match der_bit_string_octets(octets: octets, e: sig_e) { + DerBitsRefused { cause: c } => x509_der(c: c) + DerBitsRead { octets: sig } => X509Decoded { certificate: X509Certificate { + tbs_octets: cert.tbs_octets, serial: cert.serial, tbs_signature_algorithm: cert.tbs_signature_algorithm, + issuer_octets: cert.issuer_octets, not_before: cert.not_before, not_after: cert.not_after, + subject_octets: cert.subject_octets, spki_algorithm: cert.spki_algorithm, spki_named_curve: cert.spki_named_curve, spki_public_key: cert.spki_public_key, + extensions: cert.extensions, signature_algorithm: outer_alg, signature_octets: sig, + } } + } + } + } + } + } + } + } + } + } + } +} + +// ── Reading a certificate ──────────────────────────────────────────────────────────────────── +// An extension by OID, unique: §4.2 says a certificate MUST NOT include more than one instance of +// a particular extension, so two is refused rather than first-wins. +type X509ExtensionLookup + = X509ExtensionFound { extension: X509Extension } + | X509ExtensionAbsent { oid: String } + | X509ExtensionDuplicated { oid: String } + +fn x509_extension(cert: X509Certificate, oid: String) -> X509ExtensionLookup { + let hits = fold(cert.extensions, init: [], f: (acc, x) => if x.oid == oid { acc |> list_push(x) } else { acc }) + if count(hits) == 0 { X509ExtensionAbsent { oid: oid } } + else if count(hits) > 1 { X509ExtensionDuplicated { oid: oid } } + else { + match hits |> get(0) { + null => X509ExtensionAbsent { oid: oid } + h => X509ExtensionFound { extension: h } + } + } +} + +// ECDSA-Sig-Value ::= SEQUENCE { r INTEGER, s INTEGER }, rendered as the fixed-width r || s the +// curve verifiers take (P1363), each coordinate left-padded to `width` octets. A magnitude wider +// than the coordinate refuses: it is not an element of the order. +type EcdsaSigValue + = EcdsaSigValueRead { r_s_fixed: List } + | EcdsaSigValueRefused { cause: DerRefusal } + | EcdsaSigValueTooWide { component_octets: Int, width: Int } + +fn zero_octets(n: Int, acc: List) -> List { + if n <= 0 { acc } else { zero_octets(n: n - 1, acc: acc |> list_push(0)) } +} + +fn left_pad(m: List, width: Int) -> List { + concat(zero_octets(n: width - count(m), acc: []), m) +} + +fn ecdsa_sig_value(octets: List, width: Int) -> EcdsaSigValue { + match der_read_document(octets: octets) { + DerDocumentRefused { cause: c } => EcdsaSigValueRefused { cause: c } + DerDocumentRead { element: seq } => + match der_children(octets: octets, parent: seq) { + DerChildrenRefused { cause: c } => EcdsaSigValueRefused { cause: c } + DerChildrenRead { elements: kids } => + if count(kids) != 2 { EcdsaSigValueRefused { cause: DerElementAbsent { at: seq.value_at } } } + else { + match der_child_at(children: kids, i: 0, at: seq.value_at) { + DerRefused { cause: c } => EcdsaSigValueRefused { cause: c } + DerElementRead { element: re } => + match der_child_at(children: kids, i: 1, at: seq.value_at) { + DerRefused { cause: c } => EcdsaSigValueRefused { cause: c } + DerElementRead { element: se } => + match der_unsigned_integer(octets: octets, e: re) { + DerUnsignedRefused { cause: c } => EcdsaSigValueRefused { cause: c } + DerUnsignedRead { magnitude: r } => + match der_unsigned_integer(octets: octets, e: se) { + DerUnsignedRefused { cause: c } => EcdsaSigValueRefused { cause: c } + DerUnsignedRead { magnitude: s } => + if count(r) > width { EcdsaSigValueTooWide { component_octets: count(r), width: width } } + else if count(s) > width { EcdsaSigValueTooWide { component_octets: count(s), width: width } } + else { EcdsaSigValueRead { r_s_fixed: concat(left_pad(m: r, width: width), left_pad(m: s, width: width)) } } + } + } + } + } + } + } + } +} diff --git a/dag/extdeps/standards/rfc_7468.dag b/dag/extdeps/standards/rfc_7468.dag new file mode 100644 index 00000000000..2d7a8d467a1 --- /dev/null +++ b/dag/extdeps/standards/rfc_7468.dag @@ -0,0 +1,59 @@ +module extdeps.standards.rfc_7468 + +import std.types { Int, String, List } +import std.logic { Bool } +import std.integer { UInt8 } +import std.encoding { base64_decode, Standard } +import std.algebra { trim } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// RFC 7468, Textual Encodings of PKIX, PKCS, and CMS Structures: §2 (the general encapsulation: +// a "-----BEGIN