Etiquetas nutricionales para la confianza

Traducción automática del original en inglés, todavía sin revisar. Leer el original.

El hombre de la pintura al principio de esta página está haciendo el trabajo de verificación más viejo que existe. Pesa cada moneda en una balanza, de a una, porque la cara estampada en una moneda es una afirmación y su peso es la evidencia, y un cambista que confundía las dos se fundía. No confía en la casa de moneda. Confía en la balanza.

Quinientos años después, casi todo nuestro software nos pide que confiemos en el sello. Viene con un nombre, un logo, una frase tranquilizadora sobre seguridad, y ninguna balanza por ningún lado. La cuenta por confiar en el sello llega en forma de backdoors en la cadena de suministro (supply chain), dependencias que nadie auditó e insignias de “verificado” que resultaron significar una revisión de marketing, y suele llegar tarde y toda junta.

Vitalik Buterin puso la balanza que falta en una sola oración:

En un mundo ideal, todo el software y el hardware tendrían “etiquetas nutricionales” con la lista completa de dependencias de confianza: en qué matemática y en el comportamiento honesto de qué actores (y en qué escala de tiempo) se apoya el sistema para dar su funcionalidad central y las garantías implícitas.

Vitalik Buterin (@VitalikButerin)

binji respondió con la objeción obvia, y después con algo más interesante:

aunque esto existiera, igual podría terminar generando una carga cognitiva que muchos ignorarían, así que seguirían eligiendo sistemas que preseleccionan por ellos. lo ves con las etiquetas nutricionales y las dietas, etc., donde la mayoría prefiere la comodidad de que le den una canasta de “cosas para comer” de una fuente verificada (médicos, nutricionistas… influencers).

pero acá es donde el mundo agéntico se pone interesante: a medida que la ia se vuelve la nueva ui, va a ser clave la necesidad de agentes que preserven la privacidad, personalizados según las preferencias de cada usuario, que puedan manejar la carga cognitiva para complementar sus decisiones mientras prueban con lógica verificada cómo llegan a esa conclusión.

se siente como una gran oportunidad de intersección en general, y es una mezcla de verificación, privacidad, toma de decisiones asistida por agentes e higiene general de la web

binji (@binji_x)

Ese intercambio divide el problema de manera limpia. Vitalik pide el artefacto: ¿de qué depende este sistema? binji pregunta quién se supone que lo va a leer sin convertir a cada usuario en un ingeniero de seguridad. Concrete, el lenguaje de programación sobre el que vengo escribiendo, está entre esas dos preguntas. No resuelve todo. Construye la parte que nunca debería haber sido prosa.

#Dos tipos distintos de confianza

La etiqueta de Vitalik en realidad pide dos listas. Una es técnica: ¿en qué pruebas, componentes, llamadas externas, permisos y máquinas se apoya este sistema? La otra es social: ¿qué personas o instituciones tienen que comportarse honestamente, y por cuánto tiempo?

No son el mismo problema. Concrete trabaja sobre la primera lista. No dice nada profundo sobre incentivos, colusión, gobernanza, o si algún actor se mantiene honesto durante seis meses. Pero la lista técnica ya es suficiente trabajo, y es la parte que un compilador puede producir de verdad.

#Una etiqueta generada por el compilador

Concrete está construido alrededor de un hábito simple: cuando el programa hace una afirmación, el compilador debería guardar el comprobante. Un contrato, una capability, una frontera trusted, un chequeo de seguridad en tiempo de ejecución: cada uno se vuelve algo sobre lo que la herramienta puede reportar. Compilar debería dejar más que un binario. Debería dejar un registro de lo que el programa usó y de qué evidencia respalda cada afirmación.

Ese registro tiene campos reales, no eslóganes. Una porción chica podría verse así:

function: parse_config
capabilities: File
trusted_boundaries:
  - trusted extern fn os_read
obligations:
  O1 array_bounds buffer[i]
     evidence: proved_by_kernel_decision
     engine: omega
  O2 ensures result_is_valid_config
     evidence: assumed
  O3 proof link Config.Proofs.parse_config_shape
     evidence: stale
     reason: body fingerprint changed
