Nightly integration build

[elenadimitrova]

In addition to thorough unit testing, with coverage ~100%, the Colony Network should be tested end-to-end under larger volumes of interactions as an integration load and system test.

Additionally, unit testing is predominantly done using ganache-cli whereas both parity and geth should be considered where possible, i.e. not having to rely on forwarding time functionality.

The above checks can be done as part of a nightly or even weekly (depending on complexity and duration) Circle build.

This might include work on improving built times.

Tools to consider

• Solidity's own SMTChecker, tracked separately here https://github.com/JoinColony/colonyNetwork/issues/547

• Maian, blocked by https://github.com/MAIAN-tool/MAIAN/issues/29

• Verisol https://github.com/Microsoft/verisol , currently only available for Windows

• Echidna https://github.com/crytic/echidna experiment in branch maintenance/echidna-trial The echidna docker container may need a specific solc installed locally via:

apt-get install curl
curl -o /usr/bin/solc -fL https://github.com/ethereum/solidity/releases/download/v0.5.8/solc-static-linux
chmod u+x /usr/bin/solc
solc --version

• Slither https://github.com/crytic/slither

[dguido]

Hey Elena, I think we integrated all of the MAIAN checks into Slither. MAIAN's toolchain is not really keeping up with development of Solidity, but Slither is. SMTChecker is similarly deprecated.

Please let us know if you have issues that need fixing for Echidna. We'll get right on them.

[elenadimitrova]

Hey @dguido , isn't Solidity's SMTChecker actively worked on? I believe that's what @leonardoalt is doing mostly as part of this project https://github.com/ethereum/solidity/projects/8

[leonardoalt]

@dguido not sure where you got that info but it's just false, the SMTChecker was never deprecated and is under continuous development. Also, why shouldn't they run MAIAN even though Slither already does everything? Different implementations might yield different results. I always wonder why people try to diminish other tools to promote their own.

[gustavo-grieco]

I told @dguido that the SMTChecker was deprecated but I was wrong. I was confused with the why3 output for formal verification that was deprecated in 0.5.0. My apologies to @leonardoalt.

[leonardoalt]

No worries @ggrieco-tob ! I thought that this was indeed the confusion

[dguido]

Sorry for the confusion Leonardo.

Also, why shouldn't they run MAIAN even though Slither already does everything? Different implementations might yield different results. I always wonder why people try to diminish other tools to promote their own.

It's a practical matter. MAIAN was a one-and-done academic project that has seen no development since it was released last year. People have continued to file issues against the repository for it that have gone unanswered, and this will continue. Further, the researchers created their own dynamic analysis framework to discover 3 bugs. It is complex, slow, and prone to breaking. On the other hand, the issues they discuss in their research are amenable to static discovery. As implemented in Slither, they return results in less than 1 second and gain the benefit of a maintained framework that keeps up with Solidity development. Incorporating academic research into other works is generally what people want to see and the best result of publishing! We do our best to read through and apply the best of what gets published.