Advertencia
Este artículo no es una calificación de la efectividad de los analizadores automáticos. Los aplico a mis propios contratos, sintetizando errores intencionalmente, y estudio las reacciones. Tal estudio no puede ser la base para determinar "mejor-peor", para esto tiene sentido realizar un estudio ciego en una gran muestra de contratos, que, dada la naturaleza caprichosa de este tipo de software, es extremadamente difícil de realizar. Es muy posible que un pequeño error en el contrato pueda deshabilitar una gran parte de la lógica del analizador, y un simple signo heurístico puede agregar una enorme cantidad de puntos al analizador al encontrar un error generalizado que los competidores simplemente no lograron agregar. Los errores en la preparación y compilación de contratos también pueden desempeñar un papel. Todo el software en cuestión es bastante joven y se está desarrollando constantemente, por lo que no tome los comentarios críticos como problemas irreparables.
El propósito del artículo es dar al lector una comprensión de cómo funcionan los métodos de análisis de código en diferentes analizadores y la capacidad de usarlos correctamente, en lugar de "tomar una decisión". Una opción razonable es utilizar varias herramientas a la vez, centrándose en la más adecuada para el contrato analizado.
Configuración y preparación para el lanzamiento.
Mythril utiliza varios tipos de análisis a la vez, aquí hay un par de buenos artículos al respecto: el más importante , esto o esto . Antes de continuar, tiene sentido leerlos.
Primero, construyamos nuestra propia imagen Docker de Mythril (¿no importa lo que queramos cambiar en ella?):
git clone https://github.com/ConsenSys/mythril-classic.git cd mythril-classic docker build -t myth .
Ahora intente ejecutarlo en nuestros contracts/flattened.sol (uso el mismo contrato que se discutió en la introducción ), en el que hay dos contratos principales, Ownable de Zeppelin y nuestra Booking . Todavía tenemos un problema con la versión del compilador, lo arreglé de la misma manera que en el artículo anterior, agregando líneas al Dockerfile que reemplazará la versión del compilador:
COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin
Después de reconstruir la imagen, puede intentar ejecutar un análisis de contrato. Inmediatamente usemos los indicadores -v4 y --verbose-report para ver todas las advertencias. Vamos:
docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ -v4 \ --verbose-report \ -x contracts/flattened.sol
Aquí trabajamos con un contrato aplanado sin dependencias. Para analizar un contrato de Booking.sol separado y hacer que Mythril recoja todas las dependencias, puede usar algo como esto:
docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ --solc-args="--allow-paths /tmp/node_modules/zeppelin-solidity/ zeppelin-solidity=/tmp/node_modules/zeppelin-solidity" \ -v4 \ --verbose-report \ -x contracts/Booking.sol
Prefiero trabajar con la opción aplanada, como modificaremos mucho en el código. Pero Mythril también tiene un modo extremadamente conveniente: la --truffle , que simplemente --truffle todo lo que truffle y verifica la vulnerabilidad de todo el proyecto. Otra característica importante es la capacidad de especificar el nombre del contrato que se analizará a través de dos puntos, de lo contrario Mythril analizará todos los contratos que encuentre. Creemos que Ownable 's Ownable es un contrato seguro, y solo vamos a analizar Booking , por lo que la línea final para ejecutar es:
docker run -v $(pwd):/tmp -w /tmp myth:latest -x contracts/flattened.sol:Booking -v4 --verbose-report
Iniciar y desplegar contrato
Iniciamos el analizador con la línea anterior, miramos la salida y obtenemos, entre otras cosas, esta línea:
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) The analysis was completed successfully. No issues were detected.
Resulta que nuestro contrato no fue creado y "arreglado" en el emulador. Es por eso que recomiendo usar el indicador -v4 para todos los tipos de análisis para ver todos los mensajes y no perder ninguno. Veamos qué pasa. La solución a este problema práctico es bastante importante para comprender cómo usar Mythril correctamente.
Entonces, estamos leyendo sobre Mythril: It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities . Si no está muy familiarizado con estos términos, le recomiendo el wiki sobre pruebas concólicas aquí , pero aquí hay una buena presentación sobre la comprobación de manchas para x86. En resumen: Mythril emula la ejecución de un contrato, arregla las ramas a lo largo de las cuales puede ir la ejecución e intenta alcanzar un estado "roto" del contrato, clasificando varias combinaciones de parámetros e intentando sortear todas las rutas posibles. Aquí hay un diagrama de acción de muestra del artículo anterior:
1. . symbolic-, . 2. , , trace . , , . 3. . 4. trace-. 5. symbolic execution trace, symbolic , , , . 6. , . , . 7. : , , input-, , . input- , .6 . 8. .4
Si lo simplifica enormemente, Mythril, después de haber encontrado una rama en el código, puede entender bajo qué conjuntos de variables es posible ingresar en una y otra rama. En cada rama, Mythril sabe si conduce a la selfdestruct transfer , selfdestruct y otros selfdestruct relevantes para la seguridad. Por lo tanto, Mythril analiza qué conjuntos de parámetros y transacciones pueden conducir a una violación de seguridad. Y la forma en que Mythril corta ramas que nunca obtienen control y analiza el flujo de control es su truco principal. Aquí encontrará más detalles sobre el intestino Mythril y el andar de ramas.
Debido a la naturaleza determinista de la ejecución de contratos inteligentes, la misma secuencia de instrucciones siempre conduce estrictamente a un conjunto de cambios de estado, independientemente de la plataforma, la arquitectura o el entorno. Además, las funciones en los contratos inteligentes son bastante cortas y los recursos son extremadamente limitados, por lo tanto, los analizadores como Mythril, que combinan la ejecución simbólica y nativa, pueden funcionar de manera extremadamente eficiente para los contratos inteligentes.
En el proceso, Mythril utiliza el concepto de "estado": este es el código del contrato, su entorno, un puntero al comando actual, el almacenamiento del contrato y el estado de la pila. Aquí está la documentación:
The machine state μ is defined as the tuple (g, pc, m, i, s) which are the gas available, the program counter pc ∈ P256, the memory contents, the active number of words in memory (counting continuously from position 0), and the stack contents. The memory contents μm are a series of zeroes of size 256.
El gráfico de transición entre estados es el principal objeto de estudio. En caso de lanzamiento exitoso del análisis, la información sobre este gráfico se muestra en el registro de análisis. Además, Mythril puede construir este gráfico en una forma legible por humanos usando la opción --graph .
Ahora, más o menos entendiendo lo que hará Mythril, seguiremos entendiendo por qué el contrato no se analiza y de dónde proviene [WARNING]: No contract was created during the execution of contract creation . Para comenzar, --max-depth --create-timeout y --max-depth (como se recomienda) y, al no obtener el resultado, pensé que el culpable era el constructor, algo que no funcionaba. Aquí está su código:
function Booking( string _description, string _fileUrl, bytes32 _fileHash, uint256 _price, uint256 _cancellationFee, uint256 _rentDateStart, uint256 _rentDateEnd, uint256 _noCancelPeriod, uint256 _acceptObjectPeriod ) public payable { require(_price > 0); require(_price > _cancellationFee); require(_rentDateStart > getCurrentTime()); require(_rentDateEnd > _rentDateStart); require(_rentDateStart+_acceptObjectPeriod < _rentDateEnd); require(_rentDateStart > _noCancelPeriod); m_description = _description; m_fileUrl = _fileUrl; m_fileHash = _fileHash; m_price = _price; m_cancellationFee = _cancellationFee; m_rentDateStart = _rentDateStart; m_rentDateEnd = _rentDateEnd; m_noCancelPeriod = _noCancelPeriod; m_acceptObjectPeriod = _acceptObjectPeriod; }
Recordemos el algoritmo de acción de Mythril. Para ejecutar el seguimiento, debe llamar al constructor del contrato, porque toda la ejecución posterior dependerá de los parámetros con los que se llamó al constructor. Por ejemplo, si llama al constructor con _price == 0 , el constructor lanzará una excepción en require(_price > 0) . Incluso si Mythril itera sobre los muchos valores de _price , el constructor aún se romperá si, por ejemplo, _price <= _cancellationFee . En este contrato, hay una docena de parámetros asociados con restricciones estrictas, y Mythril, por supuesto, no puede adivinar las combinaciones válidas de parámetros. Intenta pasar a la siguiente rama de ejecución, clasificando los parámetros del constructor, pero prácticamente no tiene ninguna posibilidad de adivinar: hay demasiadas combinaciones de parámetros. Por lo tanto, el cálculo del contrato no funciona: todas las formas se basan en algún tipo de require(...) , y obtenemos el problema anterior.
Ahora tenemos dos formas: la primera es deshabilitar todos los require en el constructor al comentarlos. Entonces Mythril podrá llamar al constructor con cualquier conjunto de parámetros y todo funcionará. Pero esto significa que al examinar un contrato con tales parámetros, Mythril encontrará errores que son posibles con valores incorrectos pasados al constructor. En pocas palabras, si Mythril encuentra un error que surge si el creador del contrato especifica _cancellationFee mil millones de veces el precio de alquiler de _mprice , entonces no hay uso en dicho error: dicho contrato nunca se bloqueará y se _mprice recursos para encontrar errores. Implicamos que el contrato todavía está atascado con parámetros más o menos consistentes, por lo que para un análisis posterior tiene sentido especificar parámetros de constructor más realistas para que Mythril no busque errores que nunca ocurrirán si el contrato se cierra correctamente.
Pasé muchas horas tratando de entender exactamente dónde se rompe el despliegue, incluyendo e inhabilitando varias partes del constructor. Además de mis problemas, el constructor usa getCurrentTime() , que devuelve la hora actual, y no está claro cómo maneja esta llamada Mythril. No describiré estas aventuras aquí, porque Lo más probable es que con el uso regular, estas sutilezas sean conocidas por el auditor. Por lo tanto, elegí la segunda forma: para limitar los datos de entrada, y simplemente getCurrentTime() todos los parámetros del constructor, incluso getCurrentTime() , simplemente codifiqué los parámetros necesarios directamente en el constructor (idealmente, estos parámetros deben obtenerse del cliente):
function Booking( ) public payable { m_description = "My very long booking text about hotel and beautiful sea view!"; m_fileUrl = "https://ether-airbnb.bam/some-url/"; m_fileHash = 0x1628f3170cc16d40aad2e8fa1ab084f542fcb12e75ce1add62891dd75ba1ffd7; m_price = 1000000000000000000; // 1 ETH m_cancellationFee = 100000000000000000; // 0.1 ETH m_rentDateStart = 1550664800 + 3600 * 24; // current time + 1 day m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // current time + 4 days m_acceptObjectPeriod = 3600 * 8; // 8 hours m_noCancelPeriod = 3600 * 24; // 1 day require(m_price > 0); require(m_price > m_cancellationFee); require(m_rentDateStart > 1550664800); require(m_rentDateEnd > m_rentDateStart); require((m_rentDateStart + m_acceptObjectPeriod) < m_rentDateEnd); require(m_rentDateStart > m_noCancelPeriod); }
Además, para que todo comience, también debe establecer el parámetro de max-depth . Me funcionó con este constructor con --max-depth=34 en la instancia de AWS t2.medium. Al mismo tiempo, en mi computadora portátil, que es más potente, todo comienza sin ninguna max-depth . A juzgar por el uso de este parámetro , es necesario construir ramas para el análisis, y su valor predeterminado es infinito ( código ). Por lo tanto, gire este parámetro, pero asegúrese de analizar el contrato deseado. Puedes entender esto por mensajes como:
mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: .............
La primera línea solo describe el gráfico que se analizará, lea el resto de las líneas usted mismo. Se requieren recursos computacionales serios para analizar las diversas ramas que se pueden ejecutar, por lo que al analizar contratos grandes, tendrá que esperar incluso en una computadora rápida.
Buscar errores
Ahora buscaremos errores y agregaremos los nuestros. Mythril busca sucursales en las que se realizan transmisiones, autodestrucciones, afirmaciones y otras acciones que son importantes desde el punto de vista de la seguridad. Si una de las instrucciones anteriores aparece en algún lugar del código del contrato, Mythril examina las formas en que es posible llegar a esta sucursal y, además, muestra la secuencia de transacciones que conducen a esta sucursal.
Primero, veamos qué emitió Mythril para el prolongado contrato de Booking . Primera advertencia:
==== Dependence on predictable environment variable ==== SWC ID: 116 Severity: Low Contract: Booking Function name: fallback PC address: 566 Estimated Gas Usage: 17908 - 61696 Sending of Ether depends on a predictable variable. The contract sends Ether depending on the values of the following variables: - block.timestamp Note that the values of variables like coinbase, gaslimit, block number and timestamp are predictable and/or can be manipulated by a malicious miner. Don't use them for random number generation or to make critical decisions. -------------------- In file: contracts/flattened.sol:142 msg.sender.transfer(msg.value-m_price)
y surge porque
require(m_rentDateStart > getCurrentTime());
en la función de reserva.
Tenga en cuenta que Mythril se dio cuenta de que getCurrentTime() oculta en getCurrentTime() . A pesar del hecho de que el significado del contrato no es un error, el hecho de que Mythril asocie block.timestamp con la transmisión es excelente. En este caso, el programador debe comprender que la decisión se toma sobre la base del valor que el minero puede controlar. Y, si en el futuro surge una subasta u otra subasta para un servicio en este lugar del contrato, se debe tener en cuenta la posibilidad de ataques de primera línea.
Veamos si Mythril ve una dependencia en block.timestamp si block.timestamp la variable en una llamada anidada como esta:
function getCurrentTime() public view returns (uint256) { - return now; + return getCurrentTimeInner(); } + function getCurrentTimeInner() internal returns (uint256) { + return now; + }
Y si! Mythril continúa viendo la conexión entre block.timestamp y la transferencia de transmisión, esto es extremadamente importante para el auditor. La conexión entre la variable controlada por el atacante y la decisión tomada después de varios cambios en el estado del contrato puede estar muy enmascarada por la lógica, y Mythril le permite rastrearla. Aunque no vale la pena confiar en el hecho de que todas las conexiones posibles entre todas las variables posibles serán getCurrentTime() por usted: si continúa burlándose de la función getCurrentTime() y realiza una triple profundidad de anidación, la advertencia desaparece. Cada llamada a funciones para Mythril requiere la creación de nuevas ramas estatales, por lo que analizar niveles muy profundos de anidamiento requerirá enormes recursos.
Existe, por supuesto, una posibilidad bastante seria de que simplemente use incorrectamente los parámetros de análisis o que el corte ocurra en algún lugar en las profundidades del analizador. Como dije, el producto está en desarrollo activo, justo en el momento de escribir esto, veo compromisos en el repositorio con la mención de max-depth , por lo que no tome en serio los problemas actuales, ya hemos encontrado suficiente evidencia de que Mythril puede buscar muy efectivamente conexiones implícitas entre variables
Primero, agregue al contrato una función que proporcione la transmisión a cualquier persona, pero solo después de que el cliente envíe la transmisión al contrato. Permitimos que cualquiera recoja 1/5 del éter, pero solo cuando el contrato está en estado State.PAID Estado State.PAID (es decir, solo después de que el cliente haya pagado el número alquilado con el éter). Aquí está la función:
function collectTaxes() external onlyState(State.PAID) { msg.sender.transfer(address(this).balance / 5); }
Mythril encontró el problema:
==== Unprotected Ether Withdrawal ==== SWC ID: 105 Severity: High Contract: Booking Function name: collectTaxes() PC address: 2492 Estimated Gas Usage: 2135 - 2746 Anyone can withdraw ETH from the contract account. Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent a equivalent amount of ETH to it. This is likely to be a vulnerability. -------------------- In file: contracts/flattened.sol:149 msg.sender.transfer(address(this).balance / 5) -------------------- -------------------- Transaction Sequence: { "2": { "calldata": "0x", "call_value": "0xde0b6b3a7640000", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" }, "3": { "calldata": "0x01b613a5", "call_value": "0x0", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" } }
Genial, es decir Mythril incluso sacó dos transacciones, lo que lleva al hecho de que puede tomar éter del contrato. Ahora cambie el requisito State.RENT a State.RENT , así:
- function collectTaxes() external onlyState(State.PAID){ + function collectTaxes() external onlyState(State.RENT) {
Ahora se puede llamar a collectTaxes() solo cuando el contrato está en el State.RENT state, y en este momento no hay nada en el saldo, porque El contrato ya ha enviado toda la transmisión al propietario. ¡Y lo importante aquí es que Mythril esta vez NO genera el error ==== Unprotected Ether Withdrawal ==== ! Bajo la condición onlyState(State.RENT) , el analizador no llegó a la rama de código que envía el éter del contrato con un saldo distinto de cero. Mythril pasó por diferentes opciones para los parámetros, pero puede ingresar a State.RENT solo enviando toda la transmisión al arrendador. Por lo tanto, es imposible llegar a esta rama del código con un saldo distinto de cero, ¡y Mythril no molesta absolutamente al auditor!
Del mismo modo, Mythril encontrará selfdestruct y selfdestruct , mostrando al auditor qué acciones pueden conducir a la destrucción del contrato o al colapso de una función importante. No daré estos ejemplos, solo trato de hacer una función similar a la anterior, solo llamando a selfdestruct , y selfdestruct su lógica.
Además, no olvide que una de las partes de Mythril es la ejecución simbólica, y este enfoque, por sí solo, sin emular la ejecución, puede determinar muchas vulnerabilidades. Por ejemplo, cualquier uso de "+", "-" y otros operadores aritméticos puede considerarse una vulnerabilidad de "Desbordamiento de enteros" si el atacante controla de alguna manera uno de los operandos. Pero repito nuevamente, la característica más poderosa de Mythril es la combinación de ejecución simbólica y nativa y la determinación de valores de parámetros que conducen a la ramificación lógica.
Conclusión
Por supuesto, para mostrar la gama completa de problemas potenciales que Mythril es capaz de detectar, se necesitarán no solo uno, sino varios artículos. Para todo lo demás, sabe cómo hacerlo todo en una cadena de bloques real, encontrando los contratos y vulnerabilidades necesarios mediante firmas, creando hermosos gráficos de llamadas, formateando informes. Mythril también le permite escribir sus propios scripts de prueba, proporcionando una interfaz basada en python para el contrato y permitiéndole probar funciones individuales, corregir valores de parámetros o incluso implementar su propia estrategia para trabajar con código desmontado con un grado arbitrario de flexibilidad.
Mythril sigue siendo un software bastante joven, este no es IDA Pro, y hay muy poca documentación, excepto algunos artículos. El valor de muchos parámetros solo se puede leer en el código Mythril, comenzando con cli.py. Espero que en la documentación aparezca una descripción completa y detallada del funcionamiento de cada parámetro.
Además, cuando el contrato es más o menos grande, la producción de un montón de errores ocupa mucho espacio, pero me gustaría poder recibir información comprimida sobre el error encontrado, porque cuando trabaje con Mythril, definitivamente debe mirar la ruta de análisis, ver qué contratos han sido probados de la mejor manera posible y ser capaz de desactivar por la fuerza errores específicos que el auditor considera falsos positivos.
Pero en general, Mythril es una herramienta excelente y extremadamente poderosa para analizar contratos inteligentes y, por el momento, debe estar en el arsenal de cualquier auditor. Le permite al menos prestar atención a las partes críticas del código y detectar relaciones ocultas entre variables.
Para resumir, las recomendaciones para usar Mythril son:
- Limite las condiciones de inicio del contrato en estudio tanto como sea posible. Si durante el análisis Mythril gastará muchos recursos en sucursales que nunca se implementarán en la práctica, perderá la capacidad de encontrar errores realmente importantes, por lo que siempre debe tratar de reducir el área de sucursales potenciales.
- Asegúrese de que el análisis del contrato ha comenzado, no se pierda mensajes como
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) , de lo contrario puede considerar erróneamente que no hay errores. - Puede deshabilitar arbitrariamente las sucursales en el código del contrato, dando a Mythril menos variación en la elección de sucursales y el ahorro de recursos. Intente hacerlo sin restricciones en
max-depth , para no "cortar" el análisis, pero tenga cuidado de no enmascarar el error. - Preste atención a cada advertencia, incluso los comentarios ligeros a veces valen la pena al menos agregar un comentario al código del contrato, lo que facilita a otros desarrolladores.
En el próximo artículo, trataremos el analizador Manticore, pero aquí está la tabla de contenido para los artículos que están listos o planeados para su escritura:
Parte 1. Introducción. Compilación, aplanamiento, versiones de Solidity
Parte 2. Slither
Parte 3. Mythril (este artículo)
Parte 4. Manticore (durante la escritura)
Parte 5. Echidna (durante la escritura)