Was sind Smart Contracts?
In modernen Blockchain Umgebungen wie Ethereum gibt es das Konzept von Smart Contracts, einer Art ausführbaren Vertrags:
A "smart contract" is simply a program that runs on the Ethereum blockchain. It's a collection of code (its functions) and data (its state) that resides at a specific address on the Ethereum blockchain.
Smart contracts are a type of Ethereum account. This means they have a balance and they can send transactions over the network. However they're not controlled by a user, instead they are deployed to the network and run as programmed. User accounts can then interact with a smart contract by submitting transactions that execute a function defined on the smart contract. Smart contracts can define rules, like a regular contract, and automatically enforce them via the code.
(Quelle: Ethereum.org)
Bei Ethereum laufen diese Contracts in der Ethereum Virtual Machine (EVM). Solidity ist eine objekt-orientierte Hochsprache die zur einfacheren Programmierung verwendet werden kann.
Ein Beispiel für einen einfachen Contract ist folgender, welcher eine einfache Cryptowährung implementiert. Dieser Contract ermöglicht die Schöpfung neuer Münzen und den Geldtransfer:
// SPDX-License-Identifier: GPL-3.0pragma solidity >=0.7.0 <0.9.0;contract Coin { // The keyword "public" makes variables // accessible from other contracts address public minter; mapping (address => uint) public balances; // Events allow clients to react to specific // contract changes you declare event Sent(address from, address to, uint amount); // Constructor code is only run when the contract // is created constructor() { minter = msg.sender; } // Sends an amount of newly created coins to an address // Can only be called by the contract creator function mint(address receiver, uint amount) public { require(msg.sender == minter); require(amount < 1e60); balances[receiver] += amount; } // Sends an amount of existing coins // from any caller to an address function send(address receiver, uint amount) public { require(amount <= balances[msg.sender], "Insufficient balance."); balances[msg.sender] -= amount; balances[receiver] += amount; emit Sent(msg.sender, receiver, amount); }}Dieses Beispiel stammt aus der Dokumentation von Solidity, in welcher sich auch eine weiterführende Beschreibung des Beispiels findet.
Warum brauchen wir Analysen für Smart Contracts?
Analysen von Smart Contracts werden immer wichtiger, da Fehler heute schon zu Verlusten von Millionen an Dollars führen können:
"Finding The Greedy, Prodigal, and Suicidal Contracts at Scale" - In a report from 2018, five researchers published that about 34,200 Ethereum smart contracts worth $4.4 million in Ether contain identified flaws. Over the years, Ethereum got more complex, not less. This means that likely there are more vulnerable contracts than ever before.
(Quelle: G DATA)
Welche Analysen gibt es schon?
Ein Möglichkeit ist Bounded Model Checking, welches zum Beispiel in dem Paper "Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity" von Antonino et al verwendet wird (Binary-Blob):
We make some abstractions that over-approximate the way in which Solidity/Ethereum behave. Based on this formalisation, we create Solidifier: a bounded model checker for Solidity. It translates Solid into Boogie, an intermediate verification language, that is later verified using Corral, a bounded model checker for Boogie.
Hierbei wird Solidity auf Boogie abgebildet, Tools mit vergleichbarem Ansatz sind zum Beispiel Verisol von Microsoft Research und solc-verify:
This is an extended version of the compiler (v0.5.17) that is able to perform automated formal verification on Solidity smart contracts using specification annotations and modular program verification
Boogie ist eine Zwischensprache für die Verifikation. Für die Verifikation von Boogie-Ausdrücken werden SMT Solver wie Z3 verwendet.
Informationsflussanalysen
Hier am Lehrstuhl beschäftigen wir uns hauptsächlich mit Informationsfluss, also mit der Frage, wie viele Informationen in einem Programm zwischen zwei Stellen fließen (im obigen Beispiel zum Beispiel zwischen dem Erzeuger neuer Münzen und dem Ersteller einer Transaktion). Die Idee dieser Arbeit ist nun, eine Analyse für Solidity in diesem Bereich zu entwickeln. Eine beispielhafte Analyse in diesem Bereich wird im Paper "Securing Smart Contracts with Information Flow" von Cecchetti et al beschrieben:
We propose an approach based on information flow control (IFC), which supports fine-grained, compositional security policies and rules out dangerous vulnerabilities. However, existing IFC systems provide few guarantees on interaction with legacy contracts and unknown code. We extend existing IFC constructs to support these important functionalities while retaining compositional security guarantees, including reentrancy control.
Die Abschlussarbeit
Wie die Arbeit konkret ausgestaltet wird ist freigestellt. Eine Idee wäre zum Beispiel die Ideen der vorher beschriebenen, Model Checking basierten, Analysen zu nutzen um eine Quantitative Informationsflussanalyse zu entwickeln. Für C/C++ gibt es solche Analysen bereits, beschrieben zum Beispiel im Paper "Scalable Approximation of Quantitative Information Flow in Programs" von Biondi et al. In diesem Bereich wird am Lehrstuhl auch aktiv Forschung betrieben.
Diese Arbeit ist angelehnt an Forschung im Rahmen von KASTEL und wird ko-betreut von Frederik Reiche (IPD Reussner). Sie ist ein Grünwiesenprojekt, d. h. die verwendete Programmiersprache und Art der Implementierung sind frei.
Schlüsselworte
QIFC Betreuer
| Ehemalige Mitarbeiter |
|---|
| M.Sc. Johannes Bechberger |