SC-14-Formal-Vérification - Vérification Formelle

# Parameters
BATCH_MODE = "true"

<< Précédent : Fuzz & Invariants | Retour au sommaire | Suivant : Zero-Knowledge Proofs >>

Objectifs d’apprentissage

  1. Comprendre les principes de la vérification formelle
  2. Utiliser Certora Prover et le langage CVL
  3. Ecrire des spécifications et des règles
  4. Vérifier des invariants mathématiques

Prérequis

  • SC-12 et SC-13 complétés
  • Notions de logique formelle (optionnel)
  • Foundry installé, accès à Certora ou Halmos recommandé

Durée estimée : 50 minutes

1. Introduction à la Vérification Formelle

La vérification formelle prouve mathématiquement la correction d’un programme.

# Concepts de verification formelle
print("""
VERIFICATION FORMELLE vs TESTS

| Aspect           | Tests          | Verification Formelle |
|------------------|----------------|----------------------|
| Couverture       | Partielle      | Complete (exhaustive) |
| Method           | Exemples       | Preuves mathematiques |
| Complexite       | Simple         | Elevee               |
| Cout             | Faible         | Eleve                |
| Faux positifs    | Non            | Possible             |

OUTILS DISPONIBLES:
- Certora Prover (commercial, puissant)
- SMTChecker (Solidity builtin)
- KEVM (K framework)
- Act (formal verification for Move)
""")

VERIFICATION FORMELLE vs TESTS

| Aspect           | Tests          | Verification Formelle |
|------------------|----------------|----------------------|
| Couverture       | Partielle      | Complete (exhaustive) |
| Method           | Exemples       | Preuves mathematiques |
| Complexite       | Simple         | Elevee               |
| Cout             | Faible         | Eleve                |
| Faux positifs    | Non            | Possible             |

OUTILS DISPONIBLES:
- Certora Prover (commercial, puissant)
- SMTChecker (Solidity builtin)
- KEVM (K framework)
- Act (formal verification for Move)

Interpretation : Vérification formelle vs Tests

Résultat obtenu : Comparaison des approches de validation.

Critère Tests (unitaires/fuzz) Vérification formelle
Couverture Partielle (échantillonnage) Complète (exhaustive)
Méthodologie Exemples concrets Preuves mathématiques
Complexité Simple à mettre en place Requires expertise
Coût Faible Élevé (temps, ressources)
Faux positifs Non Possibles (specs incorrectes)
Faux négatifs Possibles (cas non testés) Non (si spec correcte)

Points clés : - La vérification formelle prouve qu’une propriété est vraie pour TOUTES les entrées possibles - Les tests ne peuvent que vérifier des cas spécifiques - Certora Prover est un outil commercial puissant utilisant le langage CVL - SMTChecker est une alternative gratuite intégrée au compilateur Solidity - Les deux approches sont complementaires : tests pour développement rapide, vérification formelle pour contrats critiques

2. Certora Prover

Certora utilise le CVL (Certora Vérification Language).

# Contrat Solidity a verifier
SOL_CONTRACT = '''
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.28;

contract Vault {
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;

    function deposit() external payable {
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }

    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "Insufficient balance");
        balances[msg.sender] -= amount;
        totalDeposits -= amount;
        payable(msg.sender).transfer(amount);
    }

    function getBalance(address user) external view returns (uint256) {
        return balances[user];
    }
}
'''

print("Contrat Vault a verifier:")
print(SOL_CONTRACT)
Contrat Vault a verifier:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.28;

contract Vault {
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;

    function deposit() external payable {
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }

    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "Insufficient balance");
        balances[msg.sender] -= amount;
        totalDeposits -= amount;
        payable(msg.sender).transfer(amount);
    }

    function getBalance(address user) external view returns (uint256) {
        return balances[user];
    }
}

Spécification formelle CVL (Certora Vérification Language) définissant les propriétés à vérifier sur le contrat Vault.

