Relatando um Bug em integer_squareroot na Especificação de Consenso do Ethereum

Desafio

A especificação de consenso do Ethereum é a referência em Python que todas as implementações de cliente da camada de consenso do Ethereum devem seguir. Ela governa os processos de inclusão de nós, validação e penalização de validadores. Erros nesta especificação podem se propagar a todo cliente em conformidade e, no pior caso, levar a problemas de disponibilidade ou outras interrupções operacionais da camada de consenso.

A especificação é escrita em Python. Embora trabalhos anteriores de métodos formais tivessem mirado partes da beacon chain do Ethereum 2.0, nenhum verificador baseado em BMC para Python havia sido publicamente disponibilizado; a única ferramenta diretamente comparável (MSV) não tinha código-fonte público nem artefatos reproduzíveis. Não havia, portanto, nenhum verificador limitado de modelos pronto para uso a aplicar à base de código Python do eth2spec.

Abordagem

Nossa equipe liderou o desenvolvimento do ESBMC-Python, o primeiro verificador de código Python baseado em BMC publicamente disponível (segundo o artigo ISSTA 2024 §4). O ESBMC-Python é lançado como parte do projeto open-source ESBMC. Ele faz o parsing de Python em uma AST, realiza inferência de tipos (inserindo nós AnnAssign com informação de tipo explícita) e, então, traduz expressões e comandos Python para a representação intermediária GOTO do ESBMC, onde se aplica o pipeline existente de execução simbólica + resolução SMT. As propriedades verificadas incluem divisão por zero, estouros aritméticos e falhas de asserção.

Para aplicar o ESBMC-Python à especificação de consenso do Ethereum (eth2spec), estendemos o front-end com tipos customizados; uint64, uint128 e uint256; e verificamos cada função individualmente com entradas não determinísticas.

O bug

def integer_squareroot(n: uint64) -> uint64:
  x = n
  y = (x + 1) // 2  # ← overflows to 0 when n = 2⁶⁴ − 1
  while y < x:
    x = y                 # x becomes 0 after the overflow
    y = (x + n // x) // 2  # ← ZeroDivisionError: n // 0
  return x

# Input:  n = 2⁶⁴ − 1 (maximum uint64 value)
# Result: ZeroDivisionError, the unsigned integer overflows to 0,
#         then is used as the denominator of a division operation.
# ESBMC-Python: confirmed the bug and produced a counterexample trace.

Resultados

Referências

1. Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho, Youcheng Sun, Lucas C. Cordeiro. ESBMC-Python: A Bounded Model Checker for Python Programs. ISSTA 2024: 1836–1840. doi.org/10.1145/3650212.3685304
2. ethereum/consensus-specs PR #3600. Handle integer_squareroot bound case. Merged 15 February 2024. github.com/ethereum/consensus-specs/pull/3600