Vitalik: ¿Cuál es la clave para la siguiente fase de Ethereum?

Autor: Vitalik Buterin

Traducido por: Jiahua, ChainCatcher

Un agradecimiento especial a Yoichi Hirai, Justin Drake, Nadim Kobeissi y Alex Hicks por sus comentarios y reseñas.

En los últimos meses, un nuevo paradigma de programación ha ganado rápidamente popularidad en los círculos de desarrollo de Ethereum y en muchos otros ámbitos de la informática: escribir código directamente en lenguajes de muy bajo nivel (como el código de bytes de la EVM o el lenguaje ensamblador) o en Lean, y utilizar pruebas matemáticas verificables automáticamente escritas en Lean para validar su corrección.

Si se realiza correctamente, esto no solo tiene el potencial de producir código extremadamente eficiente, sino que también es mucho más seguro que los métodos de programación anteriores. Yoichi Hirai lo denomina la "forma definitiva de desarrollo de software".

Este artículo intentará desvelar los principios subyacentes, explorar qué puede lograr la verificación formal del software e identificar sus debilidades y limitaciones en Ethereum y otros campos.

¿Qué es la verificación formal?

La verificación formal se refiere al proceso de escribir demostraciones de teoremas matemáticos de manera que puedan comprobarse automáticamente. Para ilustrarlo con un ejemplo relativamente sencillo pero interesante, consideremos un teorema básico sobre la sucesión de Fibonacci: cada tercer número es par, mientras que los demás son impares.

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …

Una forma sencilla de demostrarlo es mediante la inducción matemática, avanzando tres pasos a la vez.

Primero está el caso base. Sea F1 = F2 = 1, F3 = 2. Por observación, vemos que la afirmación ("Fi es par cuando i es múltiplo de 3, de lo contrario es impar") se cumple antes de x = 3.

A continuación, el caso inductivo. Supongamos que la afirmación es verdadera antes de 3k+3, lo que significa que ya sabemos que la paridad de F3k+1, F3k+2 y F3k+3 es impar, impar y par, respectivamente. Podemos calcular la paridad del siguiente grupo de tres números:

F3k+4 = F3k+2 + F3k+3 = impar + par = impar

F3k+5 = F3k+3 + F3k+4 = par + impar = impar

F3k+6 = F3k+4 + F3k+5 = impar + impar = par

Así, sabiendo que la afirmación es cierta antes de 3k+3, deducimos que también lo es antes de 3k+6. Podemos aplicar este razonamiento repetidamente, asegurándonos de que esta regla se cumple para todos los números enteros.

Este argumento basta para convencer a los humanos. Sin embargo, ¿qué ocurre si se quiere demostrar algo cien veces más complejo y se desea tener la absoluta certeza de no haber cometido ningún error? En ese caso, se puede proporcionar una prueba que convenza incluso a un ordenador.

Así es como se presenta:

-- Fibonacci con fib 0 = 0, fib 1 = 1, fib 2 = 1 (índices desplazados en 1)

def fib : Nat → Nat

| 0 => 0

| 1 => 1

| n + 2 => fib (n + 1) + fib n

-- Afirmación: fib (3k+1) es impar, fib (3k+2) es impar, fib (3k+3) es par.

-- Equivalentemente: cada tercer número de Fibonacci a partir de fib 3 es par.

-- Demostramos los tres a la vez por inducción sobre k, ya que cada caso

-- del siguiente bloque se construye a partir del bloque anterior.

teorema fib_triple (k : Nat) :

fib (3 * k + 1) % 2 = 1 ∧

fib (3 * k + 2) % 2 = 1 ∧

fib (3 * k + 3) % 2 = 0 := por

inducción k con

| cero => decidir

| succ k ih =>

-- Reescribe los nuevos índices en la forma (algo) + 2 para que se desarrolle la falacia de Fibonacci.

refinar ⟨?_, ?_, ?_⟩

