RFC PV-ANCHOR-001 : ProbatioVault Blockchain Anchoring Protocol¶

Statut : Proposition interne Version : 1.2.0 Date : 2026-03-02 Auteur : ProbatioVault Engineering Verification formelle : TLA+ (TLC), Alloy (SAT), Z Notation, Prolog Changelog : v1.2 — ANCHOR-07 algorithme Merkle exact (RFC 9162 §2.1, prefixes 0x00/0x01), ANCHOR-09 modele de confiance blockchain, ANCHOR-18 gouvernance politique de finalite, ANCHOR-19 limites de batch, transition PENDING_FINALITY -> FAILED via timeout, note ecarts spec/code

1. Introduction¶

1.1 Objectif¶

Ce document specifie le protocole PV Anchor, le systeme d'ancrage blockchain de ProbatioVault. L'ancrage garantit l'immutabilite et la tracabilite des evenements d'audit en les ancrant periodiquement dans une blockchain publique via des arbres de Merkle et des preuves d'inclusion compatibles avec la structure definie par RFC 9162.

1.2 Portee¶

Ce protocole couvre :

• Le cycle de vie des batches d'ancrage (PENDING -> BUILDING -> SUBMITTED -> PENDING_FINALITY -> FINALIZED / FAILED)
• L'immutabilite des batches finalises (trigger PostgreSQL)
• L'unicite des evenements dans les batches finalises
• La liberation atomique des evenements en cas d'echec
• La continuite temporelle des fenetres d'ancrage
• La tracabilite complete de chaque transition d'etat
• La construction d'arbres de Merkle (SHA-256, hashes ordonnes)
• Les preuves d'inclusion compatibles avec la structure RFC 9162 (Merkle tree hashing & path computation)
• La verification des artefacts de preuve sans acces privilegie
• La conformite EIP-155 pour les identifiants de chaine
• Le verrouillage pessimiste a la finalisation
• La gestion des reorganisations de chaine (reorg handling)
• La politique de finalite configurable par chaine cible (FINALITY_DEPTH, FINALITY_TIMEOUT)
• La revocation des adresses de signature (SignerStatus lifecycle)

1.3 References normatives¶

1.4 Terminologie¶

2. Vue d'ensemble du protocole¶

2.1 Machine a etats du batch¶

                    +------------------+
                    |     PENDING      |
                    +--------+---------+
                             |
                        CreateBatch
                             |
                    +--------v---------+
                    |    BUILDING      |
                    +--------+---------+
                             |
                        SubmitBatch
                             |
                    +--------v---------+
                    |    SUBMITTED     |
                    +--------+---------+
                             |
                       ConfirmBatch
                             |
                    +--------v---------+
                    | PENDING_FINALITY |
                    +--------+---------+
                            / \
               FinalizeBatch   HandleReorg
                      /             \
         +-----------v---+   +------v--------+
         |   FINALIZED   |   |    FAILED     |
         | (terminal,    |   | (terminal,    |
         |  immutable)   |   |  events       |
         +---------------+   |  released)    |
                             +------+--------+
                                    |
                               RetryBatch
                                    |
                             (new PENDING)

2.2 Flux d'ancrage¶

1. CreateBatch : Collecte des evenements eligibles, construction arbre de Merkle, fenetre temporelle
2. SubmitBatch : Soumission de la transaction blockchain (merkle root + chain ID + signer address ACTIVE)
3. ConfirmBatch : Reception du tx hash et du block number
4. FinalizeBatch : Verrouillage pessimiste, validation finality (confirmations >= FINALITY_DEPTH), immutabilite
5. FailBatch : Echec (timeout, erreur reseau, reorg, FINALITY_TIMEOUT depasse) avec liberation atomique des evenements
6. ExportProofArtifact : Generation d'un artefact de preuve d'inclusion verifiable offline
7. VerifyInclusionProof : Verification compatible RFC 9162 d'un evenement dans le Merkle tree
8. HandleReorg : Detection de bloc orphelin, transition PENDING_FINALITY -> FAILED
9. RetryBatch : Creation d'un nouveau batch PENDING a partir des evenements liberes
10. RevokeSigner : Revocation d'une adresse de signature (ACTIVE -> REVOKED, irreversible)
11. Tick : Avance de l'horloge logique

2.3 Proprietes de surete¶

EXIGENCE ANCHOR-01 : Les batches suivent strictement la machine a etats : PENDING -> BUILDING -> SUBMITTED -> PENDING_FINALITY -> FINALIZED (ou FAILED). FINALIZED et FAILED sont terminaux.

EXIGENCE ANCHOR-02 : Un batch FINALIZED est immutable. Aucune modification n'est autorisee apres finalisation (enforced par trigger PostgreSQL BEFORE UPDATE OR DELETE).

3. Specifications detaillees¶

3.1 Transitions d'etat¶

EXIGENCE ANCHOR-01 : Les seules transitions valides sont :

Prouve formellement (TLA+ INV-02 ValidTransitions, Alloy ValidTransitionsOnly).

3.2 Immutabilite des batches finalises¶

EXIGENCE ANCHOR-02 : Un batch a l'etat FINALIZED ne peut plus etre modifie. Enforced par trigger PostgreSQL BEFORE UPDATE OR DELETE sur la table anchor_batches. Prouve formellement (TLA+ INV-03 FinalizedImmutable, Alloy FinalizedBatchImmutable).

3.3 Unicite des evenements¶

EXIGENCE ANCHOR-03 : Chaque evenement appartient a au plus un batch FINALIZED. Un evenement ne peut pas etre ancre deux fois. Prouve formellement (TLA+ INV-04 EventUniqueness, Alloy EventUniqueInFinalizedBatch).

3.4 Liberation atomique des evenements¶

EXIGENCE ANCHOR-04 : Lorsqu'un batch passe a FAILED, tous ses evenements sont liberes atomiquement et redeviennent eligibles pour un nouveau batch. Prouve formellement (TLA+ INV-05 NoEventsLost, Alloy FailedBatchReleasesEvents).

3.5 Continuite temporelle¶

EXIGENCE ANCHOR-05 : Chaque batch a une fenetre temporelle [windowStart, windowEnd) avec windowStart < windowEnd. Les fenetres ne se chevauchent pas entre batches finalises. Prouve formellement (TLA+ INV-06 WindowOrdering, Alloy WindowContinuity).

3.6 Tracabilite des transitions¶

EXIGENCE ANCHOR-06 : Chaque transition d'etat d'un batch DOIT etre enregistree dans l'audit log. L'audit log est append-only. Prouve formellement (TLA+ INV-07 AuditCompleteness, INV-11 AuditAppendOnly, Alloy EveryTransitionAudited).

3.7 Arbre de Merkle¶

EXIGENCE ANCHOR-07 : L'arbre de Merkle est construit selon l'algorithme suivant, compatible avec la structure RFC 9162 §2.1 :

