formal verification
To perform formal verification of smart contracts we use Ursus — our Coq embedded language. We translate Solidity into Ursus and perform formal verification against the specification.
Workflow
Audit
Business level specification
Engineer level specification
Verification against the specification
Details
Informal audit
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.
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.
Informal business level specification
Formal engineer level specification
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.
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.
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.
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.
Verification of the given code against the formal 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.
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.
Ursus
99.9% trustful formally verified smart contract
Solidity
Smart contract code
Formal verification
Generating
specification
Results
The result of formal verification is that contract behavior is correct against the formulated specification, which is in turn tightly connected with what developers and task managers see and estimate from the software being under investigation.
Improved efficiency of the smart contract execution
Enhanced trust and confidence among users and stakeholders
Increased security and reliability of the smart contract
Improved reputation and credibility of the blockchain platform and its users.
Reduced risk of errors and vulnerabilities in the code
Reduced potential for legal disputes or financial losses
Enhanced credibility for integration and interoperation with other blockchain networks or systems
Improved overall performance and scalability of the blockchain platform
Interested in unprecedented security of your smart contracts?
Inquire us for the details and we’ll make it worth your time