· mostrar (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1

omega

· mostrar (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1

omega

· mostrar (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)

+ (fibra (3 * k + 3) + fibra (3 * k + 2))) % 2 = 0

omega

Se trata de la misma lógica de razonamiento, pero expresada en Lean. Lean es un lenguaje de programación comúnmente utilizado para escribir y verificar demostraciones matemáticas.

Esto difiere de la prueba "humana" presentada anteriormente, y con razón: lo que es intuitivo para una computadora (en el sentido tradicional de "computadora", es decir, un programa "determinista" compuesto de sentencias if/then, en lugar de grandes modelos de lenguaje) es fundamentalmente diferente de lo que es intuitivo para los humanos.

En la demostración anterior, no enfatizaste el hecho de que fib(3k+4) = fib(3k+3) + fib(3k+2), sino que enfatizaste que fib(3k+3) + fib(3k+2) es impar, mientras que una estrategia en Lean llamada omega combina automáticamente esto con su conocimiento de la definición de fib(3k+4).

En demostraciones más complejas, a veces hay que indicar explícitamente qué ley matemática permite dar el paso actual, y a veces hay que usar nombres poco comunes como Prod.mk.inj.

Por otro lado, puedes expandir expresiones polinómicas enormes en un solo paso y demostrar su validez con una sola expresión lineal como "omega" o "anillo".

Esta naturaleza poco intuitiva y engorrosa explica en gran medida por qué, a pesar de que existen pruebas verificables por máquina desde hace casi 60 años, el campo sigue siendo un nicho. Sin embargo, por otro lado, gracias al rápido desarrollo de la inteligencia artificial, muchas cosas que antes eran imposibles ahora se están volviendo posibles.

Cuando las demostraciones matemáticas empiezan a proteger el código

Hasta ahora, podrías estar pensando: bueno, las computadoras pueden verificar demostraciones de teoremas matemáticos, así que finalmente podremos determinar qué conclusiones nuevas y descabelladas sobre los números primos son verdaderas y cuáles son solo errores en documentos PDF de cien páginas.

¡Quizás incluso podamos averiguar si las opiniones de Shinichi Mochizuki sobre la conjetura ABC son correctas!

Pero dejando de lado la curiosidad, ¿y qué?

Existen muchas respuestas posibles. Pero una respuesta que considero muy importante es verificar la corrección de los programas informáticos, especialmente aquellos que realizan tareas criptográficas o relacionadas con la seguridad.

Al fin y al cabo, los programas informáticos son objetos matemáticos, por lo que demostrar que un programa informático se ejecuta de cierta manera es en sí mismo un teorema matemático.

Por ejemplo, supongamos que quieres demostrar si un software de comunicación encriptada como Signal es realmente seguro. En este contexto, puedes definir matemáticamente qué significa "seguro".

En términos generales, lo que se demuestra es que, asumiendo que se cumplen ciertas condiciones criptográficas, solo quienes poseen la clave privada pueden conocer el contenido del mensaje. En realidad, existen muchas propiedades de seguridad cruciales.

Resulta que sí hay un equipo que está intentando resolver precisamente este problema. Uno de sus teoremas de seguridad es el siguiente:

teorema del secreto pasivo le_ddh

(g : G)

(adv : PassiveAdversary G SK) :

Ventaja de secreto pasivo (F := F) g adv ≤

ProbComp.boolDistVentaja

(DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))

(DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

Aquí tenéis un resumen de su significado según Leanstral:

El teorema passivesecrecyle_ddh es una reducción compacta que demuestra que la confidencialidad pasiva de los mensajes de X3DH es al menos tan difícil de vulnerar como la suposición DDH en el modelo de oráculo aleatorio. Si un adversario puede romper la confidencialidad pasiva de los mensajes de X3DH, también puede romper DDH.

Dado que asumimos que DDH es difícil de vulnerar, X3DH también es seguro frente a ataques pasivos. Este teorema demuestra que si un adversario puede observar pasivamente los mensajes de intercambio de claves de Signal, no podrá distinguir la clave de sesión que produce de una clave aleatoria con una probabilidad superior a la despreciable.

Si a esto se le suma una prueba correcta de la implementación del cifrado AES, se obtiene una prueba de que el cifrado del protocolo Signal es seguro frente a atacantes pasivos.

Proyectos similares también han demostrado que las implementaciones de TLS y otras partes de la criptografía interna del navegador son seguras.

Si se realiza una verificación formal completa de extremo a extremo, no solo se demuestra que una descripción teórica del protocolo es segura, sino que el código específico que ejecutan los usuarios también es seguro en la práctica.

Desde la perspectiva del usuario, esto aumenta considerablemente la desconfianza: para confiar plenamente en el código, no es necesario revisar todo el código fuente; solo es necesario comprobar las afirmaciones sobre él que se han demostrado.

Ahora bien, hay algunas advertencias importantes que conviene tener en cuenta, especialmente en lo que respecta al significado real de la palabra clave "seguro".

Es fácil olvidar demostrar aquellas afirmaciones verdaderamente importantes. Es fácil descubrir que, a veces, las afirmaciones que se deben demostrar no son más sencillas de describir que el propio código.

Es fácil introducir inadvertidamente suposiciones en la demostración que, en última instancia, no se cumplen. También es fácil decidir que solo una parte del sistema necesita ser demostrada formalmente, para luego descubrir graves vulnerabilidades en otras partes (incluso en el hardware).

Incluso la propia implementación de Lean puede tener errores. Pero antes de analizar todos estos detalles molestos, profundicemos primero en la utopía que podría surgir al completar la verificación formal de forma correcta e ideal.

Verificación formal. Nacida para la seguridad.

Los errores en el código informático son aterradores.

Cuando se introducen criptomonedas en contratos inteligentes de cadena inmutable, y Corea del Norte puede vaciar automáticamente todos los fondos si aparece un error en el código sin que se tenga recurso alguno, los errores en el código se vuelven aún más aterradores.

Cuando todo esto se envuelve en pruebas de conocimiento cero, los errores se vuelven aún más aterradores porque si alguien logra hackear el sistema de pruebas de conocimiento cero, puede extraer todo el dinero y no tenemos idea de qué salió mal (peor aún, ni siquiera sabemos cuándo salió mal).

Cuando dentro de dos años contemos con modelos de IA potentes, como Claude Mythos, capaces de descubrir automáticamente estos errores, los fallos en el código se volverán aún más aterradores.

Ante esta realidad, algunas personas abogan por abandonar la idea fundamental de los contratos inteligentes, llegando incluso a creer que internet no puede ser un dominio donde los defensores puedan tener una ventaja asimétrica sobre los atacantes.

Algunas citas:

Para reforzar la seguridad de un sistema, es necesario gastar más tokens de los que utiliza el atacante para explotar las vulnerabilidades.

Y:

Nuestra industria se basa en código determinista. Escribirlo, probarlo, implementarlo, tener la certeza de que funciona, pero en mi experiencia, este contrato se está rompiendo.

Entre los principales operadores de empresas verdaderamente nativas de la IA, el código fuente se ha convertido en algo en lo que se "confía" para que funcione, y ya no se puede especificar con precisión su probabilidad de éxito.

Peor aún, algunas personas creen que la única solución es abandonar el software de código abierto.

Para la ciberseguridad, el panorama sería desalentador. Especialmente para quienes nos preocupamos por la descentralización y la libertad de internet, esta es una perspectiva extremadamente pesimista.

Todo el espíritu cypherpunk se basa fundamentalmente en la idea de que en internet, los defensores tienen la ventaja, y construir un "castillo" digital (ya sea mediante cifrado, firmas o pruebas) es mucho más fácil que destruirlo.

Si perdemos esto, la seguridad en internet solo podrá provenir de economías de escala, de la búsqueda de posibles atacantes en todo el mundo y, en términos más generales, solo podrá ser una elección entre dominación y destrucción.

No estoy de acuerdo; tengo una visión más optimista del futuro de la ciberseguridad.

Creo que los desafíos que plantean las potentes capacidades de detección de vulnerabilidades de la IA son serios, pero se trata de un desafío transitorio. Una vez que la situación se estabilice y alcancemos un nuevo equilibrio, tendremos un entorno más favorable para los defensores que en el pasado.

Mozilla está de acuerdo con mi punto de vista. Para citarlos:

Es posible que tengas que reajustar la prioridad de todo lo demás y dedicar energía constante y concentrada a esta tarea, pero hay luz al final del túnel.

Estamos muy orgullosos de cómo nuestro equipo está afrontando este reto, y otros también lo harán. Nuestro trabajo aún no ha terminado, pero hemos superado la tormenta y podemos vislumbrar un futuro que no solo nos permitirá mantenernos a flote, sino que será mucho mejor.

Los defensores finalmente tienen la oportunidad de ganar de forma decisiva. … Los defectos son limitados, y estamos entrando en un mundo donde finalmente podemos detectarlos todos.

Ahora bien, si buscas las palabras "formal" y "verificación" en la publicación de Mozilla usando Ctrl+F, no encontrarás ninguna coincidencia. El futuro prometedor de la ciberseguridad no depende exclusivamente de la verificación formal ni de ninguna otra tecnología en particular.

¿De qué depende? Básicamente, de este gráfico:

Tendencia de las vulnerabilidades CVE a lo largo del tiempo

Durante décadas, muchas tecnologías han contribuido a la disminución del número de vulnerabilidades:

Sistemas de tipos

Lenguajes seguros para la memoria

Mejoras en la arquitectura del software (incluyendo el aislamiento de procesos, el control de permisos y, de forma más general, la distinción entre la "base de computación confiable" y el "otro código").

Mejores métodos de prueba

Una base de conocimientos en constante expansión sobre patrones de codificación seguros e inseguros.

Un número creciente de bibliotecas de software preescritas y auditadas

La verificación formal asistida por IA no debe considerarse un paradigma completamente nuevo, sino más bien un potente acelerador de tendencias y paradigmas que ya están en marcha.

La verificación formal no es la solución definitiva. Sin embargo, resulta especialmente adecuada para situaciones en las que el objetivo es mucho más sencillo que la implementación. Esto es particularmente cierto para algunas tecnologías extremadamente complejas y delicadas que necesitaremos implementar en la próxima iteración importante de Ethereum: firmas resistentes a la computación cuántica, STARKs, algoritmos de consenso y ZK-EVM.

STARK es un software muy complejo. Pero las propiedades de seguridad básicas que implementa son fáciles de entender y formalizar: si ves un hash H que apunta al programa P, la entrada x y la salida y, entonces (i) el algoritmo hash utilizado en STARK ha sido vulnerado, o (ii) P(x) = y.

Así pues, tenemos el proyecto Arklib, que intenta crear una implementación de STARK totalmente verificada formalmente (véase VCV-io, que proporciona la infraestructura informática básica de oráculos para la verificación formal de varios otros protocolos criptográficos, muchos de los cuales son dependencias de STARK).

De forma más ambiciosa, existe evm-asm: un proyecto para construir una implementación completa de EVM totalmente verificada formalmente.

Las propiedades de seguridad en este caso no son tan sencillas: esencialmente, el objetivo es demostrar su equivalencia con otra implementación de EVM escrita en Lean, aunque dicha implementación puede escribirse para maximizar la intuición y la legibilidad sin tener en cuenta la eficiencia específica en tiempo de ejecución.

Es posible que obtengamos diez implementaciones de EVM, todas demostrablemente equivalentes, y que todas contengan la misma falla fatal que permite a un atacante extraer todo el ETH de direcciones a las que no está autorizado a acceder.

Pero esto es mucho menos probable que la posibilidad de que tales fallos existan en alguna implementación actual de EVM. Otra propiedad de seguridad cuya importancia solo comprendimos tras experiencias dolorosas, a saber, la resistencia a los ataques DoS, también es fácil de formalizar.

Otras dos áreas importantes son:

Consenso tolerante a fallos bizantinos. Formalizar todas las propiedades de seguridad esperadas resulta igualmente complejo, pero dada la frecuencia de los errores, merece la pena intentarlo. Por ello, contamos con implementaciones Lean en curso y pruebas de protocolos de consenso en Lean.

Lenguajes de programación para contratos inteligentes: consulte la verificación formal en Vyper y Verity.

En todos estos casos, uno de los enormes beneficios que aporta la verificación formal es que estas pruebas son verdaderamente integrales. Por lo general, los errores más molestos son los errores de interacción que se presentan en la interfaz de dos subsistemas considerados de forma independiente.

Para los humanos, razonar sobre todo el sistema de principio a fin es demasiado difícil. Pero los sistemas automatizados de verificación de reglas pueden hacerlo.

Verificación formal: Nacida para la eficiencia

Analicemos nuevamente evm-asm. Se trata de una implementación de EVM, pero escrita directamente en lenguaje ensamblador RISC-V.

Genuino.

Aquí está el código de operación ADD:

Importar EvmAsm.Rv64.Program

espacio de nombres EvmAsm.Evm64

Abrir EvmAsm.Rv64

/-- EVM de 256 bits ADD: binario, extrae 2, inserta 1.

Extremidad 0: LD, LD, ADD, SLTU (llevar), SD (5 instrucciones).

Extremidades 1-3: LD, LD, ADD, SLTU (transporte1), ADD (transporteIn), SLTU (transporte2), OR (transporteOut), SD (8 cada una).

Luego ADDI sp, sp, 32.

Registros: x12=sp, x7=acc, x6=operando, x5=acarreo, x11=acarreo1. -/

def evm_add : Programa :=

-- Extremidad 0 (5 instrucciones)

LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;

ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;

-- Extremidad 1 (8 instrucciones)

LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;

AÑADIR .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

AÑADIR .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

O .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;

-- Extremidad 2 (8 instrucciones)

LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;

AÑADIR .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

AÑADIR .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

O .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;

-- Extremidad 3 (8 instrucciones)

LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;

AÑADIR .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

AÑADIR .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

O .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;

-- ajuste de sp

ADDI .x12 .x12 32

fin EvmAsm.Evm64

La elección de RISC-V se debe a que los probadores ZK-EVM que se están desarrollando suelen funcionar probando RISC-V y compilando clientes Ethereum a RISC-V. Por lo tanto, si dispone de una implementación de EVM escrita directamente en RISC-V, esta debería ser la implementación más rápida que pueda obtener.

RISC-V también se puede simular de forma muy eficiente en ordenadores comunes (y existen portátiles RISC-V disponibles en el mercado).

Por supuesto, para lograr una verificación integral, es necesario verificar formalmente la implementación de RISC-V (o la aritmética del probador), pero no se preocupe, ya existen trabajos en este ámbito.

Escribir código directamente en lenguaje ensamblador era algo que hacíamos hace cincuenta años. Desde entonces, hemos abandonado esta práctica en favor de escribir código en lenguajes de alto nivel.

Los lenguajes de alto nivel sacrifican la eficiencia, pero a cambio permiten una codificación mucho más rápida y, lo que es más importante, una comprensión mucho más rápida del código de otros, lo cual es esencial para la seguridad.

Con la combinación de verificación formal e inteligencia artificial, tenemos la oportunidad de "volver al futuro".

En concreto, podemos hacer que la IA escriba código ensamblador y, a continuación, que genere una prueba formal para verificar que dicho código tiene las propiedades deseadas.

Como mínimo, las propiedades deseadas pueden ser simplemente una equivalencia perfecta con una implementación que haya sido optimizada para la legibilidad y escrita en algún lenguaje de alto nivel fácil de entender para los humanos.

Ya no necesitamos un único objeto de código para equilibrar la legibilidad y la eficiencia; en su lugar, tenemos dos objetos independientes: uno (la implementación en lenguaje ensamblador) optimizado únicamente para la eficiencia, teniendo en cuenta las exigencias de su entorno de ejecución específico; el otro (la instrucción de seguridad o la implementación en lenguaje de alto nivel) optimizado únicamente para la legibilidad, y luego demostramos la equivalencia entre ambos mediante una prueba matemática.

Los usuarios pueden verificar (automáticamente) esa prueba una sola vez y, a partir de entonces, solo necesitan ejecutar la versión rápida.

Este enfoque es increíblemente poderoso, y hay una razón por la que Yoichi Hirai lo llama "la forma definitiva de desarrollo de software".

La verificación formal no es la solución mágica.

En los campos de la criptografía y la informática, existe una tradición casi tan antigua como la historia de los métodos formales en sí: la tradición de criticar los métodos formales (o, en términos más generales, la dependencia de las "pruebas").

Estos escritos están repletos de casos prácticos. Comencemos con las pruebas manuscritas de la primera época de la criptografía simple, citando las críticas de Menezes y Koblitz de 2004:

En 1979, Rabin propuso una función criptográfica que, en cierto sentido, era "demostrablemente" segura, lo que significa que poseía una propiedad de seguridad reduccionista.

La declaración de seguridad reduccionista indica que cualquiera que pueda encontrar el mensaje m a partir del texto cifrado y también debe poder factorizar n. … Poco después de que Rabin propusiera su esquema de cifrado, Rivest señaló que, irónicamente, esta misma característica que le otorga seguridad adicional conduciría a un colapso total si se enfrentara a un atacante conocido como "texto cifrado elegido".

Es decir, si el atacante puede de alguna manera engañar a Alice para que descifre el texto cifrado elegido, entonces el atacante puede seguir los mismos pasos que Sam usó en el párrafo anterior para factorizar n.

Menezes y Koblitz proporcionaron más ejemplos. El patrón común es que los diseños destinados a hacer que los protocolos de cifrado sean más "demostrables" a menudo los hacen menos "naturales", lo que aumenta la probabilidad de que fallen de maneras que los diseñadores ni siquiera consideraron.

Ahora, volvamos a las pruebas y el código verificables por máquina. Aquí hay un artículo de 2011 que descubrió vulnerabilidades en un compilador C formalmente verificado: artículo:

El segundo problema de CompCert que encontramos se manifiesta en dos errores que conducen a la generación del siguiente código: stwu r1, -44432(r1) donde se está asignando un marco de pila PowerPC grande.

El problema radica en que el campo de desplazamiento de 16 bits se desbordó. La semántica PPC de CompCert no especificaba un límite para el ancho de este valor inmediato; asumían que el ensamblador detectaría los valores fuera de rango.

También existe un documento de 2022:

En CompCert-KVX, la confirmación e2618b31 corrigió un error: la instrucción "nand" se imprimía como "and"; "nand" solo se usaba en el patrón poco frecuente ~ (a & b). Este error se descubrió al compilar programas generados aleatoriamente.

Y hoy, en 2026, así es como Nadim Kobeissi describe las vulnerabilidades en el software formalmente verificado en Cryspen:

En noviembre de 2025, Filippo Valsorda informó de forma independiente que libcrux-ml-dsa v0.0.3 producía diferentes claves públicas y firmas en diferentes plataformas con la misma entrada determinista.

El error residía en la función interna de envoltura vxarqu64, que implementaba la operación XAR utilizada en la permutación Keccak-f de SHA-3. El mecanismo de reserva pasaba parámetros incorrectos a la operación de desplazamiento, lo que corrompía el resumen SHA-3 en plataformas ARM64 sin soporte de hardware para SHA-3.

Esto se clasifica como fallo de tipo I: la función interna estaba marcada, pero todo el sistema backend de NEON no completó una prueba de seguridad o corrección en tiempo de ejecución.

Y:

La biblioteca libcrux-psq implementa un protocolo de clave precompartida post-cuántica. En el método decrypt_out, la ruta de descifrado AES-GCM 128 llama a .unwrap() sobre el resultado del descifrado en lugar de propagar errores. Un texto cifrado mal formado puede provocar el fallo del proceso.

Los cuatro problemas mencionados se engloban en una de las dos categorías siguientes:

Se dieron casos en los que solo se verificó una parte del código (porque verificar el resto era demasiado difícil), lo que llevó al descubrimiento de que el código no verificado tenía más vulnerabilidades de las que los autores imaginaban (y de maneras más letales).

Casos en los que los autores olvidaron especificar propiedades clave que debían demostrarse.

El artículo de Nadim incluye una clasificación de los modos de fallo en la verificación formal; también proporciona otros tipos de modos de fallo (por ejemplo, otro caso importante es "la especificación formal en sí misma es incorrecta, o la prueba contiene afirmaciones falsas aceptadas silenciosamente por el sistema construido").

Finalmente, podemos analizar los fallos de la verificación formal en la interfaz entre software y hardware. Un problema común en este caso es la verificación de la resistencia a los ataques de canal lateral.

Aunque dispongas de métodos criptográficos perfectamente seguros para proteger tus mensajes, si alguien a pocos metros de distancia puede captar las fluctuaciones de las señales eléctricas y extraer tu clave privada tras cientos de miles de cifrados, seguirás estando desprotegido.

Este es un artículo sobre "análisis de potencia diferencial", un ejemplo bien conocido de dichas técnicas: artículo.

El análisis de potencia diferencial es un tipo común de ataque de canal lateral. Fuente: Wikipedia

Siempre se han realizado intentos para demostrar la seguridad frente a este tipo de atacantes. Sin embargo, cualquier prueba de este tipo requiere un modelo matemático del atacante que permita demostrar dicha seguridad.

En ocasiones se utiliza un "modelo de sondeo d": se asume que el número de ubicaciones que el atacante puede consultar en el circuito tiene un límite conocido. Sin embargo, este modelo no contempla algunas formas de fuga de información.

Como se observa en este artículo, un problema común es la fuga transitoria: si se puede observar una señal que depende no solo del valor en una ubicación determinada, sino también de cómo cambia ese valor, esto suele ser suficiente para recuperar la información necesaria a partir de dos valores (el valor antiguo y el nuevo) en lugar de un solo valor.

Este artículo ofrece clasificaciones de otras formas de fugas.

Durante décadas, estas críticas a la verificación formal han contribuido a mejorarla. En comparación con el pasado, ahora somos mejores para prevenir este tipo de problemas. Pero incluso hoy, no es perfecta.

En perspectiva, hay un hilo conductor principal. La verificación formal es poderosa.

Pero por mucho que los términos de marketing hagan que la verificación formal suene como si proporcionara una "corrección demostrable", la supuesta "corrección demostrable" en realidad no prueba que el software (o el hardware) sea "correcto".

Para la mayoría de las personas, "correcto" significa algo así como: "el comportamiento de las cosas se ajusta a la comprensión que tiene el usuario de la intención del desarrollador".

Y "seguro" significa algo así como: "el comportamiento de las cosas no viola las expectativas del usuario y no hace cosas perjudiciales para los intereses del usuario".

En ambos casos, la corrección y la seguridad se reducen a una comparación entre objetos matemáticos e intenciones o expectativas humanas.

Las intenciones y expectativas humanas son, en sí mismas, objetos matemáticamente complejos; al fin y al cabo, el cerebro humano forma parte del universo y sigue leyes físicas que pueden simularse si se dispone de suficiente capacidad de cálculo.

Pero son objetos matemáticos increíblemente complejos que ni los ordenadores ni nosotros mismos podemos comprender ni siquiera leer.

En la práctica, son cajas negras; solo podemos comprender nuestras intenciones y expectativas porque cada uno de nosotros tiene años de experiencia observando nuestros pensamientos e infiriendo los pensamientos de los demás.

Y dado que no podemos introducir las intenciones humanas en estado puro en un ordenador, la verificación formal no puede demostrar una comparación con las intenciones humanas.

Por lo tanto, la "corrección demostrable" y la "seguridad demostrable" no demuestran realmente la "corrección" y la "seguridad" que los humanos comprendemos. Nada puede lograrlo a menos que podamos simular completamente el cerebro humano.

¿Para qué sirve entonces?

Tiendo a considerar los conjuntos de pruebas, los sistemas de tipos y la verificación formal como diferentes implementaciones del mismo enfoque subyacente para la seguridad de los lenguajes de programación (que también puede ser el único enfoque razonable).

Se trata de especificar nuestras intenciones de forma redundante y de diferentes maneras, para luego comprobar automáticamente si estas diferentes especificaciones son compatibles entre sí.

Tomemos este código Python como ejemplo:

def fib(n: int) -> int:

si n < 0:

Generar excepción ("No se admiten valores negativos")

elif 0 <= n < 2:

devolver n

demás:

devolver fib(n-1) + fib(n-2)

Si __name__ == '__main__':

afirmar [fib(i) para i en rango(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

afirmar fib(15) == 610

Aquí puedes expresar tus intenciones de tres maneras diferentes:

Explícitamente, implementando la fórmula de Fibonacci en el código.

Implícitamente, a través del sistema de tipos (que especifica que las entradas, salidas y pasos intermedios en la recursión son todos enteros)

Mediante el método del "paquete de muestra": casos de prueba

Al ejecutar el archivo, se comprobará la fórmula comparándola con los ejemplos. El verificador de tipos puede comprobar si los tipos son compatibles: sumar dos enteros es una operación compatible y producirá otro entero.

Los sistemas de tipos suelen ser una buena forma de comprobar el trabajo en física: si estás calculando la aceleración pero obtienes una respuesta en metros/segundo en lugar de metros/segundo², sabes que has cometido un error.

Los casos de prueba son un ejemplo de la definición de "paquete de muestra", que suele ser una forma más natural para que los humanos manejen los conceptos que las definiciones explícitas directas.

Cuantas más formas diferentes tengas de especificar tus intenciones, idealmente de maneras que te obliguen a pensar de forma diferente sobre el problema, más probabilidades tendrás de expresar realmente lo que quieres una vez que se demuestre que todas estas expresiones son compatibles entre sí.

La programación segura consiste en expresar tus intenciones de múltiples maneras diferentes y luego verificar automáticamente si todas esas expresiones son compatibles entre sí.

La verificación formal permite ampliar aún más este enfoque. Mediante la verificación formal, se pueden especificar las intenciones de un número casi infinito de maneras redundantes diferentes, y el programa solo se puede validar si todas son compatibles.

Puedes especificar una implementación altamente optimizada y otra muy ineficiente pero legible para humanos, y verificar que coincidan. Puedes pedirles a diez amigos que te proporcionen una lista de propiedades matemáticas que, en su opinión, debería tener tu programa y luego comprobar si las cumple todas.

Si no pasa la prueba, averigua si el programa está mal o si las propiedades matemáticas están especificadas incorrectamente. Además, puedes usar inteligencia artificial para realizar todas estas operaciones con suma eficiencia.

¿Cómo puedo empezar?

En realidad, no tendrás que escribir demostraciones tú mismo. La razón por la que los métodos formales nunca se han popularizado es que la mayoría de la gente no sabe cómo escribir estas cosas tan complejas. ¿Podrías explicarme qué significa el siguiente código?

/-- Ayudante: comparación puntual ≤ a nivel de foldl con un acumulador. -/

teorema privado foldl_acc_le (ds1 ds2 : Lista Nat) (w : Nat) (ab : Nat) (hAcc : a ≤ b)

(hLE : Forall₂ (· ≤ ·) ds1 ds2) :

List.foldl (λ acc d => acc * w + d) a ds1 ≤

List.foldl (λ acc d => acc * w + d) b ds2 := by

hacer coincidir ds1, ds2, hLE con

| [], [], .nil => hAcc exacto

| d1::ds1', d2::ds2', .cons hd htl =>

simp [List.foldl]

refinar foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl

exacto Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

(Si se lo pregunta, este es uno de los muchos sublemas en la prueba de una declaración de seguridad específica para una variante de firmas SPHINCS.

En concreto, la afirmación es la siguiente: a menos que se produzca una colisión de hash, la firma de un mensaje generado a partir de un resumen hash (dig1) requerirá un valor superior en al menos algún punto de la cadena de hashes que la firma de cualquier otro mensaje, conteniendo así información que no puede calcularse a partir de esa otra firma.

No es necesario escribir código ni realizar demostraciones manualmente; basta con dejar que la IA escriba programas por usted (ya sea directamente en Lean o, para mayor rapidez, en lenguaje ensamblador) y demuestre cualquier propiedad deseada durante el proceso.

La ventaja de esta tarea es que se autovalida, por lo que no es necesario supervisarla; simplemente se deja que la IA funcione de forma continua durante varias horas.

El peor escenario posible es que dé vueltas en círculo sin progresar (o, como hizo una vez mi leanstral, que sustituya la afirmación que se le pidió que demostrara para aligerar su carga de trabajo).

Lo único que debes comprobar al final es si las afirmaciones que se demuestran cumplen con tus requisitos.

En el caso de la variante de firma SPHINCS, esta es la declaración final:

teorema wots_fullDigits_incomparable

{dig1 dig2 : Lista Nat} {w l1 l2 : Nat}

(hw : 0 < w)

(hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)

(hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)

(hL2suff : l1 * (w - 1) < w ^ l2)

(hNeq : dig1 ≠ dig2) :

¬ Para todo₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧

¬ Para todo₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

Esto está prácticamente al límite de ser casi ilegible:

Si los números generados a partir de un resumen hash (dig1) no son iguales a los generados a partir de otro resumen hash (dig2)

Entonces, ninguna de las dos condiciones siguientes se cumple:

Para todos los números, los números de dig1 son menores o iguales que los números de dig2.

Para todos los números, los números de dig2 son menores o iguales que los números de dig1.

En los "números extendidos" (wotsFullDigits) generados al sumar sumas de verificación. Es decir, en la extensión de dig1, inevitablemente habrá lugares donde los números sean más altos, mientras que en otros lugares, los números en la extensión de dig2 serán más altos.

En lo que respecta al uso de modelos de lenguaje grandes para escribir demostraciones, considero que tanto Claude como Deepseek 4 Pro son adecuados. Leanstral es un modelo de ponderación de código abierto más pequeño, específicamente optimizado para escribir Lean, y representa una alternativa prometedora.

Tiene 119 mil millones de parámetros, activando 6 mil millones por token, y se puede ejecutar localmente, aunque es más lento (alrededor de 15 tokens/segundo en mi portátil). Según las pruebas de rendimiento, Leanstral supera a modelos generales mucho más grandes:

Según mi experiencia personal actual, es ligeramente menos eficaz que Deepseek 4 Pro, pero sigue siendo muy eficaz.

La verificación formal no puede resolver todos nuestros problemas.

Sin embargo, si queremos que el modelo de seguridad en internet deje de basarse en la confianza en unas pocas organizaciones poderosas, debemos recurrir a la confianza en el código, lo que incluye confiar en el código incluso frente a poderosos adversarios de IA.

La verificación formal asistida por IA nos ha permitido dar un paso firme hacia la consecución de este objetivo.

Al igual que blockchain y ZK-SNARKs, la inteligencia artificial y la verificación formal son tecnologías altamente complementarias.

Blockchain te brinda verificabilidad abierta y resistencia a la censura a costa de la privacidad y la escalabilidad, mientras que ZK-SNARKs te devuelve la privacidad y la escalabilidad (de hecho, incluso más de lo que tenías antes).

La inteligencia artificial te brinda la capacidad de escribir grandes cantidades de código a costa de la precisión, mientras que la verificación formal te devuelve la precisión (de hecho, incluso más de la que tenías antes).

Por defecto, la IA generará una gran cantidad de código extremadamente apresurado y el número de errores aumentará.

De hecho, en algunos casos, tolerar un aumento de errores es la compensación adecuada: si los errores son menores, incluso un software con errores es mejor que no tener ningún software.

Pero en este ámbito, la ciberseguridad tiene un futuro optimista: el software seguirá dividiéndose en "partes periféricas inseguras" alrededor de un "núcleo seguro".

Las partes menos seguras del sistema se ejecutarán en entornos aislados, con los permisos mínimos necesarios para completar sus tareas.

El núcleo seguro lo gestionará todo. Si el núcleo seguro falla, todo fallará, incluyendo tus datos personales, tu dinero, etc. Pero si falla un componente periférico no seguro, el núcleo seguro aún podrá protegerte.

En lo que respecta al núcleo seguro, no podemos permitir que prolifere el código defectuoso. Tomaremos medidas drásticas para mantener el núcleo seguro pequeño e incluso reducirlo aún más.

En cambio, invertiremos todo el rendimiento adicional que aporta la IA en hacer que el núcleo seguro sea aún más seguro, lo que le permitirá soportar la enorme carga de confianza que le imponemos en una sociedad altamente digital.

El núcleo de un sistema operativo (o al menos una parte de él) se convertirá en un componente seguro.

Ethereum será otro.

Con suerte, al menos para todos los cálculos que no requieran un alto rendimiento, el hardware que utilice pasará a ser un tercer factor.

Los sistemas relacionados con el Internet de las Cosas serán el cuarto.

Al menos entre estos núcleos seguros, el viejo dicho de que "los errores son inevitables; solo puedes intentar encontrarlos antes de que lo haga el atacante" quedará desmentido, y será reemplazado por un mundo más esperanzador donde se logrará una verdadera seguridad.

Pero si estás dispuesto a entregar tus activos y datos a un software mal programado que podría, accidentalmente, engullirlos en un agujero negro, bueno, ciertamente también tienes esa libertad.