SCF #17
Award Completed
OtterSec

OtterSec is a blockchain security company focused on identifying and patching critical exploits before our clients go to market.

Awarded
Awarded
Budget request:
$
137,500
*
WebsiteCode

Project Stage

Development

Category

Tools
Soroban

Based in

United States

Team size

5

Active since

February 2022
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.

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: