This repo contains our (Liguo and myself) joint solution for Assignment 2 of SWEN90010 2022S1. The goal of the project is to detect and fix a vulnerability in a model of a small smart contract program—one that is inspired by the recursive reentrancy vulnerability of "The DAO". The program is modelled in Alloy 6, which enables rigorous automatic predicate checks to be run to verify if the model has been specified "correctly". More details on the assignment specifications are available in specs.pdf.
Download the Alloy analyzer and open the dao.als file.