Executive Summary

• On May 10th the Silo team informed us about a critical vulnerability that had been reported by an external researcher and fixed a few days before.
• We conducted a thorough investigation and manual review of the issue, the fix, and the rest of the code base.
• We added special correctness rules to prevent similar errors in the future and tested them against the vulnerable and fixed versions of Silo’s code using the Certora Prover.
• We can confirm that Silo’s fix successfully mitigated the bug.
• Certora will be allocating $100,000 via Code4rena for additional rule writing to enhance the protocol’s security in the next Silo code version.
• We will utilize our new open-source mutation-testing technology and Gambit, for checking the rule coverage.

Detailed Report

Background

Silo is a permissionless-based and risk-isolating lending protocol designed to offer secure and efficient money markets for all token assets.

Silo Finance’s formal verification project took place between May 7 and July 15, 2022, using the Certora Prover tool. During the verification process, we worked closely with Silo Finance. After learning the protocol’s design and codebase, we:

1. Instructed the Silo team on the rule-writing process.

2. Conducted properties and rules with the aid of Silo Finance.

3. Reviewed the spec files.

During the verification process, about two hundred correct rules were written. Some of these rules uncovered five issues (two of them being high and three being medium). The Silo team addressed all the issues. During the process, the Silo team mastered the usage of the Certora Prover. The rest of the rules proved the code was correct and sound. Twenty-nine rules were written for the InterestRateModel contract.

The full report can be found here:

Formal Verification of Silo V1, July 2022

On May 10th, the Silo team informed us about a critical vulnerability that had been reported by an external researcher. Silo Finance provided a detailed explanation of the issue, along with their mitigation plan and code fix.

Actions taken

Certora treated the issue as a top priority. Amit Levy, our Director of Product Security, who brings eighteen years of experience in code security, assembled a task team consisting of two security researchers and two security engineers. The work of the researchers was to review the vulnerable and fixed code while the security engineers examined the verified rules. The R&D team assisted with performance issues of the Certora Prover.

We acted on three different levels:

1. Understanding the bug

Silo provided a clear and insightful explanation of the potential exploit.

The vulnerable code existed on the Interest Rate Model contract.

The Interest Rate Model is responsible for calculating the dynamic interest rate for each asset (base asset and bridge assets) in each Silo at any given time.

In the Interest Rate Model, the utilization ratio was calculated as the ratio of totalBorrowedAmount to totalDeposits. Borrowing the liquidity that is donated to the Silo contract could cause the utilization ratio to be greater than 100%. As a result, when the utilization ratio exceeds 100%, the InterestRateModel model treats utilization as critical, causing the interest rate to rapidly soar to astronomical levels, multiplying the collateral value several times over. Interest that has not yet been repaid is also taken into account in collateral calculations.

The conditions above allowed collateral manipulations.

Exploit POC:

1. An attacker donates tokens to a silo, increasing the token’s totalBalance (but not totalDeposits).
2. The attacker borrows an amount of these tokens from the silo such that amount <= totalBalance AND amount > totalDeposits.
3. The utilizationRate will exceed 100% (borrow > totalDeposits).
4. The InterestRateModel will calculate the interest to be a huge amount.
5. Collateral token prices will increase accordingly, allowing the attacker to borrow many other tokens and drain the silo.

Two different failures that lead to this bug;

1. The borrowed amount should not exceed the total deposited amount (utilizationRate > 100%)
2. The interest should not be calculated with a utilizationRate > 100%

We confirmed that the bug exists in our working repository. We reviewed the spec files and found that none of the rules could catch these failures.

To reduce computation time, the CVL rule included an explicit assumption that the utilization rate cannot exceed 100%. Therefore, the Certora Prover did not identify the attack. The Certora and the Silo teams were aware of the assumption and did not consider these scenarios feasible.

2. Examining the fix

After we understood the bug and the exploit scenario, we reviewed Silo’s code fix. Silo chose to mitigate the vulnerability by adding limitations and boundaries in the interest calculation function to limit the utilizationRate percentage and decrease the interest curve.

We investigated the fix by asking ourselves two questions:

1. Did the fix indeed close the door for this attack scenario?
2. Are there any other ways to exploit and abuse the fact that the utilization rate can exceed 100%?

To our understanding, the fix indeed prevents the attack scenarios. The proposed fix keeps the interest rate safe, not allowing it to increase in an undesirable way. We could not find any other way to harm the protocol with the high utilization rate.

