Search

Blockchain-Programme, sogenannte Smart Contracts (SCs), sind eine Weiterentwicklung zu der im Jahr 2008 veröffentlichten Blockchain Bitcoin. Ethereum, eine der großen Blockchains, erlaubt es, diese quasi-Turing-vollständigen SCs autonom und durch die Blockchain gesichert laufen zu lassen. Die Ethereum-Virtual-Machine (EVM), ein zentraler Bestandteil von Ethereum, ermöglicht es diesen Programmen, viele neue Anwendungsgebiete zu erschließen. Prominente Beispiele hierfür sind Token, dAPPs, dezentrale Finanzsysteme (DeFi), Logistik und Protokollierung (Logging). Etwa 250.000 unterschiedliche derartige Programme wurden bereits auf Ethereum veröffentlicht. In dieser Arbeit untersuche ich einen neuartigen Ansatz zur Klassifizierung von Smart-Contract-Mustern (SC-Mustern) basierend auf ihren EVM-Bytecodes (EVM-BCs) unter Verwendung einer allgemeinen Abfragesprache. Anhand verschiedener Smart-Contract Muster (SC-Muster) zeige ich mögliche Anwendungsgebiete meiner vorgeschlagenen Abfragesprache. Für die SC-Mustererkennung entwickle ich einen Prototyp, der gegebene EVM-BCs dekompiliert und in XML-Dokumente (Extensible Markup Language) umwandelt. Die heuristisch arbeitenden Erkennungsstrategien, die auf Extensible-Markup-Language-Query-Language (XQuery) basieren, werden schließlich gegen eine bereits klassifizierte Menge von SCs evaluiert., Blockchain programs, so-called smart contracts (SCs), are a further development of the blockchain Bitcoin, which was published in 2008. Ethereum, one of the big blockchains, allows these quasi-Turing-complete SCs to run autonomously and secured by the blockchain. The Ethereum Virtual Machine (EVM), a central part of Ethereum, enables these programs to open up many new areas of application. Prominent examples of these are tokens, dAPPs, decentralized finance (DeFi), logistics and logging. About 250,000 different such programs have already been published on Ethereum.In this thesis, I investigate a novel approach to classify smart contract patterns (SC patterns) based on their EVM bytecodes (EVM-BCs) using a general query language. Using different SC patterns, I show possible areas of application of my proposed query language. For SC pattern recognition, I develop a prototype that decompiles given EVM-BC and transforms it into Extensible Markup Language (XML) documents. The heuristically working detection strategies, which are based on Extensible-Markup-Language-Query-Language (XQuery), are finally evaluated against an already classified set of SCs.

Testen bezeichnet eine Menge von Aktivitäten, die dem Vergleich des Verhaltens eines Systems mit seinem intendierten Verhalten dienen. Dieses Sollverhalten kann in Form expliziter Verhaltensmodelle angegeben werden. Abläufe validierter Modelle sind Testfälle, d.h. Sequenzen von Ein- und erwarteten Ausgaben. Da Modelle Abstraktionen sind, also Vereinfachungen, müssen abstrakte Modellabläufe in konkrete Soll-Abläufe der Implementierung konvertiert werden. Diese werden dann mit tatsächlichen Abläufen verglichen. Komplexität wird also auf Modell und die die Übersetzung vornehmende Treiberkomponente aufgeteilt. In technologischer Hinsicht werden Verfahren zur Testfallgenerierung mit symbolischer Ausführung präsentiert. Insbesondere für deterministische Systeme kann Testfallgenerierung als Suchproblem im Zustandsraum des Modells aufgefaßt werden. Dem Problem der Zustandsraumexplosion wird mit Strategien zur Speicherung von Zustandsmengen und gerichteter Suche begegnet. Für strukturelle Überdeckungsmaße werden Verfahren zur inkrementellen Generierung von Integrationstestsuiten präsentiert. Essentiell ist dabei die Ermittlung von Selektionskriterien auf der Menge der Modellabläufe, sog. Testfallspezifikationen, aus denen ein Testfallgenerator Testfälle berechnen kann. Für funktionale Testfallspezifikationen in Form von Interaktionsmustern bedeutet Testfallgenerierung, daß fehlende Signale eingefügt werden. Für universelle Eigenschaften, wie etwa Invarianten, wird eine Methodik für die Ableitung von Testfallspezifikationen skizziert, die auf der syntaktischen Transformation temporallogischer Formeln basiert. Das Resultat dieser Transformation kann dann zur automatischen Generierung von Testfällen verwendet werden. In methodischer Hinsicht werden weiterhin verschiedene Szenarien des modellbasierten Testens insbesondere im Zusammenhang mit automatischer Codegenerierung und der Rolle von Modellen als Spezifikationen präsentiert. Die Verzahnung inkrementeller Modellentwicklung mit inkrementeller Testfallentwicklung wird diskutiert. Industrielle Fallstudien aus dem Bereich der Chipkarten demonstrieren die Tragfähigkeit der vorgestellten Konzepte und Ansätze. Testing denotes a set of activities that aim at comparing a system's actual and intended behaviors. The intended behavior can be provided in the form of explicit behavior models. Runs of validated models are test cases, i.e., sequences of input and expected output signals. Since models are abstractions, or simplifications, it is necessary to translate abstract model traces into concrete intended traces of the implementation. The latter are then compared to actual traces. In this way, complexity is distributed between model and the driver component that takes care of the translation. Technologically, approaches to test case generation with symbolic execution are presented. Particularly true for deterministic systems, test case generation can be perceived as a problem of searching the model's state space. State space explosion can be alleviated by means of strategies for storing sets of states as well as variants of directed search. For structural coverage criteria, algorithms for the incremental generation of integration test suites are presented. This entails the generation of selection criteria on the runs of the model, so-called test case specifications. Test case generators are then able to automatically compute corresponding test cases. For functional test case specification in the form of interaction patterns, test case generation means to fill in missing signals. For universal properties such as invariants, a methodology is presented that allows the deduction of test case specifications by syntactically transforming temporal logic formulae. The result of this transformation can then be used for automated test case generation. Further methodological results concern different scenarios of model-based testing. In particular, the relationship with automatic code generation and models as specifications is discussed. A possible dove-tailing of incremental development of models with incremental development of test cases is scrutinized. Industrial case studies in the domain of chip card applications demonstrate the practical applicability of the presented concepts and approaches.