Recently you may have heard about our new tool Kontrol, but are still uncertain about what it is or how it might benefit your project’s security. This blog post addresses those concerns by explaining the blockchain security lifecycle, how it differs from traditional software security, and the role that Kontrol plays in ensuring that your application is as secure as possible.
Why Should I Care About the Security Lifecycle?
There is one product development truth that haunts most software projects: there is never enough time for testing, resulting in live applications which have not been properly tested. Most developers perform unit testing to verify basic functionality and then move on to the next project. Those that are fortunate enough to have a QA department to perform more rigorous testing generally fare better, but in the end, most products hit the market under-tested, resulting in fixing problems after the application is already in production.
For most applications, the consequences are manageable (poor performance, sub-optimal user experience, lost revenue, etc.). However, in the case of blockchain applications, code vulnerabilities can be exploited by malicious actors, resulting in significant financial losses for project stakeholders. Blockchain ecosystems are inundated daily with new exploits against poorly tested code, resulting in billions of dollars in lost value. These attacks can be minimized or avoided altogether through better security practices during the software development lifecycle. Properly protecting smart contracts requires advanced development and testing techniques, including security focused code reviews, enhanced unit and integration testing, property testing, fuzz testing, and even formal methods such as symbolic execution.
The challenge with these advanced testing techniques is that they typically require significant expertise that most developers and QA teams do not possess. The current accepted industry practice consists of protocol development teams performing as much testing as possible before passing the application to a third party for an audit prior to deploying it on-chain. The trouble here is that not all auditors are created equal; most only do a manual code review, find a few errors, and provide a report saying the code is ready for production. If you are fortunate enough to find an auditor skilled in formal methods you will likely achieve a more consistent, reproducible and more secure result, but even this best practice results in several challenges along the way:
- Under-tested code contains more vulnerabilities that must be fixed and re-audited
- Many projects go through several lengthy audit cycles before being ready for mainnet
- Poor auditor expertise resulting in missed exceptions and exploitable vulnerabilities
- In virtually every case where multiple auditors are used, results vary with each report
- Relying on a “one size fits all” security audit process often leaves code vulnerable
Coupling these issues with the pressure to get the project to market as fast and economically as possible generally results in a common phenomenon across the industry: do as little rework as possible to “pass” the audit, convince yourself that any remaining exceptions a “not a big deal”, promote to mainnet, and hope for the best.
Just Passing an Audit Shouldn’t Be the Goal
There is another way.
Ideally, developers should practice as much of the aforementioned security cycle as possible before submitting their code for a security audit. To do this effectively, teams should conduct security focused design and code review processes, as well as employ more formal testing methods beyond simple unit testing. Extending testing to include property testing, fuzz testing, and ultimately symbolic execution provides better confidence that a security audit will be successfully executed in an expeditious timeframe. These techniques are briefly described below, but there are volumes of information available dedicated to each:
Unit Testing
Unit testing is a software testing technique where individual components or units of software, such as functions or methods, are tested in isolation to verify that each part functions correctly. Unit testing is an essential part of the development lifecycle, helping developers identify and fix bugs early in the development process. At the same time, unit tests are traditionally designed to check specific, predefined cases, focusing on expected inputs and use cases. This narrow scope of analysis can miss unexpected or edge case inputs that other techniques discussed later in the post are more likely to uncover.
Property Testing
Property testing is a methodology in which tests are generated using a specified distribution based on a set of properties which the code should satisfy. Property tests are specified using logical properties which are automatically executed in search of counterexamples that show cases where these properties are violated. By testing these properties against a large number of randomly generated inputs, developers can identify potential edge cases and bugs that they may not have considered in their traditional unit tests.
Fuzz Testing
Fuzz Testing, also known as fuzzing, is a dynamic software testing technique that involves providing invalid, unexpected, or random data as inputs to a software program. The primary goal is to discover software vulnerabilities, crashes, or other unexpected behaviors. Similar to Property Testing, the difference centers around the level of knowledge required to generate the inputs for testing. Fuzzing is typically a “black box” method where inputs are fully generalized, whereas Property Testing shapes the test inputs to “interesting” ranges derived from the code under test.
Symbolic Testing
Symbolic testing, the practice of running tests with symbolic inputs, is an effective formal verification method that reduces specification overhead. This approach enables the use of the same test cases for both testing and formal verification. Unlike traditional testing, which verifies that a program works correctly for a limited set of inputs, symbolic testing checks the program for all possible inputs, hence a program that passes symbolic testing can be considered formally verified.
What is Kontrol?
Formal verification attempts to solve a challenging problem, but a common misconception is that it is too time consuming to use in practice. The real problem is that most formal verification tools require users to work with multiple specification languages to describe the properties that should hold during execution, thus making it more complicated than it needs to be.
Kontrol was built with developers and auditors in mind, giving them the ability to build and execute tests using languages and tools already familiar to them. Ethereum developers can build tests using Solidity rather than having to learn a new specification language, or build a completely new set of specifications for formal verification. Furthermore, Kontrol provides a way to symbolically execute existing Foundry tests, which can be augmented with additional verification-specific cheatcodes.
By combining KEVM (RV’s formalized semantic of the Ethereum Virtual Machine) and Foundry, Kontrol grants developers and auditors the ability to perform formal verification without having to learn a new language or how to use new tools, which is particularly useful for people who are not verification engineers. By using Kontrol throughout the software development lifecycle, code vulnerabilities can be addressed before deploying to mainnet, ensuring application security at product launch.
Once the project is live, Kontrol can be used to validate subsequent evolutions of the codebase and ensure that changes do not adversely impact security. K as a Service (KaaS) can even be used to integrate symbolic execution into an application’s continuous integration processes, effectively validating code security on every iteration of the application. Runtime Verification recently worked with Optimism to validate changes to their codebase before merging them into production.
Why Do I Need Kontrol?
While fuzzing is a powerful testing technique, and a considerable step up from the unit testing employed by most developers, it still has limitations that motivate the need for a complementary symbolic execution of the test suite. Due to pseudo-random input generation, fuzzing struggles to generate input values for complex or nested conditions. Symbolic execution systematically explores all feasible code paths by using symbolic variables as input and tracking path conditions, thus providing more comprehensive coverage.
Additionally, symbolic execution can automatically derive and check postconditions, providing stronger guarantees on the correctness of the program. These complementary approaches can be used to identify a wider range of bugs and vulnerabilities, leading to more reliable software.
By installing Kontrol, you unlock the capability to perform property verification. This is a big step up in assurance from property testing, but is more computationally expensive, and often requires manual intervention.
A Practical Example
To illustrate the value of Kontrol (and symbolic execution in general), first consider the following code example (if you want to run this example yourself it may be found in our Kontrol documentation):
The contract Counter has a public variable named number that is either set to a specific value by the method setNumber(uint256), or incremented by increment(). The setNumber function will update the storage variable with the passed value unless newNumber is 0xC0FFEE and the variable inLuck is true — in this case, the function will revert.
The next step is to write a test for this contract:
In this example, the testSetNumber test should pass nearly every time. Consequently, when using a fuzzing tool such as Foundry’s Forge, whether or not this test passes depends on the inputs generated during a fuzzing campaign. If the inputs x = 0xC0FFEE and inLuck = true are generated by Forge, then the test will fail; otherwise it will pass. In a vast majority of cases, this bug is not found.
Property verification in Kontrol allows you to catch errors that fuzzing in Forge might miss. Kontrol compiles the source and testing files with forge build under the hood, so there is no need to call it explicitly. Once compiled, it inspects the artifacts generated and produces the KEVM helper modules (rules for ABI properties, bytecode, etc.) for the contracts being tested, as well as the definition necessary to execute the tests symbolically.
Through symbolic execution, Kontrol explores every possible variable combination through the Counter contract as defined in CounterTest, and after three minutes or so the test will revert, producing a counterexample exhibiting that the values x = 0xC0FFEE (12648430 in decimal format) and inLuck = true result in a failure.
As a matter of good practice, Runtime Verification recommends fuzz testing your contract first in order to quickly identify errors that must be corrected. Once the code passes fuzz testing, Kontrol should be used with the same set of tests for exhaustive input coverage in order to catch even the most unlikely of edge-cases.
Get in Touch With Us!
Kontrol is actively being developed and evolving as a tool. We are actively looking for feedback from users and security experts. Should you have any suggested improvements or features that would improve Kontrol or to integrate it into your development and testing processes, please contact us.