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.
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.
5 - 10 days
Increased Test Coverage
We analyze your program’s test-suite to determine its coverage - the good, the bad, and the ugly. We will then generate new test inputs that will improve your coverage and ultimately contribute to a more secure program. Moreover, the new test inputs could very well reveal previously hidden undesired behavior. So what’s included…
1. Initial coverage analysis report (FREE):
We will review your current coverage performance and discuss how to improve your coverage so we can get as close to 100% coverage as possible.
2. Final coverage analysis & review of new tests:
We review your improved coverage and the new test inputs that helped it get there.
In some cases we may have suggested test outputs, but it will be up to you to decide whether the newly covered behaviors are desired or not.
The new tests may identify previously hidden behavior. It will likely require a more extensive analysis to determine whether or not said behavior is desired or undesired. The customer can perform this analysis themselves or engage with RV to do it for them.
10 - 15 days
Symbolic Bytecode Analysis
We analyze the compiled bytecode of your smart contracts to ensure there are no unexpected behaviors. Using KEVM, we symbolically execute your contract to systematically search for unexpected (possibly exploitable) behaviors. These behaviors can be the results of bugs found in your contract’s source code, or quirks or bugs in the compiler itself (which is why it’s important to analyze the bytecode and not the contract source). In short, this service helps mitigate the risk of unlucky encounters with such bugs. This service works as follows:
First we run our KEVM tool to generate all possible symbolic outputs of your smart contracts (FREE) for arbitrary inputs. In the initial meeting, we report how many symbolic outputs are generated for each contract/function, and discuss the scope and goal of the analysis.
Then we carefully analyze each symbolic output, and report immediately whenever we find any unexpected behavior.
In the final meeting, we go over all the symbolic outputs and review together to ensure that all the outputs are desired.
14 - 21 days
Traditional Security Audit
This package provides code review and security assessment of the smart contract, including the following:
Common anti-pattern analysis: Check if the code is vulnerable to known security issues and attack vectors such as reentrancy, transaction reordering, and overflows.
Software engineering practice evaluation: Evaluate test coverage and inheritance structure, identify code smells (with refactoring suggestion), and detect frequent programming mistakes.
Business logic review: Identify loopholes in business logic, and/or inconsistency between the logic and the implementation.
30 - 90 days
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.
30 - 90 days
Like formal modeling, formal verification can also be applied to any system. For smart contracts, this package includes and further refines the Traditional Security Review ("Audit") and Formal Modeling packages, offering formal verification of the contract's EVM bytecode against its formal model/specification, thus eliminating any concerns of potential compiler errors. Specifically:
Refine the contract’s high-level formal specification to the bytecode-level to take into account the specifics of the underlying EVM.
Formally verify the EVM bytecode of the contract against the refined formal specification. This package provides the ultimate formal guarantee for the correctness of your system or smart contract, and incorporates the best techniques and practices developed by the formal methods community.
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).
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.
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.