Solidity के लिए formal verification: Halmos और Certora

# Solidity के लिए formal verification: Halmos और Certora

ज्यादातर Solidity testing इस सवाल का जवाब देती है "क्या यह उन cases के लिए काम करता है जो मैंने आजमाए?" Fuzzing इसे बढ़ाकर "क्या यह हजारों random cases के लिए काम करता है?" कर देता है। Formal verification एक मजबूत सवाल पूछती है: "क्या कहीं कोई ऐसा input है जो मेरी property को तोड़ देता है?" जब जवाब नहीं होता, तो आपको हरे checkmark के बजाय एक mathematical proof मिलता है। यह लेख समझाता है कि verification fuzzing के ऊपर क्या जोड़ती है, properties और invariants कैसे लिखें, और दो practical tools, Halmos और Certora Prover, इस काम को कैसे करते हैं।

Formal verification fuzzing के ऊपर क्या जोड़ती है

Foundry के built-in engine जैसा fuzzer concrete inputs sample करता है। यह तेज, सस्ता है, और बहुत सारे bugs पकड़ता है, लेकिन यह input space का सिर्फ एक सीमित हिस्सा ही explore कर सकता है। अगर कोई vulnerability किसी uint256 के एक खास value में रहती है, तो fuzzer शायद कभी वह पासा न फेंके।

Formal verification tools सभी inputs पर एक साथ reasoning करते हैं। वे यह symbolic execution के जरिए करते हैं: आपके function को number 42 के साथ चलाने के बजाय, वे इसे एक symbolic variable x के साथ चलाते हैं जो हर संभव value का प्रतिनिधित्व करता है। फिर tool परिणामी logical constraints को एक SMT solver (आमतौर पर Z3 या ऐसा ही backend) को सौंपता है और पूछता है: क्या x का कोई assignment assertion का उल्लंघन कर सकता है?

• अगर solver unsat कहता है (ऐसा कोई assignment मौजूद नहीं), तो property हर input के लिए सही है।

• अगर यह sat कहता है, तो यह एक concrete counterexample लौटाता है, एक खास input जो property को तोड़ता है।

वह counterexample ही असली फायदा है। आपको सिर्फ यह पता नहीं चलता कि कुछ गलत है; आपको वह exact transaction मिलती है जो इसे साबित करती है।

इसका trade-off है path explosion। Loops और गहरे call stacks उन paths की संख्या को बढ़ा देते हैं जिन पर solver को विचार करना होता है, इसलिए ज्यादातर tools *bounded* होते हैं: वे N loop iterations या एक fixed call depth तक verify करते हैं। results पढ़ते समय इस सीमा के बारे में ईमानदार रहें।

Properties और invariants

Verification उतनी ही अच्छी है जितनी आपकी लिखी हुई property। दो आकार प्रमुख हैं।

Properties (कभी-कभी rules कहलाती हैं) बताती हैं कि एक single function call को क्या guarantee देना चाहिए। उदाहरण: "transfer(to, amount) सफल होने के बाद, sender का balance ठीक amount जितना घटता है।"

Invariants एक ऐसे तथ्य का वर्णन करते हैं जो हर reachable state में सही होना चाहिए, contract की किसी भी exposed function के पहले और बाद में। उदाहरण: "सभी balances का योग हमेशा totalSupply के बराबर होता है।" Invariant ज्यादा शक्तिशाली statement है क्योंकि यह contract को उसके पूरे lifecycle भर constrain करता है, सिर्फ एक call को नहीं।

अच्छी properties आमतौर पर होती हैं:

Total, success और revert दोनों paths को कवर करती हुई।

Relational, किसी magic constant को assert करने के बजाय पहले और बाद की state की तुलना करती हुई।

Minimal, ताकि एक failure एक ही कारण की ओर इशारा करे।

Halmos: open source, Foundry style

a16z का Halmos आपके Foundry-style Solidity tests को symbolically चलाता है। अगर आप पहले से Foundry tests लिखते हैं, तो learning curve छोटा है। convention है test के बजाय check_ से prefix की गई function। उस function का हर parameter एक symbolic value बन जाता है, इसलिए एक अकेली check_ function पूरे fuzzing campaign की जगह लेती है, लेकिन अंत में एक proof के साथ।

यहां एक minimal token के लिए property है, जो साबित करती है कि transfer ठीक amount को move करता है और supply को कभी inflate नहीं करता:

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

import {Test} from "forge-std/Test.sol";
import {Token} from "../src/Token.sol";

contract TokenSymbolicTest is Test {
    Token internal token;

    function setUp() public {
        token = new Token();
    }

    // यहां हर parameter symbolic है: Halmos सभी values explore करता है।
    function check_transfer(address from, address to, uint256 amount) public {
        vm.assume(from != to);
        vm.prank(from);
        token.mint(from, amount);

        uint256 supplyBefore = token.totalSupply();
        uint256 fromBefore = token.balanceOf(from);
        uint256 toBefore = token.balanceOf(to);

        vm.prank(from);
        bool ok = token.transfer(to, amount);

        if (ok) {
            assertEq(token.balanceOf(from), fromBefore - amount);
            assertEq(token.balanceOf(to), toBefore + amount);
            assertEq(token.totalSupply(), supplyBefore); // supply संरक्षित है
        }
    }
}

