Proof of Solvency

hgedia · December 17, 2024, 10:32am

This topic is to discuss the proposal submitted by @utkarshdagoat . Please see below for the details of the proposal and discussion.

17th Dec ,2024
Current status: Under Consideration.
Opened for community discussion on : 17th Dec, 2024.

utkarshdagoat · December 17, 2024, 10:50am

Proof of Solvency in o1js

Project Background

Proof of solvency is a tool for centralized exchanges to gain user trust and become transparent about their assets in equity and debt. It ensures that their equity >= debt at any point of time.

In design for proof of solvency we create a world state tree for the user’s account balances(debt and equity) and cex balances. The main objective is to ensure correctness and validitation for the total equity >= total debt constraint while building this world tree through zksnarks

It was developed by Privacy + Scaling Explorations you can read more about it here

Proposal Overview

Problem:
Centralized exchanges are center for all kinds of borrowing and lending. User do not trust exchanges with their funds in fear that the exchange is not solvent and this fear is justifiable as we saw the FTX crash making people loose all funds. The exchange cannot just make the data about user assets public to justify solvency as it will be a huge privacy breach.
Solution:
This problem is solved by proof of solvencies. This enables users and auditors to verify that the centralized exchange is solvent without leaking data about each user’s funds.
Impact:
By writing the proof of solvency in o1js and making it more cost efficient and less complex can lead to it’s wider adoption among central exchanges thus increasing the popularity of o1js as a ZkDSL.
The circuits can also serve as an example for developers coming to ecosystem as they can see full blown proof generation system in place with o1js. I also plan to create various benchmarks for different circuit designs that one can think off so this will definitely help zkApp developers to see the tradeoff between various design and choose one suitable to their need!
Audience:
People working on centralized exchanges or anything which handles user’s funds in a centralized way.
Additioanlly all zk and o1js enthusiasts will surely like this work!

Architecture & Design

Detailed Design/Architecture:

Explaination for Proof of Solvency

The example below is for the “updated” proof of solvency protocol. This version of the protocol mitigates the “Dummy User Attack” vulnerability which was in the initial version of the protocol.

Let’s say there are 2 assets MINA,USDC in our CEX and 4 Users operate in out cex U1,U2,U3,U4. The users interact with our CEX and do the following actions
NOTE: In the example below we will take USDC as base asset for other tokens 1 MINA = 100 USDC and 1 BTC = 10000 USDC.

U1 Deposites 100 MINA and 10,000 USDC to our CEX. then uses the 100 MINA as LOAN Collateral for 10000 USDC.
U2 deposits 20 MINA.Swap 10 MINA for 1,000 USDC
U3 deposits 10,000 USDC. Uses the 5,000 USDC as COLLATERAL Margin for 50 MINA.
U4 deposits 200 MINA. Uses 20 MINA as Loan Collateral for 2000 USDC. Swap 1000 USDC for 10 MINA from U2.

NOTE The various types of loan collateral(LOAN, COLLATERAL MARGIN, and COLLATERAL PORTFOLIO MARGIN) are to cater to binance’s loan buisness logic. These loan collateral types may differ from exchange to exchange. I have included them in this implmentation for a fair benchmark angaist other implementaion as not taking them into consideration will lower the parameters.

The user balance sheet for each token:
MINA Balance Sheet

User	Equity	Debt	COLLATERAL LOAN	COLLATERAL MARGIN	COLLATERAL PORTFOLIO MARGIN
U1	100	0	100	0	0
U2	10	0	0	0	0
U3	50	50	0	0	0
U4	210	0	0	20	0
Total	370	50	100	20

USDC Balance Sheet

User	Equity	Debt	COLLATERAL MARGIN
U1	20,000	10,000	0
U2	1,000	0	0
U3	10,000	0	5,000
U4	1,000	2,000	0
Total	32,000	12,000	5,000

So for CEX to be solvent it needs to hold net for each asset i.e Total Equity - Total Debt . As it has 320 MINA and 20,000 USDC the platform is solvent for all user

Dummy User Attack and Tier Ratios

The dummy user attack goes as follows:
A CEX has many assets under control including high market cap and low market cap coins. Let MINA be a high Market cap coin and XYZ be a low market cap. Consider the following user actions:

Alice submits 100 MINA tokens (100USDC each)
Bob submit 1000 XYZ token (10 USDC each)
Now an attacker comes and submit 1000 XYZ tokens and keep them as collateral for 100 MINA.
Now the Platform has 2000 XYZ tokens and 0 MINA tokens. If alice now would like to withdraw her tokens it can only be done by selling 1000 XYZ tokens in the open market and as the market cap of XYZ token is low such a huge sell will crash XYZ tokens price.

