First-order reasoning with aggregates

Abstract

Aggregate werden häufig für Software Verifikation verwendet und sind besonders wichtig für Smart Contracts, nachdem diese Transaktionen von Kryptowährungen zwischen Konten tätigen. Die formale Verifikation von Smart Contracts ist ein sehr aktives Forschungsgebiet, weil die größte Hürde für eine alltägliche Verwendung von Smart Contracts im Fehlen von garantierter Veranlagungssicherheit besteht. Unschärfen im Source Code können enorme Auswirkungen haben, wie jüngste Softwarefehler gezeigt haben.Im Allgemeinen benötigen Aggregate Logik höherer Stufe, aber für gewisse Fälle ist es möglich die gewünschten Operationen und Eigenschaften in Logik erster Stufe auszudrücken. In dieser Diplomarbeit versucht man dies für Aggregate beliebiger aber endlicher Länge. Es wurde ein Weg gefunden Summen in allgemeiner Logik erster Stufe auszudrücken. Die Konzepte und angestrebten Anwendungen werden in der Arbeit sorgfältig erklärt.Die Hauptidee ist es Kryptowährung in Münzen zu kodieren und diese Konten zuzuordnen. Die Invarianten stellen sicher, dass die Summe korrekt ist, indem sie kodieren, dass jede aktive Münze genau einem Konto zugeordnet ist. Auch die Transaktionen können leicht in dieses Konzept eingebettet werden. Die Experimente mit Vampire und Z3 sind vielversprechend. Beide können interessante Eigenschaften beweisen.In dieser Arbeit wurde bewiesen, dass die Übersetzung von Logik höherer Stufe in Logik erster Stufe 'sound' und 'complete' ist. Der Beweis ist Teil der Arbeit. Des Weiteren wird gezeigt, wie die Übersetzung selbst in Logik erster Stufe ausgedrückt werden kann. So eine Kodierung wird ebenfalls präsentiert. Dadurch haben wir einen Weg gefunden direkt über Summen von natürlichen Zahlen Schlüsse zu ziehen. Es werden eine naive Kodierung und zwei eingeschänkte Versionen vorgestellt. Die erste der Einschränkungen ist wesentlich um zwei Summen vergleichen zu können, die andere verkleinert lediglich den Suchbereich.Es wird ebenfalls bewiesen, dass die Einschränkungen die Allgemeinheit der Kodierung nicht beschränken. Die Experimente zeigen, dass 'Theorem Prover' mit beiden eingeschränkten Versionen gut umgehen können, aber Probleme mit der naiven Version haben. Der Grund dafür ist, dass die naive Version keinerlei Information beinhaltet in welcher Relation die beiden Summen stehen. Nichtsdestotrotz können einige Eigenschaften von Summen in den eingeschränkten Kodierungen bewiesen werden.Des Weiteren wird vorgestellt, wie man die Konzepte auf andere Aggregate wie das Minimum oder das Maximum übertragen kann. Die Idee Münzen zu verwenden und sie durch eine Relation Konten zuzuordnen kann aufgegriffen werden.Nach unserem besten Wissen ist diese Arbeit die erste die Summen endlicher aber beliebiger Länge in Logik erster Stufe kodiert. Sie ermöglicht es automatischen 'Theorem Provern' über Aggregate zu schlussfolgern und trägt dadurch zur automatischen Verifikation von Smart Contracts bei.

Aggregates are widely used in software verification and especially important for verifying smart contracts that deal with transactions of crypto-currencies between accounts. The formal verification of smart contracts is a very active area of research, since the main blocker for the use of smart contracts in every-life is the absence of a security guarantee. Vulnerabilities may have tremendous consequences, as recent bugs have shown. In general, aggregates require higher-order logics, but for certain use-cases it is possible to express in first-order logic both the allowed operations and the desired properties. This thesis addresses this challenge by suggesting encodings for aggregates of finite but arbitrary length. We have focused on sums and developed a novel way to express them using uninterpreted first-order logic. Within this work we explain the setting and the intended applications accurately. The main idea is to encode the crypto-currency as coins and to assign every existing coin to some account. This is realized using a binary relation. The invariants ensuring the sum to be correct encode that every existing coin is owned by precisely one address. The transactions, such as transferring money, can easily be fitted into this setting. The experimental results using Vampire and Z3 are promising. Both are able to prove interesting properties. We have proven that this translation from higher-order logic to first-order logic is sound and complete. The proof is given in the present thesis. Further, the translation itself is first-order expressible. In fact, we present an encoding that implements this translation. As such, we also provided a way to directly reason about sums of non-negative integers. We present a naive encoding and two equally expressive restrictions. While the first one is crucial for the comparison of two sums, the second one only decreases the search space. We also give a proof that we do not lose any generality by restricting the encodings. The experiments show that automated theorem provers can handle both of the restricted versions well, whereas they struggle with the naive encoding. The reason is that the naive encoding does not provide any information about the relation of the coins in the two compared sums. However, we can prove various results in terms of sums using the restricted encodings. We briefly explain how to adapt the presented invariants in order to be applicable for other aggregates such as the minimum or the maximum. The idea of using coins to represent the balances of accounts can be adapted, also the binary relation expressing the ownership of coins can be reused. This work is, to the best of our knowledge, the first to encode sums of finite but arbitrary length in first-order logic. It also enables automated theorem provers to reason about aggregates and hence takes a step towards automatic verification of smart contracts.