• Hash de feuille : MTH_leaf(entry) = SHA-256(0x00 || entry_hash) ou entry_hash est le SHA3-256 de l'entree d'audit (32 bytes)
• Hash de noeud interne : MTH_node(left, right) = SHA-256(0x01 || left || right)
• Niveau impair : le dernier element sans pair est promu au niveau superieur sans modification (identique a RFC 9162 §2.1)
• Ordre des feuilles : les feuilles sont ordonnees par leaf_index (entier 0-indexed, attribue dans l'ordre d'insertion dans le batch)
• Endianness : les prefixes (0x00, 0x01) sont des octets uniques. Les hashes sont en bytes bruts (pas d'encodage hex)
• Merkle root : MTH_root = MTH(leaves[0..n-1]) pour n feuilles. Si n=1, MTH_root = MTH_leaf(leaves[0])

Chaque batch BUILDING, SUBMITTED, PENDING_FINALITY ou FINALIZED DOIT avoir un merkle root non-vide. Prouve formellement (TLA+ INV-08 MerkleRootPresent, Alloy MerkleRootPresent).

3.8 Preuves d'inclusion compatibles RFC 9162¶

EXIGENCE ANCHOR-08 : Les preuves d'inclusion sont compatibles avec la structure definie par RFC 9162 (Certificate Transparency v2) pour le calcul des Merkle tree hashes et des chemins d'inclusion. Chaque evenement dans un batch finalise peut generer une preuve d'inclusion verifiable. Prouve formellement (Alloy InclusionProofValid).

Note : Ce protocole reutilise la structure de preuves d'inclusion de RFC 9162 (Merkle tree hashing & path computation) mais n'implemente pas un Certificate Transparency log public. L'ancrage est effectue dans des batches prives periodiques.

3.9 Artefact de preuve verifiable offline¶

EXIGENCE ANCHOR-09 : L'artefact de preuve (ProofArtifact) est verifiable sans acces privilegie a ProbatioVault. Il contient : - leaf_hash : SHA3-256 de l'entree d'audit - leaf_index : position dans le batch (0-indexed) - merkle_path : sibling hashes du chemin racine - merkle_root : racine de l'arbre de Merkle - tx_hash : hash de la transaction blockchain - block_number : numero du bloc contenant la transaction - chain_id : identifiant EIP-155 de la chaine

Hypothese de confiance : la verification du maillon blockchain (tx_hash dans un bloc confirme) requiert l'acces a une source blockchain publique (noeud RPC, explorateur de blocs, archive de block headers). Le verificateur DOIT specifier la source utilisee. L'artefact ne contient pas les block headers ni les transaction receipts — ces donnees sont obtenues de la source blockchain au moment de la verification.

Prouve formellement (Alloy ProofArtifactSelfContained).

3.10 Identifiant de chaine EIP-155¶

EXIGENCE ANCHOR-10 : Le chain ID suit la convention EIP-155. Chaque batch soumis a un chain ID explicite. Prouve formellement (TLA+ INV-09 TxIdPresent, Alloy ChainIdEIP155).

3.11 Verrouillage pessimiste¶

EXIGENCE ANCHOR-11 : La finalisation d'un batch utilise un verrouillage pessimiste (SELECT ... FOR UPDATE) pour empecher les modifications concurrentes. Prouve formellement (TLA+ FinalizeBatch precondition).

3.12 Adresse de signature append-only avec revocation¶

EXIGENCE ANCHOR-12 : L'ensemble des adresses de signature (signer addresses) est append-only. Une adresse ajoutee ne peut jamais etre supprimee du registre. Chaque adresse possede un statut (ACTIVE ou REVOKED) gere par ANCHOR-17. Prouve formellement (TLA+ INV-10 SignerAddressAppendOnly, Alloy SignerAddressAppendOnly).

3.13 Champ blockchain dans les preuves d'inclusion¶

EXIGENCE ANCHOR-13 : Chaque preuve d'inclusion contient le champ blockchain (chain ID + block number + tx hash) pour identifier sans ambiguite la chaine d'ancrage. Prouve formellement (Alloy InclusionProofHasBlockchain).

3.14 Gestion des reorganisations (reorg)¶

EXIGENCE ANCHOR-14 : Si un bloc contenant la transaction d'un batch est orphelin (reorganisation de chaine), le batch transite de PENDING_FINALITY a FAILED. Les evenements sont liberes atomiquement. Prouve formellement (TLA+ HandleReorg action, Alloy ReorgHandled).

3.15 Transaction ID obligatoire¶

EXIGENCE ANCHOR-15 : Tout batch a l'etat SUBMITTED ou au-dela DOIT avoir un tx_id (hash de transaction) non-vide et un block_number. Prouve formellement (TLA+ INV-09 TxIdPresent).

3.16 Politique de finalite¶

EXIGENCE ANCHOR-16 : Chaque chaine cible DOIT definir une politique de finalite comprenant :

• FINALITY_DEPTH : nombre minimum de confirmations blockchain (blocs subsequents) requis avant de considerer un bloc comme final. La valeur DOIT etre configurable par chaine.
• FINALITY_TIMEOUT : delai maximum (en secondes) d'attente de la finality apres ConfirmBatch. Le depassement de ce delai declenche FailBatch.

FinalizeBatch exige que le nombre de confirmations du bloc contenant la transaction soit superieur ou egal a FINALITY_DEPTH. Prouve formellement (TLA+ INV-12 FinalityDepthEnforced, Alloy FinalityDepthCheck).

Note : Ces valeurs par defaut sont indicatives. L'implementation DOIT permettre de les configurer sans modification de code.

3.17 Revocation des adresses de signature¶

EXIGENCE ANCHOR-17 : Chaque adresse de signature (signer address) possede un statut de cycle de vie :

• ACTIVE : l'adresse est autorisee a signer de nouveaux batches.
• REVOKED : l'adresse est revoquee et ne peut plus signer de nouveaux batches.

Regles :

1. Toute nouvelle adresse est ajoutee avec le statut ACTIVE.
2. La transition ACTIVE -> REVOKED est irreversible (une fois revoquee, jamais reactivee).
3. SubmitBatch DOIT verifier que l'adresse de signature est ACTIVE avant soumission.
4. Les batches deja FINALIZED avec un signer ulterieurement revoque restent valides (on ne reecrit pas l'historique).
5. La revocation DOIT etre enregistree dans l'audit log.

Prouve formellement (TLA+ INV-13 SignerRevocationValid, Alloy SignerRevocationEnforced).

3.18 Gouvernance de la politique de finalite¶

EXIGENCE ANCHOR-18 : Toute modification de FINALITY_DEPTH ou FINALITY_TIMEOUT pour une chaine supportee DOIT : - Etre documentee avec justification - Etre enregistree dans l'audit log (event FINALITY_POLICY_CHANGE, PROBATIVE) - Respecter les bornes minimales de securite : - FINALITY_DEPTH >= 1 (pour toute chaine) - FINALITY_TIMEOUT >= 60s - Ne s'appliquer qu'aux batches futurs (pas d'effet retroactif)

3.19 Limites de batch¶

EXIGENCE ANCHOR-19 : Chaque batch DOIT contenir entre 1 et MAX_BATCH_SIZE evenements (defaut MAX_BATCH_SIZE = 10000). La frequence de batching est configurable (defaut : toutes les 300 secondes ou lorsque MAX_BATCH_SIZE est atteint, selon la premiere condition). Un batch vide (0 evenements) NE DOIT PAS etre cree.

4. Modele formel¶

4.1 Etats et transitions¶

Le protocole est modelise comme un systeme a etats avec 11 actions :

CreateBatch -----> SubmitBatch -----> ConfirmBatch
                                          |
                        FinalizeBatch <---+----> HandleReorg
                             |                        |
                         (FINALIZED)               (FAILED)
                                                      |
                                                 RetryBatch
                                                      |
                                                  (PENDING)

        FailBatch : BUILDING/SUBMITTED -> FAILED
        ExportProofArtifact : FINALIZED -> artifact
        VerifyInclusionProof : FINALIZED -> OK/KO
        RevokeSigner : signer ACTIVE -> REVOKED
        Tick : clock advances

4.2 Invariants de surete¶

Note sur TLC : Le model checking utilise une configuration bornee (MAX_BATCHES=2, MAX_EVENTS=3, MAX_ITERATIONS=12). Des garanties complementaires proviennent des assertions structurelles Alloy (scope 5) et des schemas Z.

4.3 Theoremes prouves¶

• THM-01 : Spec => []TypeInvariant
• THM-02 : Spec => []ValidTransitions
• THM-03 : Spec => []FinalizedImmutable
• THM-04 : Spec => []EventUniqueness
• THM-05 : Spec => []NoEventsLost
• THM-06 : Spec => []WindowOrdering
• THM-07 : Spec => []AuditCompleteness
• THM-08 : Spec => []AuditAppendOnly
• THM-09 : Spec => []FinalityDepthEnforced
• THM-10 : Spec => []SignerRevocationValid

4.4 Assertions structurelles (Alloy)¶

5. Considerations de securite¶

5.1 Reorganisations de chaine (reorg)¶

5.2 Finality et confirmation¶

5.3 Multi-chain et EIP-155¶

5.4 Integrite des donnees¶

5.5 Limitations connues¶

• La verification d'inclusion necessite la connaissance du merkle root et du merkle path. Si l'arbre est perdu, la preuve est non-reconstructible a partir du seul artefact.
• Le protocole ne garantit pas la disponibilite de la blockchain. Un noeud blockchain indisponible peut bloquer SubmitBatch et ConfirmBatch indefiniment (mitigation : timeout + FailBatch).
• Les valeurs par defaut de FINALITY_DEPTH et FINALITY_TIMEOUT sont indicatives et doivent etre ajustees en fonction de la blockchain cible et de l'appetence au risque.

6. Ancrage au code reel¶

6.1 Etat d'implementation¶

Note implementation : Les composants marques "Non implemente" representent des ecarts spec/code bloquants. Le protocole n'est pas considere comme verrouille operationnellement tant que ces composants ne sont pas implementes et que les checks Prolog ne passent pas a PASS.

7. Annexes¶

7.1 Specifications formelles associees¶

7.2 Matrice de tracabilite¶

7.3 Vecteurs de test¶

7.4 Historique des revisions¶