Merge pull request #12 from thogiti/main

Added methodology section to version A and B
electisec · Jun 20, 2024 · 0e055a9 · 0e055a9
2 parents 622f35d + 62e0465
commit 0e055a9
Show file tree

Hide file tree

Showing 2 changed files with 136 additions and 54 deletions.
diff --git a/versionA.md b/versionA.md
@@ -25,32 +25,58 @@ Auditors:
 
 ## Table of Contents
 
-- [Protocol Summary](#protocol-summary)
-- [Scope](#scope)
-- [Automated Testing](#automated-testing)
-- [Findings](#findings)
-  - [High](#high):
-    - [1. Missing username range check in `big_intify_username` & `big_uint_to_fp`](#1-high-missing-username-range-check-in-big_intify_username--big_uint_to_fp)
-    - [2. Sum balance overflow](#2-high-sum-balance-overflow)
-    - [3. Inconsistency in range checks](#3-high-inconsistency-in-range-checks)
-  - [Low](#low)
-    - [1. Mixed endian usage in code](#1-low-mixed-endian-usage-in-code)
-  - [Informational](#informational)
-    - [1. Range check uses lookup_any instead of lookup](#1-informational-range-check-uses-lookup_any-instead-of-lookup)
-    - [2. `InclusionVerifier.yul`not generated](#2-informational-inclusionverifieryulnot-generated)
-    - [3. Improvement to public inputs in contract](#3-informational-improvement-to-public-inputs-in-contract)
-    - [4. Use only mapping for `addressOwnershipProofs`](#4-informational-use-only-mapping-for-addressownershipproofs)
-    - [5. `Summa.sol` : Issue with `submitProofOfAddressOwnership()`](#5-informational-summasol--issue-with-submitproofofaddressownership)
-    - [6. `Summa.sol` : Ownable: Does not implement 2-Step-Process for transferring ownership](#6-informational-summasol--ownable-does-not-implement-2-step-process-for-transferring-ownership)
-    - [7. Potential `Summa::submitCommitment()` Gas limits](#7-informational-potential-summasubmitcommitment-gas-limits)
-    - [8. Magic numbers used in code of MST Circuit to create PoseidonChip](#8-informational-magic-numbers-used-in-code-of-mst-circuit-to-create-poseidonchip)
-    - [9. Review of the `Summa.sol` smart contract](#9-informational-review-of-the-summasol-smart-contract)
-- [Final remarks](#final-remarks)
-- [Appendix](#appendix)
-  - [Automated Analysis](#a---automated-analysis)
-  - [Fuzz Testing](#b---fuzz-testing)
-  - [Code Coverage](#c---code-coverage)
-  - [Methodology]()
+- [yAcademy Summa Version A Review](#yacademy-summa-version-a-review)
+  - [Table of Contents](#table-of-contents)
+  - [Protocol Summary](#protocol-summary)
+    - [Overview of the MST-based Summa Version A (this report)](#overview-of-the-mst-based-summa-version-a-this-report)
+  - [Automated Testing](#automated-testing)
+    - [Automated Analysis](#automated-analysis)
+    - [Fuzz Testing](#fuzz-testing)
+    - [Code Coverage](#code-coverage)
+  - [Scope](#scope)
+  - [Findings Explanation](#findings-explanation)
+  - [Findings](#findings)
+    - [High](#high)
+    - [1. High: Missing username range check in `big_intify_username` \& `big_uint_to_fp`](#1-high-missing-username-range-check-in-big_intify_username--big_uint_to_fp)
+      - [Recommendation](#recommendation)
+      - [Refer](#refer)
+    - [2. High: Sum balance overflow](#2-high-sum-balance-overflow)
+      - [Refer](#refer-1)
+    - [3. High: Inconsistency in range checks](#3-high-inconsistency-in-range-checks)
+      - [Refer](#refer-2)
+    - [Low](#low)
+    - [1. Low: Mixed endian usage in code](#1-low-mixed-endian-usage-in-code)
+      - [Refer](#refer-3)
+    - [Informational](#informational)
+    - [1. Informational: Range check uses lookup\_any instead of lookup](#1-informational-range-check-uses-lookup_any-instead-of-lookup)
+      - [Refer](#refer-4)
+    - [2. Informational: `InclusionVerifier.yul`not generated](#2-informational-inclusionverifieryulnot-generated)
+      - [Refer](#refer-5)
+    - [3. Informational: Improvement to public inputs in contract](#3-informational-improvement-to-public-inputs-in-contract)
+    - [Refer](#refer-6)
+    - [4. Informational: Use only mapping for `addressOwnershipProofs`](#4-informational-use-only-mapping-for-addressownershipproofs)
+      - [Refer](#refer-7)
+    - [5. Informational: `Summa.sol` : Issue with `submitProofOfAddressOwnership()`](#5-informational-summasol--issue-with-submitproofofaddressownership)
+      - [Refer](#refer-8)
+    - [6. Informational: `Summa.sol` : Ownable: Does not implement 2-Step-Process for transferring ownership](#6-informational-summasol--ownable-does-not-implement-2-step-process-for-transferring-ownership)
+      - [Refer](#refer-9)
+    - [7. Informational: Potential `Summa::submitCommitment()` Gas limits](#7-informational-potential-summasubmitcommitment-gas-limits)
+      - [Refer](#refer-10)
+    - [8. Informational: Magic numbers used in code of MST Circuit to create PoseidonChip](#8-informational-magic-numbers-used-in-code-of-mst-circuit-to-create-poseidonchip)
+      - [Refer](#refer-11)
+    - [9. Informational: Review of the `Summa.sol` smart contract](#9-informational-review-of-the-summasol-smart-contract)
+      - [Refer](#refer-12)
+  - [Final remarks](#final-remarks)
+  - [Appendix](#appendix)
+    - [A - Automated Analysis](#a---automated-analysis)
+      - [1. Halo2-analyzer](#1-halo2-analyzer)
+      - [2. Polyexen-demo](#2-polyexen-demo)
+      - [3. NPM Audit](#3-npm-audit)
+      - [4. Cargo Audit](#4-cargo-audit)
+      - [5. Clippy](#5-clippy)
+    - [B - Fuzz Testing](#b---fuzz-testing)
+    - [C - Code Coverage](#c---code-coverage)
+    - [Methodology](#methodology)
 
 ## Protocol Summary
 
@@ -426,3 +452,25 @@ We raised the following pull requests to increase code coverage & emphasize on t
 - [PR#17](https://github.com/zBlock-2/summa-solvency-schneier/pull/17) to add end-to-end testing with full prover and verifier (instead of mock prover).
 - [PR#8](https://github.com/zBlock-2/summa-solvency-schneier/pull/8/files) to include cost estimation for circuits using `CircuitCost`
 - [PR#5](https://github.com/zBlock-2/summa-solvency-schneier/pull/5) is a stress test to determine the potential gas limits of `Summa::submitCommitment()`
+
+### [Methodology](#methodology)
+
+The audit employed a blend of automated tools and manual examination conducted by the fellows and residents. Techniques included detailed code reviews, static and dynamic analysis, fuzzing, and penetration testing to ensure a thorough validation of the protocol’s security measures.
+
+- **Tool Integration:**
+The audit utilized several specialized tools, each tailored to assess different aspects of the protocol:
+    - **Halo2-analyzer**: Verified all circuit constraints.
+    - **Polyexen-demo**: Standardized circuit formats for clarity and reusability.
+    - **Highlighter**: Identified potential code issues needing closer examination.
+    - **NPM and Cargo Audits**: Checked dependencies for known vulnerabilities.
+    - **Clippy**: Ensured Rust code quality and best practices.
+- **Analytical Techniques:**
+The audit encompassed both static and dynamic analyses to provide a comprehensive security assessment:
+    - **Static Analysis**: Examined the source code for vulnerabilities without execution.
+    - **Dynamic Analysis**: Tested the protocol in operation to identify runtime issues.
+- **Expert Review:**
+We conducted in-depth manual reviews to evaluate complex components and integrations, providing a crucial layer of scrutiny beyond automated tools.
+- **Feedback and Improvements:**
+An iterative feedback loop with the Summa’s development team allowed for the immediate addressing and re-evaluation of any issues found, ensuring all fixes were effectively implemented.
+- **Documentation:**
+Each phase of the audit was thoroughly documented, with detailed reports on tool outputs, expert insights, and overall findings, culminating in a comprehensive final report that outlined vulnerabilities, impacts, and recommended actions.
diff --git a/versionB.md b/versionB.md
@@ -23,32 +23,45 @@ Auditors:
 
 ## Table of Contents
 
-- [Protocol Summary](#protocol-summary)
-- [Scope](#scope)
-- [Automated testing](#automated-testing)
-- [Findings](#findings)
-  - [High](#high):
-    - The inclusion proof reveals whether a user holds a specific token
-    - Wrong verifying key contract permutation length can be considered valid by `validateVKPermutationsLength`
-    - Fake user Inclusion Proof verified in contract
-    - Username overflow
-  - [Medium](#medium):
-    - The return value of `GrandSumVerifier` should be tested
-  - [Low](#low):
-    - Incorrect permutation length in `validateVKPermuationsLength`
-    - CSV parsing allows duplicate crypto tokens
-    - The return value of `GrandSumVerifier` should be tested
-    - Range check tests are unreliable regarding the number of overflows
-  - [Informational](#informational):
-    - Security concerns in `Summa.sol`
-    - Update memory locations in verifiers to save gas
-    - Dynamic Errors not handled in Box of Errors for Function Results
-    - Use of unwrap in core files and improper error handling
-    - Automated tests for dependency vulnerabilities and code quality
-- [Final remarks](#final-remarks)
-- [Appendix](#appendix)
-  - [Automated Analysis](#a---automated-analysis)
-  - [Methodology]()
+- [yAcademy Summa Version B Review](#yacademy-summa-version-b-review)
+  - [Table of Contents](#table-of-contents)
+  - [Protocol Summary](#protocol-summary)
+    - [Overview of the KZG-based Implementation of the Summa Proof of Solvency Protocol](#overview-of-the-kzg-based-implementation-of-the-summa-proof-of-solvency-protocol)
+  - [Scope](#scope)
+  - [Automated testing](#automated-testing)
+    - [Automated Analysis](#automated-analysis)
+  - [Findings Explanation](#findings-explanation)
+  - [Findings](#findings)
+    - [High](#high)
+    - [1. High: The inclusion proof reveals whether a user holds a specific token](#1-high-the-inclusion-proof-reveals-whether-a-user-holds-a-specific-token)
+    - [2. High: Wrong verifying key contract permutation length can be considered valid by `validateVKPermutationsLength`](#2-high-wrong-verifying-key-contract-permutation-length-can-be-considered-valid-by-validatevkpermutationslength)
+    - [3. High: Fake user Inclusion Proof verified in contract](#3-high-fake-user-inclusion-proof-verified-in-contract)
+    - [4. High: Username overflow](#4-high-username-overflow)
+    - [Medium](#medium)
+    - [1. Medium: The return value of `GrandSumVerifier` should be tested](#1-medium-the-return-value-of-grandsumverifier-should-be-tested)
+    - [Low](#low)
+    - [1. Low: Incorrect permutation length in `validateVKPermuationsLength`](#1-low-incorrect-permutation-length-in-validatevkpermuationslength)
+    - [2. Low: CSV parsing allows duplicate crypto tokens](#2-low-csv-parsing-allows-duplicate-crypto-tokens)
+    - [3. Low: The return value of `GrandSumVerifier` should be tested](#3-low-the-return-value-of-grandsumverifier-should-be-tested)
+    - [4. Low: Range check tests are unreliable regarding the number of overflows](#4-low-range-check-tests-are-unreliable-regarding-the-number-of-overflows)
+    - [Informational](#informational)
+    - [1. Informational: Security concerns in `Summa.sol`](#1-informational-security-concerns-in-summasol)
+    - [2. Informational: Update memory locations in verifiers to save gas](#2-informational-update-memory-locations-in-verifiers-to-save-gas)
+    - [3. Informational: Dynamic Errors not handled in Box of Errors for Function Results](#3-informational-dynamic-errors-not-handled-in-box-of-errors-for-function-results)
+    - [4. Informational: Use of unwrap in core files and improper error handling](#4-informational-use-of-unwrap-in-core-files-and-improper-error-handling)
+  - [Final remarks](#final-remarks)
+  - [Appendix](#appendix)
+    - [A - Automated Analysis](#a---automated-analysis)
+      - [1. Halo2-analyzer](#1-halo2-analyzer)
+    - [1. Unused Gate](#1-unused-gate)
+    - [2. Unused columns](#2-unused-columns)
+    - [3. Underconstrained Cells](#3-underconstrained-cells)
+      - [2. Polyexen-demo](#2-polyexen-demo)
+      - [3. Highlighter](#3-highlighter)
+      - [4. NPM Audit](#4-npm-audit)
+      - [5. Cargo Audit](#5-cargo-audit)
+      - [6. Clippy](#6-clippy)
+    - [Methodology](#methodology)
 
 ## Protocol Summary
 
@@ -65,8 +78,6 @@ The prover produces a commitment `C` to the polynomial and:
 - An opening [proof](https://github.com/summa-dev/summa-solvency/blob/bd3a3d4d8fda6661e4eede00cf6176d66cb00858/prover/src/circuits/tests.rs#L167) at `x=0` to [the public](https://github.com/summa-dev/summa-solvency/blob/fec83a747ead213261aecfaf4a01b43fff9731ee/contracts/src/Summa.sol#L230)
 - An opening proof at `(w_j)^i` for the `i-th` user, who can can verify inclusion not only that the evaluation is correct but also that the commitment `C` they evaluated against is the same as the public commitment.
 
-## Methodology
-
 ## Scope
 
 The security review was limited to commit [fec83a747](https://github.com/summa-dev/summa-solvency/tree/95d63fe1a55935542810138aa5d8de7f50f4e94b). The scope of the review consisted of the following files and folders at the specific commit:
@@ -365,3 +376,26 @@ Highlighter works on a set of rules to look for error prone areas such as incorr
 #### 6. Clippy
 
 `clippy` is a linter for Rust that checks your code for common mistakes and style issues. It provides helpful suggestions to improve your code quality and maintainability. Using `clippy` helps ensure your Rust code is clean, efficient, and follows best practices. Here's the [report](https://github.com/zBlock-2/audit-report/blob/main/appendix/V2/clippy/output.md).
+
+
+### [Methodology](#methodology)
+
+The audit employed a blend of automated tools and manual examination conducted by the fellows and residents. Techniques included detailed code reviews, static and dynamic analysis, fuzzing, and penetration testing to ensure a thorough validation of the protocol’s security measures.
+
+- **Tool Integration:**
+The audit utilized several specialized tools, each tailored to assess different aspects of the protocol:
+    - **Halo2-analyzer**: Verified all circuit constraints.
+    - **Polyexen-demo**: Standardized circuit formats for clarity and reusability.
+    - **Highlighter**: Identified potential code issues needing closer examination.
+    - **NPM and Cargo Audits**: Checked dependencies for known vulnerabilities.
+    - **Clippy**: Ensured Rust code quality and best practices.
+- **Analytical Techniques:**
+The audit encompassed both static and dynamic analyses to provide a comprehensive security assessment:
+    - **Static Analysis**: Examined the source code for vulnerabilities without execution.
+    - **Dynamic Analysis**: Tested the protocol in operation to identify runtime issues.
+- **Expert Review:**
+We conducted in-depth manual reviews to evaluate complex components and integrations, providing a crucial layer of scrutiny beyond automated tools.
+- **Feedback and Improvements:**
+An iterative feedback loop with the Summa’s development team allowed for the immediate addressing and re-evaluation of any issues found, ensuring all fixes were effectively implemented.
+- **Documentation:**
+Each phase of the audit was thoroughly documented, with detailed reports on tool outputs, expert insights, and overall findings, culminating in a comprehensive final report that outlined vulnerabilities, impacts, and recommended actions.