# Specification CVL pour Vault
CVL_SPEC = '''
// Fichier: Vault.spec

// Definition du contrat a verifier
methods {
    function balances(address) external returns (uint256) envfree;
    function totalDeposits() external returns (uint256) envfree;
    function deposit() external payable;
    function withdraw(uint256) external;
}

// Invariant global: sum des balances == totalDeposits
invariant totalDepositsEqSumOfBalances()
    totalDeposits() == sum(user => balances(user));

// Invariant: chaque balance est positive ou nulle
invariant balancesNonNegative(address user)
    balances(user) >= 0;

// Invariant: totalDeposits jamais negatif
invariant totalDepositsNonNegative()
    totalDeposits() >= 0;

// Regle: apres un deposit, le solde augmente
rule depositIncreasesBalance(address user, uint256 amount) {
    require amount > 0;
    uint256 balanceBefore = balances(user);
    
    // Supposer que user fait un deposit
    env.msgSender = user;
    env.msgValue = amount;
    deposit();
    
    // Verifier le resultat
    assert balances(user) == balanceBefore + amount;
}

// Regle: withdraw reduit correctement la balance
rule withdrawDecreasesBalance(address user, uint256 amount) {
    require amount > 0;
    require balances(user) >= amount;
    
    uint256 balanceBefore = balances(user);
    uint256 totalBefore = totalDeposits();
    
    env.msgSender = user;
    withdraw(amount);
    
    assert balances(user) == balanceBefore - amount;
    assert totalDeposits() == totalBefore - amount;
}
'''

print("Specification CVL:")
print(CVL_SPEC)
Specification CVL:

// Fichier: Vault.spec

// Definition du contrat a verifier
methods {
    function balances(address) external returns (uint256) envfree;
    function totalDeposits() external returns (uint256) envfree;
    function deposit() external payable;
    function withdraw(uint256) external;
}

// Invariant global: sum des balances == totalDeposits
invariant totalDepositsEqSumOfBalances()
    totalDeposits() == sum(user => balances(user));

// Invariant: chaque balance est positive ou nulle
invariant balancesNonNegative(address user)
    balances(user) >= 0;

// Invariant: totalDeposits jamais negatif
invariant totalDepositsNonNegative()
    totalDeposits() >= 0;

// Regle: apres un deposit, le solde augmente
rule depositIncreasesBalance(address user, uint256 amount) {
    require amount > 0;
    uint256 balanceBefore = balances(user);

    // Supposer que user fait un deposit
    env.msgSender = user;
    env.msgValue = amount;
    deposit();

    // Verifier le resultat
    assert balances(user) == balanceBefore + amount;
}

// Regle: withdraw reduit correctement la balance
rule withdrawDecreasesBalance(address user, uint256 amount) {
    require amount > 0;
    require balances(user) >= amount;

    uint256 balanceBefore = balances(user);
    uint256 totalBefore = totalDeposits();

    env.msgSender = user;
    withdraw(amount);

    assert balances(user) == balanceBefore - amount;
    assert totalDeposits() == totalBefore - amount;
}

Interpretation : Spécification CVL - Invariants et règles

Résultat obtenu : Langage de spécification formelle pour Certora Prover.

Concept Syntaxe CVL Signification
Invariant invariant nom() condition Propriété toujours vraie
Règle rule nom(params) { require...; env...; call(); assert...; } Comportement attendu
Sum sum(x => f(x)) Quantification universelle

Points clés : - totalDepositsEqSumOfBalances() : invariant de conservation (somme des balances = total) - balancesNonNegative() : invariant de sécurité (pas de balances négatives) - depositIncreasesBalance() : règle de comportement (après deposit, balance augmente) - env.msgSender et env.msgValue permettent de simuler l’environnement d’appel

3. Commandes Certora

Exécution du vérifier.

