En las noticias recientes de TechFlow, la empresa de seguridad blockchain Certora ha completado una revisión de verificación formal de la extensión del token Solana. Utilizaron su herramienta de verificación formal profunda para escribir y verificar propiedades clave del código. Los principales hallazgos del equipo de Certora incluyen: identificar una oportunidad de optimización que puede mejorar el rendimiento del programa en un 20%; desarrollar reglas para fortalecer las medidas de seguridad existentes para las actualizaciones recientes de Solana; escribir especificaciones reutilizables para verificar múltiples instrucciones, descubriendo problemas que no fueron notados previamente por todos los auditores. Específicamente, Certora recomienda no utilizar sol_memcmp, sino adoptar el método de comparación independiente de la plataforma de Rust, lo que reduce las unidades computacionales de la instrucción TransferChecked en aproximadamente un 20%. Además, la verificación de Certora también descubrió y confirmó una solución para un problema de consistencia que involucra transferencias no verificadas y transferencias verificadas. Finalmente, el equipo encontró una falta de correcciones para las instrucciones de transferencia en las instrucciones de quemado (Burn y BurnChecked), lo cual ha sido reconocido y corregido por los desarrolladores de SPL.

Deep Tide TechFlow News, la empresa de seguridad blockchain Certora ha completado recientemente la revisión de verificación formal de la extensión del token Solana, utilizando su herramienta de verificación formal profunda para escribir y verificar las propiedades clave del código. Los principales hallazgos del equipo de Certora incluyen: identificar una oportunidad de optimización que puede mejorar el rendimiento del programa en un 20%; desarrollar reglas para verificar las actualizaciones recientes del equipo de Solana para fortalecer las medidas de seguridad existentes; escribir especificaciones reutilizables para verificar múltiples instrucciones, descubriendo problemas que no fueron notados previamente por todos los auditores. Específicamente, Certora recomienda no utilizar sol_memcmp, sino adoptar el método de comparación independiente de la plataforma proporcionado por Rust, lo que reduce las unidades computacionales de la instrucción TransferChecked en aproximadamente un 20%. Además, la verificación de Certora también descubrió y confirmó una solución para un problema de consistencia que involucra transferencias no verificadas y transferencias verificadas. Finalmente, el equipo encontró una falta de correcciones para las instrucciones de transferencia en las instrucciones de quemado (Burn y BurnChecked), lo cual ha sido confirmado y corregido por los desarrolladores de SPL.

Certora ha completado la verificación formal de la extensión del token de Solana, descubriendo múltiples optimizaciones y mejoras de seguridad.