Tokemak Audit Competition— rewards up to $18K in USDC

Starting Feb 26th, 2024, at 15:00 GMT to Mar 11th, 2024, at 15:00 GMT

We invite all white hat hackers to join the hunt on Tokemak audit competition

All experience levels are welcome; whether you are a seasoned security veteran or an amateur, show us what you got! Prizes will be given based on the severity level of each vulnerability found.

About the Competition

Starting Feb 26th, a new vault will open in the Hats dApp — “Tokemak”.
Participants can check the contracts in scope and start searching for bugs.

Tokemak V2 (Autopilot) introduces a new way to LP in DeFi: autonomous optimization of liquidity across DEXs and pools of your choice to capture the best yields. Launching with support for LST/ETH stable-pools, you deposit only ETH, and Tokemak will continuously rebalance into the optimal yield-bearing pools. Set and, forget, and save both gas costs and your time while returns are compounded into ETH.

Competition Focus
This competition focuses only on the Strategy portion of the Autopilot system. The purpose of the Strategy contract(s) is to weigh the return profile of a set of destinations and determine if a given rebalance (e.g. swap Pool A LP units for Pool B LP units) is favourable for the Autopool. The Strategy is able to perform this analysis via on-chain data from our Stats system. This means the Strategy always has the intention of being in the “best” destinations possible and it is up to our off-chain solvers to propose what to do. Our goal with this audit is to verify the Strategy does this in an overall safe manner.

The competition code language is Solidity and the SLOC estimation for this competition is ~800 SLOC.

The vault will be deployed to Arbitrum chain and onchain submissions will be done on Arbitrum. Please make sure that you have enough Arbitrum ETH.

Stay up-to-date with the competition, chat with the team, and get your questions answered by joining the dedicated Discord channel on the Hats server.

All audit reports will be published in our Discord on the day of the competition. Don’t miss the latest updates and insights — join now and be the first to know!

Audit competition rewards

• Deposited Amount: The deposited amount is ~$20K in USDC, making the available prize pool ~$18K in USDC.
• Service Fee: All rewards mentioned in this article and on the Hats dApp UI have already deducted a 20% Hats service fee.
• Severities: Low, Medium, High, Gas saving, Formal verification

Rewards and calculation
For our audit competition, the entire prize pool is up for grabs across all severity levels. Each severity level has a designated point value and a maximum payout cap.

Maximum Reward Caps per Submission:

• Low Severity: 90 USDC (equals 1 point)
• Medium Severity: 1080 USDC (equals 12 points)
• High Severity: 2250 USDC (equals 25 points)
• Formal verification: 9000 USDC, shared by special rules

*For simplicity, there is a relation between the points and the cap. If the cap is 2,000 USDC it equals to the allocation of 2 points per valid submission.

Points are consistently awarded within the same severity level unless the committee decides to adjust this. For instance, both the first and second low-severity findings will earn 1 point each. This standard applies to medium and high severities as well.

Calculating the Winner’s Reward:

The formula for a winner’s reward is as follows:

Point Value = Prize Pool / Total Points*

*Awarded for the entire competition

Examples for Clarity:

Example #1:

• 163 Low Severity: 163 points
• 1 Medium Severity: 12 points
• 1 High Severity: 25 points

Total points: 200

In this scenario:

• Value of 1 Point = 9000 USDC/200 Total points = 45 USDC
  The rewards for this example will be as follows:
• Low (163 points): $45 each
• Medium (12 points): $540 in total.
• High (25 points): $1125 in total.

Example #2

• 10 Low Severity: 10 points
• 1 Medium: 12 points

Total points: 32

In this scenario:

• Value of 1 Point = 9000 USDC/22 Total points = 409 USDC
  The results exceed the max reward per low severity, so the value of a point is adjusted.
• The rewards for this example will be as follows:
• Low (1 points): $409 each -> $90
• Medium (12 points): $4908 -> $1080

Severities

High Severity

Issues that will qualify for this bracket will be assigned 25 points.

High-severity vulnerability description:

For a submission to be considered a HIGH-risk vulnerability, issues must:

• Direct theft of any user funds, whether at rest or in motion
• Long-term freezing of user funds
• Theft or long-term freezing of unclaimed yield or other assets
• Protocol insolvency

Medium Severity

Issues that will qualify for this bracket will be assigned 12 points.

Medium severity vulnerability description:

Issues that lead to an economic loss but do not lead to direct loss of on-chain assets. Examples are:

• Gas griefing attacks (make users overpay for gas)
• Attacks that make essential functionality of the contracts temporarily unusable or inaccessible
• Short-term freezing of user funds

Low severity

Issues that will be qualified for this bracket will be assigned with 1 point.

Low severity vulnerability description:

• Issues where the behavior of the contracts differs from the intended behavior (as described in the docs and by common sense), but no funds are at risk.

Limitations

Reporters will not receive a bounty for any known issue, such as:

• Issues mentioned in any previous audit reports
• Vulnerabilities that were already made public (either by HATs or by a third party)
• “Centralization risks” that are known and/or explicitly coded into the protocol (e.g. an administrator can upgrade crucial contracts and steal all funds)
• Attacks that require access to leaked private keys or trusted addresses
• Issues/contracts mentioned in the out-of-scope section

Submission Guidelines — High/Medium/Low severities:

General Information:

