PD-282 — Specification Review (Step 3, Gate 3)
- Story : PD-282 — ProofEnvelope auto-verifiable : scellement HSM global et materiel eIDAS/OCSP embarque
- Reviewer : Claude Opus 4.6 (mode factuel, temperature 0.1)
- Date : 2026-03-02
- Documents audites : PD-282-specification.md, PD-282-tests.md
- Prompt :
3-specification-review v1.2.0 - Note contextuelle : Domaine
legal-compliance (backend NestJS). La note crypto-proof/Prolog est ignoree — cette story porte sur une implementation backend, pas sur la conformite formelle Prolog.
Synthese
| Gravite | Nombre |
| Bloquant | 2 |
| Majeur | 11 |
| Mineur | 3 |
| Total | 16 |
Ecarts identifies
ECR-01 — Tests d'invariants references mais non definis
Type : Incoherence Spec↔Tests
Reference : PD-282-tests.md §2 (matrice de couverture), §5 (table d'invariants) — references TC-INV-06, TC-INV-07, TC-INV-09, TC-INV-10
Description : La matrice de couverture et la table des tests d'invariants citent quatre identifiants de tests (TC-INV-06, TC-INV-07, TC-INV-09, TC-INV-10) comme preuves de couverture. Aucun scenario correspondant n'est defini dans les sections §3 (nominaux), §4 (erreurs) ou §7 (negatifs). Les observables et preconditions de ces tests sont inconnus.
Impact : Tracabilite de preuve cassee pour INV-282-06 (secrets en clair), INV-282-07 (chiffrement au repos), INV-282-09 (terminalite SEALED), INV-282-10 (downgrade interdit). Un auditeur tiers ne peut pas reproduire ces validations.
Gravite : Bloquant
ECR-02 — Contradiction test/spec sur integrite post-alteration
Type : Contradiction
Reference : PD-282-tests.md §3 TC-NOM-02 ("hors normalisation transport") vs PD-282-specification.md §4 INV-282-03 ("Tout octet modifie")
Description : INV-282-03 pose un invariant absolu : "Tout octet modifie dans l'enveloppe scellee DOIT rendre la verification invalide." Le scenario TC-NOM-02 introduit une exception non specifiee : "Un seul octet du JSON canonicalisable est modifie (hors normalisation transport)". Le terme "normalisation transport" n'est defini ni dans la specification ni dans les tests. Cette exclusion affaiblit l'invariant sans contrat explicite sur ce qui constitue une transformation de transport permise.
Impact : Un implementeur peut interpreter "normalisation transport" comme autorisant des transformations (re-encodage, re-serialisation) qui modifient des octets sans invalider le sceau, en violation de INV-282-03.
Gravite : Bloquant
ECR-03 — Politique OCSP simultanement contractualisee et ouverte
Type : Contradiction
Reference : PD-282-specification.md §6 ERR-05 vs §10.2 Q-03
Description : ERR-05 contractualise explicitement le comportement en cas d'OCSP indisponible : "Finalisation autorisee seulement avec validationPolicy=OCSP_UNAVAILABLE et ocspResponses=[]". Simultanement, Q-03 maintient la meme decision comme point a clarifier : "Politique stricte en cas OCSP indisponible — bloquant obligatoire vs mode degrade autorise". Un document contractuel ne peut pas definir un comportement et laisser la meme decision en ouvert dans la meme version.
Impact : Regle decisionnelle non stabilisee ; verdict d'acceptation potentiellement divergent selon la section lue.
Gravite : Majeur
ECR-04 — Critere d'acceptation absolu vs hypothese admettant l'echec (Mode A)
Type : Contradiction
Reference : PD-282-specification.md §7 CA-08 vs §9 H-01
Description : CA-08 definit un critere d'acceptation : "Verification mode A reussit sans reseau ProbatioVault — observable : execution air-gapped positive." H-01 admet explicitement : "La racine de confiance necessaire a la validation cert est disponible cote verificateur — Impact si faux : Mode A peut echouer malgre enveloppe correcte." Le critere est absolu (doit reussir), l'hypothese admet l'echec. Ces deux enonces ne peuvent pas coexister sans que CA-08 soit conditionne a H-01.
Impact : CA-08 est soit un critere conditionnel (ce qui doit etre explicite), soit H-01 est une hypothese incorrecte. En l'etat, un testeur ne sait pas si un echec Mode A doit etre accepte ou rejete.
Gravite : Majeur
ECR-05 — Tests assument journalisation d'audit non specifiee
Type : Incoherence Spec↔Tests
Reference : PD-282-tests.md §3 TC-NOM-01 ("log d'audit de scellement emis avec kid et signedAt"), TC-NOM-02 ("motif d'echec d'integrite est journalise"), §8 (Journal d'audit) vs PD-282-specification.md (aucune section de journalisation)
Description : Plusieurs tests nominaux incluent une clause AND exigeant l'emission de logs d'audit avec des champs specifiques (kid, signedAt, motif d'echec). La section "Observabilite requise" (§8 du document de tests) formalise un "Journal d'audit" comme observable. La specification ne contractualise aucune exigence de journalisation : ni format de log, ni evenements a enregistrer, ni champs obligatoires.
Impact : Les clauses AND des tests TC-NOM-01 et TC-NOM-02 ne sont pas verificables contractuellement. Un implementeur qui ne produit aucun log satisfait la specification mais echoue aux tests.
Gravite : Majeur
ECR-06 — Codes d'erreur non contractualises mais dependants dans les tests
Type : Incoherence Spec↔Tests
Reference : PD-282-tests.md §4 TC-ERR-03 ("Cause crypto explicite journalisee"), §8 ("code d'erreur contractuel") vs PD-282-specification.md §10.2 Q-06
Description : Les tests exigent des codes d'erreur stables et des messages explicites pour les rejets de finalisation. La specification laisse le mapping des codes d'erreur API en clarification ouverte (Q-06 : "code d'erreur contractuel exact attendu"). Les observables de test dependent d'artefacts non specifies.
Impact : Impossible de valider les tests de rejection tant que Q-06 n'est pas resolue. Risque de regression si les codes changent sans contrat.
Gravite : Majeur
ECR-07 — Bornes P95 non testables sans environnement de reference
Type : Non testable
Reference : PD-282-specification.md §5.2 (latence scellement P95 500ms, overhead P95 17KB), §10.2 Q-02 ; PD-282-tests.md §9, TC-NR-05
Description : Les bornes de performance sont contractualisees (latence scellement <= 5000ms max, overhead <= 64KB max) avec des valeurs par defaut (500ms P95, 17KB P95) mais l'environnement de reference n'est pas fixe (Q-02 : "hote cible CPU/RAM/reseau pour valider P95"). Le document de tests confirme explicitement cette regle comme "non testable" (§9). TC-NR-05 exige une mesure conforme au contrat mais admet "Requiert env de reference defini".
Impact : CA-12 n'est pas demonstrable de maniere reproductible. Le critere de non-conformite perf est contestable.
Gravite : Majeur
ECR-08 — Inclusion root CA non fixee avec impact Mode A
Type : Ambiguite
Reference : PD-282-specification.md §5.1.1 (certificateChain[]), §5.1.2 (tsaCertificateChain[], eidasCertificateChain[]), §10.2 Q-05, §9 H-01
Description : L'inclusion de la root CA dans les trois chaines de certificats est laissee en clarification ouverte (Q-05). La verification Mode A (offline strict) depend de la disponibilite de l'ancre de confiance. Si la root CA n'est pas dans la chaine embarquee ET n'est pas dans le trust-store du verificateur, la verification echoue. La decision "obligatoire ou optionnel" a un impact direct sur la taille de l'enveloppe et sur la probabilite de succes en Mode A.
Impact : Resultat de verification offline non predictible ; le contrat ne fixe pas si l'enveloppe se suffit a elle-meme ou depend d'un trust-store externe.
Gravite : Majeur
ECR-09 — Alignement PD-280 assume sans contrat inter-story
Type : Hypothese dangereuse
Reference : PD-282-specification.md §5.4, §9 H-02, §2 (hors perimetre : "Changement de schema d'etat global si PD-280 non disponible")
Description : H-02 assume que PD-280 n'impose pas de transition contradictoire avec SEALED terminal. La specification definit SEALED comme etat terminal sans transition sortante, mais le modele d'etats global de PD-280 (PENDING/INDETERMINATE) pourrait definir des transitions depuis des etats qui englobent ou intersectent SEALED. Aucun contrat inter-story ne garde cette hypothese.
Impact : Risque de conflit d'automate en integration : si PD-280 autorise une transition depuis un etat parent de SEALED, INV-282-09 est viole.
Gravite : Majeur
ECR-10 — OCSP_UNAVAILABLE sans garde-fou de frequence
Type : Risque secu/conformite
Reference : PD-282-specification.md §6 ERR-05, §5.1.2 (validationPolicy enum)
Description : Le mode degrade OCSP_UNAVAILABLE autorise la finalisation sans reponse OCSP. La specification ne definit aucun mecanisme de limitation de ce mode : pas de seuil de frequence, pas d'alerte, pas de quota. Une indisponibilite OCSP prolongee ou provoquee (attaque reseau, manipulation DNS) entrainerait la generation indefinie d'enveloppes sans verification de revocation.
Impact : Un attaquant controlant le reseau entre le backend et le repondeur OCSP peut forcer systematiquement le mode degrade, neutralisant la verification de revocation pour toutes les enveloppes. Aucun signal d'alarme n'est contractualise.
Gravite : Majeur
ECR-11 — TC-NEG-08 comportement dual non tranche
Type : Contradiction
Reference : PD-282-tests.md §7 TC-NEG-08 vs PD-282-specification.md §4 INV-282-06
Description : TC-NEG-08 definit un resultat attendu : "Rejet / nettoyage selon contrat securite". Ces deux comportements (rejet de finalisation OU nettoyage des champs secrets avec finalisation) sont mutuellement exclusifs. INV-282-06 exige qu'aucun secret ne soit "autorise dans l'enveloppe" mais ne mentionne pas de mecanisme de nettoyage. Les cas d'erreur (§6) ne couvrent pas non plus un scenario de nettoyage silencieux.
Impact : Deux implementations conformes au test mais incompatibles entre elles. Un implementeur qui rejette et un qui nettoie satisfont tous deux "Rejet / nettoyage" mais produisent des comportements divergents.
Gravite : Majeur
ECR-12 — tsaCertificateChain sans artefact TSA correspondant
Type : Ambiguite
Reference : PD-282-specification.md §5.1.2 (verificationMaterial.tsaCertificateChain[])
Description : Le verificationMaterial inclut un champ tsaCertificateChain[] (chaine de certificats TSA) comme materiel necessaire a la verification autonome. Aucun artefact TSA correspondant (token RFC 3161, reponse TSA) n'est defini dans la structure de l'enveloppe ou dans le verificationMaterial. La chaine de certificats TSA ne peut servir a rien sans la reponse TSA qu'elle est censee valider. Si le token TSA provient d'un autre composant (PD-81), ce lien n'est pas contractualise.
Impact : Materiel de verification potentiellement incomplet pour la validation temporelle. Un verificateur tiers disposant de la chaine TSA mais pas du token TSA ne peut pas verifier l'horodatage.
Gravite : Majeur
ECR-13 — Reference epic manquante
Type : Incoherence Spec↔Tests
Reference : PD-282-specification.md §10.2 Q-01, References ("Epic : Reference epique non fournie") ; PD-282-tests.md §1 ("EPIC-XX")
Description : La reference d'epic est absente cote specification (Q-01 ouvert) et placeholder cote tests (EPIC-XX). La tracabilite de gouvernance et le chainage contractuel vers l'epic sont incomplets.
Impact : Tracabilite formelle incomplete pour audit. Impact organisationnel, pas technique.
Gravite : Mineur
ECR-14 — "Resolution manuelle uniquement" non definie
Type : Ambiguite
Reference : PD-282-specification.md §5.4 ("SEALED -> * : INTERDITE (etat terminal, resolution manuelle uniquement)")
Description : La mention "resolution manuelle uniquement" entre parentheses apres l'interdiction de transition depuis SEALED introduit un concept non defini dans le contrat. Si SEALED est veritablement terminal sans transition sortante, le terme "resolution manuelle" est contradictoire. Si une resolution manuelle est possible, elle constitue une transition (SEALED -> ?) qui n'est pas specifiee.
Impact : Ambiguite sur le caractere absolu de la terminalite SEALED. Un implementeur pourrait interpreter "resolution manuelle" comme une porte de sortie non contractualisee.
Gravite : Mineur
ECR-15 — Normalisation certSerialNumber : timing non specifie
Type : Ambiguite
Reference : PD-282-specification.md §5.1.2 (ocspResponses[].certSerialNumber : "case-insensitive acceptee, normalisee uppercase")
Description : Le champ certSerialNumber accepte la saisie case-insensitive mais exige une normalisation uppercase. Le moment de cette normalisation n'est pas specifie : a l'ingestion ? au stockage ? a la comparaison ? La regex accepte les deux casses ([0-9A-Fa-f]) mais le contrat de stockage/export n'est pas fixe. Une comparaison entre une valeur stockee non normalisee et une valeur normalisee pourrait echouer.
Impact : Risque de non-correspondance lors de la verification d'une reponse OCSP si la normalisation n'est pas appliquee au meme point par l'implementeur et le verificateur.
Gravite : Mineur
ECR-16 — Detection de secrets non testable exhaustivement
Type : Non testable
Reference : PD-282-specification.md §4 INV-282-06 ("Aucune cle privee, secret HSM, token de session ou secret temporaire en clair") ; PD-282-tests.md §5 TC-INV-06 (non defini), §7 TC-NEG-08
Description : L'invariant exige l'absence de tout secret en clair dans l'enveloppe. Cette propriete negative universelle n'est pas testable exhaustivement : on peut scanner pour des patterns connus (privateKey, token, dek) mais on ne peut pas prouver l'absence de formats de secrets inconnus. Le test TC-INV-06, cense couvrir cet invariant, n'est pas defini (cf. ECR-01). TC-NEG-08 teste l'injection de champs nommes mais ne constitue pas un oracle exhaustif.
Impact : La validation de INV-282-06 est necessairement heuristique. Un audit securite ne peut pas conclure formellement a la conformite sans oracle complet.
Gravite : Majeur
Synthese par axe d'analyse
| Axe | Ecarts |
| Ambiguites | ECR-08, ECR-12, ECR-14, ECR-15 |
| Contradictions | ECR-02, ECR-03, ECR-04, ECR-11 |
| Non testable | ECR-07, ECR-16 |
| Incoherence Spec↔Tests | ECR-01, ECR-05, ECR-06, ECR-13 |
| Hypothese dangereuse | ECR-09 |
| Risque secu/conformite | ECR-10 |
Aucune correction proposee. Aucune reformulation. Aucune implementation.