# Commandes Certora
print("""
INSTALLATION:
# Via npm
npm install -g @certora/certora-cli

# Configurer la cle API
export CERTORAKEY=your_api_key

EXECUTION:
# Verifier un contrat
certoraRun Vault.sol --verify Vault:Vault.spec

# Avec optimisations
certoraRun Vault.sol --verify Vault:Vault.spec --optimistic_loop

# Debug mode
certoraRun Vault.sol --verify Vault:Vault.spec --debug

# Lister les regles
certoraRun Vault.sol --verify Vault:Vault.spec --rule depositIncreasesBalance
""")

INSTALLATION:
# Via npm
npm install -g @certora/certora-cli

# Configurer la cle API
export CERTORAKEY=your_api_key

EXECUTION:
# Verifier un contrat
certoraRun Vault.sol --verify Vault:Vault.spec

# Avec optimisations
certoraRun Vault.sol --verify Vault:Vault.spec --optimistic_loop

# Debug mode
certoraRun Vault.sol --verify Vault:Vault.spec --debug

# Lister les regles
certoraRun Vault.sol --verify Vault:Vault.spec --rule depositIncreasesBalance

3b. SMTChecker - Vérification native Solidity

Contrairement à Certora (outil externe, commercial), SMTChecker est intégré au compilateur Solidity. Il utilise des solveurs SMT (Z3, CVC5) pour vérifier automatiquement des invariants.

Aspect Certora Prover SMTChecker
Installation npm install -g @certora/certora-cli Inclus dans solc
Langage spec CVL séparé Assertions Solidity natives
Coût Commercial (API key) Gratuit
Couverture Très complet Limité (pas de boucles infinies)
Model checking Interactif Automatique

Activation : pragma experimental SMTChecker; dans le contrat.

# Contrat Vault avec SMTChecker - detection d'un bug d'overflow
vault_smt_code = """
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.28;
pragma experimental SMTChecker;

contract VaultSMT {
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;

    /// @custom:invariant totalDeposits == sum(balances)
    function deposit() external payable {
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }

    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "Insufficient balance");
        balances[msg.sender] -= amount;
        totalDeposits -= amount;

        // Assertion SMTChecker : le solde ne peut pas etre negatif
        assert(balances[msg.sender] >= 0);

        payable(msg.sender).transfer(amount);
    }

    // Assertion : totalDeposits toujours coherent
    function checkInvariant() public view {
        assert(totalDeposits >= 0);
    }
}
"""

print("Contrat VaultSMT avec assertions SMTChecker :")
print(vault_smt_code)
print("\n---")
print("Points cles :")
print("1. 'pragma experimental SMTChecker' active le model checker")
print("2. Les 'assert()' sont verifiees pour TOUTES les executions possibles")
print("3. Si une assertion peut echouer, le compilateur genere un contre-exemple")
Contrat VaultSMT avec assertions SMTChecker :

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.28;
pragma experimental SMTChecker;

contract VaultSMT {
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;

    /// @custom:invariant totalDeposits == sum(balances)
    function deposit() external payable {
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }

    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "Insufficient balance");
        balances[msg.sender] -= amount;
        totalDeposits -= amount;

        // Assertion SMTChecker : le solde ne peut pas etre negatif
        assert(balances[msg.sender] >= 0);

        payable(msg.sender).transfer(amount);
    }

    // Assertion : totalDeposits toujours coherent
    function checkInvariant() public view {
        assert(totalDeposits >= 0);
    }
}


---
Points cles :
1. 'pragma experimental SMTChecker' active le model checker
2. Les 'assert()' sont verifiees pour TOUTES les executions possibles
3. Si une assertion peut echouer, le compilateur genere un contre-exemple

Interpretation : SMTChecker - Model checking natif

Résultat obtenu : Activation du model checker Solidity avec détection potentielle de bugs.

Élément Rôle
pragma experimental SMTChecker Active le model checker natif
assert(condition) Vérifie que la condition est TOUJOURS vraie
@custom:Invariant Documentation des invariants attendus

