Secure Smart Contract Development Lifecycle Update
Considerations and Best Practices to Avoid Getting REKT
This document contains an updated development model for smart contract security and includes real world examples from several leading audit firms and links to several current resources and tools. It is meant to be used as an overview, guide, and checklist for new blockchain projects and although many examples are from Ethereum, it can be applied to any project on any chain. It contains links to various sources and tools to provide a broad (but not comprehensive) picture of current smart contract security learnings and techniques. Also note that this is not intended to be a strict set of steps that must be completed before moving on to the next phase, rather these should be seen as potential actions that can be adapted to a specific project.
Specification Creation
When getting started with a new blockchain project, it is critical to plan and design the contracts and system architecture, economics and end user behaviors by becoming familiar with current smart contract security, following smart contract best practices such as those found at the smart contract security alliance, running simulations, using Open Zeppelin standard libraries and avoiding pitfalls of not-so-smart contracts. Although these guides were written based on Ethereum there are several useful ideas and examples that carry over to other chains and smart contract languages.
Generally, the following pattern can be followed and adapted according to each development team’s style and expertise. The more steps you can complete the better.
Create business logic and detailed specifications with security, testing, invariants etc in mind. These will eventually be handed to a professional audit firm to verify that the code matches the specification.
Define all core properties and functions and try to create a 100% comprehensive specification. Consider a table that lists all external functions.
Generate initial test cases and consider potential invariants for properties. Decide which test tools and harnesses you may be using and begin education on how to use the tools. Optionally talk to the team that created the tools, join their Discord, look at examples, etc.
Run simulations for complex DeFi scenarios if you are integrating with other protocols or are assuming things about outside markets. It is critical to predict the potential behaviors of smart contract interactions, especially cross-chain scenarios such as bridges.
Plan for your audit by reaching out to potential auditing firms, and post-deployment security and monitoring early. Many audit firms are backed up several months or more so contact them once you have a roadmap for code complete.
Do a full review of your design and spec with a trusted security firm. The more eyes on your specifications the better, you should a 3rd party independently confirm your business logic, features and use of smart contracts are generally safe. This is money well spent as issues found in security audits often trace back to mistakes in the specifications rather than mistakes in code. Finding issues during code review can become costly or cumbersome as you may need to do large redesigns.
Advanced: Work with a security firm who can formally model your business logic into mathematical equations so that you are prepared for formal verification. This can be done with automated tools or manually but is most often a combination.
Design Review Example
Here is a publicly available Design Review for Folks Finance from Runtime Verification. This provides a good example of how deep you should expect a security firm to reason about your smart contracts, and the type of feedback you should receive.
For high value projects that require bulletproof security, creating a formal model of the specification is strongly recommended and is also a required step towards full formal verification (see later section). The process of creating a formal specification consists of manually creating a formal model of the business logic and properties, then performing bounded model checking and model based testing. This type of design review can also be done once the code is written.
Formal Modeling Example
Here is an example from the Algofi v2 specification of how to formally transform specifications into a mathematical model.
“B-Asset Exchange Rate Must Never Decrease. The yield bearing asset B of a market accrues the lender’s interest, and its exchange rate to the market’s underlying asset U must either stay the same or increase after every interaction with the protocol.”
The following is the mathematical inequality created:
With a formal mathematical model, testing and tools can be used to verify that the equation always holds true no matter what the input value is.
Developer Tools
Development teams code using a wide variety of tools and frameworks such as Truffle, VS Code, Solidity plug-in for Visual Studio, Remix, Embark, Hardhat, Foundry or IntelliJ IDEA desktop IDE. New tools and IDE frameworks are appearing frequently, and no matter what tools you use, the goal is to write clear, easy to test and audit code.
Here are a few others, but again do your own research to find exactly what you like best for your target chain and project.
General Development Guidelines
Follow all security best practices you can find, and study all known hacks, especially in the same category as your project. If using Solidity, stay up to date with the official latest changes and security considerations for smart contract development.
Use pre-verified contract libraries, templates and functions whenever possible. Open Zeppelin has been a pioneer in this area since Ethereum launched, and they also provide excellent security audit services.
Be extra careful with integration with advanced DeFi, bridges, cross chain, and scenarios that have external dependencies. Create a suite of manual tests that cover the scenarios you can think of.
Create 100% test coverage for your smart contracts. Not 80%, not 90%, but 100%. This is often a requirement from security audit firms and it should be your requirement as well.
After every major (ideally peer-reviewed) code check-in or change, run a sanity check on your code, ideally in an integrated CD/CI process. Take a lesson from the old school developers and create Build Verification Tests (BVT’s) that can be run easily and frequently to ensure that new code doesn't introduce any regressions.
Leverage available automated tools early and often. Some of these tools can be found in the Security Tooling Guide for Smart Contracts by ConsenSys Diligence which details 22 security tools from across web3.
Advanced: Work with a security firm who has advanced tools (fuzzing, formal verification, invariant proving), and can support your team through the cycle as needed.
More on Testing and Verifying Smart Contracts
Development and testing are very closely related and form a cycle within the overall project lifecycle. In addition, the better a team does with their own internal testing, the easier it will be for professional auditors to focus on more obscure and abstract attack vectors rather than creating and running basic tests.
Manual vs Automated?
The correct answer is both. Here is an explanation from the Ethereum Foundation.
Automated testing is efficient, uses fewer resources, and promises higher levels of coverage than manual analysis. Automated testing tools can also be configured with test data, allowing them to compare predicted behaviors with actual results. Advanced analysis techniques such as symbolic execution, SMT solving and input fuzzing can provide a high degree of confidence that the code behaves correctly no matter what.
Manual testing of smart contracts requires considerable skill and a considerable investment of time, money, and effort, but human intelligence can often find defects in contract code that might go undetected during automated testing. Manual-testing your smart contracts can also reveal vulnerabilities that exist outside the code, but can still affect it. For example, a smart contract audit can discover vulnerabilities arising from flawed interaction with off-chain components as noted above.
Automated Functional Testing
In the following example from Quantstamp, all automated tests are implemented in a JavaScript file to excercise various code pathways. The test aims to simulate a complex scenario where there are 5 pools with different parameters and owners, as well as 5 different stakeholders, 3 of which are security experts. All text boxes represent an aspect that must be tested and the line connecting a text box to the timeline represents the point in time when the test should be performed. The illustration below is quite hard to read, but illustrates how various complex smart contract use cases can be thoughtfully mapped out and simulated.
MythX
Several companies have created professional smart contract testing tools that can be used free or with a small subscription. ConsenSys currently provides a MythX plug-in for Remix which requires a subscription, but integrates directly with the Remix IDE and shows you exactly where in your code errors were found.
Echidna
Another powerful tool is Echidna from Trail of Bits. Echidna is a smart contract fuzzer that can rapidly test security properties via malicious, coverage-guided test case generation. For example, the property The expireTsFrom function always returns the encoded expireTs value can be verified with an Echidna test pass.
Trail of Bits is one of the original smart contract audit and tools firms out there and were pioneers in symbolic execution to verify smart contracts. But as mentioned earlier, there is a long waiting list.
Foundry
Here is an example of how Foundry 2.0 and the KEVM (correct by construction Ethereum Virtual Machine based on a formal specification of the EVM) can be used together to do Symbolic Property Test Coverage, and if 100% of the coverage tests pass, is a way to achieve automated formal verification. Admittedly this is an advanced security technique, but for very high TVL projects, formal verification may yet become the defacto security high bar.
Foundry tools generate random inputs for parameters and run the resulting tests.
K-Foundry executes the parametric tests symbolically, using the KEVM semantics.
Parametric tests become formal specifications, and K-Foundry formally verifies them.
Audit
Once the code is 100% frozen, do a full professional security audit using a trusted firm such as Trail of Bits, BlocTrax, Quantstamp, ConsenSys Diligence or Runtime Verification. This is one of the most critical parts of launching a new project and may be the most important step in securing your code.
Here is a 2023 list of Security Audit firms published by Alchemy. It is a good list, but there a few names missing in my opinion, and you should spend time looking at their previous audits as well as the REKT News to see if any of their audited projects have been hacked.
Security Audit Guidelines
Start investigating security audit firms as soon as the project starts to take shape in the design and modeling phase. Contact the ones you think match your goals and budget and get on their calendar. Consider hiring multiple firms with specific areas of expertise (e.g. penetration testing vs smart contract verification).
Prepare to provide access to your specs, code, test cases so they can prepare an estimate. If the firm doesn’t provide one, prepare a 2-way NDA to send immediately after the intro call.
Freeze the code and deploy to a testnet. This is also useful for private and public bug bounties.
Make sure you have an open line of communication between your smart contract developers and the audit team, e.g. a Slack or Discord channel, and check it daily to answer questions. Have frequent Q&A sessions with auditors via Slack and fix issues as they are found.
Re-audit every new version you are planning to deploy live. This has been the downfall of many projects in early 2023 – a single line of code changed and deployed live that contained an exploited vulnerability (see SafeMoon). Consider creating a retainer type relationship with the audit firm and have them check every new change you deploy live.
Advanced: formally verify the code against the specification.
What goes into an audit?
There is an art and science to performing security audits. There are also manual and automated processes that can be used for more complete coverage. It is therefore very important to choose a security firm that has experience with the smart contract language, the type of protocol, or VM you are using, and one that has a strong reputation within the industry.
How does a security engineer approach an audit? What goes on?
From the Blockswap Stakehouse Audit Report by Runtime Verification:
We created an abstract high-level model that captures the intended behavior of the system, and based on this model identified the desired properties and invariants of the protocol.
We rigorously, but manually, reasoned about the business logic of the protocol, validating security-critical properties to ensure the absence of loopholes in the business logic.
We reviewed the code for inconsistency between the logic and the implementation or vulnerability to known security issues and attack vectors.
We discussed the most catastrophic outcomes with the team, and reasoned backwards from their places in the code to ensure that they are not reachable in any unintended way.
We regularly participated in meetings with the dev team to discuss our findings and together come up with mitigations and reasonable trade-offs.
In other cases, auditors reported the following use of tools:
We symbolically executed part of the compiled bytecode to systematically search for unexpected, possibly exploitable, behaviors at the bytecode level, that are due to EVM quirks or Solidity compiler bugs.
We employed Firefly (see above) to measure the test coverage at the bytecode level, identifying missing test scenarios, and helping to improve the quality of tests.
Recommendations / Mitigations
The best audit team’s provide recommendations when they find issues, and also verify that the fixes are properly implemented. For example:
Issue: The following code is supposed to ensure that decrease is never larger than remainingCollateral:
However, this is wrong. For example, if decrease = 1 and remainingCollateral = 2, then decrease is increased to 2, even though it should have remained at 1.
Recommendation: The above code can be fixed as follows:
Status: Addressed in PR #12.
Pretty cool right? This is a great example of how to find and fix smart contract issues before going live.
Audit Disclaimers. Note that security and risk comes back to the projects and all security audit firms will have some sort of disclaimer in their report that says that they are not liable for any lost funds of any kind in any way. For example: “The Reports are not an endorsement or indictment of any particular project or team, and the Reports do not guarantee the security of any particular project. This Report does not consider, and should not be interpreted as considering or having any bearing on, the potential economics of a token, token sale or any other product, service or other asset. Cryptographic tokens are emergent technologies and carry with them high levels of technical risk and uncertainty. No Report provides any warranty or representation to any Third-Party in any respect, including regarding the bugfree nature of code, the business model or proprietors of any such business model, and the legal compliance of any such business.”
24x7 Monitoring
Security doesn’t stop after the audit is finished. Monitoring is an integral part of blockchain security that all projects must have in place to check whether their deployed projects are operating within defined parameters. This goes for hardware as well as software and smart contracts. During both the specification phase and audits phase keep smart contract properties and invariants (which must always hold true) are defined and become the heart of security monitoring.
All projects that launch on MainNet must have some level of monitoring in place in order to detect pre-defined anomalies and send alerts that there is an issue.
Transaction monitoring brings security to where the live action is happening.
Create a dashboard to monitor properties and send alerts whenever they fall outside set values (e.g. total liquidity in pool X is less than Y).
Create additional monitors for abnormal behavior, specific invariants (e.g. amount sent to bridge = wrapped amount generated).
Create a process and specific actions for each type of alert – be ready!
Advanced: Engage with a professional security firm to create and host your monitoring solution.
Property Monitoring
Specific smart contract properties and invariants that should be monitored are usually defined in the specification and re-checked during the audit. These invariants should hold for the life of the contract and can be monitored in real time.
In general, a good monitoring system:
Uses accurate real-time data and well groomed historical data to inform metrics.
Observes invariants and other properties identified during the audit or as a separate deliverable.
Triggers action when invariants are violated or when properties cross defined thresholds
Includes alerting users or initiating recovery.
Forta Network and SpiceAI are two example firms that provide monitoring solutions, custom bots, and various kinds of alerts for blockchain projects. In the future, expect more and more security to be pushed closer to the nodes and wallets where transactions are happening.
Here are some simple examples of things that can and should be monitored in real time:
Bridges: Is the final token greater or equal to the deposited token?
DEXs: Does X * Y = Z?
Liquidity Pools: Is there an X% raise or drop in one of the tokens?
Stable Coins: Is the token value within X% of the desired peg?
NFTs: Is there a rise of drop of more than X% of the floor price?
Transaction Security Checking and Malicious Attack Prevention
In the near future we will see solutions that can monitor all transactions including malicious ones before they are added to the next block in the chain, thus preventing attacks in the first place provided that the checked properties are comprehensive.
Hypernative is a new company that does threst analysis and detection in real time, and have a track record of detecting hacks prior to the first attack transaction with an average of alert time of more than 2 minutes. It is a great complement to a security audit and provides additional real-time protection.
Security Michelin Stars
Several smart contract audit firms have their own ratings systems, but to date a comprehensive single system to certify audits, create certification badges for different levels etc does not exist. However the Enterprise Ethereum Alliance has now published the EEA EthTrust Security Levels Specification v1 which should lead to a unified approach within the Ethereum ecosystem. Fun fact: I was the founder of the ETHTrust group that produced this specification, and my company 5thnode LTD is working on such a system for several blockchains.
About me: previously Chief Strategy Officer at Runtime Verification, Co-founder of ConsenSys Diligence and MythX. 20-year Microsoft veteran Researcher, Windows Security Product Owner, and WW Developer Ecosystem Director. Currently living in Nagano, Japan and Kirkland, Washington.