solidity static analysis
Alpha
Análise estática para verificação de contratos inteligentes de solidez, com base em https://github.com/shaunazzopardi/solity-cfg-builder e https://github.com/gordonpace/contractLarva.
Essa ferramenta tenta provar totalmente as propriedades da Solidity Smart Contrates e, com sucesso parcial, retorna uma propriedade residual que ainda precisa ser comprovada do Solidity Smart Contract.
Utilizamos uma representação de gráfico de fluxo de controle de um contrato inteligente de solidez, na tentativa de provar propriedades de contratos inteligentes estaticamente, apropriando-se demais do fluxo de controle de um contrato inteligente de solidez (com base no Solity-CFG-Builder e em seu estado variável.
Isso é parcialmente baseado no trabalho apresentado nos procedimentos do Prepost 2017, na série EPCTS e disponível no ARXIV.
Cada função de contrato inteligente é representado como um autômato de fluxo de controle (CFA) com transições marcadas com um triplo contendo: (i) uma condição no estado variável do programa; (ii) uma declaração que transforma o estado variável do programa; e (iii) um evento imobiliário ativado na execução da declaração.
Cada um desses autômatos é aumentado com transições abstratas (marcadas apenas por um evento da propriedade) que permitem que qualquer evento ocorra durante um estado inicial, ligue ou final do programa. Isso é usado como base da análise intraprocedural. Cada um desses autômatos aborda todas as execuções do contrato inteligente que chamam a função correspondente. Este autômato é chamado de autômato de controle de controle abstrato (ACFA).
Um algoritmo simples de propagação de afirmação propaga asserções sobre o estado variável do programa (implícito por condições e declarações) através dos estados explícitos de um CFA até que as declarações que possam afetar a afirmação sejam encontradas. Isso é bom.
Uma propriedade é representada como um autômato de evento dinâmico (DEA) que usa transições marcadas com um triplo de: (i) um evento; (ii) um guarda no estado variável da propriedade; e (iii) uma ação no estado variável da propriedade.
Um ACFA com uma abstração variável é composto com DEA, produzindo um sistema monitorado abstrato (AMS) com transições marcadas com pares de transições de CFA e DEA, ou com uma das posições que contêm o símbolo #. Quando # é usado em vez de uma transição do CFA, ele sinaliza a correspondência de uma transição abstrata, enquanto quando, em vez de uma transição de DEA, sinaliza nenhuma correspondência de transição DEA.
Em seguida, um AMS é criado para cada função do programa contra a DEA fornecida.
Um solucionador SMT, Z3, é chamado on-the-fly durante a construção do AMS para determinar se é possível que a transição fornecida seja ativada naquele momento em uma execução real. Dado um par de transição CFA-DEA, verificamos se o guarda DEA pode manter o verdadeiro na abstração variável do estado de origem atualizado com a condição e a declaração da transição do CFA. Embora seja recebido um par CFA-#, verificamos se a abstração variável do estado de origem atualizada com a condição e a declaração da transição do CFA não é inconsistente com a negação da disjunção dos guardas do mesmo estado de DEA, possivelmente ativados nesse ponto) (observe que as transições de Dea de saída do mesmo DEA são avaliadas para ter mutuamente os guardas).
Cada AMS é analisado para identificar pares de transição CFA-DEA, extraindo as transições DEA usadas dessa maneira, ignorando as correspondências de transições DEA com o espaço reservado #. A união dessas transições DEA produz um resíduo da DEA original. Às vezes, isso pode ser reduzido ainda mais através da análise sintática da DEA residual.
Além disso, a partir do AMSS, podemos identificar quando a guarda de uma transição da DEA pode ser removida (ou seja, alterada para verdadeira ), ou seja, sempre que pode ser usada no AMS, ele sempre é usado.
Se o resíduo produzido não tiver transições, a propriedade foi comprovada.
Requisitos: Cabal v2.4.* (Por exemplo, instale a plataforma Full Haskell)
Compilação: Siga as instruções aqui
Para obter resultados corretos, sempre verifique se o código de solidez compila com um compilador de solidez.
Para usar a ferramenta, passe a localização do arquivo de solidez do Smart Contract, o arquivo de propriedade DEA e o local preferido da saída para o executável, por exemplo, execute:
./Main "./examples/courierservice.sol" "./examples/courierservicespec.dea" "cfa.txt" "acfa.txt" "ams.txt" "residual.dea"
Este projeto está licenciado nos termos da licença Apache 2.0.
