PD-275 — Conformite PV Anchor ANCHOR-16/17 (Finality Depth & Signer Revocation)¶

1. Objectif¶

Contractualiser les exigences fonctionnelles et de conformite pour corriger les 5 ecarts Prolog restants (checks 28, 29, 30, 31, 32) afin d’atteindre un audit formel PV Anchor a 32/32, sans regression des 27 checks deja conformes.

Corriger explicitement les ecarts majeurs de Gate 3 sur : - la concurrence revokeSigner() / submitBatch(), - l’autorisation de revokeSigner(), - le chemin nominal d’acceptation de finalizeBatch(), - la non-usurpabilite de revokedBy.

2. Perimetre / Hors perimetre¶

Inclus¶

• Ajout du champ persistant confirmation_count sur l’agregat anchor_batch.
• Controle bloquant (fail-closed) de la finalisation d’un batch selon confirmation_count >= FINALITY_DEPTH.
• Introduction d’un registre des signers (signer_registry) avec etat metier ACTIVE | REVOKED.
• Contractualisation de la transition ACTIVE -> REVOKED avec tracabilite (revokedAt, revokedBy).
• Controle bloquant (fail-closed) a la soumission d’un batch si signer non ACTIVE.
• Verification de conformite formelle Prolog post-changement (objectif 32/32).
• Exigence de migration DDL reversible pour les nouveaux objets de schema concernes.
• Contractualisation d’un mecanisme de concurrence sur signer_registry pour serialiser revokeSigner() et submitBatch() concurrents.
• Contractualisation du controle d’autorisation pour revokeSigner() (roles ADMIN ou SIGNER_ADMIN uniquement).
• Contractualisation de la source de revokedBy depuis le contexte d’authentification (jamais depuis le payload appelant).

Exclu¶

• Rotation automatique des signers.
• Multi-signature.
• UI/API d’administration complete des signers hors besoins minimaux de revocation.
• Changement des modeles TLA+ et Alloy (valides en amont).
• Toute derogation fail-open sur controles de securite.

3. Definitions¶

• anchor_batch : lot metier d’ancrage blockchain.
• confirmation_count : nombre de confirmations blockchain persiste pour un batch.
• FINALITY_DEPTH : seuil minimal de confirmations requis pour considerer un batch finalisable.
• signer_registry : registre autoritatif des signers autorises a soumettre.
• ACTIVE : signer autorise a soumettre.
• REVOKED : signer definitivement non autorise a soumettre dans le perimetre PD-275.
• fail-closed : en cas d’incertitude, d’absence de donnee ou d’etat invalide, l’operation est refusee.
• audit trail : traces datees et attribuees des transitions de securite.
• check Prolog : regle de conformite automatique definie dans l’audit PV Anchor.
• actor identity : identite authentifiee effective issue du contexte de securite (JWT sub ou identite de service account).
• revokedBy : projection de actor identity capturee au moment de la revocation; champ derive du contexte d’authentification, jamais fourni par l’appelant.
• SELECT ... FOR UPDATE : verrou pessimiste ligne-a-ligne PostgreSQL utilise pour serialiser les acces concurrents sur signer_registry.

4. Invariants (non negociables)¶

5. Flux nominaux¶

Flux F1 — Mise a jour du nombre de confirmations¶

1. Un batch existant est suivi pour ses confirmations blockchain.
2. Le nombre observe est persiste dans anchor_batch.confirmation_count.
3. Le compteur reste dans les bornes contractuelles (voir §10.2).
4. Le batch reste dans son etat courant tant que les conditions de finalisation ne sont pas remplies.

Flux F2 — Finalisation d’un batch avec garde de finalite¶

1. Une demande de finalisation d’un batch est recue.
2. Le systeme lit confirmation_count et FINALITY_DEPTH.
3. Si confirmation_count >= FINALITY_DEPTH, la transition vers FINALIZED est autorisee.
4. Sinon, la finalisation est refusee (fail-closed) sans transition d’etat.

Flux F3 — Revocation d’un signer¶

1. Une demande de revocation cible une adresse signer existante.
2. Le systeme authentifie l’appelant et verifie les roles; seuls ADMIN ou SIGNER_ADMIN sont autorises.
3. Le systeme ouvre une transaction DB et verrouille la ligne signer ciblee via SELECT ... FOR UPDATE.
4. Le systeme resout l’entree signer_registry correspondante sous verrou.
5. Si statut ACTIVE, transition atomique vers REVOKED + ecriture audit trail (revokedAt, revokedBy).
6. revokedBy est renseigne depuis l’identite authentifiee effective (JWT sub / service account), jamais depuis le payload de requete.
7. Si statut deja REVOKED, refus metier explicite sans nouvel evenement d’audit.
8. Le statut final devient terminal pour ce perimetre (pas de retour autorise).

