Código y Señal AlphaProof: pruebas de seguridad de código máquina verificadas y suposiciones de confianza

Qué cubre este vídeo

• Los agentes de IA producen pruebas candidatas; el kernel de Lean verifica si establecen la afirmación formal aprobada por humanos.
• El objetivo verificado es un arnés CLI de libsignal compilado particular, con semántica de confianza y contratos criptográficos.
• La verificación del binario compilado elimina el compilador de Rust de la base de confianza para las propiedades declaradas de ese binario.
• Los investigadores informan de dos reintroducciones aisladas de errores previamente corregidos que violan su teorema de seguridad simbólico.
• El comparador verifica el teorema y cada definición dependiente contra una especificación aprobada protegida; las enmiendas pasan por un proceso de revisión separado.

Transcripción traducida

Traducido de la narración original en inglés. El audio y los subtítulos disponibles están controlados por YouTube.

¿Quién verifica una prueba de seguridad de IA?

0:00 Una auditoría de seguridad de IA todavía suena como confiar en un chatbot. El nuevo resultado de Signal de Google viene con pruebas matemáticas que un kernel separado verifica. En este video, ¿qué probó Google? ¿Y cómo evitan que un agente cambie los objetivos? Aquí está la respuesta útil. Los modelos escriben pruebas candidatas, y Lean verifica las pruebas contra una afirmación aprobada por humanos sobre código compilado seleccionado. Los humanos siguen siendo dueños de la afirmación y las suposiciones.

0:21 Puedes verificar el resultado sin creer el discurso de victoria del modelo. Una verificación separada detecta el cambio silencioso de la pregunta. Lo seguiremos hasta las definiciones. Es martes, diez de noviembre, y este es The Daily Diff. AlphaProof Code es el marco de Google para escribir especificaciones de software con guía humana y generar pruebas verificadas con agentes de IA. Este estudio se dirige a libsignal, la biblioteca de Rust que implementa el protocolo de mensajería de Signal, dentro de un programa de línea de comandos particular.

0:45 Google anunció el trabajo hoy. Su artículo dice que cinco investigadores trabajaron durante cuatro semanas. Los agentes escribieron las pruebas, mientras que los humanos dedicaron la mayor parte de su esfuerzo a las especificaciones. Los requisitos han encontrado una manera de convertirse en reuniones aún más caras. La especificación dice lo que el programa debe hacer,

¿Cómo se convierte una afirmación en un objetivo de prueba?

0:59 qué controla un atacante y qué suposiciones necesita el argumento. Los revisores preguntan si captura la seguridad que le importa a la gente. Una respuesta bellamente verificada a una pregunta débil deja esa pregunta intacta. El equipo se basa en investigaciones anteriores sobre el handshake de Signal y su ratcheting de clave de mensaje. Los análisis formales ya estudiaron esos diseños. La afirmación de Google conecta sus argumentos de seguridad con una implementación compilada de una biblioteca de producción no modificada, donde el diseño tiene que sobrevivir al contacto con el código real. El director de tecnología de Signal, Ehren Kret, describe una expansión más allá de los alcances más pequeños de verificación anteriores.

1:27 descrive una expansión más allá de los alcances más pequeños de verificación anteriores. Los detalles de implementación incluyen mensajes fuera de orden y sesiones archivadas para mensajes retrasados. El software real guarda los recibos que tu elegante diagrama desechó. Los investigadores compilan la biblioteca Rust sin modificar con el compilador estándar

¿Por qué probar el binario compilado?

1:41 en un ejecutable Arm 64 Linux. Sus teoremas describen ese binario usando un modelo de instrucción formal, abarcando la brecha entre el código fuente y el código máquina optimizado. Un error de compilador que rompa una propiedad declarada haría que su teorema fuera falso. Por lo tanto, el compilador deja la base de confianza para este binario. Todavía confías en el modelo de instrucción y en el verificador de Lean. El límite de confianza se movió y tiene una dirección. Alrededor de seis millones y medio de líneas de prueba verificada se basan en aproximadamente veintiséis mil líneas de especificación y semántica de instrucción de confianza.

2:06 mil líneas de especificación y semántica de instrucción de confianza. Estos son recuentos de artefactos. Tratarlos como puntuaciones de inteligencia es como clasificar a los desarrolladores por el tamaño de su carpeta de módulos de node.

