Learning Goals:

Gain a…

1. Hands on experience with program instrumentation
2. Understanding of the Scribble annotation language

Suggested Readings

1. Scribble Specification Language

Useful Links

1. solc-typed-ast Documentation
2. ERC20

Setup:

1. Download the development environment

hw6.zip

Instructions

1. Follow this tutorial to instrument an ERC20 contract: https://docs.scribble.codes/tutorials/property-checking-with-scribble-and-mythril#background
   1. The tutorial only goes over how to instrument the fourth property. For this homework you will need to implement all four.
   2. There are a few bugs in the tutorial..

      1. The first property should be: If the transfer function succeeds then the recipient sender had sufficient balance at the start

      2. before the Analysis section of the tutorial, run

         sudo scribble token.sol --output-mode files --instrumentation-metadata-file meta
         

      3. For Analysis, myth analyze Token.instrumented.sol -t 1 --execution-timeout 60 should actually be

          myth analyze **token.sol.instrumented** -t 1 --execution-timeout 60
         

****

1. Write Scribble properties for approve and transferFrom . There is one additional bug. Think about the intended functionality and write specs.

   ---

Questions: