Die Sicherheit von Smart Contract-Code hat für die Blockchain-Branche oberste Priorität. Smart Contracts enthalten die Implementierungen von DAOs, Tokens, NFTs, DeFi-Diensten und anderen Blockchain-Anwendungen und -Vermögenswerten und sind sowohl häufig Ziel von gezielten Angriffen als auch Quellen potenziell katastrophaler Folgen aufgrund unbeabsichtigter Programmierfehler.
Seit mindestens 50 Jahren bietet das Gebiet der formalen Verifikation Programmierern die verlockende Vision, Bugs und Schwachstellen in Anwendungen automatisch mithilfe formaler Logik und Mathematik zu finden.
Die formale Verifikation von Smart Contracts hat erhebliches Interesse geweckt, um die Sicherheit von Smart Contract-Code auf Blockchain-Plattformen wie Ethereum und in Sprachen wie Solidity zu erhöhen. Im Gegensatz zu allgemeinem Code eignet sich Smart Contract-Code besonders gut für die Methoden der statischen Analyse und formalen Verifikation.
Diese Präsentation wird sich mit der formalen Verifikation von C# Smart Contracts auf der Stratis-Blockchain-Plattform unter Verwendung des Silver-Tools für statische Analyse und formale Verifikation befassen. Stratis ist eine Open-Source-modulare Blockchain-Plattform, die in C# implementiert ist und ein verteiltes Hauptbuch sowie eine Umgebung für die Ausführung von in C# geschriebenen Smart Contracts unter Verwendung der .NET CLR als Smart Contract VM bereitstellt.
Silver analysiert Stratis Smart Contracts sowohl auf Quellcode- als auch auf Bytecode-Ebene und verwendet das von Microsoft Research entwickelte Spec#-Programmierframework, um C# Smart Contract-Code formal zu verifizieren.
Die Themen, die ich behandeln werde, sind:
* Überblick über grundlegende Blockchain- und Smart Contract-Konzepte
* Überblick über die Stratis-Blockchain-Plattform und die C# Smart Contract-Umgebung
* Kurzer Überblick über das C# Roslyn-Compiler-Ökosystem
* Überblick über das Silver-Befehlszeilentool und das Visual Studio Roslyn-Plugin
* Statische Analyse von .NET CIL-Code
* Kurzer Überblick über formale Verifikation
* Überblick über das Spec#-Programmiersystem
* Wiederverwendung von Spec# für modernes C# mithilfe von Roslyn-Quellcode-Umformern
* Anwendungsfälle der formalen Verifikation - Analyse verschiedener Smart Contract-Schwachstellen und wie formale Verifikation diese angehen kann
Weitere Informationen zu unseren Referenten und Vorträgen finden Sie unter