TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group

  Home  |  Forschung/Kompetenz  |  Lehre  |  Personen  |  Publikationen  |  Abschlussarbeiten  |  Sonstiges  |  Kontakt  | 

Agenda

Es sprechen Studenten über ihre abgeschlossenen Diplomarbeiten und Systementwicklungsprojekte.

Am Mittwoch, 27.11.19, ab 11:00 Uhr, im Raum Alonzo Church (01.09.014):

Modelling and Verification of Smart Contracts

In recent years, decentralized blockchain technologies have emerged rapidly and are gradually replacing centralized systems. With the introduction of smart contracts, the application of blockchain-based systems has spread beyond the domain of cryptocurrencies. Safe and secure smart contracts are the groundwork of building trust in blockchain-based systems. However, various incidents have shown that smart contracts are very vulnerable and prone to attacks and hacks. Since smart contracts cannot be updated after they are deployed, they must be safe and secure at design-time. We present a model-based engineering approach combined with formal verification to enhance the development process of Ethereum smart contracts. To this end, we introduce SCModel, a domain-specific language for modeling smart contracts as state machines. Furthermore, we enable the application of model checking to verify safety and liveness properties of those models. SCModel comes with a full Eclipse IDE integration and incorporates two code generators: one that translates the model into a functionally equivalent Solidity smart contract, and the other one that translates it into an equivalent model description in nuXmv. Our evaluation shows that our approach can indeed be used for writing verified smart contracts for real-world blockchain systems. However, our running examples reveal some technical limitations and new possible directions, which we shall address in future work.

Towards an Architecture Proof Modelling Language

As modern software systems are becoming increasingly big, their verification becomes a problem. Compositional verification can address this problem by doing verification of single components and their composition in two separate steps. In architecture-based verification, the first step is done using model checking, whereas the second step is done using interactive theorem proving (ITP). However, using a full-fledged interactive theorem prover requires expertise which is usually not found in engineers. With this thesis, we introduce APML: an architecture proof modeling language, with the aim to close the gap between ITP and the architecture domain. APML is a DSL that allows engineers to sketch contracts for components and compose those into proofs in notations similar to Message Sequence Charts. Our translation algorithms and mechanisms generate proofs for Isabelle from the APML specifications. Moreover, we develop custom validators that make the life of engineers easier in terms of development, showing custom in-line errors. We shall explain all aspects of the language in this thesis, including grammar of the language, validators, algorithms, a running example, and a case study with a larger project. The case study shows that APML indeed can bridge the gap between engineers and ITP. Moreover, it can be used easily by people with no background in ITP and formal methods. However, the case study also reveals some limitations and improvement potential which shall be addressed in future work.