Flux F4 — Soumission d’un batch avec garde signer actif¶

1. Une demande de soumission de batch est recue avec une identite signer.
2. Le systeme ouvre une transaction DB et verrouille la ligne signer ciblee via SELECT ... FOR UPDATE.
3. Le systeme verifie le statut du signer dans signer_registry sous verrou.
4. Si statut ACTIVE, la soumission peut poursuivre son flux nominal dans la meme transaction metier.
5. Si statut REVOKED (ou introuvable), soumission refusee immediatement (fail-closed).
6. La semantique concurrente est serialisee par ordre d’acquisition du verrou :
7. si revokeSigner() acquiert le verrou en premier et commit REVOKED, submitBatch() concurrent est refuse;
8. si submitBatch() acquiert le verrou en premier et valide la soumission, revokeSigner() attend puis applique REVOKED apres commit.

Modele d’etats et transitions retour (obligatoire)¶

• Signer state machine
• ACTIVE -> REVOKED : AUTORISEE (via revocation validee + autorisation role)
• REVOKED -> ACTIVE : INTERDITE (hors perimetre PD-275; eviter reactivation implicite)

• REVOKED -> * : INTERDITE (etat terminal, resolution manuelle uniquement)

• Batch (etats partiels identifies dans ce besoin)

• NON_FINALIZED -> FINALIZED : AUTORISEE uniquement si garde de finalite satisfaite

• FINALIZED -> * : INTERDITE (etat terminal dans ce perimetre; aucune transition retour specifiee)

• Checklist machine a etats

• Chaque etat identifie a des transitions sortantes documentees (autorisees/interdites)
• Chaque etat terminal identifie a la mention -> * : INTERDITE
• Couverture par invariant dedie (INV-275-07-state-machine-complete)

5bis. Diagrammes¶

5bis.1 Machine a etats — Signer (signer_registry)¶

stateDiagram-v2
    [*] --> ACTIVE : enregistrement initial

    ACTIVE --> REVOKED : revokeSigner()\n[role ADMIN | SIGNER_ADMIN]\n+ audit trail (revokedAt, revokedBy)

    REVOKED --> [*] : etat terminal\n(INV-275-06)

    note right of ACTIVE
        INV-275-04 : source de verite statut signer
        INV-275-09 : autorisation ADMIN | SIGNER_ADMIN
        INV-275-11 : SELECT ... FOR UPDATE
    end note

    note right of REVOKED
        INV-275-06 : REVOKED -> * INTERDITE
        INV-275-05 : revocation atomique + audit
        INV-275-12 : une seule transition autorisee
        Tentative re-revocation : ERR-SIGNER-ALREADY-REVOKED
    end note

5bis.2 Machine a etats — Batch (anchor_batch)¶

stateDiagram-v2
    [*] --> NON_FINALIZED : creation batch\n(confirmation_count = 0)

    NON_FINALIZED --> NON_FINALIZED : mise a jour confirmation_count\n(F1 : suivi confirmations)

    NON_FINALIZED --> FINALIZED : finalizeBatch()\n[confirmation_count >= FINALITY_DEPTH]\n(INV-275-02)

    FINALIZED --> [*] : etat terminal

    note right of NON_FINALIZED
        INV-275-03 : confirmation_count persistant, entier, init 0
        INV-275-01 : fail-closed si preconditions non demontrees
        Garde : confirmation_count < FINALITY_DEPTH -> ERR-FINALITY-INSUFFICIENT
    end note

    note right of FINALIZED
        INV-275-07 : FINALIZED -> * INTERDITE
        Etat terminal dans le perimetre PD-275
    end note

5bis.3 Diagramme de sequence — Flux complet (F1 a F4)¶

