O ABC da Verificação Formal com Move

11 de janeiro de 2023

Guia de um iniciante

# Uma visão geral do teste de software [1]

Nos últimos anos, o campo da verificação formal vem ganhando força como uma forma de provar matematicamente que um sistema, como um programa de computador ou design de hardware, se comporta como pretendido. No entanto, muitas pessoas ainda acham o conceito de verificação formal intimidador e difícil de entender. Neste artigo, abordaremos os fundamentos da verificação formal usando Move, uma linguagem de programação e estrutura originalmente desenvolvida pelo Facebook para alimentar a blockchain Diem.

Tabelas de conteúdos

• Uma introdução à verificação formal;
• Uma introdução à linguagem de programação Move;
• Verificação formal com o provador Move (Move Prover);
• Resumo;
• Referências.

Uma introdução à verificação formal

A verificação formal é um método de provar matematicamente que um sistema, como um programa de computador ou design de hardware, se comporta como pretendido. Isso é realizado pela construção de um modelo formal do sistema e, então, uso do raciocínio matemático para provar que o modelo satisfaz certas propriedades. A verificação formal pode ser usada para garantir que um sistema seja livre de certos tipos de bugs e erros e pode fornecer um alto grau de confiança de que o sistema se comportará corretamente em todos os cenários possíveis.

Existem várias abordagens diferentes para a verificação formal, cada uma com seus próprios pontos fortes e fracos. Alguns dos métodos mais comuns incluem:

• Verificação do modelo (Model checking): esse método envolve a construção de um modelo formal do sistema e, em seguida, o uso de um programa de computador para explorar sistematicamente todos os estados do modelo possíveis. O programa verifica se o modelo satisfaz certas propriedades, como propriedades de segurança (por exemplo, o sistema nunca atingirá um estado inseguro) ou propriedades de vivacidade (por exemplo, o sistema eventualmente atingirá um estado desejável).
• Prova de teorema (Theorem proving): nesse método, um conjunto de provas matemáticas é construído para estabelecer que as propriedades do sistema são verdadeiras. Esta é uma abordagem mais manual, mas pode ser mais poderosa para certos tipos de sistemas, como aqueles com lógica complexa ou restrições de tempo real.
• Solução de restrições (Constraint solving): é uma técnica onde um conjunto de restrições é definido em uma linguagem matemática e o solucionador verificará se existem quaisquer valores de variáveis que satisfazem as restrições dadas.

Aplicações da verificação formal

A verificação formal é particularmente bem adequada para sistemas críticos na segurança, como aqueles usados no setor aeroespacial, de defesa e de saúde. Esses sistemas devem ser altamente confiáveis, visto que as consequências de falhas podem ser graves. A verificação formal pode também ser usada em outras indústrias, como as de finanças e telecomunicações, onde os custos dos erros ou tempo de inatividade podem ser altos.

Prós e contras da verificação formal

Uma das maiores vantagens da verificação formal é que ela pode detectar bugs e erros que podem ser difíceis ou impossíveis de encontrar através apenas de testes. Por exemplo, um sistema pode funcionar corretamente em todos os casos de teste que forem considerados, mas ainda conter erros que apenas ocorrem em certas condições raras ou difíceis de reproduzir. A verificação formal pode descobrir esses erros, permitindo que eles sejam corrigidos antes que o sistema seja implantado.

Contudo, a verificação formal pode ser um processo demorado e complexo, especialmente para sistemas grandes ou altamente complexos. Também requer um investimento significativo em conhecimento de métodos formais, bem como em ferramentas e infraestrutura para apoiar o processo de verificação.

Uma introdução à linguagem de programação Move

# Move será o JavaScript da Web3 [2]

Move é uma nova linguagem de programação originalmente desenvolvida pelo Facebook, projetada para possibilitar uma nova classe de ativos digitais seguros e programáveis. A linguagem Move é construída com base no princípio da programação orientada a recursos, que permite que os desenvolvedores criem e gerenciem ativos garantidos como únicos e não duplicáveis. Isso faz da Move bem adequada para uma ampla gama de aplicações, incluindo moedas digitais, gerenciamento de cadeia de fornecimento e verificação de identidade.

Uma das principais características da linguagem Move é seu sistema do tipo forte. A Move tem uma série de tipos embutidos, incluindo inteiros, booleanos e endereços, usados para representar ativos e outros valores. Esses tipos são projetados para ser altamente expressivos, facilitando aos desenvolvedores criar e manipular ativos de uma forma segura e previsível.

