Decidibilidad
¿Qué significa que un lenguaje sea no Turing completo o decidible?
No Turing completo y decidible son dos términos que escucharás a menudo sobre las ventajas de seguridad de Clarity, pero ¿qué significan?
Aunque están relacionados, no son exactamente intercambiables, ya que hay algunas diferencias.
No Turing completo
Un sistema o lenguaje es no Turing completo si no puede simular una máquina de Turing, que es un modelo abstracto de computación. Los sistemas no Turing completos tienen un poder computacional limitado en comparación con los sistemas Turing completos. Un sistema o lenguaje Turing-completo puede simular cualquier máquina de Turing. Ejemplos de sistemas no Turing completos incluyen máquinas de estados finitos y algunos lenguajes específicos de dominio (como Clarity).
Los lenguajes no Turing completos típicamente no pueden expresar todos los algoritmos posibles. Específicamente, algunos problemas cuyas soluciones requieren bucles o recursión no acotados no pueden expresarse usando lenguajes no Turing completos. Esta última propiedad es especialmente importante en el contexto de Clarity, ya que hace que características como bucles no acotados y reentrancia estén prohibidas a nivel de lenguaje.
Decidible
Un problema es decidible si existe un algoritmo que siempre puede determinar si una entrada dada tiene una propiedad particular o no en una cantidad finita de tiempo. En otras palabras, un problema decidible puede ser resuelto por una máquina de Turing que está garantizada a detenerse para todas las instancias de entrada. La decidibilidad es una propiedad de los problemas, mientras que la completitud de Turing es una propiedad de los lenguajes o sistemas computacionales.
El hecho de que Clarity sea decidible significa que los desarrolladores (y las herramientas) pueden razonar más fácilmente y predecir con certeza el comportamiento de los contratos Clarity, independientemente de la entrada.
Mentalidad de un desarrollador de contratos inteligentes
Antes de profundizar en detalles, primero establezcamos el contexto y el punto de vista que debemos tener como desarrolladores de contratos inteligentes que desean escribir código seguro.
A medida que explores más las propiedades de seguridad de Solidity y Clarity, verás que siempre hay pasos de mitigación que pueden ser tomados por los desarrolladores para ayudar a abordar algunos de estos problemas de seguridad.
El problema principal, con esta línea de pensamiento, es que aumenta las probabilidades de error humano en la seguridad de los contratos inteligentes. Si podemos preservar la funcionalidad mientras mitigamos la posibilidad de error humano tanto como sea posible, debemos hacerlo.
¿Deben los contratos inteligentes ser Turing completos?
Descubriremos nuevas aplicaciones para los contratos inteligentes. Estas aplicaciones irán más allá de los contratos inteligentes actuales, los contratos tradicionales e incluso pueden abrir nuevas oportunidades económicas. Dadas estas posibilidades, ¿cómo deberíamos construir nuestros contratos inteligentes? ¿Qué características deberían tener nuestros lenguajes de contratos inteligentes?
Es buena práctica separar los datos de los programas. ¿Deben los contratos inteligentes ser datos, o programas, o algo intermedio? Si los contratos inteligentes son datos, ¿deberían los programas que los ejecutan ser Turing completos o quizás menos potentes? Si los contratos inteligentes son programas, ¿en qué lenguaje deberían escribirse? ¿Qué características debería tener este lenguaje de programación?
La tesis de Church–Turing es la hipótesis de que todas las nociones formales de computación están capturadas por las máquinas de Turing o por las computadoras modernas. Un lenguaje de programación es Turing completo si captura todas las nociones formales de computación. Muchos lenguajes de programación son Turing completos. Por ejemplo, Python, C++, Rust, Java, Lisp y Solidity son todos Turing completos.
Considera un programa y su entrada. En el peor de los casos, determinar la salida de este programa es imposible. Validar un programa, en una entrada particular, se hace generando una prueba de corrección.
Las pruebas de corrección son pruebas lógicas que pueden ser validadas mecánicamente. Encontrar pruebas de corrección para programas y sus entradas es indecidible. Kurt Gödel mostró que existen enunciados lógicos indecidibles.
Esto indica que todos los programas en lenguajes Turing completos no pueden ser validados en el peor de los casos. Por lo tanto, los lenguajes de contratos inteligentes Turing completos deben permitir contratos que no pueden ser validados.
Alonzo Church y Alan Turing demostraron que existen problemas que son no computables. Los problemas no computables no pueden ser resueltos por ninguna máquina de Turing. Por lo tanto, asumiendo la tesis de Church–Turing, estos problemas no computables no pueden ser resueltos por ninguna computadora.
Exploraremos esta idea más a fondo más adelante en esta sección.
Los lenguajes Turing completos son muy expresivos. De hecho, asumiendo la tesis de Church–Turing, los lenguajes Turing completos son, en cierto sentido, tan expresivos como sea posible.
¿Existe una compensación? ¿Qué tipos de problemas pueden ocurrir con problemas no computables y programas cuya validez puede ser indecidible?
A medida que los contratos inteligentes abarcan partes del derecho contractual, considera el gran cuerpo de leyes y regulaciones del derecho tributario.
Por ejemplo, la legislación y las regulaciones fiscales de EE. UU. ocupan varios millones de palabras. La legislación y las regulaciones fiscales internacionales elevan mucho más estas cifras.
¿Son estas leyes y regulaciones programas o son datos? Si la legislación fiscal se escribiera en un lenguaje Turing completo, la ley podría codificar problemas no computables. Es la pesadilla de un contable que su asesoramiento sea indecidible.
Clarity no es Turing completo, pero es muy expresivo. Esto hace que Clarity sea decidible y no pueda codificar problemas no computables. Hay discusiones y artículos sobre lenguajes de contratos inteligentes como Solidity que proponen subconjuntos de Solidity que no son Turing completos. Estos subconjuntos son decidibles y no pueden codificar problemas no computables. Sin embargo, no hay consenso sobre con qué subconjuntos trabajar y no se usan ampliamente.
Ventajas de la decidibilidad en los contratos inteligentes
¿Por qué es importante la decidibilidad en el contexto de los contratos inteligentes?
Primero, no es posible que una llamada de Clarity se quede sin gas en medio de una llamada. Debido a su decidibilidad, es posible obtener un análisis estático completo del grafo de llamadas para obtener una imagen precisa del coste antes de la ejecución.
Solidity permite bucles no acotados, recursión y llamadas dinámicas a funciones, lo que dificulta predecir con precisión el coste de ejecución o el uso de gas de antemano. Como resultado, los contratos en Solidity pueden quedarse sin gas durante la ejecución si el límite de gas no se establece adecuadamente o si el contrato encuentra un escenario con requisitos computacionales inesperadamente altos.
Un ejemplo práctico es el problema de un tipo específico de ataque de DoS en Solidity, donde el contrato queda inoperable debido a restricciones de ejecución no acotadas. Un ejemplo de esto es el ataque GovernMental, donde un mapping que debía eliminarse para un pago se volvió tan grande que trabajar con él superó el límite de gas por bloque.
Hay varias propiedades diferentes del diseño del lenguaje de Clarity que previenen tales ataques de DoS.
La razón por la que el sistema de análisis puede estimar con precisión el coste de ejecución es porque cierta funcionalidad está intencionalmente limitada en Clarity.
Por ejemplo, no existe recursión en Clarity, por lo que no podemos llamar infinitamente a una función una y otra vez.
Los tipos de datos en Clarity también están restringidos. Cualquier tipo de dato que no requiera un límite de longitud estricto no es iterable.
Los mapas y las tuplas, por ejemplo, no requieren que indiques una longitud máxima al definirlos, pero tampoco puedes iterar sobre ellos.
Las listas, por otro lado, que son iterables, requieren que el desarrollador defina un límite superior al definirlas. Esto es gran parte de lo que permite un análisis estático preciso de los contratos Clarity.
Entonces, ¿cómo implementaríamos un mapping de tamaño indefinido en Clarity? No lo haríamos, porque es un antipatrón en el diseño de contratos inteligentes.
En su lugar, Clarity nos obliga a pensar en una mejor solución para nuestro problema. Por ejemplo, implementar una forma para que los usuarios manejen las operaciones de elementos de mappings/listas ellos mismos, en lugar de operaciones masivas manejadas a nivel del contrato.
Si tú analizas el ataque GovernMental, verás que se aprovechó de múltiples problemas de seguridad, todos los cuales están mitigados en Clarity. También verás que se añadió una corrección para que sea económicamente inviable llevar a cabo este tipo de ataque nuevamente.
Esto plantea otro punto crucial al establecer modelos mentales apropiados para contratos inteligentes y sistemas blockchain: la complejidad significa más errores potenciales, lo que implica añadir más complejidad para abordar esos errores.
Cuando esto sucede una y otra vez, nos atrapamos en crear un sistema cada vez más complejo. Abordar estos problemas a nivel de lenguaje previene esta complejidad en constante crecimiento.
Para profundizar en cómo se diseñó Clarity, consulta SIP-002.
Puedes ver algunas vulnerabilidades comunes de contratos inteligentes y cómo se mitigan en este artículo.
Esto tiene efectos de segundo orden también cuando analizamos las pruebas de seguridad y las auditorías. Una de las herramientas comunes para probar contratos inteligentes es la verificación formal, donde demostramos matemáticamente que ciertas propiedades de los contratos inteligentes serán o no serán verdaderas en todos los casos.
Esto puede llevar al problema de explosión de caminos, donde hay tantos caminos disponibles que la verificación formal se vuelve increíblemente difícil. Este problema se mitiga en Clarity, ya que no existe la posibilidad de que un programa encuentre un bucle no acotado.
Esto nos lleva a un modelo mental más general para pensar sobre la decidibilidad a medida que los contratos inteligentes continúan convirtiéndose en una parte más grande de nuestra economía. Recuerda que el objetivo con los sistemas blockchain es crear un sistema financiero abierto, transparente y justo.
Esto significa que los contratos inteligentes serán responsables de gestionar grandes cantidades de riqueza para cantidades crecientes de personas. A medida que los contratos inteligentes abarcan más estructuras financieras, su complejidad y uso crecerán.
La complejidad es el enemigo de la seguridad. Cuanto más complejo es un sistema, mayor es el peligro de crear problemas no computables cuando no existen restricciones estrictas sobre los pasos de ejecución que se pueden tomar.
Esto es mortal en una infraestructura financiera que no solo es abierta y transparente, sino inmutable. Exploremos un poco más esta idea de la no computabilidad.
Intuición sobre la no computabilidad
Intuitivamente, la no computabilidad es una visión algorítmica de la indecidibilidad. La no computabilidad tiene las mismas bases que la indecidibilidad. Las preguntas indecidibles se enmarcan como enunciados lógicos o enunciados sobre enteros. Por supuesto, los programas son enunciados lógicos y pueden incluso verse como enteros, aunque vemos los programas de manera diferente. A menudo vemos los programas con detalles adicionales de modelos de memoria, detalles de implementación y semántica de ejecución.
El problema de la detención: Como ejemplo, dado cualquier programa P y cualquier entrada finita I para P, entonces el problema de la detención es el desafío de determinar si P se detiene con la entrada I.
Alonzo Church y Alan Turing demostraron que el problema de la detención es insoluble.
Christopher Strachey dio una prueba intuitiva por contradicción que muestra que el problema de la detención es no computable. Esto se configura suponiendo que existe un programa H que puede resolver el problema de la detención para cualquier programa P. H(P) devuelve verdadero si P se detiene y falso en caso contrario. Luego se construye un programa P que no se detiene cuando H(P) es verdadero, dando una contradicción. De manera similar, este programa P se detiene cuando H(P) es falso, también una contradicción.
Los problemas no computables son problemas que no pueden ser resueltos por un algoritmo o una computadora, sin importar cuánto tiempo o recursos se proporcionen. Estos problemas existen en varias formas, y un ejemplo de ello es el problema de correspondencia de Post, que fue propuesto por Emil Post.
El problema de correspondencia de Post puede describirse usando pares de cadenas y un entero. Imagina que tienes n pares de cadenas, llamados P. Estas cadenas están compuestas por caracteres de un conjunto de caracteres, como UTF-8 o cualquier otro alfabeto con al menos dos símbolos. Los pares de cadenas se ven así:
Ahora, también tienes un entero m que es mayor que 0. El problema de correspondencia de Post pregunta si hay una manera de crear una lista de índices (i1, i2, …, im) usando los pares de cadenas dados. Puedes repetir estos índices si es necesario, con una condición: cuando combines las cadenas x de los pares usando los índices, la cadena resultante debe ser igual a las cadenas y combinadas de los mismos pares usando los mismos índices. En otras palabras:
Cuando los desarrolladores intentan resolver el problema de correspondencia de Post, a menudo intentan usar bucles indeterminados (bucles sin un número fijo de iteraciones) en lugar de recursión. Esto se debe a que el problema parece requerir buscar a través de diferentes combinaciones de índices hasta encontrar una solución o hasta probar que no existe solución.
En términos simples, el problema de correspondencia de Post implica intentar encontrar una secuencia de índices que, cuando se aplican a los pares de cadenas dados, produzca cadenas concatenadas iguales a partir de ambos componentes x e y. Este problema se considera no computable porque no existe un algoritmo general que pueda resolverlo para todos los pares posibles de cadenas y enteros de entrada.
Resulta que muchas preguntas sobre cómo se comportan los programas son no computables. Esto tiene una serie de consecuencias para los contratos inteligentes que se construyen en lenguajes Turing completos, muchas de las cuales aún no conocemos pero de las que seguramente nos daremos cuenta a medida que nos encontremos con ellas en el futuro.
La intuición de Raymond Smullyan sobre la indecidibilidad
Esta es parte del enfoque de Raymond Smullyan para entender la indecidibilidad en la lógica proposicional. Utiliza meta-información para mostrar que algo debe ser verdadero, aunque no pueda probarse en la lógica proposicional. Esto se basa en una paradoja.
En la lógica proposicional, un enunciado lógico es indecidible si no podemos probar que sea verdadero o falso. Dado un enunciado de lógica proposicional S, una prueba es una secuencia de deducciones lógicas formales, comenzando desde hechos básicos y terminando indicando si S es verdadero o falso.
Smullyan comienza con una isla de Caballeros y Patanes. Los Caballeros siempre dicen la verdad. Los Patanes siempre mienten. No podemos distinguir a los isleños de otra manera.
Hay un gran lógico llamado Ray. Todo lo que Ray prueba es verdadero. Esto es como un buen demostrador de teoremas.
Un isleño llamado Jack proclama: “No puedes probar que soy un Caballero” al lógico Ray.
El razonamiento siguiente se basa en el meta-conocimiento de esta situación. Este meta-conocimiento muestra que algunos problemas son indecidibles en la lógica proposicional.
Si Ray puede probar que Jack es un Caballero, entonces Jack debe ser un Patán, ya que Jack debe haber mentido. Eso es porque Ray probó que Jack es un Caballero. Como Jack es un Patán, la prueba de Ray contradice la suposición de que Ray solo prueba cosas verdaderas. Por lo tanto, este caso no puede ocurrir.
Si Ray no puede probar que Jack es un Caballero, entonces Jack debe ser un Caballero, ya que Jack dijo la verdad. Pero Ray no puede probar el hecho de que Jack es un Caballero.
En el contexto de los contratos inteligentes y los lenguajes de programación, los lenguajes Turing completos como Solidity conllevan la posibilidad de problemas indecidibles.
Estos problemas indecidibles son similares a la paradoja presentada en la historia de Caballeros y Patanes, donde es imposible determinar si Jack es un Caballero o un Patán con la información dada.
En la historia de Caballeros y Patanes, Ray es análogo a un demostrador de teoremas o a un contrato inteligente en un lenguaje Turing completo. Ray se enfrenta a una afirmación que es indecidible dentro de las limitaciones del sistema (Caballeros y Patanes), lo que conduce a una paradoja.
De manera similar, un lenguaje de contratos inteligentes Turing completo podría enfrentarse a problemas indecidibles que no pueden resolverse, lo que conduce a comportamientos inesperados, vulnerabilidades o problemas de consumo de recursos (como quedarse sin gas en Ethereum).
Por otro lado, los lenguajes no Turing completos como Clarity están diseñados para evitar problemas indecidibles limitando su expresividad.
En el contexto de la historia de Caballeros y Patanes, un lenguaje no Turing completo simplemente no permitiría que Jack hiciera una afirmación que pudiera conducir a una paradoja. Al prohibir ciertas características como bucles no acotados y recursión, los lenguajes no Turing completos pueden proporcionar garantías más sólidas sobre el comportamiento y el uso de recursos de los contratos inteligentes.
Esta predictibilidad es deseable en muchos casos, especialmente al tratar con transacciones de alto valor o sistemas críticos.
Referencia
The Mathematics of Various Entertaining Subjects: Research in Recreational Math Illustrated Edition, Jennifer Beineke (Editor), Jason Rosenhouse (Editor), Raymond M. Smullyan (Prólogo), Princeton University Press, 2016.
Última actualización
¿Te fue útil?