RFC PV-AUDIT-001 : Audit immuable et anti-rollback¶

Statut : Proposition interne Version : 1.1.0 Date : 2026-03-02 Auteur : ProbatioVault Engineering Verification formelle : TLA+ (TLC), Alloy (SAT), Z Notation, Prolog Revision : 1.1.0 — chaine de certificats dans export, schema canonique versionne, taxonomie normative probatif/informatif, chainage inter-entrees, procedure gaps destruction_seq, politique de retention

1. Introduction¶

1.1 Objectif¶

Ce document specifie le protocole PV Audit, le systeme d'audit immuable et anti-rollback de ProbatioVault. Le protocole unifie les contrats d'audit des normes ENV (PV-ENV-001) et PRE (PV-PRE-001) en un pipeline d'audit unique garantissant l'immutabilite, la tracabilite et la valeur probante des evenements.

1.2 Portee¶

Ce protocole couvre :

• Le format d'evenement canonique (JSON per RFC 8785)
• La liaison cryptographique : hash SHA3-256 + signature ECDSA P-384 via HSM
• L'append-only avec triggers PostgreSQL (BEFORE UPDATE OR DELETE)
• La revocation de TRUNCATE
• La verification offline via cle publique
• L'audit de destruction avec sequence PostgreSQL monotone
• Le fail-closed : l'indisponibilite de l'audit bloque la destruction
• Les evenements probatifs legaux : HSM + TSA obligatoires
• Les evenements informatifs legaux : TSA best-effort, HSM obligatoire

1.3 References normatives¶

1.4 Terminologie¶

2. Vue d'ensemble du protocole¶

2.1 Structure de l'Audit Log¶

+----------------------------------------------------------------------+
|                        Audit Log (append-only)                        |
|  Table: audit_logs                                                    |
|  Schema: vault_audit                                                  |
+----------------------------------------------------------------------+
|                                                                      |
|  +------------------------------------------------------------+     |
|  | AuditEntry                                                  |     |
|  |  id            : UUID                                       |     |
|  |  previous_entry_hash : BYTEA (SHA3-256, chainage)            |     |
|  |  entry_canonical : JSONB  (RFC 8785)                        |     |
|  |  entry_hash     : BYTEA  (SHA3-256)                         |     |
|  |  hsm_signature  : BYTEA  (ECDSA P-384)                      |     |
|  |  hsm_key_id     : VARCHAR (pv-master-signing-*)             |     |
|  |  tsa_token      : BYTEA  (RFC 3161, optional for inform.)   |     |
|  |  created_at     : TIMESTAMPTZ                               |     |
|  +------------------------------------------------------------+     |
|                                                                      |
|  Triggers:                                                           |
|    BEFORE UPDATE OR DELETE -> RAISE EXCEPTION (immutable)            |
|    REVOKE TRUNCATE ON audit_logs FROM public                         |
|                                                                      |
+----------------------------------------------------------------------+
|                                                                      |
|  +------------------------------------------------------------+     |
|  | Destruction Audit                                           |     |
|  |  destruction_seq : BIGINT (monotone PostgreSQL sequence)    |     |
|  |  document_id     : UUID                                     |     |
|  |  destruction_reason : VARCHAR                               |     |
|  |  audit_entry_id  : UUID -> AuditEntry                       |     |
|  +------------------------------------------------------------+     |
|                                                                      |
|  +------------------------------------------------------------+     |
|  | Verification Material                                       |     |
|  |  HSM key label   : pv-master-signing-*                     |     |
|  |  Hash algorithm  : SHA3-256                                 |     |
|  |  Sig algorithm   : ECDSA_SHA384 (P-384)                    |     |
|  |  Public key      : SPKI/DER                                 |     |
|  +------------------------------------------------------------+     |
|                                                                      |
+----------------------------------------------------------------------+

2.2 Flux d'audit¶

1. LogEntry : Serialisation canonique (RFC 8785), hash SHA3-256, signature ECDSA P-384 via HSM, insertion append-only
2. LogProbativeEvent : Comme LogEntry + token TSA obligatoire (RFC 3161)
3. LogInformativeEvent : Comme LogEntry + token TSA best-effort
4. LogDestruction : Comme LogProbativeEvent + increment sequence monotone + fail-closed check
5. VerifyEntry : Recalcul du hash, verification de la signature via cle publique
6. ExportProof : Export d'une entree avec evidences cryptographiques pour verification offline
7. VerifyExportedProof : Verification offline d'un proof exporte (sans acces ProbatioVault)
8. EnsureAvailable : Verification de la disponibilite de l'audit (fail-closed gate)

2.3 Proprietes de securite¶

Immutabilite : Les entrees d'audit ne peuvent etre ni modifiees ni supprimees (triggers PostgreSQL). La commande TRUNCATE est revoquee.

Anti-rollback : La sequence de destruction est monotone croissante. Tout gap dans la sequence est detectable.

Fail-closed : Si l'audit est indisponible, les operations de destruction sont bloquees. Aucune destruction silencieuse n'est possible.

3. Specifications detaillees¶

3.1 Format d'evenement canonique¶

EXIGENCE AUDIT-01 : Chaque entree d'audit DOIT etre serialisee au format JSON canonique (RFC 8785 / JCS) avant le calcul du hash. Ce format garantit un hash reproductible independamment de l'ordre des cles ou du formatage. Prouve formellement (TLA+ INV-02 EntryHashBinding, Alloy HashBindingValid).

3.2 Hash cryptographique¶

EXIGENCE AUDIT-02 : Le hash de chaque entree DOIT etre calcule avec SHA3-256 (FIPS 202) sur la forme canonique. Prouve formellement (TLA+ INV-02 EntryHashBinding, Z INV-02).

3.3 Signature HSM¶

EXIGENCE AUDIT-03 : Chaque entree d'audit DOIT etre signee par le HSM avec ECDSA P-384 (FIPS 186-5). La cle HSM utilisee DOIT porter un label pv-master-signing-*. Prouve formellement (TLA+ INV-03 EntrySignatureBinding, Alloy SignatureBindingValid, Z INV-03).

3.4 Append-only¶

EXIGENCE AUDIT-04 : La table d'audit DOIT etre protegee par un trigger PostgreSQL BEFORE UPDATE OR DELETE qui leve une exception. Aucune modification ou suppression n'est autorisee apres insertion. Prouve formellement (TLA+ INV-04 AppendOnly, Alloy AppendOnlyEnforced, Z INV-04).

3.5 Revocation TRUNCATE¶

EXIGENCE AUDIT-05 : Le privilege TRUNCATE DOIT etre revoque sur la table d'audit pour tous les roles applicatifs. Prouve formellement (TLA+ INV-10 NoUpdateOrDelete, Prolog check_audit_truncate_revoked).

3.6 Sequence de destruction monotone¶

EXIGENCE AUDIT-06 : Les operations de destruction DOIVENT utiliser une sequence PostgreSQL monotone croissante (destruction_seq). Tout gap dans la sequence est un indicateur de corruption ou de manipulation. Prouve formellement (TLA+ INV-06 DestructionSeqMonotone, Alloy SequenceMonotone, Z INV-06).

3.7 Fail-closed¶

EXIGENCE AUDIT-07 : Si le service d'audit est indisponible, les operations de destruction DOIVENT echouer (fail-closed). Aucune destruction ne peut avoir lieu sans trace d'audit. Prouve formellement (TLA+ INV-07 FailClosed, Z INV-07).

3.8 Evenements probatifs legaux¶

EXIGENCE AUDIT-08 : Les evenements a valeur probante legale DOIVENT inclure un token TSA (RFC 3161) en plus de la signature HSM. Le token TSA est obligatoire. Prouve formellement (TLA+ INV-08 ProbativeEventComplete, Alloy ProbativeEventsHaveTSA, Z INV-08).

3.9 Evenements informatifs legaux¶

EXIGENCE AUDIT-09 : Les evenements informatifs legaux DOIVENT inclure la signature HSM. Le token TSA est en mode best-effort (present si le service TSA est disponible). Prouve formellement (TLA+ INV-03, Z INV-09).

3.10 Verification offline¶

EXIGENCE AUDIT-10 : Chaque entree d'audit DOIT etre verifiable offline a l'aide de la cle publique HSM, sans acces a ProbatioVault. La verification recalcule le hash SHA3-256 et verifie la signature ECDSA P-384. Prouve formellement (TLA+ VerifyEntry, Alloy OfflineVerificationPossible, Z INV-10).

3.11 Format de cle HSM¶

EXIGENCE AUDIT-11 : Le label de la cle HSM utilisee pour signer les entrees d'audit DOIT respecter le format pv-master-signing-*. Prouve formellement (TLA+ INV-09 KeyLabelFormat, Alloy KeyLabelConsistent, Z INV-11).

3.12 Export de preuve¶

EXIGENCE AUDIT-12 : L'export d'une preuve d'audit (AuditProof) DOIT inclure : l'entree canonique, le hash, la signature, le label de cle, l'algorithme de hash, l'algorithme de signature, la cle publique, la chaine de certificats HSM (PEM array), et les preuves de non-revocation au moment de la signature (reponses OCSP stapled ou CRL pertinentes, DER Base64). Aucun secret cryptographique (cle privee) ne DOIT etre inclus dans l'export. L'inclusion de la chaine de certificats permet de verifier non seulement l'integrite technique (signature) mais aussi l'authenticite de la cle publique (chaine de confiance). Prouve formellement (Alloy NoSecretsInExport, Z INV-12).

3.13 Sequence monotone globale¶

EXIGENCE AUDIT-13 : Le compteur de sequence general (sequence_counter) est monotone croissant. Chaque nouvelle entree d'audit recoit un numero de sequence strictement superieur au precedent. Prouve formellement (TLA+ INV-05 SequenceMonotone, Z INV-13).

3.14 Timestamp¶

EXIGENCE AUDIT-14 : Le timestamp de creation (created_at) DOIT etre au format TIMESTAMPTZ (avec fuseau horaire). Le clock de l'audit ne recule jamais. Prouve formellement (Z INV-14).

3.15 Audit append-only structurel¶

EXIGENCE AUDIT-15 : L'audit log ne perd jamais d'entrees. Garanti structurellement par le modele (append-only, pas de suppression). Prouve formellement (TLA+ INV-11 AuditAppendOnly, Z INV-15).

3.16 Schema canonique versionne des evenements¶

EXIGENCE AUDIT-16 : Chaque entree d'audit DOIT respecter un schema JSON canonique versionne. Le schema definit les champs obligatoires :

L'ajout de nouveaux champs est autorise (extensibilite forward-compatible). La suppression ou modification de champs existants requiert un bump de schemaVersion MAJEUR. Le schema initial est "1.0.0".

3.17 Taxonomie normative des types d'evenements¶

EXIGENCE AUDIT-17 : Chaque type d'evenement DOIT etre classe comme PROBATIVE ou INFORMATIVE. La classification est normative et ne peut pas etre modifiee par l'implementation. Un evenement classe PROBATIVE ne peut pas etre "down-grade" en INFORMATIVE.

3.18 Chainage cryptographique inter-entrees¶

EXIGENCE AUDIT-18 : Chaque entree d'audit DOIT inclure le hash SHA3-256 de l'entree precedente dans son contenu canonique (champ previousEntryHash). La premiere entree utilise un hash sentinelle de 32 bytes de zeros (0x0000...0000, 64 caracteres hex "0"*64). Ce chainage permet de detecter toute suppression ou insertion d'entree, meme par un attaquant disposant d'un acces superuser PostgreSQL ayant contourne les triggers.

La verification du chainage recalcule la chaine H(entry_n-1) pour chaque entree et compare avec le previousEntryHash stocke. Toute rupture de chaine est un indicateur de corruption.

3.19 Procedure de qualification des gaps destruction_seq¶

EXIGENCE AUDIT-19 : Tout gap detecte dans destruction_seq DOIT declencher une alerte de securite. La procedure de qualification est :

1. Detection : verification periodique (CRON, toutes les 6 heures minimum) de la continuite de destruction_seq
2. Correlation crash : tentative de correlation avec un crash PostgreSQL (WAL logs, pg_stat_activity, journaux systeme)
3. Qualification BENIGN : si correle a un crash PostgreSQL documente, le gap est qualifie BENIGN. Un audit entry de qualification (type GAP_QUALIFICATION, PROBATIVE) est emis avec la justification.
4. Qualification SUSPICIOUS : si non correle, le gap est qualifie SUSPICIOUS. Les operations de destruction sont suspendues (fail-closed) jusqu'a investigation manuelle. Un audit entry de qualification est emis.
5. Remediation : investigation manuelle obligatoire pour les gaps SUSPICIOUS. Reprise des destructions uniquement apres validation par le DPO.

3.20 Politique de retention¶

EXIGENCE AUDIT-20 : Les entrees d'audit DOIVENT etre conservees pour la duree la plus longue parmi :

• 10 ans (exigence eIDAS pour les preuves electroniques qualifiees)
• La duree de retention du document audite
• Toute obligation legale applicable (RGPD art. 5.1.e — conservation limitee a la finalite)

L'archivage a froid est autorise apres 2 ans si les conditions suivantes sont remplies : (a) l'integrite du chainage (AUDIT-18) est verifiee avant archivage, (b) la signature HSM reste verifiable avec la cle publique historique, © l'archivage est trace dans l'audit log (event PROBATIVE).

4. Modele formel¶

4.1 Etats et transitions¶

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

LogEntry -----> LogProbativeEvent -----> LogInformativeEvent
                       |
                LogDestruction
                       |
VerifyEntry <----------+
    |
ExportProof -----> VerifyExportedProof
    |
EnsureAvailable
    |
Tick (clock advance)

4.2 Invariants de surete¶

Note sur TLC : Le model checking utilise une configuration bornee (MAX_ENTRIES=3, MAX_DESTRUCTION=2, 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 => []EntryHashBinding
• THM-03 : Spec => []EntrySignatureBinding
• THM-04 : Spec => []AppendOnly
• THM-05 : Spec => []SequenceMonotone
• THM-06 : Spec => []DestructionSeqMonotone
• THM-07 : Spec => []FailClosed
• THM-08 : Spec => []AuditAppendOnly

4.4 Assertions structurelles (Alloy)¶

5. Considerations de securite¶

5.1 Modele de menace¶

5.2 Limitations connues¶

• La verification offline necessite la cle publique HSM correspondant a la cle de signature. Si la cle a ete tournee, la cle publique historique doit etre conservee.
• Le token TSA pour les evenements informatifs est en mode best-effort. En cas d'indisponibilite du service TSA, l'event est tout de meme signe par le HSM.
• La sequence de destruction detecte les gaps mais ne peut pas les prevenir a 100% en cas de crash de la base pendant un NEXTVAL.

6. Ancrage au code reel¶

6.1 Etat d'implementation¶

7. Annexes¶

7.1 Specifications formelles associees¶

7.2 Matrice de tracabilite¶

7.3 Vecteurs de test¶

7.4 Historique des revisions¶