OUSD Completa la Auditoría de Verificación Formal con Certora
El token OUSD ha completado su tercera auditoría de seguridad.
En Origin, creemos en la seguridad a fondo. Más allá de las pruebas unitarias, auditorías internas, fuzzing, auditorías externas y tener una de las recompensas de errores más grandes en el mundo cripto, también hemos traído a Certora para usar el poder de la verificación de software formal avanzada en el contrato de OUSD.
- Auditoría completa de Certora sobre el Token OUSD.
Verificación formal
Los métodos de verificación formales convierten el código en una ecuación matemática gigante que luego se puede resolver para ver si las propiedades particulares son siempre verdaderas.
Trabajar con métodos formales trae un cambio en la perspectiva mental casi tan valioso como la verificación del software en sí.
La forma normal de realizar pruebas es con pruebas unitarias, y cada prueba comprueba que en una única situación específica el código hace lo correcto. Pero con las pruebas/el pensamiento basado en la propiedad, usted se enfoca en las reglas que deben aplicarse a cualquier situación en la que posiblemente se encuentre el contrato, y luego verifica las situaciones que podrían violar esto. Este cambio de pensamiento puede exponer errores que estaban ocultos detrás de las suposiciones que tenía sobre cómo funcionaba el código, o sus suposiciones anteriores sobre situaciones en las que podría estar el código.
Como ejemplo de una regla, puede tomar el siguiente código:
contract Test {
uint256 public counter = 0;
function increment() public {
counter = counter + 1;
}
}Y la siguiente regla simple y obvia de que el contador sólo se hace más grande:
rule counter_only_counts_up {
env e;
uint before = counter();
increment(e);
uint after = counter();
// After should always be bigger than before
assert after > before;
}Y después de que este código se convierta en una ecuación, el probador le dice que esta simple regla en realidad no siempre es cierta. A veces, el contador baja después de una llamada a next (), debido a un desbordamiento matemático.
La experiencia
Hemos tenido una gran experiencia trabajando con el equipo de Certora. La verificación formal para proyectos de blockchain está entrando en el ámbito de lo posible. Es maravilloso trabajar con personas extremadamente inteligentes que piensan profundamente en cómo deberían funcionar nuestros contratos inteligentes, que son capaces de construir y modificar las herramientas para que la verificación funcione y que aportan una nueva perspectiva a la seguridad y la corrección.
El futuro
Este es sólo el comienzo de nuestro compromiso con la seguridad de OUSD. Continuamos trabajando con Certora para verificación adicional y comenzaremos otra auditoría externa completa el próximo mes, agregando OpenZepplin a nuestra lista de auditores de OUSD.
Aprende más sobre Origin:
- Obtén tus primeros OUSD en: www.ousd.com/mint
- Pon en staking tus Tokens de Origin (OGN) y Gana más: ousd.com/stake
- Lanza tu tienda descentralizada: originprotocol.com/dshop
- Compra Tokens de Origin (OGN): Binance, Huobi, Upbit, Bittrex Global
- Sigue las métricas del Token OGN: originprotocol.com/dashboard
- Aprende más sobre nuestra compañía en nuestra página web: originprotocol.com
