Pruvendo
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.
formal verification
Verification against the specification
Engineer level specification
Business level specification
Audit
Workflow
Details
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 audit
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.
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.
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.
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
Generating
specification
Formal verification
Smart contract code
Solidity
99.9% trustful formally verified smart contract
Ursus
Improved overall performance and scalability of the blockchain platform
Enhanced credibility for integration and interoperation with other blockchain networks or systems
Reduced potential for legal disputes or financial losses
Reduced risk of errors and vulnerabilities in the code
Improved reputation and credibility of the blockchain platform and its users.
Increased security and reliability of the smart contract
Enhanced trust and confidence among users and stakeholders
Improved efficiency of the smart contract execution
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.
Results
Inquire us for the details and we’ll make it worth your time
Interested in unprecedented security of your smart contracts?