आप इसे command line से चलाते हैं:

halmos --function check_transfer

अगर property सही है, तो Halmos path को passing बताता है। अगर नहीं, तो यह from, to, और amount के concrete values के साथ एक counterexample print करता है। चूंकि loops bounded हैं, आप depth को स्पष्ट रूप से control करते हैं:

halmos --function check_transfer --loop 4

Halmos का मुख्य फायदा reuse है। आप test harness, cheatcodes (vm.assume, vm.prank), और जो mental model आपके पास पहले से है उसका लाभ उठाते हैं, और prefix का नाम बदलकर तथा assumptions कसकर एक fuzz test को एक bounded proof में upgrade कर देते हैं।

Certora Prover: CVL में dedicated specs

Certora Prover specification को test harness से अलग करता है। आप properties को एक dedicated language में लिखते हैं, CVL (Certora Verification Language), जो contract के साथ एक .spec file में संग्रहीत होती है। CVL verification के लिए बना है, इसलिए यह invariants और relational rules को सीधे express करता है, और Prover कई patterns के लिए वही loop bounds नहीं थोपता जो Foundry-style runner थोपता है (loops फिर भी handle होती हैं, अक्सर एक unrolling के जरिए जिसे आप configure करते हैं)।

एक CVL rule ऊपर वाली property को दर्शाता है:

rule transferPreservesSupply(address to, uint256 amount) {
    env e;
    require e.msg.sender != to;

    uint256 supplyBefore = totalSupply();
    uint256 senderBefore = balanceOf(e.msg.sender);
    uint256 toBefore      = balanceOf(to);

    transfer(e, to, amount);

    assert totalSupply() == supplyBefore, "supply संरक्षित होनी चाहिए";
    assert balanceOf(e.msg.sender) == senderBefore - amount;
    assert balanceOf(to) == toBefore + amount;
}

जहां Certora चमकता है वह है invariants। Prover एक invariant को दो steps में जांचता है: यह पुष्टि करता है कि constructor इसे स्थापित करता है, फिर पुष्टि करता है कि हर public method इसे preserve करती है। आप methods की गिनती नहीं करते; Prover करता है। यह उदाहरण बताता है कि total supply दो tracked balances के योग के बराबर है और पूरे contract भर सही रहता है:

invariant supplyEqualsBalances()
    totalSupply() == balanceOf(alice) + balanceOf(bob)
    {
        preserved {
            require alice != bob;
        }
    }

preserved block आपको ऐसी assumptions बताने देता है जो हर method चलने से पहले सही होनी चाहिए। आप filtered clause के साथ यह भी सीमित कर सकते हैं कि किसी invariant को किन functions के खिलाफ जांचा जाए, उदाहरण के लिए एक privileged mint को skip करना जो वैध रूप से supply बदलता है।

इनमें से चुनाव कैसे करें

| | Halmos | Certora Prover |

|---|---|---|

| Spec language | Solidity (check_ tests) | CVL .spec files |

| Setup | Foundry harness reuse करता है | अलग spec, config file |

| Cost | Open source, मुफ्त | Commercial, community access tiers के साथ |

| Sweet spot | तेज bounded proofs, तेज iteration | सभी methods भर गहरे invariants |

ये दोनों प्रतिद्वंद्वी के बजाय पूरक हैं। एक आम workflow यह है कि Halmos में properties prototype करें क्योंकि idea से result तक का loop छोटा है, फिर सबसे महत्वपूर्ण invariants को CVL में promote करें ताकि Certora Prover जो मजबूत, method-spanning guarantees देता है वे मिलें।

कुछ सावधानियां दोनों tools पर लागू होती हैं। Verification उस property को साबित करती है जो आपने लिखी, उस property को नहीं जो आपका मतलब था, इसलिए एक कमजोर spec झूठा भरोसा देती है। External calls और unbounded loops कठिन रहते हैं, और आपको अक्सर उन्हें model या summarize करना होगा। काम को iterative मानें: एक property लिखें, एक counterexample पाएं, refine करें, दोहराएं।

इसे Solingo पर practice करें

इस सबको आत्मसात करने का सबसे तेज तरीका है जानबूझकर एक property को तोड़ना और counterexample को प्रकट होते देखना। app.solingo-blockchain.xyz पर आप एक छोटा token लिख सकते हैं, supply conservation जैसा एक invariant बता सकते हैं, एक सूक्ष्म bug डाल सकते हैं, और देख सकते हैं कि वहां एक proof obligation कैसे fail होती है जहां एक fuzzer हरा रह सकता था। एक invariant से शुरू करें, उसे साबित करें, फिर उसे तोड़ने की कोशिश करें।