tcb:
  - Concrete checker
  - Lean kernel
  - proof attachment and fingerprint machinery
  - LLVM/backend/runtime/OS/hardware

La sintaxis de arriba es ilustrativa, pero las categorías son reales: autoridad, frontera trusted, obligación, clase de evidencia, prueba desactualizada (stale), base trusted. La etiqueta sale del programa y de los artefactos de prueba. Nadie la escribe después como un párrafo de compliance.

Capabilities. Concrete registra los efectos como un vocabulario visible de capabilities: los permisos concretos File, Network, Process, Console, Clock, Random, Env, Alloc y Unsafe, más una macro Std que se expande al conjunto estándar y alias definidos por el usuario que se expanden en tiempo de parseo. Una función sin anotación es pura. Una función que hace asignación de memoria (allocation) en el heap tiene que decir with(Alloc). Una función que toca la red tiene que decir with(Network), y lo mismo todo lo que la llame de forma transitiva. La etiqueta no puede reportar de menos, porque un programa que usa un efecto que no declaró no compila.

Fronteras trusted. Cada lugar donde el programa sale de lo que el checker puede garantizar está marcado y se puede ubicar: trusted fn, trusted impl, trusted extern fn, y las funciones o llamadas que llevan with(Unsafe). Le podés pedir al compilador que las enumere, y te responde con una lista y rangos de código fuente (source spans) en lugar de encogerse de hombros. “Hace trucos con punteros internamente” y “puede llamar código externo arbitrario” son riesgos distintos, y tienen marcadores distintos.

Clases de evidencia. Mi detalle favorito es que no hay una única tilde verde. Cada obligación dice cómo se justifica: proved_by_lean para un teorema verificado por el kernel, proved_by_kernel_decision para un procedimiento de decisión, solver_trusted para el resultado de un solver externo, tested_by_oracle, assumed, trusted, stale, unproven, y más. “Esto pasa el type checker”, “esto está probado” y “acá estamos confiando en el autor” son afirmaciones distintas. Concrete las mantiene separadas. Es la distinción del cambista devuelta al software: la moneda que pesaste, la que no, y la que elegís aceptar de buena fe.

Nada de eso es pseudocódigo, así que acá está la mitad de autoridad en Concrete real. Una llamada externa es una frontera con nombre y auditada; una función que toca la consola tiene que decirlo; y el requisito sube solo por el grafo de llamadas:

trusted extern fn putchar(c: i32) -> i32;        // foreign boundary, audited

fn print_int(n: i64) with(Console) { /* ... */ } // needs Console
fn greet() with(Console) { print_int(42); }      // inherits it from print_int
fn main() with(Std) -> Int { greet(); return 0; }

Borrá with(Console) de greet y el programa deja de compilar, porque greet llama a algo que lo necesita. La autoridad no es un comentario que puede quedar desactualizado. Es parte del tipo, y se vuelve a verificar en cada edición.

#La etiqueta lleva pruebas, no solo declaraciones

Una pantalla de permisos dice que una app puede usar la red. Un software bill of materials dice que un binario contiene cierta biblioteca en cierta versión. La etiqueta de Concrete puede decir algo que una lista de dependencias no puede: que una propiedad específica de una función específica fue probada mecánicamente, y con qué.

El mecanismo es el diseño por contrato de siempre, apuntado a la verificación. Una función lleva cláusulas #[requires] y #[ensures] e invariantes de ciclo. Cada una se vuelve una obligación de prueba con un identificador estable. Una precondición se asume a la entrada de la función y se expone en cada llamador, así que no se puede descartar en silencio; según la política activa, el llamador o la descarga o carga con una obligación explícita sin probar.

Cómo se descarga es donde la versión de marketing normalmente empezaría a mentir. Concrete pone el kernel primero. Los procedimientos de decisión omega, para aritmética entera lineal, y bv_decide, para vectores de bits, producen certificados que se verifican dentro del toolchain, así que usarlos no suma ningún solver externo a la base trusted. Pero las salvedades siguen a la vista. bv_decide depende de un checker LRAT compilado, lo que trae un nivel con nombre de confianza en código nativo; no es reducción pura del kernel, y el inventario de axiomas lo dice. Concrete también puede pasarle una condición a un solver SMT externo. Cuando lo hace, el resultado se etiqueta solver_trusted, y ese binario del solver pasa a ser parte de la base trusted para esa obligación. La confianza no desapareció. La etiqueta te dice qué tipo de confianza acabás de usar.

