Analysis of smart contracts, most notably on the Ethereum platform, has attracted a lot of interest in the programming languages community. This tutorial aims to spread this specialized knowledge of this area by showing how sophisticated analyses can be declaratively specified on top of the Gigahorse platform. This platform has been at the core of many recent analysis tools and comes with a variety of program analysis libraries, allowing users to specify these sophisticated and fast analyses in a relatively short number of lines of Datalog code.

The tutorial will briefly cover the following:

• Setting up the Gigahorse framework development environment and related toolchains

• Specifying simple program analyses

• Implement analyses for known vulnerabilities such as reentrancy

• Run these analyses at scale, and compare their results

• Introduce basic analysis design considerations and their effect on precision, completeness and scalability

Necessary background:

The tutorial will make as few assumptions as possible regarding the background of participants, especially relative to the blockchain and smart contracts. Necessary concepts of smart contract execution will be introduced in the tutorial, although the emphasis will be on static analysis. Participants should have some background in intermediate languages and simple program analysis, at the level of a Compilers course. If you are not at all familiar with declarative/logic-based programming, brief experimentation with the Souffle language’s examples should enhance your learning experience.

Medium:

There will be an initial presentation of tutorial material (slides + screen sharing for command line and setup). Afterwards, the tutorial is expected to be interactive, with extensive screen sharing among participants to jointly examine code.

Platform:

Participants should have machines with a Unix-like OS (Linux preferred, MacOS should be ok). The latest official release of the Souffle language will be ideally installed and tested before the tutorial. To participate you will need to clone the gigahorse-toolchain (check the Readme instructions, you need to clone submodules as well) and the MadMax repos. This can be done during the tutorial, with our assistance for setting up.

For experimenting with analysis of actual programs, we will use the gigahorse-benchmarks collection.