Points clés : - Contrairement aux tests (qui échantillonnent), SMTChecker explore TOUTES les exécutions possibles - Si une assertion peut échouer, le compilateur génère un contre-exemple concret - Les limitations : pas de support complet pour les boucles, certains appels externes - Avantage majeur : intégré au compilateur, gratuit, pas besoin de langage de spec externe

# Invocation REELLE du compilateur Solidity avec SMTChecker
# (Stop & Repair : la version precedente hardcodait une sortie supposee "reelle".
#  On invoque maintenant le vrai binaire solc et on affiche sa sortie effective.
#  Le .sol est ecrit en chemin relatif (cwd) pour garder une sortie propre, sans
#  chemin machine - regle secrets-hygiene case A : on corrige la source, jamais la sortie.)
import subprocess, os, shutil

def _locate_solc() -> str:
    """Localise le binaire solc installe (solcx, puis PATH)."""
    try:
        import solcx
        if hasattr(solcx, "get_executable"):
            return solcx.get_executable("0.8.28")
        # solcx ancienne API : construire le chemin depuis le dossier d'installation
        bin_dir = os.path.join(solcx.get_solcx_install_folder(), "solc-v0.8.28")
        for name in ("solc.exe", "solc"):
            cand = os.path.join(bin_dir, name)
            if os.path.isfile(cand):
                return cand
    except Exception:
        pass
    return shutil.which("solc") or "solc"

def run_smtchecker(contract_code: str, label: str) -> None:
    """Invoque le vrai solc avec le model checker SMT et affiche sa sortie reelle."""
    rel_path = "sc14_smtcheck.sol"
    with open(rel_path, "w", encoding="utf-8") as f:
        f.write(contract_code)
    try:
        solc_bin = _locate_solc()
        print(f"=== {label} ===")
        print(f"$ {os.path.basename(solc_bin)} --model-checker-engine all {rel_path}\n")
        try:
            res = subprocess.run(
                [solc_bin, "--model-checker-engine", "all", rel_path],
                capture_output=True, text=True, timeout=120,
            )
        except FileNotFoundError:
            print("[solc introuvable : installer solc (solcx install_solc 0.8.28) pour executer SMTChecker]")
            return
        # SMTChecker emet ses diagnostics (warnings/contre-exemples) sur stderr
        diag = (res.stderr + ("\n" + res.stdout if res.stdout.strip() else "")).strip()
        print(diag if diag else "(compilation reussie, aucun diagnostique)")
        print(f"\n[code de sortie solc : {res.returncode}]")
    finally:
        if os.path.exists(rel_path):
            os.unlink(rel_path)

# 1) Contrat sain : checks-effects-interactions respecte (etat mis a jour AVANT le transfer)
run_smtchecker(vault_smt_code, "Contrat VaultSMT (sain)")

# 2) Contrat buggy : reentrancy (transfer AVANT mise a jour de l'etat)
vault_buggy_code = """
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.28;
pragma experimental SMTChecker;
contract VaultBuggy {
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;
    function deposit() external payable {
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }
    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount, "Insufficient balance");
        payable(msg.sender).transfer(amount);  // BUG : transfer AVANT mise a jour
        balances[msg.sender] -= amount;
        totalDeposits -= amount;
        assert(balances[msg.sender] >= 0);
    }
}
"""
print("\n" + "=" * 60 + "\n")
run_smtchecker(vault_buggy_code, "Contrat VaultBuggy (reentrancy)")
=== Contrat VaultSMT (sain) ===
$ solc.exe --model-checker-engine all sc14_smtcheck.sol

Warning: Solver z3 was selected for SMTChecker but it is not available.

Warning: The SMTChecker pragma has been deprecated and will be removed in the future. Please use the "model checker engine" compiler setting to activate the SMTChecker instead. If the pragma is enabled, all engines will be used.
 --> sc14_smtcheck.sol:4:1:
  |
