Die Ethereum-Blockchain ist die bekannteste Plattform, die die Ausführung von Smart Contracts im Zuge von Transaktionen ermöglicht. Ein Smart Contract ist ein Programm, welches beschreibt, wie der durch die Blockchain geführte Zustand angepasst werden soll. Im Rahmen seiner Ausführung kann ein Smart Contract auch andere Contracts aufrufen oder erzeugen. Fehler in der Implementierung eines Smart Contracts können zu einem inkonsistenten oder unerwarteten Zustand des Smart Contracts führen, was katastrophale finanzielle Konsequenzen haben kann. Wir präsentieren daher multeThor, ein Tool zur statischen Analyse, welches in der Lage ist, Abfragen bezüglich der Erreichbarkeit bestimmter Ausführungszustände von Smart Contracts zu beantworten. Um mit statisch unbekannter Information umgehen zu können, nutzen wir Techniken der abstrakten Interpretation. Die Implementierung der Analyse nutzt dann eine abstrakte Variante der Bytecode-Semantik von Ethereum Smart Contracts, die durch Resolution von Horn-Klauseln automatisch ausgeführt werden kann. Während einer Präanalyse versucht das Tool, andere Contracts, die aufgerufen werden können, konkret zu bestimmen. Danach wird der Bytecode solcher Aufrufziele automatisch heruntergeladen und schlussendlich in späteren Phasen der Analyse eingebunden. Das erlaubt es, die Effekte von Aufrufen bekannter Contracts präziser zu bestimmen, und ermöglicht im Besonderen eine brauchbare Analyse von Contracts mit Bibliotheksaufrufen. Eine wesentliche Eigenschaft von multeThor ist dessen Korrektheit, womit gemeint ist, dass das Tool stets eine Abstraktion eines erreichbaren Ausführungszustands ableitet. Dadurch kann multeThor genutzt werden, um die Abwesenheit problematischer Ausführungszustände zu beweisen. Wir legen eine Beweisskizze vor, um die Korrektheit von multeThor formal zu zeigen. Mittels einer experimentellen Evaluierung, basierend auf einem aus Contracts der Ethereum-Blockchain bestehenden Datensatz, demonstrieren wir, dass multeThor genutzt werden kann, um die generische Sicherheitseigenschaft Single-Entrancy nachzuweisen. Wir vergleichen die Ergebnisse auch mit jenen des vorhergehenden Tools eThor, dessen Analyse lediglich auf dem Bytecode des einzelnen analysierten Contracts basiert. Im Besonderen beobachten wir, dass multeThor die Single-Entrancy-Eigenschaft für eine höhere Anzahl an Instanzen erfolgreich beweisen kann, was empirisch zeigt, dass dessen Analyse präziser als jene von eThor ist. Schlussendlich demonstrieren wir anhand eines Beispiels die Fähigkeit von multeThor, funktionale Korrektheitseigenschaften von Contracts mit Bibliotheksaufrufen zu verifizieren.
de
The Ethereum blockchain is the most prominent platform that enables the execution of smart contracts as part of transactions. A smart contract is a program which describes how the state maintained by the blockchain should be updated. As part of its execution, a smart contract may also call or create other contracts. Bugs in the implementation of a smart contract can lead to an inconsistent or unexpected contract state, which may have catastrophic financial consequences. We hence present multeThor, a static analysis tool which is able to answer queries regarding the reachability of certain execution states of smart contracts. In order to deal with statically unknown information, we use techniques from abstract interpretation. The implementation of the analysis then uses an abstract variant of the bytecode semantics of Ethereum smart contracts, which can automatically be executed through Horn clause resolution. During a preanalysis, the tool aims to concretely determine other contracts that may be called. Thereafter, the bytecode of such call targets is automatically downloaded and ultimately incorporated in later stages of the analysis. This allows to more precisely determine the effects of calls to known contracts and especially enables a reasonable analysis of contracts with library calls. One key property of multeThor is its soundness, which means that the tool always derives an abstraction of a reachable execution state. Therefore, multeThor can be used to prove the absence of problematic execution states. We provide a proof sketch to formally show the soundness of multeThor. Through an experimental evaluation on a dataset consisting of contracts obtained from the Ethereum blockchain, we demonstrate that multeThor can be used to verify the generic security property single-entrancy. We also compare the results with those of the previous tool eThor, whose analysis is solely based on the bytecode of the single analyzed contract. In particular, we observe that multeThor can successfully prove the single-entrancy property for a higher number of instances, which empirically shows that its analysis is more precise than that of eThor. Finally, by means of an example, we demonstrate the ability of multeThor to verify functional correctness properties of contracts with library calls.
