Computación de propósito general basada en pruebas con Magnetar

A primera vista

• Una nueva forma de computación. Las pruebas de conocimiento cero permiten ejecutar una carga de trabajo y recibir, junto con el resultado, una breve prueba que demuestra que el programa se ejecutó correctamente. Cualquiera puede verificar la prueba en milisegundos, sin tener que volver a ejecutar el programa, sin confiar en quien lo ejecutó y sin necesitar datos sobre los cuales se ejecutó el programa.
• Tres grandes desafíos han obstaculizado la adopción general: lograr que las pruebas sean lo suficientemente rápidas para producirse, hacerlas accesibles para programas normales sin conocimientos en criptografía, y basarlas en una criptografía que seguirá siendo confiable dentro de muchos decenios.
• El Magnetar ha logrado avances significativos en los tres desafíos. Demuestra que los programas escritos en Rust, Go o C funcionan de 10 a 39 veces más rápido en promedio que los sistemas comparables más rápidos anteriores, y su seguridad se basa únicamente en funciones de hash estándar. Este es el resultado más reciente de más de una década de investigación en Microsoft Research sobre la implementación práctica de pruebas de conocimiento cero.

Una nueva forma de computación

Cada resultado que produce la computadora viene acompañado de una pregunta implícita: ¿el programa se ejecutó como se prometió y produjo resultados correctos? Hoy en día, responder a esa pregunta a menudo requiere un grado de confianza junto con verificación. Confiamos en el operador, el proveedor, la contraparte o el agente, y nos basamos en contratos, auditorías y registros para establecer esa confianza.

Las pruebas de conocimiento cero ofrecen un enfoque fundamentalmente diferente para establecer confianza. Un programa se ejecuta y, junto con su salida, genera una prueba corta, un certificado criptográfico que demuestra que el programa, con estas entradas, produjo esa salida. La prueba es pequeña y fácil de verificar. Quien la reciba puede confirmar el resultado en milisegundos sin tener que volver a ejecutar el programa, y puede pasar la prueba a cualquier otra persona que necesite la misma garantía. Con la propiedad de cero conocimiento, la prueba tampoco revela nada sobre los datos de entrada que deben permanecer privados.

Esto cambia lo que significa la corrección en el mundo real. Un resultado ya no tiene que ser confiado por quien lo produjo; puede ser verificado por lo que lo acompaña. Un agente de IA actuando en nombre de alguien podría adjuntar una prueba de que cada acción se ajustó a la política que se le asignó. Las instituciones financieras reguladas podrían demostrar que las transacciones fueron procesadas correctamente sin hacer públicas sus transacciones. Todo esto se vuelve posible una vez que producir una prueba es tan rutinario como ejecutar el programa.

Tres grandes desafíos

Las pruebas de conocimiento cero fueron inventadas en la década de 1980, y las ideas detrás de probar la ejecución de programas han existido desde hace casi tanto tiempo. Lo que ha impedido que se conviertan en una herramienta general son tres desafíos que han resistido ser resueltos al mismo tiempo.

Eficiencia. Históricamente, la producción de una prueba requería millones de veces más computación que el ejecutar el programa en sí. A lo largo de los años de investigación, esa sobrecarga se ha reducido, pero los sistemas más rápidos lograron su velocidad haciendo concesiones en otros aspectos.

Generalidad y usabilidad. Muchos sistemas de prueba requieren que los desarrolladores reescriban manualmente su programa como un circuito criptográfico, lo cual es una descripción aritmética fija de ese cálculo exacto. Esto lleva meses. Cada cambio en la aplicación implica un nuevo circuito, y la traducción es en sí misma una fuente frecuente de errores de seguridad. Una alternativa de propósito general es probar la ejecución de un procesador ordinario, de modo que cualquier programa compilado pueda ser probado tal como está escrito. Hasta hace poco, esa generalidad implicaba un costo elevado en términos de velocidad o seguridad.

Seguridad. Una prueba es tan fuerte como la criptografía que la sustenta. Muchos sistemas de prueba se basan en curvas elípticas, las cuales pueden ser rompidas por un ordenador cuántico suficientemente potente. Microsoft aborda este problema con su Programa Quantum Safe, que trasladará sus productos y servicios a criptografía postcuántica, un objetivo que recientemente se aceleró para 2029. Los sistemas de prueba postcuántica ya existen, pero algunos se basan en supuestos de lattice, y la mayoría se basan en nuevas funciones criptográficas inventadas para reducir el costo de la prueba. Estas nuevas funciones criptográficas no han enfrentado las décadas de revisión que se ha dado a la criptografía que protege Internet hoy, y algunas se basan en conjeturas matemáticas sobre códigos de corrección de errores que aún no han sido demostradas. Han adquirido su velocidad con supuestos sólidos.

SERIE DE PODCASTS

La forma de las cosas que vendrán

Únete a Doug Burger de Microsoft y a los invitados mientras exploran las verdades fundamentales sobre la IA y cómo esta cambiará el futuro.

Más de una década de trabajo

Durante más de una década, Microsoft Research ha trabajado en hacer que las pruebas de conocimiento cero y el cómputo verificable sean prácticos. Las investigaciones iniciales siguieron dos enfoques, ambos prácticos solo para programas pequeños. El primero (se abre en nueva pestaña) (se abre en nueva pestaña) permite que un verificador verifique una computación larga a través de una breve conversación con el emisor, utilizando una técnica llamada el protocolo de verificación de suma (se abre en nueva pestaña), pero esto se aplicaba solo a computaciones con una estructura de capas específica. El segundo (se abre en nueva pestaña) (se abre en nueva pestaña) utilizó criptografía de curvas elípticas para crear pruebas muy pequeñas para casi cualquier computación. Pero esto requiere una configuración de confianza única que involucra información secreta, y si esta se filtra, cualquiera podría falsificar las pruebas. Este enfoque también es vulnerable a los ordenadores cuánticos.

En 2019, un nuevo sistema de prueba de conocimiento cero llamado Spartan volvió al enfoque de verificación de sumas y lo hizo funcionar para programas de uso general sin una configuración confiable. Spartan también puede ser instanciado con diferentes bloques criptográficos. Esa flexibilidad fue lo que más tarde permitió que el sistema de prueba se construyera únicamente sobre funciones de hash. Una secuencia de resultados luego completó los restantes elementos:

• Phalanx (se abre en nueva pestaña), en 2021, mostró cómo explotar la repetición, como un procesador que ejecuta el mismo ciclo de instrucción en cada paso, para demostrar que los cálculos son una orden de magnitud más rápidos que los del Spartan. La descripción del procesador de Magnetar se basa en esta idea.
• Nova (se abre en pestaña nueva), HyperNova (se abre en pestaña nueva), NeutronNova (se abre en pestaña nueva), Neo y SuperNeo (se abre en pestaña nueva) demostraron que detener el proceso de prueba de Spartan de forma temprana y combinar los resultados parciales permite probar cálculos de cualquier tamaño a un costo mucho menor.
• Brakedown (se abre en pestaña nueva), en 2021, introdujo un esquema de compromiso basado en hash rápido y lo combinó con Spartan, dando así la primera variante de Spartan cuya seguridad se basa en funciones de hash estándar.
• Spice (se abre en pestaña nueva), Lasso (se abre en pestaña nueva), Nebula (se abre en pestaña nueva), y luego Twist and Shout (se abre en pestaña nueva) hicieron que las operaciones de memoria en el corazón de un procesador de uso general fuera económica para probar, y Jolt (se abre en pestaña nueva) mostró que combinarlas con Spartan puede probar eficientemente la ejecución de un procesador completo.
• A principios de este año, Vega (se abre en una nueva pestaña) aplicó este enfoque al identificación digital, demostrando los datos de una credencial gubernamental en menos de un décimo de segundo.
• Recientemente, BinarySpartan (se abre en pestaña nueva) ha llevado a Spartan a los campos binarios, donde la lógica del procesador y las funciones de hash estándar pueden expresarse de manera eficiente. BinarySpartan también se basa en Ligerito (se abre en pestaña nueva), un esquema de compromiso al estilo Brakedown con pruebas mucho más cortas, y en el cambio de anillo (se abre en pestaña nueva), lo que hace eficiente el compromiso con vectores de bits.

