Poolshark
Security review case study
“Keel Formal treated Poolshark Limit and Cover as if the protocol was theirs. […] This is how auditing DeFi protocols should be.”
Poolshark Protocol
Overview
This document serves as an exposition of the Keel Formal security review process, detailing two engagements between the Keel Formal team and Poolshark protocol.
Keel Formal
Keel Formal is a Smart Contract security service provider re-imagining the traditional audit model with two competing internal Keel Formal teams, Smart Contract fuzzing, and a Pay-Per-Vulnerability pricing alternative. Keel Formal’s novel approach effectively incentivizes their security team to uncover as many vulnerabilities as possible and leave no stone unturned.
Poolshark
Poolshark protocol is a concentrated liquidity AMM which enables on-chain spot, limit, and stop-loss orders through it’s novel directional AMM technology.
Why Keel Formal?
Keel Formal boasts a security team with extensive experience in banking, DeFi, economics, trading, and software correctness. With a protocol as novel and complex as Poolshark’s Cover & Limit pools, it was paramount that Poolshark engaged a highly specialized team offering rigorous attention to detail. Keel Formal was exactly that team.
“10/10 They are hands down some of the absolute best security minds in the space.”
”Do not fade Keel Formal Audits”
Alphak3yPoolshark
The Reports
Dissecting The Security Reviews
In March of 2023 Keel Formal conducted a security assessment of Poolshark’s first protocol, Cover. The auditing approach championed manual analysis to uncover novel exploits and verify intended behavior with ancillary verification from formal methods such as fuzzing and symbolic execution.
Given the results of the first engagement, four months later Poolshark engaged Keel Formal a second time to review their Limit protocol.
Review #1, Poolshark Cover — Superior Communication and Collaboration
A team of three security researchers, with two Lead Security Researchers, began a 4-week Keel Formal review on the 17th of March. The review began with a kickoff call, where the Poolshark team detailed the Cover implementation and the Keel Formal team stress tested the design with precise questions.
Throughout the review, findings and recommendations were shared with the Poolshark team as they were uncovered by Keel Formal. Explicit written PoC (proof-of-concept) tests accompanied High and Critical issues. At the end of each week, the Keel Formal and Poolshark teams convened to discuss the findings uncovered, potential remediations, and design improvements.
Finally, Keel Formal scrutinized remediations made by the Poolshark team and included these updates in the scope of the ongoing audit.
During the 4 week review a total of 11 Critical, 5 High, 7 Medium, and 13 Low findings were uncovered by Keel Formal, confirmed and promptly remediated by Poolshark, and these remediations were finally reviewed by Keel Formal.
Review #2, Poolshark Limit — Invariant Testing 22 Critical Invariants
A team of six security researchers, with two Lead Security Researchers, began a 4-week Keel Formal review on the 18th of July. Similarly to the first review, Keel Formal held a kickoff call to understand and stress test the Limit codebase design.
Keel Formal continued to share findings and PoC tests as they were unearthed and discuss potential remediations in a weekly correspondence with the Poolshark team.
Additionally, during the weekly meetings Keel Formal worked with Poolshark to identify core protocol invariants and implement these in an Echidna fuzzing suite for the Limit protocol. Throughout the engagement 22 critical invariants were assessed with over a half a billion combined fuzzing runs.
During the 4 week review a total of 15 Critical, 9 High, 13 Medium, and 38 Low findings were uncovered by Keel Formal confirmed and promptly remediated by Poolshark, and these remediations were finally reviewed by Keel Formal.
At the end of the engagement, Keel Formal delivered a fully functioning Echidna fuzzing harness that Poolshark continues to use to provide invariant verification upon updates and modifications made to the protocol.
Results
During both reviews a combined 111 findings, 40 of which being High or Critical severity, were reported, remediated, and confirmed to be resolved.
Throughout both the Cover and Limit engagements the code coverage and edge case coverage of the repository tests improved dramatically, with additions of Keel Formal’s own test cases and PoCs.
Keel Formal directly assessed 22 core protocol invariants with a prepared Echidna harness for the Limit codebase. But more importantly, Keel Formal transferred Echidna fuzzing expertise to the Poolshark team who has gone on to implement and assess dozens of additional invariants across both the Cover and Limit codebases.
After engaging Keel Formal several times, the Poolshark team has significantly improved their security as a result of resolving over 40 pressing issues uncovered. Not only has Poolshark benefitted from periods of review from Keel Formal, but they will continue to develop with a security guided approach as a result of new testing and fuzzing practices moving forward.