feat(formal): extend source-linked authorization assurance

.github/workflows/postgres-lifecycle.yml

@@ -26,17 +26,19 @@ jobs:
         with:
           toolchain: 1.97.1
       - name: Start TLS PostgreSQL
-        run: docker compose -f product/stores/auths-stores/tests/postgres_tls/compose.yaml up -d --wait
+        run: |
+          mkdir -p target/test-support/auths-stores/postgres-tls
+          docker compose -f product/stores/auths-stores/tests/postgres_tls/compose.yaml up -d --wait
       - name: Run multi-host lifecycle evidence
         env:
           AUTHS_POSTGRES_URL: host=localhost port=55438 dbname=auths_lifecycle user=auths password=local-fixture-password sslmode=require
-          AUTHS_POSTGRES_CA_PEM: ${{ github.workspace }}/product/stores/auths-stores/tests/postgres_tls/generated/ca.crt
+          AUTHS_POSTGRES_CA_PEM: ${{ github.workspace }}/target/test-support/auths-stores/postgres-tls/ca.crt
           AUTHS_POSTGRES_SERVER_NAME: localhost
         run: cargo test -p auths-stores --test postgres_lifecycle -- --ignored
       - name: Run gateway attempt-store conformance and hostile suites
         env:
           AUTHS_POSTGRES_URL: host=localhost port=55438 dbname=auths_lifecycle user=auths password=local-fixture-password sslmode=require
-          AUTHS_POSTGRES_CA_PEM: ${{ github.workspace }}/product/stores/auths-stores/tests/postgres_tls/generated/ca.crt
+          AUTHS_POSTGRES_CA_PEM: ${{ github.workspace }}/target/test-support/auths-stores/postgres-tls/ca.crt
           AUTHS_POSTGRES_SERVER_NAME: localhost
         run: |
           cargo test -p auths-gateway --lib -- --ignored postgres

.gitleaksignore

@@ -82,3 +82,9 @@ d92064d919b7c2498ce62588ff48a82284f0bcd7:formal/proof-coverage-v1.json:generic-a
 # Ordinary progress prose triggered the generic key rule. The current prose
 # avoids the ambiguous wording; no credential occurred in the historical line.
 3e9704b5d4d12bc654fc48de9b03ab6adb9fcb41:docs/PROGRAM_BOARD.md:generic-api-key:477
+
+# Public upstream function/type identifiers in the immutable Aeneas template:
+# ed25519_dalek::VerifyingKey::verify_strict and its typed arguments, no key
+# bytes or credential. This template is inventoried but never compiled; the
+# separate explicit implementation interface has no global crypto axiom.
+92606918fdb9b6e5163f2e59d210a852004c1e30:formal/qualification/aeneas/generated/signature/FunsExternal_Template.lean:generic-api-key:61

Cargo.toml