4 | pragma experimental SMTChecker;
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Warning: CHC analysis was not possible since no Horn solver was found and enabled. The accepted solvers for CHC are Eldarica and z3.

Warning: BMC analysis was not possible since no SMT solver was found and enabled. The accepted solvers for BMC are cvc5 and z3.

[code de sortie solc : 0]

============================================================

=== Contrat VaultBuggy (reentrancy) ===
$ solc.exe --model-checker-engine all sc14_smtcheck.sol

Warning: Solver z3 was selected for SMTChecker but it is not available.

Warning: The SMTChecker pragma has been deprecated and will be removed in the future. Please use the "model checker engine" compiler setting to activate the SMTChecker instead. If the pragma is enabled, all engines will be used.
 --> sc14_smtcheck.sol:4:1:
  |
4 | pragma experimental SMTChecker;
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Warning: CHC analysis was not possible since no Horn solver was found and enabled. The accepted solvers for CHC are Eldarica and z3.

Warning: BMC analysis was not possible since no SMT solver was found and enabled. The accepted solvers for BMC are cvc5 and z3.

[code de sortie solc : 0]

Interpretation : SMTChecker vs Certora

Résultat obtenu : invocation réelle du binaire solc (--model-checker-engine all) sur les deux contrats. Sur ce build solc (Windows statique), aucun solveur SMT (z3/cvc5) n’est lié au binaire : SMTChecker signale Solver z3 was selected ... but it is not available et CHC/BMC analysis was not possible since no SMT solver was found. Les contrats compilent, mais l’analyse formelle ne s’est pas exécutée ici.

