Allows us to realize the program architecture and dependencies, construct the call graph of contracts methods, find the potential security flows and prepare ourselves for the specification creation step.
During this phase, we actively communicate with developers and project managers to fully understand the system, purpose, and environment where it should be run.
It happens that after this stage, we offer the developers some workarounds to mitigate the revealed issues and to correct architectural limitations, if any.
We summarize the audit results to the so-called informal specification — that is a free but technical description of what a system does, which high level properties it should have and describe the main user scenarios of exploitation.
One can think of scenarios as a user guide, where we state how a user should act to get the estimated results or particular process flow.
This high level document we use also to reconcile with developers to be assured that we are on the same wave.
Informal business level specification
To perform the verification process, we need to represent both specification and code in a way which could be understood by the Coq proof assistant.
And we developed our Coq embedded language, which we call Ursus to perform that task. Ursus toolkit allows translating the original solidity code to the form which is very syntactically close but at the same time is correct Coq term.
Having both artifacts — specification and code — in Ursus language, we can perform further steps.
Formal engineer level specification
We run sophisticated randomized tests after the completion of Ursus translation.
That is taking the propositions formulated on the previous steps inside Coq ecosystem we use special methods to run property-based checker, which apply brute forcing algorithms to find the counter examples.
After that, when most of the issues are gone, we use the deductive verification schemes to mathematically prove the correctness of the properties revealed.
Verification of the given code against the formal specification