Stellar Community Fund

Products & Services

OtterSec plans to develop formal verification tooling for the Stellar ecosystem to help identify and mitigate critical exploits. Formal verification tooling enables developers to easily specify critical contract invariants, providing stronger guarantees and more confidence in development.

No items found.

Previous Project(s)

No items found.

Progress so far

Goals

To get there, we request a budget of

137,500

to:

Additional information

Pitch deck

No items found.

Deliverables

First Deliverable

[Almost finished]

We will develop a proof-of-concept harness to enable the verification of simple properties within Soroban contracts. We will need to adapt our existing work an formal verification from other blockchain frameworks to Stellar. Although the exact implementation may vary, this will likely involve designing a custom macro framework to support high level specification properties.The first property we will implement for our initial deliverable will be around error conditions of contracts. For example, an escrow contract should have well-defined error conditions around authentication.

Regarding the details on formal verification, happy to add some more color here. I think the end result would be built into the CLI. People would write down specifications in their Rust code, and run a single command to verify all the properties.

soroban verify

This draws inspiration from our work with existing tools such as the Move Prover, which is also a one command verification tool.as a trivial example of what this might look like in practice, consider atomic_swap from soroban-examples. it could make sense to declare

#[errors_if(amount_b < min_b_for_a || amount_a < min_a_for_b)]

‍

As a more meaningful example, in liquidity_pool it could make sense to define an invariant on the share value. for example, a critical security property of the pool is that share value should never decrease across operations.this becomes much more ergonomic to express as a data invariant, such as:

#[invariant(get_balance_a(old_e) * get_total_shares(e) < get_balance_a(e) * get_total_shares(old_e))]

‍

These sorts of invariants make it a lot easier to express critical security properties. from basic AMM xy=k invariants, to ensuring sufficient collateralization of lending protocols, to more complex global/data invariants, we’ve worked with developers across a variety of chains to use verification to write robust, declarative smart contracts.

We will produce a proof-of-concept codebase to enable verification of a simple property. A reviewer with understanding of Soroban contracts will be able to read our code and ensure that the verification proceeds as intended.

Links:

Check out our blog, Twitter, LinkedIn and Discord for updates:

Otter Audits, LLC

We are a blockchain cybersecurity firm focused on patching critical vulnerabilities before our clients go to market.

Team

OtterSec is a blockchain security company focused on identifying and patching critical exploits before our clients go to market. We work closely with leading teams to provide a holistic and collaborative approach to security.

Check out our blog, Twitter, LinkedIn and Discord for updates:

‍

The USD valuation of the budget request in XLM will be calculated using the CF Stellar Lumens-Dollar Settlement Price on December 5, 2022 as administered, maintained, and reported by the cryptocurrency index provider CF Benchmarks Ltd. (using the ticker “XLMUSD_RR”) (available at https://www.cfbenchmarks.com/indices/XLMUSD_RR). Learn more in the SCF Handbook.

*The USD valuation of the award in XLM is calculated using the CF Stellar Lumens-Dollar Settlement Price on July 5th as administered, maintained, and reported by the cryptocurrency index provider CF Benchmarks Ltd. (using the ticker “XLMUSD_RR”) (available at https://www.cfbenchmarks.com/indices/XLMUSD_RR)

**The USD valuation of the award in XLM is calculated using the CF Stellar Lumens-Dollar Settlement Price on December 16, 2021 as administered, maintained, and reported by the cryptocurrency index provider CF Benchmarks Ltd. (using the ticker “XLMUSD_RR”) (available at https://www.cfbenchmarks.com/indices/XLMUSD_RR)

*The USD valuation of the award in XLM is calculated using the CF Stellar Lumens-Dollar Settlement Price on September 27, 2021 as administered, maintained, and reported by the cryptocurrency index provider CF Benchmarks Ltd. (using the ticker “XLMUSD_RR”) (available at https://www.cfbenchmarks.com/indices/XLMUSD_RR)

* The USD valuation of the award in XLM is calculated using the CF Stellar Lumens-Dollar Settlement Price on the date of transfer as administered, maintained, and reported by the cryptocurrency index provider CF Benchmarks Ltd. (using the ticker “XLMUSD_RR”) (available at https://www.cfbenchmarks.com/indices/XLMUSD_RR)

*This budget request has not been fully awarded to the project. The USD valuation of the budget request in XLM will be calculated using the CF Stellar Lumens-Dollar Settlement Price on day of payment as administered, maintained, and reported by the cryptocurrency index provider CF Benchmarks Ltd. (using the ticker “XLMUSD_RR”) (available at https://www.cfbenchmarks.com/indices/XLMUSD_RR). Learn more in the SCF Handbook.

*This budget request has been awarded to the project in XLM. The USD valuation of the budget request in XLM will be calculated using the CF Stellar Lumens-Dollar Settlement Price on day of payment as administered, maintained, and reported by the cryptocurrency index provider CF Benchmarks Ltd. (using the ticker “XLMUSD_RR”) (available at https://www.cfbenchmarks.com/indices/XLMUSD_RR). Learn more in the SCF Handbook.