sequenceDiagram
    autonumber
    participant BC as Blockchain Network
    participant Worker as Confirmation Worker
    participant Service as Anchor Service
    participant DB as PostgreSQL
    participant Registry as signer_registry
    participant Audit as Audit Trail
    participant Caller as Appelant (API)

    %% F1 — Mise a jour confirmation_count
    rect rgb(230, 245, 255)
        note over BC, DB: F1 — Mise a jour du nombre de confirmations
        BC ->> Worker : nouveau bloc confirme
        Worker ->> Service : updateConfirmationCount(batchId, n)
        Service ->> DB : UPDATE anchor_batch SET confirmation_count = n\nWHERE id = batchId AND n BETWEEN 0 AND 2147483647
        alt n hors bornes contractuelles
            DB -->> Service : ERR-CONFIRMATION-COUNT-INVALID
            Service -->> Worker : rejet mise a jour
        else n valide
            DB -->> Service : OK (confirmation_count persiste)
            Service -->> Worker : OK
        end
    end

    %% F2 — Finalisation batch
    rect rgb(230, 255, 230)
        note over Caller, DB: F2 — Finalisation avec garde de finalite (INV-275-02)
        Caller ->> Service : finalizeBatch(batchId)
        Service ->> DB : SELECT confirmation_count FROM anchor_batch WHERE id = batchId
        DB -->> Service : confirmation_count = C
        alt C >= FINALITY_DEPTH
            Service ->> DB : UPDATE anchor_batch SET status = ‘FINALIZED’
            DB -->> Service : OK
            Service -->> Caller : 200 FINALIZED
        else C < FINALITY_DEPTH (fail-closed, INV-275-01)
            Service -->> Caller : 422 ERR-FINALITY-INSUFFICIENT\n(aucun changement d’etat)
        end
    end

    %% F3 — Revocation signer
    rect rgb(255, 240, 230)
        note over Caller, Audit: F3 — Revocation signer (INV-275-05, 09, 10, 11, 12)
        Caller ->> Service : revokeSigner(address)\n[JWT sub = actor-A]
        Service ->> Service : verifier role (ADMIN | SIGNER_ADMIN)
        alt role non autorise
            Service -->> Caller : 403 ERR-REVOKE-UNAUTHORIZED
        else role autorise
            Service ->> Service : rejeter si revokedBy dans payload\n(INV-275-10)
            alt revokedBy dans payload
                Service -->> Caller : 400 ERR-REVOKEDBY-SPOOFING
            else payload conforme
                Service ->> DB : BEGIN TRANSACTION
                Service ->> Registry : SELECT ... FOR UPDATE\nWHERE address = X (INV-275-11)
                Registry -->> Service : signer row (verrouillee)
                alt status = ACTIVE
                    Service ->> Registry : UPDATE status = ‘REVOKED’,\nrevokedAt = NOW(), revokedBy = actor-A
                    Service ->> Audit : INSERT audit event\n(ACTIVE -> REVOKED, actor-A)
                    Service ->> DB : COMMIT
                    Service -->> Caller : 200 REVOKED
                else status = REVOKED (INV-275-12)
                    Service ->> DB : ROLLBACK
                    Service -->> Caller : 409 ERR-SIGNER-ALREADY-REVOKED\n(aucun nouvel audit trail)
                else signer introuvable
                    Service ->> DB : ROLLBACK
                    Service -->> Caller : 404 ERR-SIGNER-NOT-FOUND
                end
            end
        end
    end

    %% F4 — Soumission batch avec garde signer
    rect rgb(245, 230, 255)
        note over Caller, DB: F4 — Soumission batch avec garde signer actif (INV-275-04, 11)
        Caller ->> Service : submitBatch(batchData, signerAddress)
        Service ->> DB : BEGIN TRANSACTION
        Service ->> Registry : SELECT ... FOR UPDATE\nWHERE address = signerAddress (INV-275-11)
        Registry -->> Service : signer row (verrouillee)
        alt status = ACTIVE
            Service ->> DB : INSERT/UPDATE anchor_batch\n(soumission dans la meme transaction)
            DB -->> Service : OK
            Service ->> DB : COMMIT
            Service -->> Caller : 200 batch soumis
        else status = REVOKED (fail-closed, INV-275-01)
            Service ->> DB : ROLLBACK
            Service -->> Caller : 403 ERR-SIGNER-REVOKED
        else signer introuvable (fail-closed, INV-275-01)
            Service ->> DB : ROLLBACK
            Service -->> Caller : 404 ERR-SIGNER-NOT-FOUND
        end
    end

5bis.4 Diagramme de sequence — Concurrence revoke/submit (INV-275-11, INV-275-12)¶

