A segurança do código de contratos inteligentes é de extrema importância para a indústria de blockchain. Contratos inteligentes contêm as implementações de DAOs, tokens, NFTs, serviços DeFi e outras aplicações e ativos de blockchain, e são frequentemente alvo de explorações deliberadas por atacantes, além de serem fontes de consequências potencialmente desastrosas devido a erros de programação inadvertidos.
Por pelo menos 50 anos, o campo da verificação formal tem oferecido aos programadores a visão tentadora de encontrar automaticamente bugs e vulnerabilidades em aplicações usando lógica formal e matemática.
A verificação formal de contratos inteligentes atraiu considerável interesse como uma forma de aumentar a segurança do código de contratos inteligentes em plataformas de blockchain como Ethereum e em linguagens como Solidity. Em contraste com o código de propósito geral, o código de contratos inteligentes é singularmente adequado aos métodos de análise estática e verificação formal.
Esta apresentação abordará a verificação formal de contratos inteligentes em C# na plataforma de blockchain Stratis usando a ferramenta de análise estática e verificação formal Silver. Stratis é uma plataforma de blockchain modular de código aberto implementada em C# que fornece um livro-razão distribuído e um ambiente para executar contratos inteligentes escritos em C# usando o .NET CLR como a VM de contratos inteligentes.
Silver analisa contratos inteligentes Stratis tanto no nível de código-fonte quanto no nível de bytecode e utiliza o framework de programação Spec# criado pela Microsoft Research para verificar formalmente o código de contratos inteligentes em C#.
Os tópicos que abordarei são:
* Visão geral dos conceitos básicos de blockchain e contratos inteligentes
* Visão geral da plataforma de blockchain Stratis e do ambiente de contratos inteligentes em C#
* Breve visão geral do ecossistema do compilador C# Roslyn
* Visão geral da ferramenta de linha de comando Silver e do plugin Visual Studio Roslyn
* Análise estática do código .NET CIL
* Breve visão geral da verificação formal
* Visão geral do sistema de programação Spec#
* Reaproveitamento do Spec# para C# moderno usando reescritores de código-fonte Roslyn
* Casos de uso da verificação formal - analisando diferentes vulnerabilidades de contratos inteligentes e como a verificação formal pode abordá-las
Confira mais de nossos palestrantes e palestras em