Input Output demonstra o Blaster para verificação de contratos inteligentes da Cardano

Cardano Community publicou uma apresentação do Blaster, uma ferramenta de verificação automatizada concebida para verificar se os contratos inteligentes da Cardano seguem as regras especificadas. Os engenheiros da Input Output Romain Soulat e Jean-Frédéric Etienne demonstram como a ferramenta examina essas propriedades e pode produzir um contraexemplo quando encontra uma violação. Eles também discutem o trabalho em andamento sobre reconstrução de provas e formas de tornar os resultados mais fáceis de inspecionar.

Definindo o que um contrato da Cardano deve fazer

Contratos inteligentes estabelecem condições para transações em blockchain e determinam como os aplicativos lidam com ativos. Um desenvolvedor pode especificar, por exemplo, que apenas um usuário autorizado pode desbloquear fundos mantidos por um contrato. Verificação formal usa métodos matemáticos para verificar se um sistema satisfaz propriedades escritas em uma especificação. Enquanto um teste convencional examina casos selecionados, a verificação formal busca estabelecer se uma propriedade declarada se mantém nos casos cobertos pelo modelo.

Soulat, líder técnico de Cardano High Assurance, explicou que o Blaster tem como objetivo automatizar grande parte do trabalho de prova. Desenvolvedores ainda precisam definir o comportamento que desejam verificar e fornecer a especificação correspondente. Quando a ferramenta encontra uma violação, ela pode produzir um contraexemplo para inspeção. Soulat descreveu uma transação ou sequência de transações que poderia mostrar alguém que não o usuário autorizado desbloqueando uma saída.

Como o Blaster verifica propriedades de contratos

O Blaster usa Lean 4, um sistema para expressar declarações matemáticas e trabalhar com provas, juntamente com um solucionador automatizado. Primeiro ele simplifica o problema; se a propriedade não for resolvida nessa fase, o problema restante pode ser enviado ao solucionador. Para tornar as verificações relevantes para a Cardano, a equipe formalizou partes do ambiente em que os contratos são executados, incluindo execução de scripts e regras de transações.

Etienne, engenheiro sênior de métodos formais, apresentou três resultados possíveis: uma propriedade pode ser relatada como válida, refutada ou indeterminada. Um contraexemplo associado a um resultado refutado pode ajudar desenvolvedores a identificar uma falha no contrato, uma suposição ausente ou um erro na especificação. Um resultado indeterminado significa que o solucionador não estabeleceu se a propriedade se mantém. O escopo de uma verificação depende das propriedades que os desenvolvedores escolhem expressar.

[NEWSBREAK]

A reconstrução de provas está em desenvolvimento

Desenvolvedores podem compilar contratos escritos em linguagens como Plinth, Aiken ou Plutarch para Untyped Plutus Core, a representação usada para executar scripts da Cardano. Eles podem então importar o código compilado no Lean 4 e especificar as propriedades a serem verificadas. A Input Output anteriormente lançou duas bibliotecas de código aberto que fornecem os modelos específicos da Cardano para esse processo. Em uma demonstração anterior, a equipe usou o pipeline em um contrato de prática de um desafio de segurança, gerando um contexto de transação que mostrou como o contrato poderia ser explorado.

Etienne explicou que a reconstrução de provas ainda está em desenvolvimento. O objetivo é permitir que o Lean verifique de forma independente as evidências que sustentam um resultado válido; a ferramenta atual ainda não produz uma prova reconstruída em Lean quando o solucionador retorna esse resultado. Soulat também delineou planos para visualizações de contraexemplos mais claras, permitindo que os desenvolvedores inspecionem os detalhes da transação por trás de uma propriedade que falhou.