feat(duvet): RFC 8032 (EdDSA) requirement coverage + annotation-regression CI

.duvet/README.md

@@ -0,0 +1,88 @@
+# Duvet — requirement-to-code coverage for aws-lc
+
+[Duvet](https://github.com/awslabs/duvet) traces normative requirements from a
+specification to the source that implements and tests them. Each requirement is
+cited in-tree with a `//=` annotation, and Duvet reports which requirements are
+covered, tested, or missing.
+
+This directory is a scoped demonstration: it wires **RFC 8032 (EdDSA)** to the
+Ed25519 / Ed25519ph surface in `crypto/fipsmodule/curve25519/`.
+
+## Links
+
+- Duvet project: https://github.com/awslabs/duvet
+- Config schema (v0.4.0): https://awslabs.github.io/duvet/config/v0.4.0.json
+- RFC 8032 (EdDSA): https://www.rfc-editor.org/rfc/rfc8032
+
+## Layout
+
+| Path | Purpose |
+|------|---------|
+| `config.toml` | Source patterns, specifications, requirement patterns, report config |
+| `specifications/` | Cached copy of the spec text Duvet extracts from |
+| `requirements/` | Requirements extracted from the RFC prose (`duvet extract`) |
+| `rfc8032-requirements/` | Hand-authored requirements for descriptive (non-RFC-2119) prose |
+| `scripts/check_annotations.py` | Annotation-regression guard (see below) |
+| `annotations.baseline` | Committed snapshot of source-code annotations |
+| `reports/` | Generated reports — gitignored, never committed |
+
+## Generate reports locally
+
+Install Duvet (Rust toolchain required):
+
+```sh
+cargo install duvet --locked
+```
+
+Generate the HTML + JSON coverage reports (run from the repo root):
+
+```sh
+duvet report
+open .duvet/reports/report.html
+```
+
+Output paths and formats come from the `[report.*]` blocks in `config.toml`.
+`reports/` is gitignored — this PR does not publish the report anywhere.
+
+## Annotation-regression check
+
+`scripts/check_annotations.py` snapshots every source-code `//=` citation Duvet
+finds and fails if any snapshotted annotation is later removed or broken. The
+`Duvet Annotation Coverage` GitHub Actions workflow runs it on every PR that
+touches `.duvet/` or the annotated source, so a dropped citation fails CI.
+
+```sh
+# Verify no baselined annotation went missing (what CI runs):
+python3 .duvet/scripts/check_annotations.py
+
+# After intentionally adding/removing annotations, refresh the baseline:
+python3 .duvet/scripts/check_annotations.py --update
+```
+
+Adding annotations never fails the check — it just reminds you to refresh the
+baseline. Only removals are treated as regressions.
+
+### Why a custom baseline instead of Duvet's `[report.snapshot]`
+
+Duvet's native snapshot records requirement-coverage state — whether a given
+spec requirement is cited at all, and by which kind (impl/test), at spec-section
+granularity. This check instead snapshots every individual source `//=`
+citation, keyed by `target-section + kind + source-file + line`.
+
+The finer granularity is deliberate for shippable crypto source. A requirement
+can stay "covered" at the section level while the specific citation documenting
+one code path is silently dropped during a refactor — the section-level snapshot
+would not flag that, but this check does, and its failure output names the exact
+`file:line` to restore. The tradeoff is that moving an annotated line requires a
+`--update` to re-baseline; that is intended, since a moved citation is exactly
+the kind of change a reviewer should confirm.
+
+## TODOs
+
+- Expand annotation coverage of the extracted RFC 8032 requirements (many
+  `MUST`/`SHOULD` statements are currently uncited — see the HTML report).
+- Add a matching `type=test` annotation for the `section-8.7` implementation
+  citation (currently implementation-only).
+- Decide whether to publish the HTML report (e.g. GitHub Pages) once coverage
+  is meaningful; kept local-only for this PR.
+- Extend the pattern to additional FIPS-relevant specs beyond EdDSA.

.duvet/annotations.baseline

@@ -0,0 +1,5 @@
+https://www.rfc-editor.org/rfc/rfc8032#section-5.1	impl	crypto/fipsmodule/curve25519/curve25519.c	167
+https://www.rfc-editor.org/rfc/rfc8032#section-5.1	impl	crypto/fipsmodule/curve25519/curve25519.c	383
+https://www.rfc-editor.org/rfc/rfc8032#section-5.1	test	crypto/fipsmodule/curve25519/ed25519_test.cc	128
+https://www.rfc-editor.org/rfc/rfc8032#section-5.1	test	crypto/fipsmodule/curve25519/ed25519_test.cc	16
+https://www.rfc-editor.org/rfc/rfc8032#section-8.7	impl	crypto/fipsmodule/curve25519/curve25519.c	312

.duvet/config.toml

@@ -0,0 +1,43 @@
+'$schema' = "https://awslabs.github.io/duvet/config/v0.4.0.json"
+
+# Source patterns: the FIPS-approved-algorithm surface.
+# - crypto/fipsmodule/**  — the module itself (per-algorithm implementations)
+# - crypto/evp/**         — the EVP dispatch layer (public entry points)
+# - include/openssl/evp.h — the public API surface
+
+[[source]]
+pattern = "crypto/fipsmodule/**/*.c"
+
+[[source]]
+pattern = "crypto/fipsmodule/**/*.h"
+
+[[source]]
+pattern = "crypto/fipsmodule/**/*_test.cc"
+type = "test"
+
+[[source]]
+pattern = "crypto/evp/**/*.c"
+
+[[source]]
+pattern = "crypto/evp/*_test.cc"
+type = "test"
+
+[[source]]
+pattern = "include/openssl/evp.h"
+
+# RFC 8032 (EdDSA) — a normative IETF spec, so requirements are extracted
+# from the RFC prose (`duvet extract`) rather than hand-authored. Covers the
+# Ed25519 / Ed25519ph surface in crypto/fipsmodule/curve25519/.
+[[specification]]
+source = "https://www.rfc-editor.org/rfc/rfc8032"
+format = "ietf"
+
+[[requirement]]
+pattern = ".duvet/rfc8032-requirements/**/*.toml"
+
+[report.html]
+enabled = true
+blob-link = "https://github.com/aws/aws-lc/blob/main"
+
+[report.json]
+enabled = true

.duvet/requirements/www.rfc-editor.org/rfc/rfc8032/section-5.1.toml

@@ -0,0 +1,63 @@
+target = "https://www.rfc-editor.org/rfc/rfc8032#section-5.1"
+
+# Ed25519ph, Ed25519ctx, and Ed25519
+#
+#    Ed25519 is EdDSA instantiated with:
+# 
+#    +-----------+-------------------------------------------------------+
+#    | Parameter | Value                                                 |
+#    +-----------+-------------------------------------------------------+
+#    |     p     | p of edwards25519 in [RFC7748] (i.e., 2^255 - 19)     |
+#    |     b     | 256                                                   |
+#    |  encoding | 255-bit little-endian encoding of {0, 1, ..., p-1}    |
+#    |  of GF(p) |                                                       |
+#    |    H(x)   | SHA-512(dom2(phflag,context)||x) [RFC6234]            |
+#    |     c     | base 2 logarithm of cofactor of edwards25519 in       |
+#    |           | [RFC7748] (i.e., 3)                                   |
+#    |     n     | 254                                                   |
+#    |     d     | d of edwards25519 in [RFC7748] (i.e., -121665/121666  |
+#    |           | = 370957059346694393431380835087545651895421138798432 |
+#    |           | 19016388785533085940283555)                           |
+#    |     a     | -1                                                    |
+#    |     B     | (X(P),Y(P)) of edwards25519 in [RFC7748] (i.e., (1511 |
+#    |           | 22213495354007725011514095885315114540126930418572060 |
+#    |           | 46113283949847762202, 4631683569492647816942839400347 |
+#    |           | 5163141307993866256225615783033603165251855960))      |
+#    |     L     | order of edwards25519 in [RFC7748] (i.e.,             |
+#    |           | 2^252+27742317777372353535851937790883648493).        |
+#    |   PH(x)   | x (i.e., the identity function)                       |
+#    +-----------+-------------------------------------------------------+
+# 
+#                       Table 1: Parameters of Ed25519
+# 
+#    For Ed25519, dom2(f,c) is the empty string.  The phflag value is
+#    irrelevant.  The context (if present at all) MUST be empty.  This
+#    causes the scheme to be one and the same with the Ed25519 scheme
+#    published earlier.
+# 
+#    For Ed25519ctx, phflag=0.  The context input SHOULD NOT be empty.
+# 
+#    For Ed25519ph, phflag=1 and PH is SHA512 instead.  That is, the input
+#    is hashed using SHA-512 before signing with Ed25519.
+# 
+#    Value of context is set by the signer and verifier (maximum of 255
+#    octets; the default is empty string, except for Ed25519, which can't
+#    have context) and has to match octet by octet for verification to be
+#    successful.
+# 
+#    The curve used is equivalent to Curve25519 [CURVE25519], under a
+#    change of coordinates, which means that the difficulty of the
+#    discrete logarithm problem is the same as for Curve25519.
+
+[[spec]]
+level = "MUST"
+quote = '''
+The context (if present at all) MUST be empty.
+'''
+
+[[spec]]
+level = "SHOULD"
+quote = '''
+The context input SHOULD NOT be empty.
+'''
+

.duvet/requirements/www.rfc-editor.org/rfc/rfc8032/section-8.3.toml

@@ -0,0 +1,60 @@
+target = "https://www.rfc-editor.org/rfc/rfc8032#section-8.3"
+
+# Use of Contexts
+#
+#    Contexts can be used to separate uses of the protocol between
+#    different protocols (which is very hard to reliably do otherwise) and
+#    between different uses within the same protocol.  However, the
+#    following SHOULD be kept in mind when using this facility:
+# 
+#       The context SHOULD be a constant string specified by the protocol
+#       using it.  It SHOULD NOT incorporate variable elements from the
+#       message itself.
+# 
+#       Contexts SHOULD NOT be used opportunistically, as that kind of use
+#       is very error prone.  If contexts are used, one SHOULD require all
+#       signature schemes available for use in that purpose support
+#       contexts.
+# 
+#       Contexts are an extra input, which percolate out of APIs; as such,
+#       even if the signature scheme supports contexts, those may not be
+#       available for use.  This problem is compounded by the fact that
+#       many times the application is not invoking the signing and
+#       verification functions directly but via some other protocol.
+
+[[spec]]
+level = "SHOULD"
+quote = '''
+However, the
+following SHOULD be kept in mind when using this facility:
+'''
+
+[[spec]]
+level = "SHOULD"
+quote = '''
+The context SHOULD be a constant string specified by the protocol
+using it.
+'''
+
+[[spec]]
+level = "SHOULD"
+quote = '''
+It SHOULD NOT incorporate variable elements from the
+message itself.
+'''
+
+[[spec]]
+level = "SHOULD"
+quote = '''
+Contexts SHOULD NOT be used opportunistically, as that kind of use
+is very error prone.
+'''
+
+[[spec]]
+level = "SHOULD"
+quote = '''
+If contexts are used, one SHOULD require all
+signature schemes available for use in that purpose support
+contexts.
+'''
+

.duvet/requirements/www.rfc-editor.org/rfc/rfc8032/section-8.5.toml

@@ -0,0 +1,44 @@
+target = "https://www.rfc-editor.org/rfc/rfc8032#section-8.5"
+
+# Choice of Signature Primitive
+#
+#    Ed25519 and Ed25519ph have a nominal strength of 128 bits, whereas
+#    Ed448 and Ed448ph have the strength of 224.  While the lower strength
+#    is sufficient for the foreseeable future, the higher level brings
+#    some defense against possible future cryptographic advances.  Both
+#    are demolished by quantum computers just about the same.
+# 
+#    The Ed25519ph and Ed448ph variants are prehashed.  This is mainly
+#    useful for interoperation with legacy APIs, since in most of the
+#    cases, either the amount of data signed is not large or the protocol
+#    is in the position to do digesting in ways better than just
+#    prehashing (e.g., tree hashing or splitting the data).  The
+# 
+#    prehashing also makes the functions greatly more vulnerable to
+#    weaknesses in hash functions used.  These variants SHOULD NOT be
+#    used.
+# 
+#    Ed25519ctx and Ed448 have contexts.  However, this is balanced by the
+#    problems noted in Section 8.3 about contexts.
+# 
+#    On the implementation front, Ed25519 is widely implemented and has
+#    many high-quality implementations.  The others have much worse
+#    support.
+# 
+#    In summary, if a high 128-bit security level is enough, use of
+#    Ed25519 is RECOMMENDED; otherwise, Ed448 is RECOMMENDED.
+
+[[spec]]
+level = "SHOULD"
+quote = '''
+These variants SHOULD NOT be
+used.
+'''
+
+[[spec]]
+level = "SHOULD"
+quote = '''
+In summary, if a high 128-bit security level is enough, use of
+Ed25519 is RECOMMENDED; otherwise, Ed448 is RECOMMENDED.
+'''
+

.duvet/requirements/www.rfc-editor.org/rfc/rfc8032/section-8.7.toml

@@ -0,0 +1,31 @@
+target = "https://www.rfc-editor.org/rfc/rfc8032#section-8.7"
+
+# Signing Large Amounts of Data at Once
+#
+#    Avoid signing large amounts of data at once (where "large" depends on
+#    the expected verifier).  In particular, unless the underlying
+#    protocol does not require it, the receiver MUST buffer the entire
+#    message (or enough information to reconstruct it, e.g., compressed or
+#    encrypted version) to be verified.
+# 
+#    This is needed because most of the time, it is unsafe to process
+#    unverified data, and verifying the signature makes a pass through the
+#    whole message, causing ultimately at least two passes through.
+# 
+#    As an API consideration, this means that any Initialize Update
+#    Finalize (IFU) verification interface is prone to misuse.
+# 
+#    It is a bad idea to modify Ed25519 or Ed448 signing to be able to
+#    create valid Ed25519/Ed448 signatures using an IUF interface with
+#    only constant buffering.  Pretty much any error in such would cause
+#    catastrophic security failure.
+
+[[spec]]
+level = "MUST"
+quote = '''
+In particular, unless the underlying
+protocol does not require it, the receiver MUST buffer the entire
+message (or enough information to reconstruct it, e.g., compressed or
+encrypted version) to be verified.
+'''
+

.duvet/rfc8032-requirements/ed25519ph-prehash.toml

@@ -0,0 +1,12 @@
+target = "https://www.rfc-editor.org/rfc/rfc8032#section-5.1"
+
+# Ed25519ph (HashEdDSA) pre-hash behavior. This is descriptive prose in the
+# RFC, not an RFC-2119 keyword statement, so `duvet extract` does not surface
+# it — we pin it by hand because getting the pre-hash wrong (double-hashing,
+# or hashing an already-digested input) produces signatures no compliant
+# verifier accepts. aws-lc covers it with ED25519ph_sign and the §7.3 KATs.
+[[spec]]
+level = "MUST"
+quote = '''
+For Ed25519ph, phflag=1 and PH is SHA512 instead.
+'''