Skip to content

Commit

Permalink
f
Browse files Browse the repository at this point in the history
  • Loading branch information
HrikB committed Feb 5, 2024
1 parent 306309d commit 701813e
Show file tree
Hide file tree
Showing 6 changed files with 84 additions and 61 deletions.
1 change: 1 addition & 0 deletions .prettierignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
lib/
100 changes: 56 additions & 44 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,96 +1,108 @@
```
,-. .---. .-. .-. ,---. ,---. .---. _______ .---. ,--, .---. ,-.
|(|/ .-. ) | \| | | .-.\ | .-.\ / .-. )|__ __|/ .-. ) .' .') / .-. ) | |
(_)| | |(_)| | | | |-' )| `-'/ | | |(_) )| | | | |(_)| |(_)| | |(_)| |
| || | | | | |\ | | |--' | ( | | | | (_) | | | | | \ \ | | | | | |
| |\ `-' / | | |)| | | | |\ \ \ `-' / | | \ `-' / \ `-.\ `-' / | `--.
`-' )---' /( (_) /( |_| \)\ )---' `-' )---' \____\)---' |( __.'
(_) (__) (__) (__)(_) (_) (_) (_)
,-. .---. .-. .-. ,---. ,---. .---. _______ .---. ,--, .---. ,-.
|(|/ .-. ) | \| | | .-.\ | .-.\ / .-. )|__ __|/ .-. ) .' .') / .-. ) | |
(_)| | |(_)| | | | |-' )| `-'/ | | |(_) )| | | | |(_)| |(_)| | |(_)| |
| || | | | | |\ | | |--' | ( | | | | (_) | | | | | \ \ | | | | | |
| |\ `-' / | | |)| | | | |\ \ \ `-' / | | \ `-' / \ `-.\ `-' / | `--.
`-' )---' /( (_) /( |_| \)\ )---' `-' )---' \____\)---' |( __.'
(_) (__) (__) (__)(_) (_) (_) (_)
```

# Ion Protocol
Ion Protocol is a decentralized money market purpose-built for all types of staked and restaked assets. Ion protocol unlocks capital efficiency for yield-bearing staking collaterals using reactive interest rates, collateral-specific utilization, and price-agnostic liquidations. Borrowers can collateralize their yield-bearing staking assets to borrow WETH, and lenders can gain exposure to the boosted staking yield generated by borrower collateral.

## Documentation
Ion Protocol is a decentralized money market purpose-built for all types of staked and restaked assets. Ion protocol unlocks capital efficiency for yield-bearing staking collaterals using reactive interest rates, collateral-specific utilization, and price-agnostic liquidations. Borrowers can collateralize their yield-bearing staking assets to borrow WETH, and lenders can gain exposure to the boosted staking yield generated by borrower collateral.

## Documentation

To learn more about Ion Protocol without code, please visit:

- [Our website](https://ionprotocol.io)
- [User Docs](https://docs.ionprotocol.io)

To learn more about the protocol's technical details, please visit:

- [Audit Docs for Security Researchers](https://ionprotocol.notion.site/Ion-Protocol-Audit-Docs-c871ff178bf54447bd28018cd5a88f75?pvs=74)

## Audits
## Audits

> Please report any white hat findings for potential vulnerabilities to [email protected]
- OpenZeppelin Audit December 2023
- [Report to be released soon]
- [Hats Finance January 2024](https://app.hats.finance/audit-competitions)
- Regular Audit and Formal Verification Competition with Certora
- [Competition Ongoing]
- [Report to be released soon]
- [Hats Finance January 2024](https://app.hats.finance/audit-competitions)
- Regular Audit and Formal Verification Competition with Certora
- [Competition Ongoing]

## Community

To engage in conversations around Ion Protocol and the staking/restaking ecosystem, please join the [Discord](https://t.co/6np4WvIx70) channel or follow [@ionprotocol](https://twitter.com/ionprotocol) on X.
To engage in conversations around Ion Protocol and the staking/restaking ecosystem, please join the [Discord](https://t.co/6np4WvIx70) channel or follow [@ionprotocol](https://twitter.com/ionprotocol) on X.

## Usage

### Installing Dependencies
### Installing Dependencies

Install Bun

Install Bun
```shell
curl -fsSL https://bun.sh/install | bash
curl -fsSL https://bun.sh/install | bash
```

Run Bun install for javascript dependencies

```shell
bun install
```

Install jq
Install jq

```shell
brew install jq
brew install jq
```

### Environmental Variables
### Environmental Variables

Copy .env.example to .env and add environmental variables.
Copy .env.example to .env and add environmental variables.

```bash
MAINNET_RPC_URL=https://mainnet.infura.io/v3/
MAINNET_ARCHIVE_RPC_URL= # Archive node used for creating fork environments
MAINNET_ARCHIVE_RPC_URL= # Archive node used for creating fork environments
MAINNET_ETHERSCAN_URL=https://api.etherscan.io/api
ETHERSCAN_API_KEY=
RPC_URL= # RPC of the desired testnet used in deployment scripts
```

### Test

1. The test suite includes fork tests that require foundry ffi.
2. Add RPC_URLs to the .env and run forge test with the --ffi flag.
1. The test suite includes fork tests that require foundry ffi.
2. Add RPC_URLs to the .env and run forge test with the --ffi flag.

```shell
forge test --ffi
forge test --ffi
```

### Testnet Setup
1. Set up anvil as a mainnet fork.
- For the contracts using mainnet contract addresses as constants to work properly, the testnet needs to be a fork of a mainnet environment.
```bash
anvil --fork-url $MAINNET_ARCHIVE_RPC_URL --chain-id 31337
```

1. Set up anvil as a mainnet fork.
- For the contracts using mainnet contract addresses as constants to work properly, the testnet needs to be a fork of a mainnet environment.
```bash
anvil --fork-url $MAINNET_ARCHIVE_RPC_URL --chain-id 31337
```
2. Set anvil as the target RPC for the deployment script in `.env`
```bash
# ...other environmental variables
RPC_URL=http://localhost:8545
```
3. Run the testnet deployment script
```bash
bash node.sh
```
4. Run the foundry script to verify that the contracts are working properly.
```bash
forge script script/__TestFlashLeverage.s.sol --rpc-url $RPC_URL
```

```bash
# ...other environmental variables
RPC_URL=http://localhost:8545
```

3. Run the testnet deployment script
```bash
bash node.sh
```
4. Run the foundry script to verify that the contracts are working properly.
```bash
forge script script/__TestFlashLeverage.s.sol --rpc-url $RPC_URL
```

### Format

Expand Down
Binary file modified bun.lockb
Binary file not shown.
36 changes: 21 additions & 15 deletions certora/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,26 +6,28 @@ The Formal Verification (FV) component of the contest is about using the Certora

## Scope

| Contract | SLOC |
| ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | --- |
| [IonPool.sol](https://github.com/Ion-Protocol/ion-protocol/blob/master/src/IonPool.sol) | 578 |
| [Liquidation.sol](https://github.com/Ion-Protocol/ion-protocol/blob/master/src/Liquidation.sol) | 149 |
| [InterestRate.sol](https://github.com/Ion-Protocol/ion-protocol/blob/master/src/InterestRate.sol) | 212 |
| Contract | SLOC |
| ------------------------------------------------------------------------------------------------- | ---- |
| [IonPool.sol](https://github.com/Ion-Protocol/ion-protocol/blob/master/src/IonPool.sol) | 578 |
| [Liquidation.sol](https://github.com/Ion-Protocol/ion-protocol/blob/master/src/Liquidation.sol) | 149 |
| [InterestRate.sol](https://github.com/Ion-Protocol/ion-protocol/blob/master/src/InterestRate.sol) | 212 |

## Overview

- 25% (10,000 USDC) of this contest will be allocated for FV.
- Conventional bug submission, issue judgment, and all reward distribution will be managed by Hats Finance.
- FV component is unique as participants are incentivized to implement and verify high coverage properties using the Certora Prover.
- The judging of FV is conducted by Certora, with different submissions, incentives, and judging processes compared to the standard contest. These processes are explained in this document.

## Getting Started

- **Get access to the Prover**:
- First time participants, [Register](https://www.certora.com/signup?plan=prover) to automatically receive an access key.
- **Update expired key**:
- **Update expired key**:
- Send a message in the [Certora Discord](https://discord.gg/usnJm6p4)'s `access-key-request` channel.
- **Tool Installation**:
- **Tool Installation**:
- Follow [installation instructions](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) to download the `certora-cli` tool. Use the latest version of the tool available at the start of the contest, throughout the whole contest.
- **Learning Resources**:
- **Learning Resources**:
- Complete the [tutorials](https://docs.certora.com/projects/tutorials/en/latest).
- Search the [docs](https://docs.certora.com/en/latest/index.html) for any additional information.
- Check out some of our [examples](https://www.github.com/certora/examples).
Expand All @@ -34,24 +36,26 @@ The Formal Verification (FV) component of the contest is about using the Certora
- Conduct verifications on the main branch.
- Grant access to `teryanarmen` and `pistiner` for judging.
- **Support Channels**:
- For tool-related issues, send a detailed message with a job link in `help-desk` channel in Discord. Remove the anonymousKey component from the link if you wish to limit viewing to Certora employees.
- For tool-related issues, send a detailed message with a job link in `help-desk` channel in Discord. Remove the anonymousKey component from the link if you wish to limit viewing to Certora employees.
- For FV contest questions, use the relevant community verification channel in Discord.

## Incentives

- 25% (10k) of the total pool is allocated for FV.
- FV pool is split into three categories
- **Participation**: 10% of pool awarded for properties identifying public mutants.
- **Participation**: 10% of pool awarded for properties identifying public mutants.
- **Real Bugs**: 20% of pool awarded for properties uncovering actual bugs.
- **Coverage**: 70% of pool awarded for properties identifying private mutants.
- If no properties are accepted for real bugs, the pool will be rebalanced to 90% coverage and 10% participation.
- Mutants are mutated versions of the original code which create vulnerabilities. These mutants are used to gauge verified properties' coverage of the original code.
- Public mutants used for evaluating participation rewards can be found in `certora/mutations`.
- Participation and coverage reward can be calculated as follows
- Each mutant is worth $0.9^{n-1}$ points where $n$ is the number of participants that caught the mutant.
- If we let $P$ be the total FV pool and $T$ be the sum of all mutants' points, we can define each participant's reward as $ \frac{P}{T} \cdot \frac{0.9^{n-1}}{n} $
- Each mutant is worth $0.9^{n-1}$ points where $n$ is the number of participants that caught the mutant.
- If we let $P$ be the total FV pool and $T$ be the sum of all mutants' points, we can define each participant's reward as $ \frac{P}{T} \cdot \frac{0.9^{n-1}}{n} $
- Real bug rewards will be awarded for properties that are violated because of the bug. Only the bug submitter can submit a spec for that bug. 25, 12, or 1 points will be allocated based on the severity of the bug (H/M/L).

## Submission Guidelines

- **Development Constraints**:
- Participants are allowed to create and modify configuration, harnesses, and specification files.
- Some conf files have commented out settings which can be used to help with running time.
Expand All @@ -64,7 +68,7 @@ The Formal Verification (FV) component of the contest is about using the Certora
- Submissions with tool errors, compilation errors, or timing-out rules will not be considered.
- Ensure configurations do not time out; retest to confirm consistency.
- **Configuration Naming**:
- For coverage and participation: Name configuration files as `ContractName_[identifier]_verified.conf`. The identifier is optional and should be used when multiple configurations are created for one contract.
- For coverage and participation: Name configuration files as `ContractName_[identifier]_verified.conf`. The identifier is optional and should be used when multiple configurations are created for one contract.
- Example: `ERC20_summarized_verified.conf`.
- For real bugs: Replace `_verified` with `_violated` in the configuration file name.
- **Real bug submissions**:
Expand All @@ -77,14 +81,16 @@ The Formal Verification (FV) component of the contest is about using the Certora
- A verified run of the property on the fixed version must be included.

## Evaluation Process

- **Preliminary Results**: Initial findings will be announced along with the mutations used for evaluation. A google sheet showing which mutants were caught by which participants will be shared. Participants will have a 72-hour period for review and submit corrections in case a certain mutant is marked as not caught but they actually caught it.
- **Correction Submissions**: Corrections must include a verified run on the source code and a violated run on the mutant. Any changes other than the mutation will result in exclusion of the correction.
- **Check your work**: Use `certoraMutate` to evaluate your work on public mutations and random mutations created by gambit.
- Gambit confs will be provided for all the in scope contracts. To run mutation testing, you can do `certoraMutate --prover_conf certora/confs/contract_verified.conf --mutation_conf certora/confs/gambit/contract.mconf` from root of the directory, same as `certoraRun`.
- Gambit confs will be provided for all the in scope contracts. To run mutation testing, you can do `certoraMutate --prover_conf certora/confs/contract_verified.conf --mutation_conf certora/confs/gambit/contract.mconf` from root of the directory, same as `certoraRun`.
- You can change the number of bugs that are injected by adding manual mutations in the `mutations` folder in a similar fashion to the public mutations or by changing the value of automatic mutation in the contract's mutation conf.
- Use `--dump_csv file_path.csv` flag with `certoraMutate` to get a csv output of your results. During evaluation, the data from this output is aggregated for all participants used for coverage and participation evaluation. Make sure everthing looks right, specifically, all rules should have "SUCCESS" for the original run.

Check failure on line 90 in certora/README.md

View workflow job for this annotation

GitHub Actions / codespell (ubuntu-latest)

everthing ==> everything

Check failure on line 90 in certora/README.md

View workflow job for this annotation

GitHub Actions / codespell (ubuntu-latest)

everthing ==> everything

## Report Compilation

- **Public Disclosure**: The report, encompassing top submissions and mutation descriptions, will be made public post-analysis.
- Not all top properties focus on the quantity of mutations caught; high-level invariants are highly valued.
- Future mutations will be adjusted to properly value high quality properties.
Expand All @@ -95,4 +101,4 @@ The Formal Verification (FV) component of the contest is about using the Certora
- Focus on concise, high-level properties.
- Reduce overuse of `require` statements.
- Ensure clear documentation, proper naming, and formatting.
- **Participant Contributions**: The top participants' `certora` folders will be included in the public repository.
- **Participant Contributions**: The top participants' `certora` folders will be included in the public repository.
6 changes: 4 additions & 2 deletions offchain/scrapePastExchangeRates.ts
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,10 @@ const ETHERSCAN_URL =
CHAIN_ID! == "5"
? process.env.GOERLI_ETHERSCAN_URL
: process.env.MAINNET_ETHERSCAN_URL;
const RPC_URL =
CHAIN_ID == "5" ? process.env.GOERLI_ARCHIVE : process.env.MAINNET_ARCHIVE_RPC_URL;
const RPC_URL =
CHAIN_ID == "5"
? process.env.GOERLI_ARCHIVE
: process.env.MAINNET_ARCHIVE_RPC_URL;

const exchangeRateAddresses = {
lido: {
Expand Down
2 changes: 2 additions & 0 deletions package.json
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
"module": "index.ts",
"type": "module",
"scripts": {
"prettier": "prettier --write '**/*.{md,yml,yaml,ts,js}'",
"coverage": "./coverage.sh",
"solhint": "solhint 'src/**/*.sol'",
"slither": "slither src",
Expand All @@ -16,6 +17,7 @@
"date-fns": "^2.30.0",
"dotenv": "^16.3.1",
"ethers": "^6.7.1",
"prettier": "^3.2.5",
"solhint": "^3.6.2",
"viem": "^1.14.0",
"web3": "^4.1.2"
Expand Down

0 comments on commit 701813e

Please sign in to comment.