sequenceDiagram
    autonumber
    participant R as revokeSigner(addr)
    participant S as submitBatch(addr)
    participant DB as PostgreSQL
    participant Reg as signer_registry (row lock)

    note over R, S: Scenario A — revoke acquiert le verrou en premier

    R ->> DB : BEGIN TX-1
    R ->> Reg : SELECT ... FOR UPDATE (addr)\n→ verrou acquis par TX-1
    S ->> DB : BEGIN TX-2
    S ->> Reg : SELECT ... FOR UPDATE (addr)\n→ BLOQUE (attend TX-1)
    R ->> Reg : UPDATE status = ‘REVOKED’
    R ->> DB : COMMIT TX-1 (verrou libere)
    Reg -->> S : row deverrouillee, status = REVOKED
    S -->> S : status = REVOKED → fail-closed
    S ->> DB : ROLLBACK TX-2
    S -->> S : ERR-SIGNER-REVOKED

    note over R, S: Scenario B — submit acquiert le verrou en premier

    S ->> DB : BEGIN TX-3
    S ->> Reg : SELECT ... FOR UPDATE (addr)\n→ verrou acquis par TX-3
    R ->> DB : BEGIN TX-4
    R ->> Reg : SELECT ... FOR UPDATE (addr)\n→ BLOQUE (attend TX-3)
    S ->> DB : soumission batch OK
    S ->> DB : COMMIT TX-3 (verrou libere)
    Reg -->> R : row deverrouillee, status = ACTIVE
    R ->> Reg : UPDATE status = ‘REVOKED’
    R ->> DB : COMMIT TX-4
    R -->> R : revocation appliquee apres soumission

6. Cas d’erreur¶

• ERR-FINALITY-INSUFFICIENT : tentative de finalisation avec confirmation_count < FINALITY_DEPTH -> refus metier, aucun changement d’etat.
• ERR-CONFIRMATION-COUNT-INVALID : valeur compteur hors bornes contractuelles -> rejet de la mise a jour.
• ERR-SIGNER-NOT-FOUND : signer absent du registre lors de soumission/revocation -> refus fail-closed.
• ERR-SIGNER-REVOKED : soumission par signer REVOKED -> refus immediat.
• ERR-SIGNER-ALREADY-REVOKED : tentative de revocation d’un signer deja REVOKED -> refus idempotence metier stricte, aucun nouvel audit trail de revocation.
• ERR-AUDIT-TRAIL-MISSING : impossibilite de persister revokedAt/revokedBy pendant la transition -> operation invalide, transition non appliquee.
• ERR-REVOKE-UNAUTHORIZED : appel a revokeSigner() sans role ADMIN ou SIGNER_ADMIN -> refus sans effet de bord.
• ERR-REVOKEDBY-SPOOFING : presence d’un champ revokedBy fourni par appelant (payload/query/header metier) -> requete invalide/refusee.
• ERR-COMPLIANCE-NOT-MET : execution audit Prolog post-changement avec score < 32/32 -> livraison non conforme.

7. Criteres d’acceptation (testables)¶

8. Scenarios de test (Given / When / Then)¶

• T1 — Persistance confirmations
• Given un batch existant avec confirmation_count = 0
• When le suivi confirmations publie n = 3

• Then confirmation_count persistant devient 3

• T2 — Garde finalite refus

• Given un batch non finalise et FINALITY_DEPTH = D, confirmation_count = D-1
• When finalizeBatch() est invoque

• Then la requete est refusee et le batch ne passe pas a FINALIZED

• T3 — Garde finalite succes

• Given un batch non finalise et confirmation_count = D
• When finalizeBatch() est invoque

• Then la transition vers FINALIZED est autorisee

• T4 — Revocation signer active (autorisee)

• Given un signer ACTIVE et un appelant avec role ADMIN (ou SIGNER_ADMIN)
• When revokeSigner(address) est invoque

• Then le signer devient REVOKED avec revokedAt et revokedBy renseignes depuis l’identite auth

• T5 — Revocation deja revoque

• Given un signer deja REVOKED
• When revokeSigner(address) est invoque par un role autorise

• Then la requete est refusee avec erreur metier explicite ERR-SIGNER-ALREADY-REVOKED et sans nouvel audit trail de revocation

• T6 — Soumission avec signer revoque

• Given un signer REVOKED
• When submitBatch() est invoque

• Then la soumission est refusee immediatement (fail-closed)

• T7 — Soumission avec signer inconnu

• Given une adresse absente de signer_registry
• When submitBatch() est invoque

