Aller au contenu

PD-275 — Expression de Besoin

1. Contexte

L'audit de vérification formelle PV Anchor (Prolog, 32 checks) identifie 5 écarts non conformes sur les règles ANCHOR-16 (Finality Depth) et ANCHOR-17 (Signer Revocation). Les 27 autres checks passent à 100%.

Vérification formelle amont : Les modèles TLA+ (13 invariants) et Alloy (12 assertions) valident déjà le design. L'écart est uniquement sur le mapping implémentation — les features ne sont pas encore codées dans le backend.

Références : - Règles Prolog : docs/normes/pv-anchor/formal/pv_anchor_compliance.pl - Rapport d'audit : docs/normes/pv-anchor/formal/AUDIT-REPORT.md - Synthèse : docs/normes/AUDIT-SYNTHESIS.md (29/32 OK → objectif 32/32) - Modèle TLA+ : docs/normes/pv-anchor/formal/PV_ANCHOR.tla

2. Problème

ANCHOR-16 : Finality Depth (2 checks KO)

Check ID Prolog Description État actuel
28 check_confirmation_count_col Colonne confirmation_count absente sur anchor_batch ConfirmationTracker track en mémoire, pas de persistance
29 check_finalize_confirmations_guard finalizeBatch() sans garde confirmation_count >= FINALITY_DEPTH Garde implicite dans ConfirmationTracker.track() mais non contractualisée dans AnchorBatchService

ANCHOR-17 : Signer Revocation (3 checks KO)

Check ID Prolog Description État actuel
30 check_signer_status_mechanism Mécanisme signer_status absent Non implémenté
31 check_signer_revoke_method Méthode revokeSigner() absente Non implémenté
32 check_submit_active_signer_guard submitBatch() sans garde signer ACTIVE Non implémenté

3. Solution attendue

3.1 ANCHOR-16 — Finality Depth

  1. Colonne confirmation_count (integer, default 0) sur l'entité anchor_batch
  2. Persistance : ConfirmationTracker met à jour anchor_batch.confirmation_count à chaque poll
  3. Garde dans finalizeBatch() : vérifier confirmation_count >= FINALITY_DEPTH avant transition vers FINALIZED. Rejet si insuffisant (fail-closed, cf. learning PD-39)
  4. Migration TypeORM : ajouter la colonne avec valeur par défaut

3.2 ANCHOR-17 — Signer Revocation

  1. Entité signer_registry (nouvelle) avec colonnes :
  2. signerId (UUID, PK)
  3. address (EIP-55 checksum, unique)
  4. status (enum ACTIVE | REVOKED)
  5. revokedAt (timestamp, nullable)
  6. revokedBy (string, nullable — audit trail)
  7. createdAt, updatedAt
  8. Méthode revokeSigner(address) sur AnchorBatchService (ou SignerRegistryService) :
  9. Transition ACTIVE → REVOKED atomique
  10. Enregistrement revokedAt + revokedBy (audit trail)
  11. Validation : impossible de révoquer un signer déjà REVOKED
  12. Garde dans submitBatch() : vérifier que le signer est ACTIVE dans signer_registry avant soumission. Rejet immédiat si REVOKED (fail-closed)

3.3 Vérification formelle

Après implémentation, régénérer les faits Prolog et relancer : 

swipl -l _generated-facts.pl -l pv_anchor_compliance.pl -g "run_audit." -t "halt."
Objectif : 32/32 OK (0 KO, 0 WARN).

4. Critères d'acceptation

  • CA-01 : La colonne confirmation_count existe sur anchor_batch (migration TypeORM)
  • CA-02 : finalizeBatch() rejette si confirmation_count < FINALITY_DEPTH (fail-closed)
  • CA-03 : L'entité signer_registry existe avec colonnes address, status, revokedAt, revokedBy
  • CA-04 : La méthode revokeSigner(address) effectue la transition ACTIVE → REVOKED avec audit trail
  • CA-05 : submitBatch() rejette si le signer est REVOKED (fail-closed)
  • CA-06 : L'audit Prolog passe 32/32 (5 checks corrigés : 28, 29, 30, 31, 32)
  • CA-07 : Les tests unitaires couvrent les 5 nouveaux comportements
  • CA-08 : Migration TypeORM réversible (up/down)

5. Hors périmètre

  • Rotation automatique des signers (story future)
  • Multi-signature (hors scope ANCHOR-17)
  • Interface d'administration des signers (API CRUD complète)
  • Modification du modèle TLA+ ou Alloy (déjà conformes)

6. Dépendances

  • PD-177 (wallet Ethereum) : signerAddress déjà présent sur anchor_batch — PD-275 s'appuie dessus
  • PD-52 (Ethereum L2 setup) : infrastructure blockchain opérationnelle
  • PD-264 (nonce TSA RFC 3161) : module blockchain adjacent, pas de couplage direct

7. Risques

Risque Mitigation
Migration sur table anchor_batch avec données existantes Valeur par défaut 0, migration non-bloquante
signer_registry vide au démarrage (cold start) Seed initial avec les signers actifs connus
Performance garde submitBatch() (lookup signer_registry) Index unique sur address, query O(1)

8. Learnings injectés

  • PD-39 : Fail-closed obligatoire pour features sécuritaires — pas de mode permissif par défaut
  • PD-5 : Contraintes d'irréversibilité pour les états terminaux (Vault Lock pattern)