@@ -261,7 +261,7 @@ reqwest = { version = "0.13.4", default-features = false, features = ["blocking"
 postgres = { version = "0.19.12", default-features = false }
 r2d2 = "0.8.10"
 r2d2_postgres = "0.18.2"
-rustls = { version = "0.23.45", default-features = false, features = ["ring", "std", "tls12"] }
+rustls = { version = "0.23.46", default-features = false, features = ["ring", "std", "tls12"] }
 rustix = { version = "1.1.4", default-features = false, features = ["fs", "net", "process"] }
 seccompiler = "0.5.0"
 zeroize = { version = "1.9.0", features = ["derive"] }

README.md

@@ -71,15 +71,15 @@ own test key.
   verifiers agree on a shared corpus of test vectors.
 - **Proof coverage, measured.**
   <!-- proof-coverage:begin -->
-  110 of 1,031 decision-scope functions (10.7%) and 1,289 of 11,353 code lines
-  (11.4%) are translated to Lean and reached from audited theorem statements,
-  and 15 of 82 kernel check sites map only to such functions. The rest of the
-  decision path, including the staged verifier control flow, the composition
-  evaluator, the registry handlers, the codec, and the signature suites, is
-  tested, not proved. For K-of-N approval the proofs cover the approval count
-  and per-approver verdict functions and the requirement attenuation law, not
-  the verifier step that classifies each approval (binding, window, signature,
-  status). Figures, method, and what they do not mean:
+  134 of 1,047 decision-scope functions (12.8%) and 1,833 of 11,563 code lines
+  (15.9%) are translated to Lean and reached from audited theorem statements,
+  and 23 of 82 kernel check sites map only to such functions. The rest of the
+  decision path, including the staged verifier control flow, the registry
+  handlers, and the codec, is tested, not proved. For K-of-N approval the proofs
+  cover the approval count and per-approver verdict functions and the
+  requirement attenuation law, not the verifier step that classifies each
+  approval (binding, window, signature, status). Figures, method, and what they
+  do not mean:
   [`docs/assurance/PROOF_COVERAGE.md`](docs/assurance/PROOF_COVERAGE.md).
   <!-- proof-coverage:end -->
 

architecture/dependency-graph.json

@@ -1786,7 +1786,7 @@
       "target": "minicbor",
       "target_layer": null,
       "scope": "external",
-      "kind": "normal",
+      "kind": "dev",
       "target_condition": null,
       "optional": false,
       "default_features": false,

bindings/independent/go/auths/adapters.go

@@ -337,6 +337,9 @@ func decodeMultikey(encoded string) ([]byte, string, error) {
 	}
 	switch {
 	case decoded[0] == 0xed && decoded[1] == 0x01 && len(decoded) == 34:
+		if !canonicalEd25519Encoding(decoded[2:]) {
+			return nil, "", errors.New("invalid Ed25519 multikey")
+		}
 		return decoded[2:], "ed25519-v1", nil
 	case decoded[0] == 0x80 && decoded[1] == 0x24 && len(decoded) == 35:
 		if _, ok := p256PublicKey(decoded[2:]); !ok {

bindings/independent/go/auths/ed25519_encoding.go

@@ -0,0 +1,50 @@
+package auths
+
+import "math/big"
+
+// canonicalEd25519Encoding implements RFC 8032 section 5.1.3's field/sign
+// form. It does not replace curve-point or signature verification.
+func canonicalEd25519Encoding(raw []byte) bool {
+	if len(raw) != 32 {
+		return false
+	}
+	encoded := make([]byte, 32)
+	for i := range raw {
+		encoded[31-i] = raw[i]
+	}
+	negative := encoded[0]&0x80 != 0
+	encoded[0] &= 0x7f
+	ordinate := new(big.Int).SetBytes(encoded)
+	prime := new(big.Int).Sub(new(big.Int).Lsh(big.NewInt(1), 255), big.NewInt(19))
+	orderTwo := new(big.Int).Sub(new(big.Int).Set(prime), big.NewInt(1))
+	return ordinate.Cmp(prime) < 0 && (!negative || (ordinate.Cmp(big.NewInt(1)) != 0 && ordinate.Cmp(orderTwo) != 0))
+}
+
+// For a valid point, y=0 or ±1 has order dividing four; [2]P has y=0
+// exactly when d*y^4+2*y^2-1=0. Substituting RFC 8032's d=-121665/121666
+// gives the remaining order-eight cases, without decoding an x-coordinate.
+// Point recovery and signature verification remain the crypto primitive.
+func strictEd25519PointEncoding(raw []byte) bool {
+	if !canonicalEd25519Encoding(raw) {
+		return false
+	}
+	encoded := make([]byte, 32)
+	for i := range raw {
+		encoded[31-i] = raw[i]
+	}
+	encoded[0] &= 0x7f
+	y := new(big.Int).SetBytes(encoded)
+	prime := new(big.Int).Sub(new(big.Int).Lsh(big.NewInt(1), 255), big.NewInt(19))
+	orderTwo := new(big.Int).Sub(new(big.Int).Set(prime), big.NewInt(1))
+	if y.Sign() == 0 || y.Cmp(big.NewInt(1)) == 0 || y.Cmp(orderTwo) == 0 {
+		return false
+	}
+	square := new(big.Int).Mul(y, y)
+	square.Mod(square, prime)
+	fourth := new(big.Int).Mul(square, square)
+	polynomial := new(big.Int).Mul(fourth, big.NewInt(121665))
+	polynomial.Sub(polynomial, new(big.Int).Mul(square, big.NewInt(243332)))
+	polynomial.Add(polynomial, big.NewInt(121666))
+	polynomial.Mod(polynomial, prime)
+	return polynomial.Sign() != 0
+}

bindings/independent/go/auths/ed25519_encoding_test.go

@@ -0,0 +1,82 @@
+package auths
+
+import (
+	"math/big"
+	"testing"
+)
+
+func coordinateEncoding(value *big.Int, negative bool) []byte {
+	encoded := make([]byte, 32)
+	value.FillBytes(encoded)
+	for left, right := 0, 31; left < right; left, right = left+1, right-1 {
+		encoded[left], encoded[right] = encoded[right], encoded[left]
+	}
+	if negative {
+		encoded[31] |= 128
+	}
+	return encoded
+}
+
+func TestEd25519CanonicalEncodingBoundaries(t *testing.T) {
+	prime := new(big.Int).Sub(new(big.Int).Lsh(big.NewInt(1), 255), big.NewInt(19))
+	for offset := int64(0); offset < 19; offset++ {
+		value := new(big.Int).Add(prime, big.NewInt(offset))
+		for _, negative := range []bool{false, true} {
+			if canonicalEd25519Encoding(coordinateEncoding(value, negative)) {
+				t.Fatal("out-of-field coordinate accepted")
+			}
+		}
+	}
+	for _, value := range []*big.Int{big.NewInt(1), new(big.Int).Sub(prime, big.NewInt(1))} {
+		if !canonicalEd25519Encoding(coordinateEncoding(value, false)) {
+			t.Fatal("canonical boundary refused")
+		}
+		if canonicalEd25519Encoding(coordinateEncoding(value, true)) {
+			t.Fatal("negative zero accepted")
+		}
+	}
+	if !canonicalEd25519Encoding(coordinateEncoding(big.NewInt(0), true)) {
+		t.Fatal("nonzero-x sign choice refused")
+	}
+	for _, length := range []int{0, 31, 33} {
+		if canonicalEd25519Encoding(make([]byte, length)) {
+			t.Fatal("incorrect width accepted")
+		}
+	}
+}
+
+func TestEd25519StrictRejectsWeakSignature(t *testing.T) {
+	prime := new(big.Int).Sub(new(big.Int).Lsh(big.NewInt(1), 255), big.NewInt(19))
+	for _, value := range []*big.Int{big.NewInt(0), big.NewInt(1), new(big.Int).Sub(prime, big.NewInt(1))} {
+		for _, negative := range []bool{false, true} {
+			if strictEd25519PointEncoding(coordinateEncoding(value, negative)) {
+				t.Fatal("small-order point accepted")
+			}
+		}
+	}
+	identity := coordinateEncoding(big.NewInt(1), false)
+	signature := make([]byte, 64)
+	signature[0] = 1
+	if verifySignature("ed25519-v1", identity, []byte("unrelated message"), signature) {
+		t.Fatal("a weak key and R must not authenticate an arbitrary message")
+	}
+}
+
+func TestEd25519OrderEightPointsAreExcluded(t *testing.T) {
+	prime := new(big.Int).Sub(new(big.Int).Lsh(big.NewInt(1), 255), big.NewInt(19))
+	y, ok := new(big.Int).SetString("55188659117513257062467267217118295137698188065244968500265048394206261417927", 10)
+	if !ok {
+		t.Fatal("public torsion coordinate")
+	}
+	for _, value := range []*big.Int{y, new(big.Int).Sub(prime, y)} {
+		for _, negative := range []bool{false, true} {
+			encoded := coordinateEncoding(value, negative)
+			if !canonicalEd25519Encoding(encoded) {
+				t.Fatal("canonical torsion form refused")
+			}
+			if strictEd25519PointEncoding(encoded) {
+				t.Fatal("order-eight point accepted")
+			}
+		}
+	}
+}

bindings/independent/go/auths/p256_corpus_test.go

@@ -0,0 +1,54 @@
+package auths
+
+import (
+	"encoding/hex"
+	"os"
+	"strings"
+	"testing"
+)
+
+func TestPublishedP256CorpusAndStrictAuthsDerivations(t *testing.T) {
+	corpus, err := os.ReadFile("../../../../core/fixtures/crypto/p256-sha256-v1.tsv")
+	if err != nil {
+		t.Fatal(err)
+	}
+	cases, accepted := 0, 0
+	keys := make(map[string]bool)
+	for _, line := range strings.Split(strings.TrimSuffix(string(corpus), "\n"), "\n") {
+		if strings.HasPrefix(line, "#") || strings.HasPrefix(line, "id\t") {
+			continue
+		}
+		fields := strings.Split(line, "\t")
+		if len(fields) != 6 {
+			t.Fatal("fixture fields")
+		}
+		name, result := fields[0], fields[4]
+		switch result {
+		case "ok", "invalid-key", "invalid-signature-encoding", "verification-failed":
+		default:
+			t.Fatalf("unknown fixture result: %s", result)
+		}
+		decode := func(value string) []byte {
+			valueBytes, err := hex.DecodeString(value)
+			if err != nil {
+				t.Fatal(err)
+			}
+			return valueBytes
+		}
+		key, message, signature := decode(fields[1]), decode(fields[2]), decode(fields[3])
+		if verifySignature("p256-sha256-v1", key, message, signature) != (result == "ok") {
+			t.Errorf("signature verdict differs: %s", name)
+		}
+		if _, valid := p256PublicKey(key); valid != (fields[5] == "true") {
+			t.Errorf("key verdict differs: %s", name)
+		}
+		cases++
+		if result == "ok" {
+			accepted++
+			keys[fields[1]] = true
+		}
+	}
+	if cases != 653 || accepted != 173 || len(keys) != 98 {
+		t.Fatalf("incomplete corpus: %d cases, %d accepted, %d keys", cases, accepted, len(keys))
+	}
+}

bindings/independent/go/auths/semantic.go

@@ -1261,8 +1261,9 @@ func evidenceContent(object *evidenceObject) []byte {
 func verifySignature(suite string, key, message, signature []byte) bool {
 	switch suite {
 	case "ed25519-v1":
-		return len(key) == ed25519.PublicKeySize &&
+		return strictEd25519PointEncoding(key) &&
 			len(signature) == ed25519.SignatureSize &&
+			strictEd25519PointEncoding(signature[:32]) &&
 			ed25519.Verify(ed25519.PublicKey(key), message, signature)
 	case "p256-sha256-v1":
 		if len(signature) != 64 {

bindings/independent/typescript/ed25519-encoding.test.ts

@@ -0,0 +1,62 @@
+import assert from "node:assert/strict";
+import test from "node:test";
+import { canonicalEd25519Encoding, strictEd25519PointEncoding } from "./ed25519-encoding.ts";
+
+function coordinate(value: bigint, negative = false): Uint8Array {
+  const bytes = new Uint8Array(32);
+  for (let index = 0; index < 32; index += 1) {
+    bytes[index] = Number(value & 255n);
+    value >>= 8n;
+  }
+  if (negative) bytes[31] = bytes[31]! | 128;
+  return bytes;
+}
+
+test("RFC 8032 field and negative-zero boundaries", () => {
+  const prime = (1n << 255n) - 19n;
+  for (let offset = 0n; offset < 19n; offset += 1n) {
+    for (const negative of [false, true]) {
+      assert.equal(canonicalEd25519Encoding(coordinate(prime + offset, negative)), false);
+    }
+  }
+  for (const value of [1n, prime - 1n]) {
+    assert.equal(canonicalEd25519Encoding(coordinate(value)), true);
+    assert.equal(canonicalEd25519Encoding(coordinate(value, true)), false);
+  }
+  assert.equal(canonicalEd25519Encoding(coordinate(0n, true)), true);
+  for (const length of [0, 31, 33]) assert.equal(canonicalEd25519Encoding(new Uint8Array(length)), false);
+  assert.equal(canonicalEd25519Encoding(new Uint8Array([
+    0xd7, 0x5a, 0x98, 0x01, 0x82, 0xb1, 0x0a, 0xb7,
+    0xd5, 0x4b, 0xfe, 0xd3, 0xc9, 0x64, 0x07, 0x3a,
+    0x0e, 0xe1, 0x72, 0xf3, 0xda, 0xa6, 0x23, 0x25,
+    0xaf, 0x02, 0x1a, 0x68, 0xf7, 0x07, 0x51, 0x1a,
+  ])), true);
+});
+
+test("Auths strict verification excludes canonical small-order points", () => {
+  const prime = (1n << 255n) - 19n;
+  for (const value of [0n, 1n, prime - 1n]) {
+    for (const negative of [false, true]) {
+      assert.equal(strictEd25519PointEncoding(coordinate(value, negative)), false);
+    }
+  }
+  const publicKey = Uint8Array.from([
+    0xd7, 0x5a, 0x98, 0x01, 0x82, 0xb1, 0x0a, 0xb7,
+    0xd5, 0x4b, 0xfe, 0xd3, 0xc9, 0x64, 0x07, 0x3a,
+    0x0e, 0xe1, 0x72, 0xf3, 0xda, 0xa6, 0x23, 0x25,
+    0xaf, 0x02, 0x1a, 0x68, 0xf7, 0x07, 0x51, 0x1a,
+  ]);
+  assert.equal(strictEd25519PointEncoding(publicKey), true);
+});
+
+test("order-eight points are excluded for both sign choices", () => {
+  const prime = (1n << 255n) - 19n;
+  // Public torsion coordinate of Edwards25519, defined by RFC 8032's curve
+  // parameters. The two ordinates and two signs give its four order-eight points.
+  const y = 55188659117513257062467267217118295137698188065244968500265048394206261417927n;
+  for (const value of [y, prime - y]) for (const negative of [false, true]) {
+    const encoded = coordinate(value, negative);
+    assert.equal(canonicalEd25519Encoding(encoded), true);
+    assert.equal(strictEd25519PointEncoding(encoded), false);
+  }
+});

bindings/independent/typescript/ed25519-encoding.ts

@@ -0,0 +1,27 @@
+// RFC 8032 §5.1.3 compressed-coordinate/sign form. Curve and signature
+// verification remain the selected cryptographic primitive's responsibility.
+export function canonicalEd25519Encoding(raw: Uint8Array): boolean {
+  if (raw.length !== 32) return false;
+  const bigEndian = Uint8Array.from(raw).reverse();
+  const negative = (bigEndian[0]! & 0x80) !== 0;
+  bigEndian[0] = bigEndian[0]! & 0x7f;
+  const ordinate = BigInt(`0x${Buffer.from(bigEndian).toString("hex")}`);
+  const prime = (1n << 255n) - 19n;
+  return ordinate < prime && (!negative || (ordinate !== 1n && ordinate !== prime - 1n));
+}
+
+// For a valid Edwards25519 point, y = 0, ±1 has order dividing four.
+// The y-coordinate of [2]P is zero precisely when d*y^4 + 2*y^2 - 1 = 0.
+// With d = -121665/121666, the polynomial below therefore identifies the
+// remaining order-eight points. Point recovery and the signature equation
+// still belong to the crypto primitive; this enforces Auths' strict rule.
+export function strictEd25519PointEncoding(raw: Uint8Array): boolean {
+  if (!canonicalEd25519Encoding(raw)) return false;
+  const bigEndian = Uint8Array.from(raw).reverse();
+  bigEndian[0] = bigEndian[0]! & 0x7f;
+  const y = BigInt(`0x${Buffer.from(bigEndian).toString("hex")}`);
+  const prime = (1n << 255n) - 19n;
+  if (y === 0n || y === 1n || y === prime - 1n) return false;
+  const square = y * y % prime;
+  return (121665n * square * square - 243332n * square + 121666n) % prime !== 0n;
+}