La seguridad del código de contratos inteligentes es de suma importancia para la industria de blockchain. Los contratos inteligentes contienen las implementaciones de DAOs, tokens, NFTs, servicios DeFi y otras aplicaciones y activos de blockchain, y son tanto objeto de ataques deliberados por parte de atacantes como fuentes de consecuencias potencialmente desastrosas debido a errores de programación inadvertidos.
Durante al menos 50 años, el campo de la verificación formal ha ofrecido a los programadores la tentadora visión de encontrar automáticamente errores y vulnerabilidades en aplicaciones utilizando lógica formal y matemáticas.
La verificación formal de contratos inteligentes ha atraído un considerable interés como una forma de aumentar la seguridad del código de contratos inteligentes en plataformas de blockchain como Ethereum y en lenguajes como Solidity. A diferencia del código de propósito general, el código de contratos inteligentes es especialmente adecuado para los métodos de análisis estático y verificación formal.
Esta presentación examinará la verificación formal de contratos inteligentes en C# en la plataforma de blockchain Stratis utilizando la herramienta de análisis estático y verificación formal Silver. Stratis es una plataforma de blockchain modular de código abierto implementada en C# que proporciona un libro mayor distribuido y un entorno para ejecutar contratos inteligentes escritos en C# utilizando el CLR de .NET como la VM de contratos inteligentes.
Silver analiza los contratos inteligentes de Stratis tanto a nivel de código fuente como de bytecode y utiliza el marco de programación Spec# creado por Microsoft Research para verificar formalmente el código de contratos inteligentes en C#.
Los temas que cubriré son:
* Visión general de conceptos básicos de blockchain y contratos inteligentes
* Visión general de la plataforma de blockchain Stratis y el entorno de contratos inteligentes en C#
* Breve visión general del ecosistema del compilador Roslyn de C#
* Visión general de la herramienta de línea de comandos Silver y el plugin de Visual Studio Roslyn
* Análisis estático del código CIL de .NET
* Breve visión general de la verificación formal
* Visión general del sistema de programación Spec#
* Reutilización de Spec# para C# moderno utilizando reescritores de código fuente de Roslyn
* Casos de uso de verificación formal - análisis de diferentes vulnerabilidades de contratos inteligentes y cómo la verificación formal puede abordarlas
Consulta más de nuestros ponentes y charlas destacadas en