• The Hats team will create a new repository called “Tokemak audit competition-…” under the Hats.finance organization on GitHub. The repository will be kept private until the competition starts. Hats bot will fork it on the first submission. To participate, security researchers must submit their findings on-chain, and an automatic GitHub issue will be generated in the forked repository.
• How it Works: Video Explanation

SUBMISSION GUIDELINES:

• Submissions should be made using our Dapp.
• You can submit one on-chain submission mentioning all issues found on the repo.
• All new submissions will be created on Hats forked repo on Hats: Hats GitHub

Report Format:

• Please send a plain ASCII description in the following format:
• [TITLE]: A short description of the issue.
• SEVERITY: Either High, Medium, or Low (as per the rules).
• Submission should contain at least one test demonstrating the problem and, if possible, a possible fix.

Report Template:

• Description: Describe the context and the effect of the vulnerability.
• Attack scenario: Describe how the vulnerability can be exploited.
• Attachment:
• Proof of Concept (PoC) File: Provide a file containing a proof of concept (PoC) that demonstrates the vulnerability.
• Revised Code File (Optional): If possible, provide a second file containing the revised code that offers a potential fix for the vulnerability. This file should include:
• Comment with a clear explanation of the proposed fix.
• The revised code with suggested changes.
• Add any additional comments or explanations clarifying how the fix addresses the vulnerability.
• Recommendation: Describe a patch or potential fix for the vulnerability.

***Due to the nature of the audit competition mechanism, the report will not be encrypted.***

Evaluation:

• The first participant to submit an issue following guidelines gets a bounty for that issue (issues already received or out of scope will not receive a reward).
• The competition starts on Feb 26th at 15:00 GMT and ends on Mar 11th at 15:00 GMT.
• Issues that we are aware of (as witnessed by any open issues in the repository) will not be eligible for the bug bounty.

Formal verification

Researchers are given the opportunity to utilize the Certora Prover to find bugs and prove properties regarding the predefined contracts that have been setup within the codebase. Specs will be evaluated based on the properties below.

50% of the total prize pool plus any leftover rewards from the audit pool will be allocated for formal verification.

Getting Started

Get access to the Prover:

• First time participants, Register to receive an access key.

Update expired key:

• Send a message in Certora Discord’s `access-key-request` channel.

Tool Installation: Follow installation instructions 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:

• Complete the tutorials.
• Search the docs for any additional information.

Contest Participation:

• Import the public repository into a new private repository at the contest’s commencement.
• Conduct verifications on the main branch.
• Grant access to `teryanarmen` and `nd-certora` 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 FV contest questions, use the relevant community verification channel in Discord.

Formal verification Incentives

The FV pool is split into three categories

• 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.

Participation and coverage reward can be calculated as follows:

• Each mutant’s is worth 0.9(n-1)n points where n is the number of participants that caught the mutant.
• If we let P be the pool amount and T be the sum of all mutants’ points, and n the number of participants that caught the mutant, we can define each participant’s reward as PT0.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).

Formal verification Submission Guidelines

• Submissions should be marked as formal verification severity and include links to a private repo containing the spec for the entire project.
• Properties for real bugs will be submitted as github issues on the same private repo and must contain a link to the normal bug submission through Hats platform marked with relevant severity (L/M/H).
• Submissions will not be public and will only be shared with the committee by sharing your private repo on github with @teryanarmen.

Development Constraints:

• Participants are allowed to create and modify configuration, harnesses, and specification files.
• All coverage and participation submissions must pass on the unaltered original codebase.
• Source code modifications are prohibited.
• Evaluations are based on the original code; configurations reliant on code changes will be disregarded.
• Utilize the latest version of `certoraRun` available at contest start.
• Avoid updates during the contest, even if new versions are released.
• 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 exist per contract.
• Example: `ERC20_summarized_verified.conf`.
• For real bugs: Replace `_verified` with `_violated` in the configuration file name.

Real bug submissions:

• Real bug submissions must include:
• A link to the accepted underlying issue submitted through the Hats platform.
• Explaination of the property that finds the bug.
• A link to a violated run of the property must be included.
• A proposed solution as a diff between the buggy and fixed code.
• A verified run of the property on the fixed version must be included.

Formal verification Evaluation Process

Preliminary Results: Initial findings will be announced along with the mutations used for evaluation. Participants will have a 72-hour period for review and submit corrections.

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.
• You can change the number of bugs that are inject 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 gambit conf.
• Use — dump_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, all rules should have “SUCCESS” for the original run.

Compensation and Impact

A prize pool of ~$18K USDC and NFT rewards from our hacker collection will be distributed among security researchers who submit eligible vulnerability disclosures.

Compensation payment timeline:

• Ten days after the competition ends, we will announce a winner list.
• Alongside the winner announcement post, submitters can send disputes to the committee team and request clarification. They can also involve the Hats security team in the process. The goal is to facilitate honest and professional debate regarding disputed submissions.
• Between 7–14 days after the announcement, we will publish a split contract where the winners can claim their rewards.
• HATS Service Fee: A 10% deduction from the payout will always be allocated as the service fee.

Security researchers play a crucial role in fostering trust and confidence in Web3 technologies, paving the way for mass adoption. By participating in this competition, security researchers can gain recognition for their work, raise their profile, and make valuable connections in the Web3 security ecosystem. Ultimately, they can contribute to creating a more secure and equitable community.

Join TokemakAudit Competition today and participate in the movement to secure the future of Web3 and decentralized finance. Check the Hats Finance dApp for more information and in-scope contracts.

Stay tuned and check Hats dApp:https://app.hats.finance/audit-competitions