Implementing smart contract security analyses using the MadMax/Gigahorse framework
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.
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 Souffle language will be ideally installed and tested before the tutorial.