Thus the platform is insolvent as:

The platform now can’t meet its obligations to users because it doesn’t have enough MINA in reserves.
The attacker (Dummy User) effectively caused a drain of the platform’s high-market-cap assets (MINA), while leaving the platform stuck with low-market-cap XYZ Coin that can’t be easily sold.

Tier Ratios
To mitigate the Dummy User attack we introduce tier ratio’s which define an array of a collateral haircut which is a reduction in the usable value for collateral asset. For example tier ratios for MINA might look like:
[0-1000 USDC: 100%, 1000-2000 USDC: 90%, 2000-5000 USDC: 80%, ...]
This means that:
If the USDC value for MINA to be used as collateral is within the first range (0-1000), 100% of its value can be used as collateral.
If it’s between 1000-2000 USDC, only 90% of its value can be used as collateral.
If it’s between 2000-5000 USDC, only 80% can be used.
Thus for low market cap we can adjust the tier ratio’s for those asset in such a way that we can prevent the dummy user attack.

Constraints and Circuit Design

Main Structures
A UserAction struct is made for every interactions that user does with the exchange. These user actions alter the state of the CexAssetTree and the AccountTree.With the constraints in the circuit we ensure the correctness in building these Merkle Tree’s.
Below are some basic structures along with the UserAction Struct.

class TierRatio extends Struct({
    BoundryValue: UInt64,
    Ratio: UInt64
})

class CexAssets extends Struct({
    totalEquity: UInt64,
    totalDebt: UInt64,
    Baserice: UInt64,
    // All loan Variables
    LoanCollateral: UInt64,
    ...
    
    LoanTierRations: Provable.Array(TierRatio,10) // There will always be 10 tier ratios for each percentage [100-90%,90-80%..]
})

class Asset extends Struct({
    Equit: UInt64,
    Debt: UInt64,
    BasePrice: UInt64,
    // All other loan variables
    LoanCollateral: UInt64,
    ...
})

class UserAction extends Struct({
    beforeAccountRoot: Field, // Account Tree Root before the user actions
    afterAccountRoot: Field, // changed root after the user action
    AccountIndex: UInt64, // the account index in db where the user is stored
    AssetForUpdate: Asset // This will most probably be an array I will try with various lenghts and try to find the best optimized result
}){}

Commitment for Assets
The Asset Map is used to calculate the commitment for asset’s.

Here the key is the hash(assetIndex) where assetIndex represent the index that it is stored by in the database.
The value is hash(TotalEquity,TotalDebt,BasePrice....commitment(loan_variables)) and the commitment is the root of the AssetMap

Commitment for User Accounts
An Indexed merkle map is used to represent the account tree. In this map

Key - hash(accountId) where the accountId uniquely represents a User
Value - hash(TotalEquity,TotalDebt,assetCommitment) where TotalEquity and TotalDebt is in the base price. assetCommitment is calculated simply in this case as it is infeasable to store an Asset Map for each user’s asset.

Circuits and Contract

In our circuit design the main goal is to verify the correctness in buidling of the world state tree i.e

CexAsset Tree/Map
UserAssets Tree/Map

We will run our circuits for a batch of operations. Thus, Let there be k batches for building the current world state. So the following circuits are for the k+1 batch.
CexAsset Circuit
Let Proof_k be the proof of the last batch. Then the following are the inputs to the circuit

Proof_k
IndexedMerkleMap of the CexAssets
userActions[] array of useractions done in the batch
Public Output is the root commitment of the CexAsset Map.
Constraints
Proof_k.publicOutput = CurrentMap.root
Apply the userActions[] update to the tree ensuring that for each token TotalEquity > TotalDebt and the calculation is done in accourdance to the collateral haircuts.

User Asset
For User Asset things get a little complicated as the size of IndexMerkleMap for user Tree can get large while for the CexAsset a Centralized Exchange such as binance only supports 500 Assets So for this the depth of 9-10 is fine and we can take directly as input to the circuit. But for user’s let’s say binance have 200million which a approx. of depth 28 which may increase proof generation time if we take it direct input. So the Approaches differ in the way we construct circuit inputs and do DB management while the constraint remains the same.
Approach 1: Direct Map Input
This is pretty much same as the last circuit.Let Proof_k be the proof of the last batch. Then the following are the inputs to the circuit

Proof_k
IndexedMerkleMap of the Users
userActions[] array of useractions done in the batch
Public Output is the root commitment of the CexAsset Map.
Constraints
Proof_k.publicOutput = CurrentMap.root
for each user in userActions[]:
- the equity of each token should be equal to or greater than the total collateral
- collateral must be sufficient to cover their debts according to the collateral ratio tiers
- update the tree
- userActions[i].beforeAccountRoot = userActions[i-1].afterAccountRoot

Approach 2: Whole lot of MerkleWitness
In Approach 2 we store the whole Users Map but to the Circuit we provide witness to prove that a user is solvent. So for a Batch Let’s say:

userActions[] These are userActions taken by the user
MerkleMapWitness it is the witness after theUser's MerkleMap is updated with the userActions[].
userAssets[] is TotalAssets for the ith user in the userActions[]. The Asset can also be a IndexedMerkleMap but storing IndexedMerkleMap for each user may be storage inffecient.
LastProof is the proof from the lastBatch for this user
Constraints:
compute the value of the node for each asset which will be hash(userId,comm(userAssets)) and use the witness api to see if it matched userActions[BATCH_SIZE].root.
for each action in userActions[]:
- userActions[i].beforeRoot = userActions[i].root
- Total Equity > Total Debt for each Asset at every i.

NOTE This circuit will be recursive as we would not store a proof for every evaluation of this circuit. It is better to have a aggregated proof for each user which verifies that each action that the user took does not create insolvency.
We can also aggregate each User’s proof and the Cex proof to create one big proof of solvency.
This method enables high parallelization at the trade off of storage and precomputation that we store and create the MekleMapWitness for every.
Another Note. By parralellization I mean that we compute the circuit in a forked process on the cpu as typescript is not multi-threaded this can be a hack

Approach3: Sharding of the UserMap
This is basically same as Approach 1 but the way we store User’s Map is different.
We shard the MerkleMap say on userId i.e create 2 or more different IndexedMerkleMap this can decrease proving times as we have decrease the size of the map input.
This method will include a lot of hit and trials to see which height vs storage is the best output.

BatchProofs
The user proof and cex proof can be aggregated into a single proof and
The input to the circuit is the following BatchCircuitInput:

Class BatchCircuitInput extends Struct({
    beforeCexAssetRoot: Field,
    batchCommitment: Field,
    afterCexAssetRoot: Field,
    beforeUserRoot: Field,
    afterUserRoot: Field,
    userProof: Proof<>,
    cexProof:Proof<>
}){}

There is also a public input to the program BatchCommitment which is defined as hash(beforeAccountRoot,AfterAccountRoot,beforeCexAssetRoot,AfterCexAssetRoot)
Following are the constraints for BatchCircuitInput:

verify batchCommitment is computed correctly.
verify the userProof.publicOutput.root = afterCexAssetRoot
verify the cexProof.publicOutput.root = afterUserRoot

Verification
The Users and auditors can verify the computation is done correctly when all the Maps and proofs are published. They can do the following steps:

check equation: batch_commitment_n = hash(cexAssetRoots[n-1], cexAssetRoots[n], userAccountRoots[n-1], userAccontRoots[n]).
- when n = 0, theCexAssetRoots[-1] and userAccounRoots[n-1] is the empty root;
- check verify(batch_commitment_0, proof_0, verifying key) output;
- check whether AssetTreeRoot equals to the commitment of published AssetList by CEX

A user can do the following fetch the account info and the userProof from the cex and do:

create the asset commitment and compute the witness for his proof in a merkle tree and verify. userProof.root = root

Proof System

The implementation for the proof system can be done in two ways. First is to use a proof generating backend with storing the maps in the DBs. Another way is to store the commitments of users on the protokit runtime itself and change the circuits accordingly.

Backend Server

The following is the proof generation system/backend in place:

Storage Service: A storage service will be made which stores the proofs and Maps in databases. This will also need some sort of experimentaion which db like mysql,postgresql,mongoDb and cache layer for storing maps like redis gives the best fetching and writing time.
PreProcessor: The role of the preprocessor is to take inputs from the userBalanceSheet/ the db entries and prepare inputs to the above mentioned circuit. I would like to test different low level languages(rust,golang,c) for this as to which gives the fastest result write the results to files and have them read in the circuit’s process.
Circuits: The circuits are ran in a child forked process this allows for less memory consumption as javascript’s heap fills out way too fast. I think this pardigm can help people creating proof generation backends so will definitely try to make a nice wrapper for this.

Protokit

For the protokit implementation we can store the each user’s asset commitments (which are hash(TotalEquity,TotalDebt,assetCommitment)) and store the root commitments and everything in runtimes. So something along the lines:

NOTE We do not directly store the user assets on the runtime as they are private in a cex backend and cannot be exposed to the public due to privacy concerns.

export class UserRuntime extends RuntimeModule<UserRuntimeConfig> {
    ...
    // here the key - hash(AccountId)
    // the value is hash(TotalEquity,TotalDebt,assetCommitment)
    @state public userCommitments: StateMap.from<Field,Field>(Field,Field)
    // the account tree root commitment
    @state public rootCommitment: State.from<Field>(Field)
    ...
}

