🗒️

Internal Protocol audit for Snap deals

Intro

We are starting this document as a part of our audit process for Snap deals implementation.

Snapdeals team believes that this is a mandatory step for us to take since we want to make sure that all the changes we made on Lotus, Actors, and Proofs sides are aligned and created the way we originally imagined them in the FIP and other specification docs

Important dates:

  • We plan to start the audit events train on - @November 19, 2021
  • We will continue reviewing the codebase/implementation paths during the entire week between - @November 22, 2021 and @November 26, 2021

Resources that can be valuable:

SnapDeals main doc

SnapDeals Security Analysis expanded doc

Circuit Design doc

Apex Cut doc

Jake's circuit description

Team:

As a part of this effort, we formed a working group

  • @Friedel Ziegelmayer from the proofs side
  • @Kubuxu - ffi, lotus and actors
  • @Nicola - General review for the entire flow
  • @Luca - General review for the entire flow

Audit items relevant for our review

Item under reviewReview statusMain findings from the review processRelated to:
Circuits and verification algorithm of proofs
Done
main items are listed below, but also linked here
Circuits (Proofs)
Smart contracts (actors code)
Done
Actors
Pathways from actors to FFI for the verification storage subsystem
Done
ActorsFFI
Storage subsystem capability of updating deals/test suite testing deal updates
Done

Checkboxes

Action items/issues found from the circuit review we did on 2021-11-22:

@Kubuxu @Friedel Ziegelmayer -We need to finish the circuit spec for Snapdeals - V2 - we are missing the end
hSelect and k packing is not in the spec
descriptions of public inputs to what they represent outside
k \in [0, P)
We are fine with using one DST tag for different inputs: (CommR, CommD), (\phi, counter), (CommD, counter)
@jake , @Kubuxu - Update items in the spec, including adding items from the notion doc doc: https://www.notion.so/protocollabs/Circuit-Design-SnapDeals-Lightweight-CC-Sector-Updates-3923fe75202d4740bbdb011067838cb3
check apex_leaf_count
Update the comment on fn hs , it isn't about challenges but about encoding randomness
Check that parition_path is verified
k_bits to k conversion circuit.rs#L379 could be simpler for clarity
verify that bit_len is correct in gadgets.rs#L173
gadget.rs#L232 comment is misleading
gadget.rs#103 change from floats to ints for ceil of digests_per_parititon
From the internal audit, change H to 1024
@Friedel Ziegelmayer, @Kubuxu - this is where we left it off on @November 22, 2021 - https://github.com/filecoin-project/rust-fil-proofs/blob/empty-sector-update/storage-proofs-update/src/circuit.rs#L656
gadget review
apex_por gadget review
por gadget review
select
L40 and L43 uses bintree should be octtree
change the order CommD PoR in the code is after CommR
ApexTree gadget: values is not defined
align spec and circuit itself

Meeting on 2021- 11-23 - Lotus and Actors audit

Checklist:

Actors code - we will check for these items of the implementation:

We will check for:

Sector is CC
Deals are valid
CommD corresponds to Comm(CommP...), or better there is no parameter for it
SectorKey CommR comes from the state, or there is no parameter for it
const ProveReplicaUpdatesMaxSize = PreCommitSectorBatchMaxSize = 256 how can we confirm this is a good number, and gas usage analysis yet, i.e.: smaller than block limit?

Action items/issues found:

@Aayush Rajasekaran @Wyatt Daviau We will correct this one - https://github.com/filecoin-project/specs-actors/pull/1529/files#r755402700

Future improvements:
We should review solutions if SP wants to reuse the proofs? We should probably add some ID that will help us track this and not allow proofs to be reused. @Kubuxu @Nicola
We would need to add SnarkPack to the SnapDeals implementation, at some point - @Nicola