Badger eBTC Audit + Certora Formal Verification Competition

Badger eBTC Audit + Certora Formal Verification details

• Total Audit + Formal Verification Prize Pool: $149,725 USDC

• Total Audit Prize Pool: $119,725 USDC

  • HM awards: $100,000 USDC
  • QA awards: $2,112.50 USDC
  • Gas awards: $2,112.50 USDC
  • Judge awards: $9,000 USDC
  • Lookout awards: $6,000 USDC
  • Scout awards: $500 USDC

• Total FV Prize Pool: $30,000 USDC

  • Real Bug Rules: $6,000 USDC
  • Coverage Rules $18,000 USDC
  • Participation: $3,000 USDC
  • Beginner Pool: $3,000 USDC

• Join C4 Discord to register

• Submit findings using the C4 form

• Read our guidelines for more details

• Starts October 24, 2023 20:00 UTC

• Ends November 14, 2023 20:00 UTC

Automated Findings / Publicly Known Issues

The 4naly3er report can be found here.

Badger provided 4 previous audit reports and known issues

Note for C4 wardens: Anything included in this Automated Findings / Publicly Known Issues section is considered a publicly known issue and is ineligible for awards.

Overview

eBTC is a collateralized crypto asset soft pegged to the price of Bitcoin and built on the Ethereum network. It is backed exclusively by Staked Ether (stETH) and powered by immutable smart contracts with minimized counterparty reliance. It’s designed to be the most decentralized synthetic BTC in DeFi and offers the ability for anyone in the world to borrow BTC at no cost.

• See Primary Readme.
• See Intro Video.
• See the eBTC Cheatsheet for additional videos and an up to date list of additional resources.
• See the Formal Verification Readme for FV details.

Links

Primary Readme contains further links.

• Previous audits: All findings contained in theses reports:
  • RiskDAO: https://github.com/Risk-DAO/Reports/blob/main/eBTC.pdf
  • Trust: https://badger.com/images/uploads/trust-ebtc-audit-report.pdf
  • Spearbit: https://badger.com/images/uploads/ebtc-security-review-spearbit.pdf
  • Cantina: https://badger.com/images/uploads/ebtc-security-review-cantina.pdf
  • Many additional links (cheatsheet): https://gist.github.com/GalloDaSballo/7b060bb97de09c539ec64c533dd352c6
• Documentation: Primary Readme
• Website: ebtc.finance
• Twitter: eBTCProtocol

Scope

See scope.txt

Legend:

💰 Can Receive Funds 🖥 Uses Assembly 📤 Transfers ETH 👥 DelegateCall 🧮 Uses Hash Functions 🔖 ECRecover 🌀 New/Create/Create2 ♻️ TryCatch Σ Unchecked

Scope Table:

Out of scope

All other contracts in the repo.

Especially:

• CRLens.sol
• EBTCDeployer.sol
• FeeRecipient.sol
• Migrations.sol
• MultiCdpGetter.sol
• LiquidationSequencer.sol
• SyncedLiquidationSequencer.sol
• /Proxy
• /TestContracts
• Echidna and Foundry Files
• Tellor related Files, Tellor will not be used

Additional Context

• Describe any novel or unique curve logic or mathematical models implemented in the contracts.
  • None.
• Please list specific ERC20 that your protocol is anticipated to interact with. Could be "any" (literally anything, fee on transfer tokens, ERC777 tokens and so forth) or a list of tokens you envision using on launch.
  • ONLY stETH, eBTC token
• Please list specific ERC721 that your protocol is anticipated to interact with.
  • none
• Which blockchains will this code be deployed to, and are considered in scope for this audit?
  • Ethereum mainnet
• Please list all trusted roles (e.g. operators, slashers, pausers, etc.), the privileges they hold, and any conditions under which privilege escalation is expected/allowable

All governable permissions can be assumed to be managed by a multisig + timelock configuration by default. Some functions will be callable my a smaller threshold of users with no timelocks to prioritize speed.

Governable Function

ActivePool

claimFeeRecipientCollShares
sweepToken
setFeeRecipientAddress
setFeeBps
setFlashLoansPaused

CollSurplusPool

sweepToken

BorrowerOperations

setFeeRecipientAddress
setFeeBps
setFlashLoansPaused

CdpManager

setGracePeriod
setStakingRewardSplit
setRedemptionFeeFloor
setMinuteDecayFactor
setBeta
setRedemptionsPaused

EBTCToken

mint
burn
(both variants of each)

PriceFeed

setFallbackCaller

The following functions can be assumed to be exemptions from a timelock due to impact on operational efficiency and ability to respond to emergency scenarios. See Known Issues for our stance on governance parameters.

ActivePool

claimFeeRecipientCollShares
sweepToken
setFlashLoansPaused

CollSurplusPool

sweepToken

BorrowerOperations

setFlashLoansPaused

CdpManager

setRedemptionsPaused

DOS Minimum Duration

• User operations, outside of Race Conditions, User Mistake or Design (e.g. Recovery Mode) should never be blocked
• Liquidations should always offer at least a 3% premium and Gas Stipend
• Coll Surplus should always pay back the surplus to the rightful Cdp owner

EIP Compliance

• ActivePool: Should comply with EIP3156
• BorrowerOperations: Should comply with EIP3156
• EBTCToken: Should comply with ERC20, ERC2612

Attack ideas (Where to look for bugs)

See Known Issues section and previous audit reports.

Main invariants

• PROPERTIES.md file contains the main invariants.
• Also see Price Feed state machine for reference.

Scoping Details

- If you have a public code repo, please share it here:  https://github.com/ebtc-protocol/ebtc
- How many contracts are in scope?:   41
- Total SLoC for these contracts?:  5805
- How many separate interfaces and struct definitions are there for the contracts within scope?:  17 Interfaces, 16 Structs
- Does most of your code generally use composition or inheritance?:   Inheritance
- How many external calls?: 6 seperate calls (to stETH token and Chainlink)
- What is the overall line coverage percentage provided by your tests?: 99%
- Is this an upgrade of an existing system?:  False
- Check all that apply (e.g. timelock, NFT, AMM, ERC20, rollups, etc.): ERC-20
- Is there a need to understand a separate part of the codebase / get context in order to audit this part of the protocol?:  False 
- Please describe required context:   n/a
- Does it use an oracle?:  Chainlink with potential to connect an arbitrary backup oracle.
- Describe any novel or unique curve logic or mathematical models your code uses:  No
- Is this either a fork of or an alternate implementation of another project?:  Liquity
- Does it use a side-chain?: No
- Describe any specific areas you would like addressed: Accounting / yield accrural math

Tests

Fresh build / run / test

yarn
cd packages/contracts
forge build 
forge test
yarn test

Gas report

forge test --gas-report

Certora Formal Verification Setup

See ./certora/README.md

Echidna and Medusa Invariants One Liners

Run Medusa with

yarn && git submodule init && git submodule update && solc-select use 0.8.17 && cd packages/contracts/ && medusa fuzz

Run Echidna With

yarn && git submodule init && git submodule update && solc-select use 0.8.17 && cd packages/contracts/ && yarn echidna --test-mode assertion --test-limit 100000

If you're having issues, use the Dockerfile