Automated security analysis of blockchain protocols

Abstract

Blockchain protocols are a popular target for attacks since they manipulate valuable funds while operating in a pseudo-anonymous environment,where “code is law”. That means stealing funds through a loophole in a protocol is considered legal, and the stolen funds can be used unrestrainedly bythe attacker. Such attacks can target different aspects of a blockchain protocol:the implementation, the cryptography, and the incentive structures. When itcomes to ensuring the security of a blockchain protocol, all of them have to be considered. Most existing research on blockchain security focuses on implementation or cryptography aspects. However, blockchain protocols rely heavily on economic incentives to ensure correct execution, and it is hence essential to also study them. Such incentives can be captured using game-theoretic analysis of the behavior of blockchain users.In this thesis, two aspects of blockchain security are addressed. Primarily, a comprehensive framework for game-theoretic security analysis is developed,combining extensive form games, symbolic payoffs, and automated reasoning techniques to rigorously model and evaluate a protocol’s incentive structures.Additionally, this dissertation extends to the security of a protocol’s implementation, proposing methods for formalizing and verifying unbounded summations in blockchain protocols. Thereby, this thesis enables both theoretical and practical advancements in blockchain security.Regarding game-theoretic security, this thesis discusses how to ensure the incentives favor the intended behavior in every case. It provides a formal definition of game-theoretic security and advocates the use of extensive form games with symbolic utilities to model blockchain protocols. This dissertation further presents automation techniques for game-theoretic security analysis, making even the analysis of immense game models feasible. These techniques are implemented in the two versions of the automated game-theoretic security analysis tool CheckMate presented in this thesis. Our tool goes beyond conventional automation and enables piece-wise, so-called compositional automated analysis, allowing for greater scalability.Moreover, approaches that target the security of the implementation have struggled to fully formally capture summation with an arbitrary, unbounded number of summands. In this work, a generalization to Presburger arithmetic is introduced that can express properties about summations. It is further shown how this generalization can be used to formalize verification problems of smart contracts, a specific type of blockchain protocols, thereby enhancing implementation security efforts.

Blockchain Protokolle sind ein beliebtes Ziel für Angriffe, weil sie wertvolle Güter verwalten und in einer pseudoanonymen Umgebung agieren, in der Code “Gesetz” ist. Das heißt Schwachstellen in Protokollen auszunützen, um Gelder zu stehlen, gilt als legal und die gestohlenen Gelder stehen der Angreifer*in uneingeschränkt zur Verfügung. Solche Angriffe können unterschiedliche Aspekte eines Blockchain Protokolls betreffen: die Implementierung, die Kryptographie und die Anreizstrukturen. Um die Sicherheit eines Blockchain Protokolls zu garantieren, müssen alle Aspekte betrachtet werden. Der Großteil der bestehenden Forschung konzentriert sich auf die Implementierung oder die Kryptographie. Da Blockchain Protokolle jedoch stark auf finanzielle Anreize angewiesen sind, um eine korrekte Ausführung sicherzustellen, ist es wesentlich auch diese zu untersuchen. Solche Anreize können mittels spieltheoretischer Analysen des Verhaltens der Blockchain Nutzer*innen erfasst werden. In dieser Arbeit werden zwei Bereiche der Blockchain Sicherheit behandelt. Einerseits wird ein umfassender Ansatz zur spieltheoretischen Sicherheit entwickelt, der Spiele in Extensivform, abstrakte Gewinne und automatisches Schlussfolgern kombiniert, um die Anreizstrukturen von Protokollen rigoros zu modellieren und zu evaluieren. Andererseits erstreckt sich diese Dissertation auch zur Sicherheit der Implementierung, durch die Entwicklung von Methoden zum Formalisieren und Verifizieren von unbeschränkten Summationen. Dadurch werden sowohl theoretische als auch praktische Fortschritte in der Blockchain Sicherheit ermöglicht. Hinsichtlich der spieltheoretischen Sicherheit diskutiert diese Arbeit wie sichergestellt werden kann, dass die Anreize in jedem Fall das gewünschte Verhalten fördern. Sie liefert eine formale Definition der spieltheoretischen Sicherheit und plädiert für die Verwendung von Spielen in Extensivform mit symbolischen Nutzenfunktionen zur Modellierung von Blockchain Protokollen. Darüber hinaus werden Automatisierungstechniken für die spieltheoretische Sicherheitsanalyse präsentiert, die es ermöglichen, selbst riesige Modelle zu analysieren. Diese Techniken wurden in den beiden Versionen unseres automatisierten Tools für spieltheoretische Sicherheitsanalysen, CheckMate, implementiert. Es geht über herkömmliche Automatisierung hinaus und ermöglicht eine stückweise, also zusammensatzbare, automatisierte Analyse, wodurch eine höhere Skalierbarkeit erreicht wird.Weiters haben Ansätze zur Sicherheit der Implementierung bisher Schwierigkeiten, Summationen mit einer beliebigen Anzahl von Summanden vollständig formal zu erfassen. In dieser Arbeit wird eine Verallgemeinerung der Presburger Arithmetik eingeführt, die Eigenschaften von Summationen ausdrücken kann. Es wird zudem gezeigt, wie diese Verallgemeinerung genutzt werden kann, um Fragestellungen der Verifikation von Blockchain Protokollen zu formalisieren und so die Bemühungen zur Implementierungssicherheit zu verbessern.