Invariant Breaks (Quebra de Invariantes)

Ocorre quando as condições ou “invariantes” que deveriam permanecer sempre verdadeiras dentro de um contrato inteligente são violadas. As invariantes são propriedades ou regras fundamentais que não devem mudar durante a execução do contrato. Se um atacante — ou até mesmo um usuário legítimo — encontrar uma forma de quebrar essas invariantes, podem ocorrer comportamentos inesperados, erros críticos ou perdas financeiras.

Exemplo: Considere um contrato inteligente de uma stablecoin que deve manter uma relação de 1:1 entre os tokens emitidos e os colaterais em reserva. Se por alguma falha na lógica do contrato ou manipulação externa essa relação for rompida — por exemplo, emitindo mais tokens do que colateral disponível — isso representaria uma quebra de invariante. Tal situação comprometeria a estabilidade e confiança na stablecoin, podendo causar perdas para os usuários:

contract Stablecoin {
    mapping(address => uint) public balances;
    uint public totalSupply;
    uint public totalCollateral;

    function mint(uint amount) external payable {
        require(msg.value == amount, "Must send exact collateral");
        balances[msg.sender] += amount;
        totalSupply += amount;
        totalCollateral += msg.value;
    }

    function burn(uint amount) external {
        require(balances[msg.sender] >= amount, "Insufficient balance");
        balances[msg.sender] -= amount;
        totalSupply -= amount;
        payable(msg.sender).transfer(amount);
        totalCollateral -= amount;
    }
}

Neste contrato, a invariante crítica é que totalSupply deve ser sempre igual a totalCollateral, garantindo que cada token emitido esteja lastreado por um valor equivalente em colateral.

Suponha que o contrato permita realizar operações de mint e burn dentro de uma mesma transação, mas não verifica corretamente o estado intermediário entre essas operações:

function mintAndBurn(uint mintAmount, uint burnAmount) external payable {
    mint(mintAmount);
    burn(burnAmount);
}

Se um atacante conseguir encontrar uma sequência específica de chamadas em que essa invariante seja quebrada temporariamente, ele poderá manipular o estado do contrato em benefício próprio. Por exemplo, poderia mintar mais tokens do que estão lastreados pelo colateral disponível ou queimar tokens sem reduzir o colateral equivalente, o que levaria a um desequilíbrio na reserva.

Mitigação:

1. Validação de invariantes: Após cada operação crítica (como mint ou burn), o contrato deve validar explicitamente que as invariantes fundamentais foram mantidas. Isso pode ser feito por meio de funções de verificação, que asseguram que as relações entre variáveis importantes não foram violadas durante a execução da transação.

   function checkInvariants() internal view {
       require(totalSupply == totalCollateral, "Invariant violation: totalSupply must equal totalCollateral");
   }
   
   function mint(uint amount) external payable {
       require(msg.value == amount, "Must send exact collateral");
       balances[msg.sender] += amount;
       totalSupply += amount;
       totalCollateral += msg.value;
       checkInvariants();
   }
   
   function burn(uint amount) external {
       require(balances[msg.sender] >= amount, "Insufficient balance");
       balances[msg.sender] -= amount;
       totalSupply -= amount;
       payable(msg.sender).transfer(amount);
       totalCollateral -= amount;
       checkInvariants();
   }

2. Uso de modelos formais: Aplicar técnicas de verificação formal para modelar e testar o comportamento do contrato em diferentes cenários, garantindo que as invariantes sejam mantidas em todas as execuções possíveis. Ferramentas como Certora, K Framework, KEVM, ou métodos baseados em SMT solvers permitem analisar logicamente o código e detectar violações de invariantes antes da implementação real na blockchain.

3. Restrição de operações compostas: Evitar que múltiplas operações críticas sejam realizadas dentro da mesma transação sem validação adequada do estado após cada uma delas. Se for necessário permitir tais operações compostas, isso deve ser feito com máximo cuidado, garantindo que as invariantes sejam preservadas em todos os pontos intermediários da execução.