cyrille-artho.github.io

Github.io web page

View the Project on GitHub

SmartVis: Smart Visual Model Learning

We need new ways to explain and understand the behavior of smart contracts, which are small programs that run on blockchains and handle assets worth billions of Euros. SmartVis will achieve this by learning, modeling, and visualizing their detailed behavior. This is possible by extending our previous award-winning work with new technologies (LearnLib, Graphviz, and Eclipse Trace Compass) to build a full modeling and visualization framework.

Smart contracts are revolutionizing how we manage electronic currency and other assets. Leveraging blockchains, they digitalize modern society without requiring a centralized agency to provide services ranging from shipment manifestos and energy certificates to financial applications. The first blockchain technologies were immensely wasteful, with Bitcoin at its peak using as much electricity world wide as the Netherlands. Enter Algorand, a new type of blockchain that is designed from the ground up to be efficient and sustainable.

However, even a small mistake in a smart contract can be exploited by an unscrupulous attacker and cost millions of Euro. Like competing platforms, Algorand currently lacks advanced tools for modeling and analysis and requires increased human effort to develop safely. In particular, we need tools to specify and understand the behavior of smart contracts in the form of models. To this end, machine learning can support the creation of models, which are then analyzed and refined by a human expert.

Our recent work at ISSTA 2022 has shown that high-quality models can be learned from the transaction history of smart contracts Finding Permission Bugs in Smart Contracts with Role Mining. Y. Liu, Y. Li, S. Lin, C. Artho. ISSTA 2022. ACM Distinguished Paper Award..

Mock-up

In this project, we want to extend this approach to (1) machine-learn more general and expressive models such as extended finite state machines or Dynamic Condition Response (DCR) graphs and (2) use visualization of the models alongside the smart contract execution data to allow experts to validate the model against the test results (similar to our past work for Java using Eclipse Trace Compass and its next-generation Theia Trace Viwer client). Such an inspection will be enabled by building our experience with monitoring internal variables of smart contracts in addition to the transactions themselves. The use of Eclipse Trace Compass makes it possible for the first time to create a platform that visualizes not only transaction data, but also detailed internals of smart contracts, thus truly explaining their behavior.

The work plan is as follows:

By showing how transactions evolve against learned models, SmartVis will explain their behavior and prevent the theft of millions or billions of Euro in electronic assets. In this way, smart contracts will not only be sustainable, but also safe and secure.

Apply through the web page of KTH

Partnership between KTH and NTU

This project will be a collaboration between the KTH Royal Institute of Technology and the Nanyang Technological University (NTU) in Singapore. Main supervisor will be Cyrille Artho at KTH; co-supervisor will be Yi Li at NTU.

Cyrille Artho is Associate Professor at the KTH Royal Institute of Technology, Stockholm. His main interests are software verification and software engineering, in particular for concurrent and networked systems. In his Master’s thesis and his Ph.D. thesis at ETH Zurich, he investigated different approaches for finding faults in multi-threaded programs. In particular, in joint work with NASA Ames he found that high-level data races can show potential problems in concurrent software even if individual data accesses are safe.

After obtaining his Ph.D., he moved to Tokyo, where he worked for two years at the National Institute of Informatics as a Postdoctoral Researcher before working at the National Institute of Advanced Industrial Science and Technology (AIST) in Tokyo and Osaka until July 2016. He is now active in research on smart contracts and secure software and network architectures.

Cyrille Artho has been on the program committee of numerous top computer science conferences and chaired the ATVA conference that took place in 2016 in Chiba, Japan, and eight international workshops. He has also edited a number of special journal issues. He has published in top software engineering venues including IEEE TSE, ICSE, ASE, CAV, ISCT, ISSTA, and won the ACM Distinguished Paper Award at ASE 2015, Best Presentation Award at ICSE 2017, and ACM Distinguished Paper Award at ISSTA 2022 (jointly with Yi Li), among others.

Yi Li is an Assistant Professor at the School of Computer Science and Engineering, Nanyang Technological University (NTU) and an Associate Director at the NTU Centre in Computational Technologies for Finance (CCTF). He received his BComp degree in Computer Science from the National University of Singapore in 2011, and both his MSc and PhD degrees in Computer Science from the University of Toronto in 2013 and 2018, respectively.

Dr. Li has been leading the Software Reliability and Security Lab (SRSLab@NTU) since 2018. His research interests are in program analysis and automated reasoning techniques with applications in software engineering and software security. Together with his research team, he develops solutions enabling the construction of high-quality software systems that are both reliable and sustainable.

Currently, his work focuses on the security and fairness of decentralized applications and blockchain systems, as well as the robustness and dependability of AI systems. His work in these areas won three ACM Distinguished Paper Awards and two Best Artifact Awards at top-tier conferences, including ASE’15, ICSME’20, FSE’21, and ISSTA’22. He serves on the program committees of many flagship conferences in software engineering, including ICSE, FSE, and ASE. He co-chaired the program committees of ICFEM’23, ICECCS’20, SEAIS’22, and ICFEM’19 Doctoral Symposium.