Mooly Sagiv, científico jefe de Certora: la seguridad de la cadena de bloques es algo más que código

La segunda idea errónea de Sagiv es la que la mayoría de los usuarios quieren creer: que “auditado” implica seguridad.

“Nunca es totalmente seguro. We can make it safer… but it’s never fully safe.”

Las auditorías son sin duda una parte integral de la cripto seguridad, pero no son en absoluto una garantía. La gente desarrolla una falsa sensación de seguridad una vez que ven que una aplicación ha sido auditada, pero los usuarios DeFi ciertamente shouldn’t olvidar las prácticas básicas de seguridad.

El enfoque híbrido de la seguridad de Certora

Sagiv no descarta las auditorías. De hecho, se opone explícitamente a la idea de que la verificación formal sustituya a la revisión humana. En lugar de ello, lo ideal sería que la verificación formal y las auditorías humanas se utilizaran en tándem para proporcionar la mayor cobertura posible.

Hablando con SolanaFloor, Sagiv esbozó cómo las auditorías suelen defender contra patrones de ataque conocidos, mientras que la verificación formal puede reducir la exposición a “desconocidos desconocidos.”

“Cuando usted’está haciendo auditoría, usted está revisando su código [con] su mejor persona contra el ataque conocido. Cuando usted es capaz de hacer la verificación formal… usted tiene algún tipo de [prevención] de unknown[s].”

Esa diferencia importa porque la criptografía es una carrera armamentística. Las técnicas de ataque evolucionan, y los hackers y los ciberdelincuentes siempre están encontrando nuevos métodos y técnicas para romper las aplicaciones multimillonarias que todos usamos a diario.

Se descubren clases completamente nuevas de bugs porque alguien, en algún lugar, encontró una forma inteligente de romper suposiciones que la industria ni siquiera se daba cuenta de que estaba haciendo. El objetivo de la verificación formal es proporcionar otra línea de defensa contra estas "incógnitas desconocidas".

Sagiv describe un patrón que Certora ha visto repetidamente. Los equipos pueden hacer todo “bien”, dedicando enormes recursos internos a la seguridad, contratando auditores de élite, y luego la verificación formal todavía saca a la superficie problemas adicionales de alta gravedad.

“Dejas que el mejor [investigador]de seguridad” encuentre 10 críticos. Estás muy contento. Y luego ejecutas la verificación formal. Encuentra dos más.”

Esta tesis se vio reforzada por Pamina Georgiev, jefa del equipo de verificación formal de Certora, que subió al escenario de Solana Breakpoint para ilustrar la importancia y el impacto de la verificación formal.

A pesar de todas las promesas y la protección que ofrece la verificación formal, aún dista mucho de ser un sistema perfecto. La verificación formal es difícilmente un campo de fuerza impenetrable que detiene a los hackers en su camino, a pesar de lo que ciertos bolsillos de cripto Twitter podrían hacerte creer.

Sagiv es contundente acerca de por qué ese encuadre es peligroso.

“El mayor problema [en] la verificación formal es entender qué propiedad [especificar]”.

La verificación formal no prueba que el código sea seguro en un sentido absoluto. Prueba que el código satisface un conjunto de propiedades; propiedades que le pediste que probara. Si eliges las propiedades equivocadas, acabas con algo que parece extremadamente creíble pero que está lejos de ser hermético.

CI, Automatización, y “Ningún Humano en el Bucle”

Uno de los puntos más claros de Sagiv en Breakpoint es que la seguridad no es un hecho aislado. No porque una aplicación haya superado una auditoría hace varios años seguirá siendo segura hoy en día. Esto es especialmente cierto en criptografía, donde los protocolos y métodos de ataque iteran constantemente y los cambios en una sola línea de código pueden tener repercusiones en otras partes de la pila.

“Cambia por completo, un cambio de una línea puede romper todo el código.”

Por eso Certora introduce la verificación en el flujo de trabajo del desarrollador. Sagiv dice que Certora se integra en los pipelines de CI, por lo que cada nuevo commit dispara las comprobaciones de verificación automáticamente, estableciendo un guardrail continuo en lugar de un hito puntual.

“Cada vez que cambian, hacen un commit en el código, ejecutamos la verificación formal. Esa es realmente la belleza de nuestra herramienta. Nuestra herramienta es automática; el humano no está en el bucle.”

Certora mantiene documentación dedicada para la verificación formal de programas Solana, con el “Certora Solana Prover” diseñado para verificar contratos inteligentes Solana escritos en Rust.

Cypherpunks & Academia

A diferencia de muchas historias de origen criptográfico, que a menudo tienen sus raíces en un ethos cypherpunk, anti-establecimiento, Sagiv trae un poco de clase académica muy necesaria para la industria. Describe su transición desde el mundo académico como una colisión entre el desafío intelectual y los retos del mundo real.

“La criptografía es el único ámbito en el que un código pequeño tiene mucho valor”

La criptografía es el único ámbito en el que un código pequeño tiene mucho valor.

En el software tradicional de seguridad crítica, el código puede ser masivo, pero suele ser antiguo, estable y la antítesis completa de la rápida iteración de la criptografía. Esto puede haber servido de base para uno de los eslóganes favoritos de Certora: "Muévete rápido y no rompas nada".

Sagiv considera que la criptografía encaja a la perfección con los métodos formales porque gran parte de ella es inherentemente matemática: equilibrios, invariantes, restricciones de conservación, reglas de control de acceso y transiciones de estado que pueden expresarse con precisión.

“Sigo dando conferencias académicas. A algunas personas no les gusta la criptografía. Intento motivarles en el aspecto técnico. Vuelvo a lo técnico, y les digo lo que es un reto.”

Aunque sus colegas académicos se muestren escépticos con el cripto, Sagiv subraya que el cripto es una de las áreas de la informática más estimulantes y motivadoras para los desarrolladores emergentes.

Solana’s “Can-Do Attitude”

Certora no es en absoluto una empresa de seguridad exclusiva de Solana, pero eso no significa que la compañía no esté profundamente entrelazada en la escena DeFi de la cadena. Después de haber trabajado con algunas de las aplicaciones más grandes e influyentes de Solana, Sagiv ofrece al ecosistema un nivel de respeto operativo que sólo se obtiene al codearse con los mejores equipos.

El primer compromiso de Certora con Solana fue con Squads, a quienes Sagiv califica de “increíbles.” A partir de ahí, Certora trabajó con la Fundación Solana y verificó las propiedades de los programas SPL, describiendo la colaboración como inusualmente receptiva.

Certora ha trabajado con la Fundación Solana y ha verificado las propiedades de los programas SPL.

Lo que más destaca es su comparación con otros entornos. Refiriéndose a su experiencia con Solidity Developers, Sagic señaló que los equipos pueden resistirse a los cambios.

“Cuando hablamos con la gente, a veces en Solidity, les pedimos que cambien código son muy reacios. Dicen que tenemos una cantidad limitada de tiempo… Aquí [Solana] la gente tiene más una actitud de ‘puedo hacerlo’. Si les pides que cambien el código, son muy directos”

Amenazas a la seguridad en 2026

Cuando se le preguntó sobre las mayores amenazas que la gente debe tener en cuenta en 2026, Sagiv destacó una vez más que la gente no debería’centrarse demasiado en las vulnerabilidades del código. Una buena seguridad operativa es una bestia multifacética, y el poseedor medio de criptomonedas tiene muchas más probabilidades de ser víctima de la ingeniería social o de un error de custodia que de perder fondos en un exploit DeFi.

“Estamos viendo todo tipo de cosas que suceden, it’s no sólo el código.