solidity static analysis
Alpha
Análisis estático para la verificación de los contratos inteligentes de solidez, basado en https://github.com/shaunazzopardi/solidity-cfg-builder y https://github.com/gordonpace/contractlarva.
Esta herramienta intenta probar completamente las propiedades de la solidez de los contratos inteligentes, y en el éxito parcial devuelve una propiedad residual que queda por probar del contrato inteligente de solidez.
Utilizamos una representación de gráfico de flujo de control de un contrato inteligente de solidez en un intento por probar las propiedades de los contratos inteligentes estáticamente al hacer una sobremaña sobre el flujo de control de un contrato inteligente de solidez (basado en Solity-CFG-Builder y su estado variable.
Esto se basa parcialmente en el trabajo presentado en las Actas de Prepost 2017, en la serie EPCTS y disponible en ARXIV.
Cada función de contrato inteligente se representa como un autómata de flujo de control (CFA) con transiciones etiquetadas con un triple que contiene: (i) una condición en el estado variable del programa; (ii) una declaración que transforma el estado variable del programa; y (iii) un evento de propiedad activado en la ejecución de la declaración.
Cada automatón se aumenta con transiciones abstractas (etiquetadas solo por un evento de propiedad) que permite que ocurra cualquier evento mientras esté en un estado inicial, llamado o final del programa. Esto se utiliza como base del análisis intraplacedural. Cada uno de estos autómatas hace todo lo que abarca todas las ejecuciones del contrato inteligente que llaman a la función correspondiente. Este autómata se llama Automaton de flujo de control abstracto (ACFA).
Un algoritmo de propagación de afirmación simple propaga afirmaciones sobre el estado variable del programa (implícito en condiciones y declaraciones) a través de los estados explícitos de un CFA hasta que se encuentran declaraciones que pueden afectar la afirmación. Esto es sonido.
Una propiedad se representa como un automatón de evento dinámico (DEA) que utiliza transiciones etiquetadas con un triple de: (i) un evento; (ii) una guardia en el estado variable de propiedad; y (iii) una acción sobre el estado variable de propiedad.
Una ACFA con una abstracción variable se compone con DEA, que produce un sistema monitoreado abstracto (AMS) con transiciones etiquetadas con pares de transiciones CFA y DEA, o con una de las posiciones que contienen el símbolo #. Cuando se usa # en lugar de una transición de CFA, señala la coincidencia de una transición abstracta, mientras que cuando en lugar de una transición de la DEA indica que no hay coincidencia de transición de DEA.
Luego, se crea un AMS para cada función del programa contra la DEA dada.
Un solucionador SMT, Z3, se llama sobre la marcha durante la construcción del AMS para determinar si es posible que las transiciones dadas se activen en ese momento en una ejecución real. Dado un par de transición CFA-DEA, verificamos que la Guardia DEA pueda ser válida en la abstracción variable del estado de origen actualizado con la condición y la declaración de la transición CFA. Si bien dado un par CFA# verificamos que la abstracción variable del estado de origen actualizado con la condición y la declaración de la transición de CFA no es inconsistente con la negación de la disyunción de los guardias de las transiciones de la DEA posiblemente activadas en este punto (tenga en cuenta que las transiciones de la DEA salen de los mismos estados de la DEA tienen que tener argumentos mutuamente excluidos).
Cada AMS se analiza para identificar pares de transición CFA-DEA, extrayendo las transiciones DEA utilizadas de esta manera, ignorando las coincidencias de transiciones DEA con el marcador de posición #. La unión de estas transiciones de la DEA produce un residuo de la DEA original. Esto a veces se puede reducir aún más a través del análisis sintático de la DEA residual.
Además, del AMSS podemos identificar cuándo se puede eliminar la guardia de una transición de la DEA (es decir, cambiar a verdadero ), es decir, siempre que se pueda usar en el AMS, siempre se usa.
Si el residual producido no tiene transiciones, entonces la propiedad ha sido probada.
Requisitos: Cabal v2.4.* (Por ejemplo, instale la plataforma Haskell completa)
Compilación: siga las instrucciones aquí
Para obtener resultados correctos, siempre asegúrese de que el código de solidez se compile con un compilador de solidez.
Para usar la herramienta, pase la ubicación del archivo de solidez de contrato inteligente, el archivo de propiedades de la DEA y la ubicación preferida de la salida al ejecutable, por ejemplo, ejecutar:
./Main "./examples/courierservice.sol" "./examples/courierservicespec.dea" "cfa.txt" "acfa.txt" "ams.txt" "residual.dea"
Este proyecto tiene licencia bajo los términos de la licencia Apache 2.0.