concrete prove es el flujo de trabajo que hace esto usable. Genera un workspace de pruebas en Lean para una función, vincula los teoremas registrados con sus obligaciones, y soporta replay para que una prueba quede atada al código fuente exacto contra el que se escribió. Una huella (fingerprint), hoy un SHA-256 truncado sobre la estructura de la función, detecta cuando el código se mueve por debajo de su prueba, y la clase de evidencia pasa a stale. La etiqueta no puede seguir diciendo “probado” sobre una función que cambió desde entonces.

Acá está la mitad de pruebas en código real, igual de chica. Una rotación de bits cuya precondición dice que el desplazamiento tiene que quedar dentro del rango:

#[requires(0 <= n && n < 32)]
fn rotr(x: u32, n: u32) -> u32 {
    return (x >> n) | (x << (32 - n));
}

Ese #[requires] no es un comentario ni un assert en tiempo de ejecución. El compilador lo convierte en una obligación, la empuja a cada llamador, y después reporta, un punto de llamada a la vez, cómo cada llamada la descarga:

call rotr(x, 13)       requires 0 <= n && n < 32   ->  proved_at_callsite
call rotr(x, n) [n=7]  requires 0 <= n && n < 32   ->  proved_by_kernel_decision (bv_decide)
call rotr(x, 40)       requires 0 <= n && n < 32   ->  failed_at_callsite
call rotr(x, k)        requires 0 <= n && n < 32   ->  unproven_at_callsite

Cuatro llamadas, cuatro veredictos honestos. Una constante dentro del rango se reduce a probada. Un valor fijado antes por un let se le pasa a un procedimiento de decisión y se cierra con evidencia verificada. Una constante fuera de rango se reporta como violación, y la política puede convertir eso en una falla dura. Un argumento que el compilador no puede precisar queda unproven, etiquetado exactamente así, nunca redondeado en silencio a que está todo bien. La última línea es la que más importa: la etiqueta prefiere decirte que no sabe antes que contarte una mentira reconfortante. Es el cambista que aparta una moneda porque la balanza no fue concluyente, en lugar de dejarla pasar.

Volvamos al ejemplo de la configuración. El hecho útil no es que el programa esté “verificado”. Es que su autoridad File es visible, que se verifica que no tiene autoridad Network ni Alloc, que su frontera con el sistema operativo tiene nombre, que una obligación de límites la descarga omega, que una afirmación semántica de parseo está solo assumed, y que una prueba vieja quedó stale. Seis hechos, seis tipos distintos de confianza, ninguno colapsado en una tilde. Aprendés más de eso que de una insignia verde de “verificado”, justamente porque te muestra dónde la insignia habría estado mintiendo.

La palabra “verificado” tiene que mantenerse disciplinada. Las capabilities y las fronteras las impone o las reporta el sistema de tipos. Eso es útil, pero no es lo mismo que una prueba. Un contrato que llega a proved_by_lean o proved_by_kernel_decision tiene detrás un argumento verificado por máquina. La etiqueta mantiene esos casos separados para que lo impuesto no se haga pasar por probado.

#La etiqueta se incluye a sí misma

La mejor parte es que Concrete se aplica la misma sospecha a sí mismo. Imprime la trusted computing base: las capas en las que tenés que confiar para que cualquier prueba signifique algo. El checker y el compilador. El kernel de Lean. La maquinaria de vinculación de pruebas y de huellas. El backend LLVM. El runtime, el sistema operativo, el hardware. Y el código externo detrás de cada extern fn. La mayoría de los sistemas esconden esta lista. Concrete la imprime.