¿Qué propiedades de seguridad sobrevivieron a la brecha de implementación?

2:16 Los argumentos cubren la confidencialidad y autenticación de mensajes, con secreto hacia adelante y seguridad post-compromiso bajo modelos declarados. Esos dos últimos describen límites en el daño por clave robada y la recuperación después de nuevos intercambios. Cada garantía tiene condiciones sobre el atacante y la sesión. Las primitivas criptográficas se encuentran detrás de contratos de confianza. La prueba asume que esas rutinas se comportan como se especifica y se basa en suposiciones de seguridad criptográfica. Una prueba idealiza la criptografía; la otra razona sobre las probabilidades de éxito del atacante. probabilidades de éxito del atacante.

2:42 Ambos tienen restricciones en los escenarios que cubren. Pregunta qué compilación, qué propiedad y qué suposiciones. Este resultado se refiere al arnés de línea de comandos de los investigadores. La mensajería de grupo es trabajo futuro, y el modelo computacional excluye el estado multidispositivo. Llamar a cada instalación de Signal libre de errores se sale del teorema. Los investigadores reintrodujeron dos errores de Signal previamente corregidos en

¿Puede la especificación rechazar código roto?

3:02 copias aisladas y los compilaron. Las pruebas verificadas mostraron que esos binarios violaban el teorema de seguridad simbólica. Eso probó si la especificación podía rechazar implementaciones rotas reales. Tu marca de verificación verde necesita una prueba roja. Google publica las especificaciones y pruebas con instrucciones de verificación. El repositorio dice que una compilación limpia lleva horas y mucha memoria. Leer el anuncio es considerablemente más fácil en el portátil. El modelo de hardware y los contratos de confianza aún necesitan revisión.

3:26 No he reconstruido el enorme artefacto para este episodio. Estamos informando el resultado publicado y sus límites. Los de fuera tienen un camino para inspeccionarlo, lo que me importa más que otra vuelta de victoria de la IA. Ahora la trampa.

¿Puede una prueba correcta responder a la pregunta equivocada?

3:36 Lean puede aceptar una prueba correcta de una declaración que no pide casi nada. Las suposiciones imposibles pueden hacer que un teorema sea vacío. Cambiar una definición enterrada debajo del teorema principal puede debilitar el objetivo. El documento diseña controles contra esto. El guardián mantiene una especificación aprobada retenida a la que los agentes de prueba no pueden escribir. Pueden proponer correcciones a través de un proceso de enmienda separado. El debilitamiento de la seguridad se escala como un posible error. La declaración de éxito del probador no tiene autoridad aquí.

4:00 Los humanos juzgan los cambios en las suposiciones de confianza, directamente o a través de su política, y revisan las enmiendas después de cada campaña. El juicio de expertos permanece en entredicho. El agente puede solicitar una asignación diferente. No puede ponerse una nota de aprobado.

¿Qué atrapa los objetivos cambiantes?

4:13 Aquí está la comprobación prometida. El comparador de Lean compara el teorema y cada definición de la que depende con esa copia aprobada protegida. También verifica los axiomas permitidos y reproduce la prueba en un nuevo kernel. Debilitar silenciosamente una definición auxiliar, por lo tanto, cambia lo que se está comparando. Una prueba aceptada debe establecer el objetivo aprobado. Eso todavía deja a los humanos responsables de elegir un objetivo fuerte y suposiciones honestas. Para tu propio flujo de trabajo de IA, mantén los criterios de aceptación fuera de los

4:37 permisos de edición del trabajador y revisa los cambios propuestos por separado. El resultado de Google hace esa separación concreta. El escritor de pruebas hace el trabajo; el límite de verificación decide si cuenta. Si prefieres leer esto antes que oírme decirlo, el "diff" llega a tu bandeja de entrada cada mañana, gratis en thedailydiff.dev, enlace abajo. Así que el veredicto de hoy es SHIP IT.

¿Implementaría este flujo de trabajo de pruebas?

4:54 Yo implementaría este flujo de trabajo de prueba verificada porque la afirmación aprobada se mantiene separada del agente que produce la respuesta. Mantendría el alcance y las suposiciones adjuntas a cada resultado. Suscríbete, dale a la campana y dime en los comentarios si lo habrías sellado de manera diferente. Y esa es la diferencia de hoy. Soy Niko de Axrisi. Fusiona con responsabilidad.

Fuentes

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub