Pre and Post Deployment
Here is a massive list of the available security products for smart contracts. This data has been compiled from company websites, Discord servers, GithHub orgs, and Twitter accounts.
Testing Software, Pre-Deployment
Certora - Formal Verification
Certora is a pre-deployment formal verification software that checks for bugs given invariants. When provided an invariant, the software does a proof by induction to find counter examples where the invariant does not hold. If there are counter examples, then there exists a bug. If there are no counter examples, Certora spits out a proof proving that the invariant holds. This basically creates boundaries for your protocol to operate within- saying “this piece of software cannot introduce this bug literally because it is mathematically proven it cannot.”
However, building proper specifications and rules is difficult. There are three components to a rule: precondition, operation, and postcondition. Poorly designed conditions can lead to undesired situations where a rule is created that does not test the intended scenario.
In the case of a vacuous rule, the precondition asserts a ridiculous claim like 0 > 1 that makes it so that there is no starting state. Therefore, the software can not come up with any counter examples given no starting state. In the case of a tautology, the postcondition asserts a condition that does not rely on the operation at all. These bad proofs create false positives that can lead to deployment of buggy code.
Certora tackles this by integrating automation for checking these scenarios. The vacuous rule can be detected by asserting something ridiculous as the postcondition and if it fails then it exists. Tautology can be detected by removing the pre condition and operation and if it passes then it exists.
When to use: When you have an app that has a myriad of different parameters, features, and complex interactions, Certora’s formal verification is a great fit. The more complex a system is, the more important it is for it to be formally tested. It may reduce the boundaries of acceptable functionality, but will also allow you to build within guard rails.
TL;DR: It's better to be suspicious of proofs and take returned bugs seriously. Writing specifications is hard; however, automation and tools are being built to ensure good specifications. Formal verifications require you to come up with invariants. Make a bad rule, get a bad proof.
Slither - Static Analysis
Slither is a pre-deployment static analysis software that checks for common vulnerabilities, and ranks them by severity: high, medium, and low. It is effective at detecting common smart contract vulnerabilities, such as reentrancy. We were able to find a mistake reentrancy for a cross-contract call. It is also easy to integrate into your CI/CD process making it easy to help you avoid common pitfalls with each iteration.
One thing to note is that while there are reports of false positives, the number has decreased as improvements have been made. Another concern is the laziness of the developer. Often easy to use tools like these leave a false pretense that the codebase is safe; however, we highly encourage developers to not rely on static analysis alone. Security is important, it is always best to test in conjunction with other products to get rid of noise and pinpoint unsafe code.
When to use: Slither is built for every protocol. Slither is easy to integrate into CI/CD making it essential to integrate into projects of all sizes. It also does not rely on test cases, unlike formal testing or fuzzing.
TL;DR: Static analysis is great to use, we found a mistake reentrancy for a cross-contract call. However, this can be dangerous to rely solely upon. It is simple to integrate into your developer work flow that it is a no-brainer to include. Beware of false-positives.
MythX - Overall Analysis
MythX, a SaaS app ($50/month) from Consensys, is built on multiple other pieces of software to provide a holistic testing suite for smart contracts, mainly in isolation. One of the components of this software is Mythril, which focuses on multi-contract interactions, even contracts that have already been deployed to production. It uses the smart contract weaknesses registry.
We’ve found a lot of help from using this software - they provide a history log of your testing invocations, and the associated risk score. Would be cool if they were able to propose solutions to the problem without relying on the developer to fix it.
When to use: Same as Slither, but for cross-contract calls, too. So can include in your CI/CD build.
TL;DR: Holistic testing suite with multi-contract analysis, which is something a lot of other software misses. Especially in smart contracts, you can introduce a reentrancy attack between two protocols, even though, individually, they are protected from reentrancy.
Echidna - Fuzzing
Echidna (developed by the same team as Slither) is a tool that helps you test the robustness of your application, down to the silicon. The problem with testing functions with concrete values is that it is infeasible to test all scenarios, one of which could include different types of information that bypasses your conditions, specified limits, and ranges.
Upon fuzz testing, Echidna provides details on gas usage, failed assertions, and specific values that caused the test to fail. The problem, like formal testing, is writing the invariants. These are properties that should always remain true. Like the constants you declare, or a reentrant modifier flipping from 0 → 1. It’s weird to wrap your head around initially, but you get the hang of it really quickly after writing a few of them.
Using it in CI/CD is easy, but unlike Slither or MythX, when you make logic changes or add features, you also need to update the invariants and add fuzz testing for the new changes. This becomes difficult to track, especially on a developer team with multiple engineers. Especially if there are updating state values that have dependent logic.
Consensys Fuzzer (Harvey Greybox Fuzzer)
This software is more closed-source, so we aren’t able to derive a lot. But, we can share what we’ve learned from conversations and the resources published.
Harvey is basically a better fuzzer that can be integrated into CI/CD. It applies weights to the inputs to measure the effectiveness of the invariant, which goes one step beyond the other fuzzers. It still requires you to write invariant tests using Scribble. In the paper, they state that they plan on adding “static analysis and lightweight dynamic symbolic execution,” which basically makes it an all-in-one tester for smart contracts.
They found that 74% of bugs in smart contracts require generating more than one transaction to be found. They detected lot more bugs and were 3x more effective (not sure on the measure for effectiveness).
When to use: same reasons as a normal fuzzer, a complex series of smart contracts with state that updates frequently.
tl;dr: A much better fuzzer that has a concept of “distance” that suggests concrete input values based on information from previous executions, instead of performing arbitrary mutations like other fuzzers. It tests not just single function transactions, but multiple functions across multiple state changes across multiple contracts.
Security Software, Post-Deployment
Forta - Realtime Alerts & Monitoring
Forta is a post-deployment decentralized real-time alert and monitoring network that runs detection bots. The nodes provide confirmation that the bot that is deployed is running provided parameters with no tampering by any party. A common belief is that hacks are atomic, and once the block is confirmed, there is no way to prevent it. However, in many hacks, Forta observed that hacks are often executed in stages across several blocks. The hacker typically follows these steps:
Funding through Tornado cash
Deployment of unverified contract on main-net
Execution of flashloan through flashbots transaction
Exiting funds through Tornado cash
While this may not apply to all of the hacks, it makes a statement that it is possible to detect a majority of hacks through a detection of patterns. Forta provides pre-built detection kits for popular protocol types like DeFi, NFTs, and governance. Furthermore, Forta encourages developers from the community to develop models and deploy them to the Forta network, which drives the discovery of new patterns and opens the doors for bot composability.
Bot alerts can be configured with threat levels and alert messages to provide control over what is emitted. We can design alerts around inconsistencies in the invariants of a particular protocol. For example, in a bridge protocol we should never see an imbalance in balances. In an NFT protocol, we should never mint an NFT with no actual funds to back it up. Critical alerts can consist of ACL changes, ownership transfers, and dangerous state changes.
It is one thing for a bot to raise alerts on patterns but it is also important that there are as few false positives as possible. Given a bot with low precision, bot operators will find it difficult to consume and act upon alerts if there is a lot of noise. A potential solution is an aggregator of bots whose purpose is to filter out noise, enabled by the composability of the network mentioned earlier.
False positives requires that response are made manually because automatic responses could render your protocol unusable. It’s like the boy who cried “wolf!” Forta suggests that pausing a protocol is a surefire way to shut down the protocol, so there could be other administrative options to solve. However this does not seem viable because, given the time span of the attack, operators only have a small amount of time to decide on a course of action.
When to use: Right now, the service is free to use, so there is no down side risk. I’m sure it will change in the future, but it allows you to try their product. Just be wary of the number of false positives from a bot, as you could get used to ignoring the alerts and eventually miss a hack.
TL;DR: Hacks often follow a specific pattern. While bots do most of the heavy lifting, they are prone to false positives meaning it is the operator's responsibility to parse through the noise and act upon it (within less than a few blocks). The benefit of this system is while it does have its issues, it significantly reduces the timeline of the hack occurring to performing an incident response by providing real-time alerts. Reliance on one hack prevention system is not good enough, have redundancies to increase confidence.
OZ Defender - Alerts and Monitoring, Safer Deployment
OZ is a full-stack company- they handle the protocol development (ERC’s for EIP’s), audit all the way through deployment, and have Defender to protect while the protocol is live. They’re aiming to automate the smart contract deployment process, and have done a successful job of delivering products to do that.
Defender and Forta work hand in hand- where Forta has the detection bots, Defender has the software to protect the contract. Sentinels is a product that provides a circuit breaker to potential token withdrawals, and Autotasks can trigger on-chain actions when something is off. For instance, if a Forta bot picks up that something malicious is about to happen, it can trigger something in the contract. Since Forta bots pick up activities well before a hack, the countermeasure can be added to the blockchain before the hack.
When to use: If you are an enterprise org with lots of contracts, this is a great solution. You can basically get anything done with them, after you have finished development of your smart contracts and are ready to hand the contracts over for an audit.
TL;DR: Defender + Forta provide a good overall defense system
Seraph - Off-chain Notary Service
Created by Halborn, Seraph is an off-chain notary service to sign off on what is a valid transaction and what is not. They monitor the call-stack of the function execution, basically stopping the transaction based on parameters, then forwarding the call-stack to this execution-based reader. Halborn makes a decision on if it is good or not depending on your specified rules, then either stops it or let’s it pass.
This product works with you when you are developing the protocol, before an audit, then monitors after the deployment. You will create the rule set with them, and they can provide recommendations on what to do. Halborn can do the audit for you, or you can go to someone else. Though, they are pretty badass- have had nothing but good interactions with their team.
When to use: Probably good for teams who don’t have the bandwidth for a large security team internally.
TL;DR: Easy to use product when you’re developing a protocol, then you can outsource decision-making to them.
Hackless - Monitoring and Prevention
Hackless has a bunch of products, we’ll do our best to explain them. They have a monitoring system for sus transactions, private nodes to handle those transactions, a circuit breaker called SafeMigrate to move funds, and an advanced analytics system to process hack information.
Their software has proven to stop a couple of transactions in the wild, and they operate on a few different chains.
tl;dr: They have an escrow system to stop sus transactions, monitoring, and private nodes to divert hacks.
When to use: Similar reasons as any of the other monitoring services, but seems to be aimed for individuals and defi protocols.
LossLess - Monitoring and Prevention
LossLess is another post-deployment solution, offering token-level security, freezing of suspicious transactions, evidence-based resolution, and fees charged on prevented loss. They also have a community Etherscan-like interface to track transactions, and reward people who find malicious transactions.
Seems like they are also going after the all-in-one post deployment provider, considering they recently partnered with Harmony.
tl;dr: They have an escrow system to stop sus transactions, monitoring, and private nodes to divert hacks.
When to use: Similar reasons as any of the other monitoring services, but seems to be aimed for defi and bridges.
Honorable mentions for compliance:
TRM Labs: warns protocols is a malicious wallet connects their UI, also handles lost funds
Unit21: AML/risk compliance, helps with tracing and connectivity for fintech companies
Honorable mentions for retail customers:
Harpie: website
Pocket Universe: Chrome extension
Fire: Chrome extension