3. Writing rules

During our manual checks and investigations, we added rules to guarantee that the fix corrected the issue.

We wrote the following rules:

1. cantExceedMaxUtilization — An invariant for guaranteeing that utilization cannot exceed 100%. This means that no one can borrow more than the deposited amount.

We’ve set the following invariant:

getAssetTotalDeposits(asset) >= getAssetTotalBorrowAmount(asset)

We’ve run the invariant on the fixed version and, as expected, got several violations. As described earlier we couldn’t find any other way to exploit these invariant violations.

2. interestNotMoreThenMax — A rule for testing the fix and proving that there is no other path for increasing the interest above its max limit. The plan was to test the rule against the vulnerable version (expected to see violations) and on the fixed version for proving the fix (expected proof).
The logic behind the rule we wrote was to measure the highest interest rate with parameters that will provide 100% utilization (10¹⁸) and then measure the interest rate again without requiring anything on the utilization (which means no utilization boundary).

We then placed the following logical expression:

assert unbounded_interest <= max_interest;

By doing this we are proving that in any path, any value of the interest won’t exceed the highest amount of interest calculated from the max utilization rate.

However, the InterestRateModel has various calculations that are complex to formally verify.

Inexplicitly, the following function called during the interest calculation contains a sophisticated exponential computation:

/// @notice Calculates the binary exponent of x using the binary

function exp2(uint256 x) internal pure returns (uint256 result) {..}

This function caused the verification of the rule to time out.

After some internal investigation, we finally came up with a solution that was approved by Silo’s team:

1. We redacted the overflow detection from the source code. This function contains the call for the exp2() function. In a case of overflow, the interest rate will be 0 and the property will still hold.
2. We restricted the prover to utilize the configuration of deployed assets in Silo and all fallback configurations, as they can only be changed by their owner.

After we overcame the timeout we ran the rules on the vulnerable version and got an expected violation, and on the fixed version we indeed got proof for the fix.

3. Fixing some rules for supporting the new version of the code (due to interface changes)

Lessons learned

1. Specifications need constant improvement
2. Don’t give up on a rule that timed out

The Certora Prover uses a unique technology for formal verification. It converts the source code and the spec file (which contains the rules) to an SMT formula that can later be solved via multiple SMT solvers. The final formula represents all possible running paths in the code with any value for any parameter. It’s equated to making a test with all the possible states.

Due to computational complexity, not all generated formulas can be solved. If the tool solves a formula — we will get a proof or counter-example. However, the Prover will time out if it cannot solve the formula.

For instance, complex code and complicated math could lead to such a timeout. In Silo’s interest calculation, we’ve faced complicated math with non-linear operations.

When a rule times out — the best solution is to simplify the code or the rule.

Simplification forces the tool to reduce the number of paths to check, making the proving work easier and quicker. There are a couple of techniques to achieve this, some of which involve creating assumptions for the validation process. Those assumptions must be carefully checked.

3. All assumptions must be proved and confirmed.

In the original project, we assumed that the utilization rate is always bounded between 0–100 to avoid time-outs. Therefore, the Prover ignored any other scenario. For the vulnerable code, this was an unsafe assumption. Assumptions can be proved by other rules or by careful manual review. During our analysis, together with Silo’s team, we approved a specific configuration and initialized states that pruned some infeasible paths that eventually solved the time-out for the interest module rules.

4. Unbounded utilization rate as a generic property

Borrowing more than the total deposited assets can be very dangerous, as we saw in the reported vulnerability.

Donating or transferring assets not through the deposit function is common among lending protocols. As we saw in previous attacks, a donation can lead to undesirable code behaviors.

Certora Prover simulates this scenario and with a proper rule can find any of its consequences.

The rules that we conducted for the utilization rate and the interest model can be considered as a generic property for other lending protocols as well.

While each protocol may have unique characteristics and complexities, most lending protocols share fundamental principles that should remain consistent. These principles can be expressed logically and translated into CVL rules.

Conclusion

Certora is excited to help the amazing Silo team secure their code. We plan to assist in the following ways:

1. Manually reviewing new code.
2. Writing new correctness rules in collaboration with the Code4rena community. We will allocate up to $100,000 for finding missing rules and suggesting new rules.
3. Utilizing the Certora Prover for early detection of bugs in the code and formally verifying the rules.
4. Utilizing Gambit for finding if the rules cover enough scenarios.