Ken Thompson dio la razón en su conferencia del Premio Turing de 1984. No podés confiar del todo en código que no escribiste vos mismo, y la podredumbre puede llegar hasta el compilador: un compilador puede llevar un backdoor que sobrevive incluso después de que su propio código fuente quede limpio, reconociendo cuándo se está compilando a sí mismo y reinsertando el truco en silencio. Eso no hace que la confianza sea imposible. Significa que “confiá en mí, el compilador está limpio” no es una respuesta. Tenés que nombrar a qué te compromete confiar en el compilador. Un compilador que imprime su propia base trusted y los axiomas en los que se apoyan sus pruebas es la pregunta de Thompson respondida en voz alta en lugar de esquivada.

Hasta imprime los axiomas. Un control de inventario de axiomas corre sobre cada teorema y hace fallar el build ante cualquier cosa no documentada. Los supuestos matemáticos en los que las pruebas tienen permitido apoyarse tienen nombre: propext, Classical.choice, Quot.sound, y el nivel marcado de confianza en código nativo para la verificación de certificados compilados. Esa es la respuesta literal al “en qué matemática te estás apoyando” de Vitalik, extraída automáticamente en lugar de declarada en un README.

La etiqueta también se puede regenerar. Mismo código fuente, mismos reportes. concrete diff compara dos versiones y avisa cuando la confianza se debilita, cuando una prueba queda desactualizada, cuando la autoridad escala, cuando una frontera se erosiona. Una etiqueta que podés regenerar y comparar es evidencia. Una que no, es marketing.

#Lo que no cubre

Esta es la parte que prefiero decir yo antes de que me la marques vos.

Concrete no modela para nada la segunda mitad de la etiqueta de Vitalik. No hay noción de actores, incentivos, colusión, honestidad hasta cierto momento, ni confianza social en ningún lado. Su contabilidad es estática, sobre en qué capas y en qué matemática confiar, no dinámica, sobre qué humanos se portan bien y por cuánto tiempo. La mitad de actores y escalas de tiempo es un problema real y separado, y le corresponde al diseño de mecanismos y a la economía, no a un lenguaje de sistemas.

La verificación también es parcial, y la etiqueta lo dice. Las pruebas se vinculan al nivel del contrato y del modelo de prueba, sobre una representación intermedia y un modelo idealizado de enteros. La cadena desde ahí, pasando por el backend, hasta el binario final es trusted, no verificada, y la corrección del binario figura abiertamente entre las cosas que Concrete declara explícitamente que no afirma. Muchas obligaciones todavía están missing o terminan en una prueba de Lean escrita a mano en lugar de una descarga automática.

Así que la afirmación no es “Concrete prueba que tu programa es correcto de punta a punta”. Es más chica y más útil: Concrete prueba afirmaciones seleccionadas sobre su modelo de prueba, y después te dice qué propiedades están probadas, con qué, en qué base trusted se apoyan, y qué propiedades no están probadas en absoluto. Eso vale más que una insignia verde.

#Quién lee la etiqueta

La objeción de binji es correcta y sobrevive incluso a una etiqueta perfecta. Las etiquetas generan carga cognitiva, la mayoría de la gente las ignora, y termina recurriendo a una canasta armada por alguien en quien confía. Pasa con las etiquetas de los alimentos y con las dietas, y pasaría también con las etiquetas de confianza. Un manifiesto que nadie lee es decoración.

Pero su respuesta apunta al tipo de artefacto que produce Concrete. Quiere agentes que carguen con el peso cognitivo mientras muestran lógica verificada para sus conclusiones. Para que eso funcione, el agente necesita hechos estructurados que no haya inventado él.

La etiqueta de Concrete la puede consumir una máquina. Tiene identificadores, rangos de código fuente, dependencias y clases de evidencia. Un agente la puede leer directamente. La carga cognitiva que le preocupa a binji es un problema para un humano mirando una pared de hechos, no para un software que filtra esos hechos según la política de un usuario.

Y las conclusiones más fuertes de Concrete llegan con pruebas que el kernel ya verificó, o con etiquetas explícitamente más débiles cuando no. binji quiere que el agente pruebe la lógica detrás de su recomendación. Con Concrete, la evidencia de prueba que sostiene todo se verificó de forma independiente de cualquier agente. No hace falta confiar en que el agente produzca esa evidencia. Solo tiene que señalar evidencia que ya existe y que no puede falsificar sin cambiar el artefacto.

