We have experience in formal modeling, analysis, safety, security, validation and verification, having pioneered many of the techniques used by the community, such as the K-framework and language-independent verification technology. We've worked with NASA, DARPA, Boeing, and Toyota, on formalizing and verifying safety and mission critical systems, and with IOHK and the Ethereum Foundation to formally model and verify not only smart contracts, but also consensus protocols, programming languages and virtual machines.
Interested in reviewing the work we’ve done to date? Please visit our GitHub repository, or click on one of the links below.
Analysis and verification packages
We believe our primary competitive advantage, and thus main point of differentiation as compared to competing security service providers, is our proven expertise in formal verification and assurance.
Design Review
Runtime Verifications’s speciality in formal methods allows us to take a critical look at your product’s design. Errors in design are the most critical and the most costly to fix, so it’s best to catch and correct them early. Our experienced engineers will review your specifications and implementation, consulting continuously with your developers, to understand your product, ensure there are no holes or inconsistencies in your design, and discover important properties and invariants for the product’s safe operation. We will contribute directly to your specifications where issues are found, which can be used as part of the public documentation of the product and lays the foundation for later steps in a security audit.
Following Design Review, our team will have a thorough understanding of your product and a completed specification to work from as reference. We systematically review your codebase, ensuring that it conforms to the specifications produced in the Design Review phase. Our training in formal methods allows us to take a verification oriented approach to this review by manually proving the important properties of the product hold for each component of the code. All issues found in the process will be documented and reported to your developers in real-time.
Following Design Review and one of either Code Review or Formal Verification, we can produce a unified report describing the work we’ve done with your product. This report can be published among our public audit reports as a record of this work. The report will include any design documentation we have produced, important properties we have specified, a description of the scope of the audit, any issues we discovered over the entire course of the engagement, and any verification artifacts that are relevant for the codebase.
This package applies to any system, including programming languages, virtual machines and protocols, not only to smart contracts. For smart contracts, it includes the following:
Formally specify the contract’s business logic to produce a formal model that provides a precise, unambiguous, and comprehensive documentation. The model is executable, so it can serve as a reference implementation, and is used to generate and support “blackbox testing”.
Validate the critically important properties of the contract’s business logic to provide the ultimate formal guarantee for the absence of loopholes. Please note this package does not include formal verification of the smart contract code.
The highest level of guarantee that can be achieved for a codebase is formal verification, where we prove that the code will always behave as expected. In this process, we translate the discovered properties and specifications from the Design Review phase into machine-readable specifications via our property-testing framework. In the case of Ethereum, we use Kontrol, which enables writing verification conditions as Solidity property tests. This intuitive approach to verification allows us to directly enable the verification in your CI process and enables your developers to maintain and continue the verification work past the engagement’s end.
How smart contract analysis and formal verification work
Our team will meticulously review your code line by line checking for bugs, errors, security vulnerabilities, and exploits. On top of this manual review, we incorporate our own bounded model checking tool, powered by the K-framework using its symbolic execution capability, to augment and enhance your review.
Meet & greet
You present your company, dive into your contract, and identify requirements.
RV runs through available review and verification packages.
RV introduces a typical engagement from start to finish.
Package Selection & Agreement
You select the package that best meets your needs.
RV provides an estimated timeline for delivery of your engagement.
We sign contract and you provide initial deposit.
Engagement & Report
RV reviews and/or verifies your code.
RV drafts preliminary report and provides debrief on findings.
You implement code improvements.
RV delivers and publishes final report (requires client approval).
What is the difference between security reviews ("audits") and formal verification?
Formal verification is not the same as a traditional security audit. With formal verification, contract code is verified at the bytecode level using tools developed based on a mathematical model of the EVM. The result is a level of assurance that traditional reviews, limited to reviewing the Solidity code itself, cannot offer with respect to the functional correctness of the code.
During a formal verification engagement, RV formalizes the requirements of the smart contract. That is, all the properties shared become mathematical theorems, proved using RV’s verifier/prover at the EVM bytecode level, making sure all corner cases are rigorously specified and verified. With respect to work allocation, the majority of tasks assigned to verification engineers do not go into the actual verification, but rather in formalizing the actual properties. Security auditors do not do this because they do not possess the required expertise or access to the necessary tools to verify the code against the specs.
RV has discovered issues in all the contracts its verified. Not always issues that can be exploited, but issues clients chose to fix because they are committed to the correctness of their contracts. Contracts that appear correct can be broken with specific inputs at particular corner cases. The human mind simply cannot keep track of all such corner cases, which is why tools based on mathematical models of the computing infrastructure, i.e. the EVM bytecode, are necessary.
How long does it take to formally verify a contract?
It depends. Providing formal verification is a bespoke exercise that is custom to the contract or contracts in question. To lock down both timeline and price, RV and the interested party will engage in a bout of back and forth due diligence that will allow RV to better understand the true intent of your contract, a requirement for any verification project. RV will then provide a work plan that includes incremental tasks and deliverables, itemized cost for each deliverable, and delivery estimate for each deliverable. The work plan can then be modified to best align with your roadmap and/or budget requirements.
Academic papers published by Runtime Verification experts
Tools And Application
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