The CEX Runtime can be as follows which stores the Cex Commitments. As Cex Assets have to be public to maintain transparency

export class CEXRuntime extends RuntimeModule<CEXRuntimeConfig> {
    ...
    @state public assets: StateMap.from<AssetId,CEXAssets>(AssetId,CexAssets)
    // here the key - hash(AccountId)
    // the value is hash(TotalEquity,TotalDebt,..loan variables...)
    @state public assetCommitment: StateMap.from<Field,Field>(Field,Field)
    // the account Cex Asset tree root commitment
    @state public rootCommitment: State.from<Field>(Field)
    ...
}

With above runtime and little tweaks to our approach we can have a full proof generation system in place with help of protokit.

NOTE There can be performance issues with this as in my knowledge we cannot really do batch updates on maps which would lead to multiple writes on the runtime as number of user to updates in a batch can be in thousands. I don’t know how efficient this is. So I will include a performace benchmark on both approaches

UI Dashboard

A UI dashboard is made for users to see the cexes and verify the accounts. On devnet a dummy CEX is created. In Which user can edit their token balances and collateral to play around with this stuff. User can login via credentials provided to them by the cex. I will create a mock set of credentials for people to tryout!. Here is the figma link and below are the images

Vision, Existing work

Vision:
- The long term goal is to make scalable and fast proof of solvencies.
Existing Work :
- There are many implmentaions for proof of solvency the one of the first one was Summa by pse and another is by binance in gnark

Budget & milestones

Deliverables:
- Fully working proof of solvencies generation system in place
- Various performance benchmarks including but not limited to:
  - A benchmark on proving times with different sized IndexedMerkleMaps input to the circuit.
  - Best db/cache to store indexed merkle maps
- I think the way to evalute circuits in child process for js backends can be made into a template which would help people making proof generation backends
- Implementaion of protokit approach + performance benchmarks on this.
- The dashboard UI and verification of the proofs on devnet.
Mid-Point milestones:
- I would like to have the full circuit implmentations + benchmarks on different sized IndexedMerkleMaps.
Project Timeline : 1.5-2.5M
Budget Requested : 13000 MINA
Budget Breakdown:
- Cloud server: 2,000 MINA (This is to benchmark angaist existing implementaions like binance implmentaion they did this on an m5.8xlarge AWS Server )
- Developement cost: 11,000 MINA
Wallet Address: B62qr9SfvvhE7GWJTJC77UutJRoydxLxaLxcJbk77oKeEdjC1L7kX7T

Team Info

Proposer Github:
- utkarshdagoat (Utkarsh Sharma) · GitHub
Proposer Experience:
- I have build on Mina before here are the projects:
  - AuraFl: This was build during EthOnline. It was federated learning framework that uses Zero-Knowledge Proofs (ZKPs) to ensure the integrity of distributed model training and inference. Unforunately this did not win :(. Here is the github.
  - StealthTradeDao: Allows user to trade futures in perpetual marketplace on Mina privately and sercured by the proof of solvency . Goverened by a chain abstracted Dao with help of Near. This was made at EthSingapore and was the winner for Mina and Near Track! Here is the showcase.
Achievements:
- I generally make cool stuff for hackathons and win majority of them just to list a few
  - VeilNet It was federated learning platform built on top of the NEAR protocol using fully homomorphic encryption maintaing privacy between clients and worker nodes. Using krum functions , onchain governance for fault tolerance. This won the NEAR Track in funding the commons hackathon
  - KeyShard was a dkg(FROST) protocol done on fluence and I won the fluence compute track
  - Hermit is a a Secure MutltiParty Computation Collaboration Platform build on top of Filecoin to enhance AI privacy. This was the runner up for filecoin data economy hackathon
  - MOVEx was a dynamically collateralized stablecoin protocol on movement and this won in the defi track in movementlabs hackathon
    and many more!

Risks & Mitigations

Risk

A lot of my work depends around IndexedMerkleMaps which is an experimental feature in o1js.

Mitiagtions

If they remove the feature I would have to take a different design approach similar to approach 2 for building the user map and cex asset map.

Topic		Replies	Views
Provable verification of JWT in o1js Mina Navigator Proposals	9	596	August 12, 2024
zkProver Engine Mina Navigator Proposals	7	331	December 3, 2024
Mina Wallet via Google OAuth - Lit Protocol Integration Mina Navigator Proposals	1	107	November 25, 2024
zkUSD - Algo stablecoin Mina Navigator Proposals	7	292	December 13, 2024
Interactive ZK Proofs and Proof Recursion Research Mina Navigator Proposals	6	299	December 1, 2024