Cada uno de estos resolvió una parte del problema. El magnetar es donde los fragmentos se unen.

Magnetar

Magnetar es una máquina virtual de conocimiento cero, o zkVM, y ha logrado avances significativos en los tres desafíos al mismo tiempo.

Es de uso general. Magnetar demuestra la ejecución de RISC-V, una arquitectura de procesador abierta con compiladores maduros para cada lenguaje mainstream. Un desarrollador escribe un programa en Rust, Go o C, lo compila como de costumbre y Magnetar lo prueba tal como está escrito. Considere lo que esto significa en la práctica. Una política empresarial, una tubería de datos o un intérprete para la máquina virtual Ethereum (EVM) son simplemente programas, y los ingenieros que ya lo mantienen pueden demostrar que su ejecución es exactamente como está escrito. Como resultado, la demostración deja de ser una actividad especializada.

Es más rápido que los sistemas anteriores de la misma categoría. Magnetar demuestra 7.2 a 8.7 millones de instrucciones del procesador por segundo en un portátil. En 15 programas de benchmark, desde el cifrado de hash hasta las transferencias de tokens dentro de un pequeño intérprete EVM, es en promedio 10 a 39 veces más rápido que los zkVMs más rápidos existentes en la misma máquina, y más de 300 veces más rápido que otros dos en un benchmark de transferencia de tokens. Un Magnetar optimizado demuestra 9.5–12.8 millones de ciclos por segundo, lo que aumenta cada aceleración reportada en este texto en aproximadamente 1.3×. Sus pruebas se verifican en unos 12 milisegundos.

Su seguridad se basa en criptografía estándar. Magnetar depende de una función de hash estándar como SHA-256 o SHA-3; son las mismas primitivas que ya protegen los sistemas de todas las organizaciones. No se requieren curvas elípticas, no hay ladrillos, no hay funciones de hash especiales, no hay configuración de confianza, y no hay conjeturas no comprobadas sobre códigos de corrección de errores. Las funciones de hash son las primitivas más estudiadas en el conjunto de herramientas criptográficas, y constituyen la base de las firmas basadas en hashes sin estado, que NIST ha estandarizado como su propia opción conservadora post-quantum. Para un sistema que aún debe ser confiable en muchas décadas futuras, depender únicamente de funciones de hash estándar elimina la necesidad de una migración criptográfica del plan de acción.

La misma decisión de diseño genera un segundo beneficio. Comprobar una prueba de Magnetar consiste principalmente en evaluar funciones de hash estándar y aritmética de campo binario, que son exactamente las operaciones que Magnetar demuestra de manera eficiente. Por lo tanto, verificar una prueba es una tarea ordinaria para él. Esto permite que Magnetar demuestre cálculos de cualquier tamaño, demostrándolos por partes y luego combinando esas partes. También permite que Magnetar demuestre un sistema de larga duración, como un registro o una cadena de bloques.

El artículo técnico proporciona el diseño completo, el análisis de seguridad y las mediciones.

Mirando hacia el futuro

Magnetar avanza las pruebas de conocimiento cero y el cómputo verificable hasta un nivel en el que pueden implementarse utilizando la criptografía en la que las organizaciones ya confían, a velocidades que sean accesibles para ingenieros que escriben código normal. Magnetar posibilita un futuro en el que las pruebas criptográficas sean un resultado habitual del cálculo. Esperamos que los líderes tecnológicos dejen de preguntar si las pruebas de ejecución son prácticas y en cambio, concentrarse en cuyos resultados haría Prefieren verificar antes que aceptar confianza.

Si está interesado en explorar cómo las pruebas de conocimiento cero pueden apoyar su caso de uso, nos encantaría escucharlo (se abre en una pestaña nueva).