Outra característica importante da linguagem Move é seu modelo de programação orientada a recursos. Na Move, todos os ativos são representados como “recursos”, que são únicos e não duplicáveis. Isso significa que, uma vez que um ativo for criado, não pode ser copiado ou duplicado. Essa propriedade é aplicada no nível da linguagem, impossibilitando a duplicação acidental de um ativo.

Aqui está um exemplo de um programa simples da linguagem Move que cria e manipula um ativo de moeda digital:

module MyCurrency {
 // Define o recurso para a moeda.
 resource Currency {
   let balance: U64;
 }

 // Cria uma nova moeda com um saldo inicial de 100.
 public fun create_currency(): Currency {
   return Currency { balance: 100 };
 }

 // Transfere fundos de uma moeda para outra.
 public fun transfer(from: &Currency, to: &Currency, amount: U64): bool {
   if (from.balance >= amount) {
     from.balance = from.balance - amount;
     to.balance = to.balance + amount;
     return true;
   }
   return false;
 }
}

Neste exemplo, definimos um novo módulo Move chamado MyCurrency, que contém um tipo de recurso chamado Currency. O recurso Currency tem um único campo, balance, usado para armazenar o saldo da moeda. O módulo também contém duas funções: create_currency, que cria uma nova instância do recurso Currency com um saldo inicial de 100, e transfer, que permite que os fundos sejam transferidos de uma moeda para a outra.

Você pode ver na função transfer, que está usando uma proteção a nível de linguagem utilizando & antes do nome da variável, que está garantido que a função transfer não pode copiar a moeda, pode apenas se referenciar à original e realizar as mudanças necessárias. Dessa forma, você pode usar Move para criar e gerenciar ativos digitais garantidos como exclusivos e não-duplicáveis, tornando-o adequado para uma ampla variedade de aplicações.

Observe que este é apenas um exemplo introdutório, e que a linguagem Move tem características muito mais poderosas que permitem fazer coisas como criar tipos de recursos personalizados, verificação de assinatura e pagamentos de gas, para citar alguns.

Verificação formal com o Move Prover (provador Move)

O Move Prover é uma ferramenta que usa um programa e um conjunto de propriedades como entrada e, então, utiliza raciocínio matemático para provar que um programa satisfaz essas propriedades. O Move Prover pode ser usado para verificar as propriedades de um programa Move, como garantir que o programa não viole quaisquer propriedades de segurança ou correção.

Um exemplo de uso do Move Prover para verificar formalmente as propriedades de um sistema é checar se uma carteira digital implementada na linguagem Move não permite saldo negativo.

Vamos supor que definimos um tipo de recurso chamado “Balance” (saldo), que representa o saldo atual da carteira digital de um usuário. Um usuário pode depositar e retirar fundos da carteira, que atualiza o saldo conforme a movimentação. Para garantir que um usuário não pode ter um saldo negativo, podemos usar o Move Prover para provar que a operação “withdraw” (retirar) sempre verificará o saldo atual antes de permitir a retirada e não permitirá a retirada se ela resultar em um saldo negativo.

fun withdraw<CoinType>(addr: address, amount: u64) : Coin<CoinType> acquires Balance {
       let balance = balance_of<CoinType>(addr);
       assert!(balance >= amount, EINSUFFICIENT_BALANCE);
       let balance_ref = &mut borrow_global_mut<Balance<CoinType>>(addr).coin.value;
       *balance_ref = balance - amount;
       Coin<CoinType> { value: amount }
   }

Em seguida, podemos usar o Move Prover para verificar se essa operação sempre impõe a restrição de um saldo não-negativo, fornecendo uma propriedade de que o saldo deve ser não-negativo após a chamada da função de retirada. Essas restrições são chamadas de especificação em Move [3].

spec withdraw {
       let balance = global<Balance<CoinType>>(addr).coin.value;

       aborts_if !exists<Balance<CoinType>>(addr);
       aborts_if balance < amount;

       let post balance_post = global<Balance<CoinType>>(addr).coin.value;
       ensures result == Coin<CoinType> { value: amount };
       ensures balance_post == balance - amount;
   }

Com o comando a seguir, podemos executar o Prover:

move prove

# O resultado seria: 
[INFO] preparing module 0x12::Medium
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 6 verification conditions
[INFO] running solver
[INFO] 0.644s build, 0.005s trafo, 0.010s gen, 0.964s verify, total 1.624s

A arquitetura do Move Prover (por exemplo, como ele funciona)

O Move Prover é construído em cima do solucionador Z3 SMT (Satisfiability Modulo Theories - Teorias de módulo de satisfabilidade), que é uma ferramenta eficiente e largamente utilizada na verificação formal, fornecendo uma base sólida de implementação.

A arquitetura do Move Prover [4]

O Move Prover usa o código-fonte Move anotado como entrada e verifica se o código atende às especificações fornecidas. O processo envolve várias etapas, incluindo a extração das especificações, compilação do código-fonte, remoção de operações de staking e tradução do código para um programa na linguagem de verificação intermediária (IVL - intermediate verification language) Boogie. Esse programa é, em seguida, verificado pelo sistema de verificação Boogie e um solucionador (solver) SMT. Se o código atender às especificações, é relatado como tal para o usuário. No entanto, se o resultado não for satisfatório, o provador (prover) fornece um diagnóstico que o usuário pode usar para melhorar o código e repetir o processo. O Move Prover é escrito na linguagem de programação Rust e está disponível no repositório do GitHub da linguagem Move [5].

Gerando contra-exemplos

No Move Prover, um contra-exemplo é gerado quando o processo de verificação determina que o código e as especificações fornecidas não correspondem. Especificamente, quando o solucionador (solver) SMT retorna um resultado de SAT (que significa “satisfatório”), isso significa que a fórmula do SMT criada pelo sistema de verificação Boogie tem pelo menos uma solução ou um conjunto de valores para as variáveis que tornam a fórmula verdadeira. Isso representa uma violação das especificações e o contra-exemplo é um conjunto de valores que demonstram como o código se comporta de uma maneira que não corresponde às especificações.

Considere a seguinte função “add” (adicionar) simples, que passa no teste de unidade com sucesso, mas sabemos que ela pode se comportar incorretamente com argumentos de entrada específicos.

public fun add(a: u64, b: u64): u64 {
       if (a * b == 40) {
           return 0
       };
       a + b
   }

#[test]
// Este teste passa
public fun test_add() {
   assert!(add(10, 20) == 30, 0);
}

Como explicado anteriormente, podemos determinar as especificações da função e verificá-las formalmente com o Move Prover. O objetivo é garantir que a função retorna a soma das suas entradas em todos os cenários possíveis. Depois de executar o Move Prover, você notará que ele gera um contra-exemplo (neste caso, a=1, b=40) para orientar o desenvolvedor.

spec add {
       ensures result == a + b;
}

error: post-condition does not hold
  ┌─ ./sources/Medium.move:33:9
  │
33 │         ensures result == a + b;
  │         ^^^^^^^^^^^^^^^^^^^^^^^^
  │
  = Related Bindings:
  =         a = 40
  =         b = 1
  =         result = 0
  = Execution Trace:
  =     at ./sources/Medium.move:25: add
  =         a = 40
  =         b = 1
  =     at ./sources/Medium.move:26: add
  =     at ./sources/Medium.move:27: add
  =         result = 0
  =     at ./sources/Medium.move:33: add (spec)
  =         `ensures result == a + b;` = false

Error: exiting with verification errors

Conclusão

Em conclusão, a verificação formal é uma técnica poderosa para provar matematicamente que um sistema se comporta como pretendido. Esse método pode detectar bugs e erros que podem ser difíceis ou impossíveis de encontrar por meio de testes e é particularmente adequado para sistemas críticos de segurança, como os usados no setor aeroespacial, de defesa e de saúde.

Move é uma nova linguagem de programação e estrutura desenvolvida pelo Facebook, que permite uma nova classe de ativos digitais programáveis e seguros usando o princípio da programação orientada a recursos.

A verificação formal pode ser feita com o Move Prover, uma ferramenta de verificação formal para contratos inteligentes escritos em Move, que permite aos desenvolvedores provar matematicamente a correção de seus contratos e pode ser usada para verificar se a implementação de um contrato atende às propriedades desejadas, bem como provar a ausência de certos tipos de erros. O processo de verificação formal pode ser demorado e complexo, mas dá aos desenvolvedores um alto grau de confiança que o sistema se comporta corretamente em todos os possíveis cenários.

Referências

Todos os links eram válidos em 10 de janeiro de 2023.

1. https://blog.digitalasset.com/developers/what-is-formal-verification-and-what-it-means-for-daml
2. https://github.com/MystenLabs/awesome-move
3. https://github.com/move-language/move/blob/main/language/move-prover/doc/user/spec-lang.md
4. Zhong, J. E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., … & Dill, D. L. (julho de 2020). The move prover. In International Conference on Computer Aided Verification (pp. 137–150). Springer, Cham.
5. https://github.com/move-language/move/tree/main/language/move-prover

Esse artigo foi escrito por Seyyed Ali Ayati e traduzido por Isabela Curado Nehme. Seu original pode ser lido aqui.