• Then la soumission est refusee (fail-closed)

• T8 — Verification conformite formelle

• Given les changements PD-275 deployes
• When l’audit Prolog est execute

• Then les checks 28, 29, 30, 31, 32 sont OK et le total est 32/32

• T9 — Reversibilite migration

• Given un environnement de test avec donnees representatives
• When migration up, puis down, puis up

• Then les objets attendus et contraintes sont restaures conformement au contrat

• T10 — Autorisation revokeSigner refusee

• Given un signer ACTIVE et un appelant authentifie sans role ADMIN ni SIGNER_ADMIN
• When revokeSigner(address) est invoque

• Then la requete est refusee avec ERR-REVOKE-UNAUTHORIZED et le signer reste ACTIVE

• T11 — Anti-usurpation revokedBy

• Given un appelant autorise avec identite auth sub = actor-A et un payload contenant revokedBy = actor-B
• When revokeSigner(address) est invoque

• Then la valeur persistee revokedBy vaut actor-A (ou la requete est refusee avec ERR-REVOKEDBY-SPOOFING selon contrat API), jamais actor-B

• T12 — Concurrence revoke/revoke

• Given un signer initialement ACTIVE
• When deux revokeSigner(address) sont lances concurremment

• Then une seule transaction applique ACTIVE -> REVOKED et cree l’audit trail; l’autre retourne ERR-SIGNER-ALREADY-REVOKED

• T13 — Concurrence revoke/submit

• Given un signer initialement ACTIVE
• When revokeSigner(address) et submitBatch() sont lances concurremment
• Then le resultat respecte la serialisation par verrou :
  • si revoke commit en premier, submitBatch() est refuse;
  • si submit commit en premier, la soumission reussit puis revoke applique REVOKED
• And aucun etat impossible n’est observe (pas de double revocation, pas d’audit incoherent)

9. Hypotheses explicites¶

10. Contraintes techniques et points a clarifier¶

10.1 Contraintes techniques (stack reelle cible)¶

• Projet cible : ProbatioVault-backend.
• Stack contractuelle : NestJS + TypeORM + PostgreSQL.
• Langage : TypeScript.
• Interdits de specification : toute mention de stack non conforme (ex: Spring Boot, Swift/SwiftUI) est non conforme.

10.2 Bornes numeriques contractualisees¶

10.3 SLA temporels¶

• Aucune transition temporelle identifiee (pas de TTL/expiration/deadline contractuelle dans PD-275).
• Le champ revokedAt est un marqueur d’audit, pas un SLA de transition.

10.4 Strategie migration DDL¶

• Modification de colonne existante : non applicable (ajout de nouveaux champs/objets, pas de type-change de colonne existante).
• Exigence maintenue : migration up/down reversible et testee (CA-08).

10.5 Atomicite multi-composant (DB + async)¶

• Aucune ecriture async de type queue/append-only/Merkle explicitement incluse dans le perimetre PD-275.
• Aucune contrainte d’atomicite multi-composant applicable a ce stade.

10.6 Contraintes inter-modules¶

• Aucune contrainte inter-module applicable (les regles concernent le module d’ancrage et son registre de signer dans le meme domaine fonctionnel).

10.7 Concurrence et verrouillage transactionnel (contractualise)¶

• revokeSigner() et submitBatch() doivent encapsuler la lecture du signer et la decision metier dans une transaction DB.
• La ligne signer_registry ciblee est verrouillee via SELECT ... FOR UPDATE avant evaluation du statut.
• Les ecritures d’audit de revocation sont dans la meme transaction que la transition d’etat signer.
• Une tentative concurrente ne doit jamais produire deux transitions ACTIVE -> REVOKED ni deux audit trails de revocation pour la meme adresse.
• La politique de timeout/gestion des deadlocks doit etre fail-closed (erreur explicite, pas de succes implicite).

10.8 Questions ouvertes (donnees manquantes)¶

References¶

• Epic : Reference epique non fournie (a completer).
• JIRA : PD-275.
• Repos concernes : ProbatioVault-backend.
• Documents associes :
• docs/normes/pv-anchor/formal/pv_anchor_compliance.pl
• docs/normes/pv-anchor/formal/AUDIT-REPORT.md
• docs/normes/AUDIT-SYNTHESIS.md
• docs/normes/pv-anchor/formal/PV_ANCHOR.tla
• Dependances : PD-177, PD-52, PD-264