#La confianza debería venir del artefacto, no del agente

Esto cambia el rol del agente. La historia habitual hace del agente la cosa en la que tenés que confiar: alinearlo, auditarlo, creerle. Concrete empuja parte de la confianza hacia abajo, al artefacto. El trabajo del agente pasa a ser más chico. Lee hechos que no puede falsificar fácilmente y les aplica la política del usuario.

La división es simple. Concrete produce la entrada verificada. El agente aplica las preferencias del usuario. El kernel de Lean ancla la evidencia más fuerte. Las capas trusted que quedan tienen nombre en lugar de estar escondidas. El agente sigue sin ser magia, pero al menos está leyendo hechos anclados fuera de sí mismo.

Una línea más para no venderlo de más. Concrete responde el problema de la entrada: hechos confiables sobre un artefacto. No responde el problema de alineación: si el agente sirve fielmente al usuario. Puede hacer que las entradas del agente sean más difíciles de falsificar. No hace que el agente sea bueno.

#Los ingredientes, no solo el plato

Todo lo de arriba etiqueta un programa que escribiste vos. Pero la dependencia de confianza que de verdad muerde es la que no escribiste: el parser que en silencio empieza a escribir logs a disco, el helper de hash que agrega una llamada de red “para telemetría”, la dependencia cuya prueba se degrada en silencio entre versiones. La frase de Vitalik es “una lista completa de dependencias de confianza”, y en la práctica tus dependencias son tus imports. La canasta de ingredientes de binji es la lista de imports.

Las notas de diseño de Concrete dan el paso siguiente, y quiero ser exacto: esta parte está escrita como una dirección, todavía no está implementada. El principio es que un import no debería otorgar poder en silencio. Debería decir qué trae y qué tiene prohibido traer. Así que un import lleva un techo y un piso:

import std.parse      requires(no File, no Network, no Unsafe)
import hmac.compute   requires(proved_by_lean)
import crypto.compare requires(constant_time, no secret_sink)

y un manifiesto fija un presupuesto de autoridad para todo el proyecto:

[authority]
allowed = ["Alloc"]
forbidden = ["File", "Network", "Process", "Unsafe"]

Ahora el desvío falla cerrado. Si el parser gana autoridad File, o la evidencia del helper de hash baja de proved_by_lean a assumed, el build se detiene y exige un cambio explícito en la restricción. Ese es el backdoor en la cadena de suministro del principio de este post, atrapado en tiempo de compilación en lugar de explicado en un postmortem.

Las capabilities, los contratos y las clases de evidencia existen hoy; los imports acotados y los presupuestos de autoridad son un diseño en papel, no una funcionalidad que puedas correr. Pero la dirección es lo central, porque es donde la etiqueta deja de describir un programa y empieza a describir todo el árbol de dependencias, que es el único nivel en el que “una lista completa de dependencias de confianza” es realmente cierto.

#Las etiquetas deberían ser artefactos del compilador

Las etiquetas de confianza del software no deberían ser prosa del proveedor. Deberían ser artefactos del compilador: deterministas, comparables con diff, y respaldados por evidencia verificada por máquina en todos los lugares donde se hacen las afirmaciones fuertes. Concrete muestra cómo se ve eso para capabilities, contratos, obligaciones de prueba, clases de evidencia, axiomas y fronteras trusted. Es el mismo argumento que un compilador que produce hechos y cuando el compilador es el oráculo, apuntado a una conversación que está pasando en otro lado.

El mundo de los lenguajes de sistemas y el mundo de la confianza cripto están dando vueltas alrededor del mismo objeto desde lados opuestos. Uno quiere que el software emita un manifiesto verificable de lo que depende. El otro quiere un lenguaje donde ese manifiesto salga de la compilación. Concrete no resuelve la mitad de los actores honestos, y no pretende hacerlo. Toma la mitad que se puede mecanizar y la mecaniza: la parte que el CI puede rechazar, que un revisor puede comparar con diff, y sobre la que un agente se puede parar sin pedir que le crean.