Verdict (EPIC #3801, axe-2 SOTA) : RECOVERABLE-MACHINE. Le vrai outil SOTA (solc SMTChecker) fonctionne sur un binaire solc compilé avec z3 — typiquement le binaire statique Linux de soliditylang.org ou apt install solc z3. Sur cette machine (solc Windows sans z3 lié, WSL sans solc), le contre-exemple reel n’est pas atteignable ; il faut re-exécuter sur une machine Linux+z3 pour le voir.

Aspect SMTChecker Certora Prover
Intégration Natif dans solc Outil externe (npm)
Langage Solidity (assert) CVL (spec séparée)
Coût Gratuit Commercial
Couverture Limitations (boucles) Très complet
Dépendance Solveur z3/cvc5 lié au binaire solc Solveur SMT interne

Forme attendue du contre-exemple (reference, d’après la documentation Solidity — non produite par cette exécution car solveur absent) : SMTChecker explore symboliquement toutes les exécutions possibles du contrat — la vérification est exhaustive, là où les tests fuzz échantillonnent ; quand une assertion peut échouer, il produit un contre-exemple concret avec les valeurs d’entrée qui déclenchent le bug. Pour VaultBuggy, il générerait un Counterexample montrant qu’après le transfer et avant le decrement, balances[msg.sender] reste incohérent avec totalDeposits — fenêtre de reentrancy exploitable. Le pattern correct est “checks-effects-interactions” : mettre à jour l’état AVANT les appels externes, ce que fait VaultSMT.

Exercice 2 : SMTChecker - Assertions pour un TokenVault

En vous basant sur l’exemple de VaultSMT ci-dessus, identifiez les assertions SMTChecker manquantes dans un contrat TokenVault avec transfer et withdraw.

Objectif : Ajoutez les assert() manquants dans le code Solidity pour que SMTChecker puisse vérifier les invariants de conservation et de non-négativité.

Indice : - Dans transfer(), que doit-on vérifier sur totalSupply ? - Dans withdraw(), que doit-on vérifier sur balances[msg.sender] ? - Pensez au pattern “checks-effects-interactions”

Étapes : 1. Ecrire l’assertion de conservation des tokens dans transfer() 2. Ecrire l’assertion de non-négativité dans withdraw()

# Exercice 2 : SMTChecker - Assertions pour un TokenVault
# TODO etudiant : identifiez les assertions SMTChecker manquantes
TOKEN_VAULT_CODE = """
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.28;
pragma experimental SMTChecker;

contract TokenVault {
    mapping(address => uint256) public balances;
    uint256 public totalSupply;

    function deposit() external payable {
        balances[msg.sender] += msg.value;
        totalSupply += msg.value;
    }

    function transfer(address to, uint256 amount) external {
        require(balances[msg.sender] >= amount);
        balances[msg.sender] -= amount;
        balances[to] += amount;
        // TODO etudiant : assert conservation des tokens (totalSupply inchange)
    }

    function withdraw(uint256 amount) external {
        require(balances[msg.sender] >= amount);
        balances[msg.sender] -= amount;
        totalSupply -= amount;
        // TODO etudiant : assert balance non negative
        payable(msg.sender).transfer(amount);
    }
}
"""

# TODO etudiant : listez les 2 assertions manquantes sous forme de commentaires Solidity
# Indice 1 : dans transfer(), totalSupply doit rester identique apres l'operation
# Indice 2 : dans withdraw(), la balance de msg.sender ne peut pas etre negative
# Etape 1 : ecrire assert(totalSupply == totalSupply) avant et apres transfer
# Etape 2 : ecrire assert(balances[msg.sender] >= 0) apres le decrement dans withdraw
missing_asserts = []  # TODO etudiant : ajoutez vos assertions en strings

print("Exercice a completer")
print("Identifiez les assertions SMTChecker manquantes dans le contrat TokenVault")
Exercice a completer
Identifiez les assertions SMTChecker manquantes dans le contrat TokenVault

4. Patterns Courants

4.1 Conservation des tokens (ERC-20)

# Specification ERC-20 simplifiee
ERC20_SPEC = '''
methods {
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function transfer(address, uint256) external returns (bool);
    function allowance(address, address) external returns (uint256) envfree;
    function approve(address, uint256) external returns (bool);
    function transferFrom(address, address, uint256) external returns (bool);
}

// Invariant: conservation des tokens
invariant totalSupplyConservation()
    totalSupply() == sum(user => balanceOf(user));

// Invariant: pas de balance negative
invariant balanceNonNegative(address user)
    balanceOf(user) >= 0;

// Regle: transfer conserve les tokens
rule transferConservesTokens(address from, address to, uint256 amount) {
    require from != to;
    require balanceOf(from) >= amount;
    
    uint256 fromBalanceBefore = balanceOf(from);
    uint256 toBalanceBefore = balanceOf(to);
    uint256 supplyBefore = totalSupply();
    
    env.msgSender = from;
    transfer(to, amount);
    
    assert balanceOf(from) == fromBalanceBefore - amount;
    assert balanceOf(to) == toBalanceBefore + amount;
    assert totalSupply() == supplyBefore;
}
'''

print("Specification ERC-20:")
print(ERC20_SPEC)
Specification ERC-20:

methods {
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function transfer(address, uint256) external returns (bool);
    function allowance(address, address) external returns (uint256) envfree;
    function approve(address, uint256) external returns (bool);
    function transferFrom(address, address, uint256) external returns (bool);
}

// Invariant: conservation des tokens
invariant totalSupplyConservation()
    totalSupply() == sum(user => balanceOf(user));

// Invariant: pas de balance negative
invariant balanceNonNegative(address user)
    balanceOf(user) >= 0;

// Regle: transfer conserve les tokens
rule transferConservesTokens(address from, address to, uint256 amount) {
    require from != to;
    require balanceOf(from) >= amount;

    uint256 fromBalanceBefore = balanceOf(from);
    uint256 toBalanceBefore = balanceOf(to);
    uint256 supplyBefore = totalSupply();

    env.msgSender = from;
    transfer(to, amount);

    assert balanceOf(from) == fromBalanceBefore - amount;
    assert balanceOf(to) == toBalanceBefore + amount;
    assert totalSupply() == supplyBefore;
}

Exercice 3 : CVL - Règle pour approve() et transferFrom()

L’exemple ERC-20 ci-dessus spécifie la règle transferConservesTokens. Écrivez une règle CVL supplémentaire pour vérifier que transferFrom respecte les allowances.

Objectif : Completer la règle transferFromRespectsAllowance qui vérifie que transferFrom réduit correctement l’allowance et déplace les tokens.

Indice : - La fonction transferFrom(owner, to, amount) nécessite allowance(owner, spender) >= amount - Vérifiez que l’allowance diminue du bon montant - Vérifiez que les balances sont mises à jour correctement

Étapes : 1. Définir les preconditions (require) dans la règle CVL 2. Capturer les valeurs avant l’appel (balances, allowance) 3. Appeler transferFrom avec le bon env.msgSender 4. Ecrire les 3 assertions de vérification

# Exercice 3 : CVL - Regle pour approve() et transferFrom()
# TODO etudiant : completez la regle CVL transferFromRespectsAllowance
TRANSFERFROM_RULE = """
// TODO etudiant : completez la regle CVL ci-dessous

rule transferFromRespectsAllowance(address owner, address spender, address to, uint256 amount) {
    // Etape 1 : Preconditions
    // TODO etudiant : ajouter les require necessaires
    // require owner != to;
    // require balanceOf(owner) >= amount;
    // require allowance(owner, spender) >= amount;

    // Etape 2 : Capturer les valeurs avant l'appel
    // uint256 ownerBalBefore = balanceOf(owner);
    // uint256 toBalBefore = balanceOf(to);
    // uint256 allowanceBefore = allowance(owner, spender);

    // Etape 3 : Appeler transferFrom avec spender comme msgSender
    // env.msgSender = spender;
    // transferFrom(owner, to, amount);

    // Etape 4 : Verifier les resultats
    // TODO etudiant : ecrire les 3 assertions
    // assert balanceOf(owner) == ownerBalBefore - amount;
    // assert balanceOf(to) == toBalBefore + amount;
    // assert allowance(owner, spender) == allowanceBefore - amount;
}
"""

print("Exercice a completer")
print("Completez la regle CVL transferFromRespectsAllowance dans TRANSFERFROM_RULE")
Exercice a completer
Completez la regle CVL transferFromRespectsAllowance dans TRANSFERFROM_RULE

5. Exercices

# Exercice: Verifier un SimpleAuction
# TODO etudiant : ecrire les specifications CVL pour le contrat SimpleAuction
# Indice : quelles proprietes un enchere doit-elle garantir ?
# Etape 1 : definir les invariants (highestBid toujours positif, ended ne peut que passer a true)
# Etape 2 : ecrire une regle pour verifier que bid() met a jour highestBidder et highestBid

EXERCISE_AUCTION = '''
// Contrat
contract SimpleAuction {
    address public beneficiary;
    address public highestBidder;
    uint256 public highestBid;
    bool public ended;

    function bid() external payable {
        require(!ended, "Auction ended");
        require(msg.value > highestBid, "Bid too low");
        highestBidder = msg.sender;
        highestBid = msg.value;
    }

    function end() external {
        require(!ended, "Already ended");
        ended = true;
    }
}

// Specification CVL
// TODO: etudiant - definissez les invariants ci-dessous
/*
methods {
    // TODO: etudiant - declarer les fonctions du contrat
}

// Invariant: le highest bid est toujours positif ou nul
invariant highestBidPositive()
    // TODO: etudiant - ecrire la condition

// Invariant: ended ne peut que passer de false a true
invariant endedIsMonotonic()
    // TODO: etudiant - ecrire la condition
    // Indice : ended => toujours(ended)

// Regle: un bid valide met a jour le highest bidder
rule bidUpdatesHighestBidder(address bidder, uint256 amount) {
    // TODO: etudiant - ecrire la precondition (pas ended, amount > highestBid)
    // TODO: etudiant - appeler bid() avec les bons parametres env
    // TODO: etudiant - verifier highestBidder == bidder et highestBid == amount
}
*/
'''

print("Exercice Auction Formal Verification - a completer")
print("Implementez les specifications CVL marquees TODO dans EXERCISE_AUCTION")
Exercice Auction Formal Verification - a completer
Implementez les specifications CVL marquees TODO dans EXERCISE_AUCTION

Indice : Pour les invariants, réfléchissez aux propriétés qu’une enchère valide doit toujours respecter : le plus haut enchère est toujours positif, une enchère terminée ne peut pas reprendre. Pour la règle, vérifiez que bid() met correctement à jour highestBidder et highestBid.

6. Résumé

Concept Description
Invariant Propriété toujours vraie
Règle Comportement attendu après une action
methods Déclaration des fonctions du contrat (CVL)
envfree Fonction sans effets de bord
env Environnement (msg.sender, msg.value, block.timestamp)
assert Assertion SMTChecker vérifiée exhaustivement
pragma experimental SMTChecker Activation du model checker natif

Outils de vérification formelle

Outil Type Coût Complexité
Certora Prover Externe (CVL) Commercial Élevée
SMTChecker Natif Solidity Gratuit Moyenne
Halmos Symbolic EVM Open source Élevée

Avantages

  • Couverture complète (tous les cas possibles)
  • Preuves mathématiques rigoureuses
  • Détection de bugs subtils (reentrancy, overflow)

Limites

  • Complexité de configuration (Certora)
  • Temps de vérification
  • Faux positifs possibles
  • SMTChecker : pas de support complet des boucles

Notebook suivant : Zero-Knowledge Proofs

Résumé et perspectives

Ce notebook a introduit la vérification formelle des smart contracts, une approche qui complète les tests unitaires et le fuzz testing en apportant des preuves mathématiques exhaustives. Nous avons exploré le langage CVL (Certora Vérification Language) pour ecrire des invariants (conservation des tokens, non-négativité des soldes) et des règles de comportement sur un contrat Vault, puis découvert SMTChecker, l’alternative native et gratuite intégrée au compilateur Solidity. La demonstration du contrat VaultBuggy a illustré la puissance de l’approche : SMTChecker produit un contre-exemple concret quand une assertion peut être violée — sous réserve de disposer d’un binaire solc lié à un solveur SMT (z3), absent de ce build Windows (verdict RECOVERABLE-MACHINE : re-exécuter sur Linux+z3).

La vérification formelle reste un investissement significatif en temps et en expertise, mais elle est indispensable pour les contrats critiques qui sécurisent des milliards de dollars en valeur verrouillée (DeFi, bridges, protocoles de gouvernance). Les outils évoluent rapidement : Certora Prover pour les spécifications expressives en CVL, Halmos pour l’exécution symbolique sur l’EVM, et SMTChecker pour les assertions natives sans dépendance externe. La complémentarité avec les tests classiques (foundry test, fuzz testing, invariant testing) définit une stratégie de validation multicouche ou chaque méthode couvre les angles morts des autres.

Le prochain notebook aborde les preuves à divulgation nulle (Zero-Knowledge Proofs), une technique cryptographique fondamentale pour la confidentialité sur blockchain : prouver qu’un énoncé est vrai sans révéler aucune information supplémentaire. Ce concept, au coeur des zk-SNARKs et des zk-rollups, constitue l’un des domaines les plus actifs de la recherche blockchain actuelle : SC-15-Zero-Knowledge-Proofs-Python.

<< Précédent : Fuzz & Invariants | Retour au sommaire | Suivant : Zero-Knowledge Proofs >>

Retour au sommet