Releases: shaunazzopardi/solidity-static-analysis
Working proof of concept in producing DEA Residuals
Features:
-Representing smart contracts as automata with transitions tagged with conditions and statements
-Added a simple variable propagation algorithm that propagates assertions (implied by conditions and statements) until a statement that affects them;
-Producing approximations of executions through a smart contract function by abstracting behaviour outside of it chaotically;
-Analysing the composition of these approximations against property automata (DEAs), which enables the creation of residual DEAs with less transitions and/or guards.
Input:
[input solidity file] [input dea file] [output cfa files] [output acfa files] [output ams files] [output residual dea file]
Output:
-Control-flow automaton representation of smart contract functions;
-Abstracted smart contract function automata (with abstracted outside behaviour and states tagged by assertions true at those states in successful (i.e. non-reverting and non-throwing) executions of the smart contract;
-Abstract monitored system of each function;
-Residual DEA.
Requirements:
-z3 installation
Limitations:
-We are not dealing function modifiers, and smart contract inheritance (inline everything to enable analysis);
-DEA script not fully supported. A file only containing the "DEA ...." part of the script should be included.
-Reaching a call state removes every known assertion about the program state.
Future work:
-Identification of invariants of the program;
-Intraprocedural abstractions of the program, e.g. an abstraction that is custom for each DEA (i.e. depending on its structure), or an abstraction that is fully precise down to a certain level of nesting.