# Vulneralbility in ZKP

## Soundness : Invalid proof should be rejected
### Forging, altering and replaying proofs

* #### No Nullifier（prevent proof replay) uniqueness check
#### Example 1: Missing nullifier uniqueness check
Semaphore
Nullifier hash wrapping around over scalar field fits into uint 256, causing double spend

https://github.com/semaphore-protocol/semaphore/issues/16

#### Example 2 Non-deterministic nullifier
Aztec 2.0
Missing bit length check on the index (i.e. position) of a note in the Aztec 2.0 tree was used in the computation of the note nullifier, resulting in attacker could double spend of the same note with different nullifier
https://github.com/0xPARC/zk-bug-tracker#5-aztec-20-missing-bit-length-check--nondeterministic-nullifier

#### Example 2: Trivial nullifier uniqueness check (nullifiers = 0)
Polygon nightfall (ZK transaction on Optmistic Rollup)

    function ChallengeNullifier(
        Structures.Transaction memory tx1,
        uint256 nullifierIndex1,
        Structures.Transaction memory tx2,
        uint256 nullifierIndex2
    ) public pure {
        require(
            tx1.nullifiers[nullifierIndex1] == tx2.nullifiers[nullifierIndex2],
            'Not matching nullifiers'
        );
        require(
            Utils.hashTransaction(tx1) != Utils.hashTransaction(tx2),
            'Transactions need to be different'
        );
    }



* ### Fake proof as the result of centralized ownership of verifier contract

  ####  Example 1
  `Key_Registry` has a single owner/operator, if they are compromised or malicious, attacker can replace the circuit with a malicious one and register the associated verfication key which can verify a fake proof of a malicious transaction causing damage to the user   
  
  

contract Key_Registry is Ownable, Structures {

//event VkChanged(TransactionTypes txType);

mapping(TransactionTypes => uint256[]) public vks;

function initialize() override virtual public initializer {
Ownable.initialize();
}
/**
Stores verification keys (for the 'deposit', 'transfer' and 'withdraw' computations).
*/
function registerVerificationKey(
uint256[] calldata _vk,
TransactionTypes _txType)
external onlyOwner {
// CAUTION: we do not prevent overwrites of vk's. Users must listen for the emitted event to detect updates to a vk.
vks[_txType] = _vk;

}

function getVerificationKey(TransactionTypes txType) public view returns(uint[] memory) {
return vks[txType];
}
}

  Instead the contract should be owned by a multi-sig account, key updating should be approved by DAO. As a mitigation, the contract owner should  renounce ownership by renounceOwnership after the contract deployment and setup is completed, making updating the veification key impossible.

function completeSetup() public override onlyOwner {
renounceOwnership();
}

* ### Forge proof as a result of insecure/centralized trusted setup(proof and verification key generation)
  1. Prover is the single party in the trusted setup,  they can forge proof without detected by any other party 
  
  2. CRS(Common reference string, aka. "toxic waste" some trapdoor parameter for proving and verifying) is not destroyed properly after trusted setup 
 **Example: ZCash trusted setup flaw** https://electriccoin.co/blog/zcash-counterfeiting-vulnerability-successfully-remediated/#counterfeiting-vulnerability-details
  

* ### Public input overflow for verifier curves scalar field modulus 



  ####  Example 1 Missing public input scalar field overflow check
  Polygon nightfall (**found during writing this doc**, [fixed](https://github.com/EYBlockchain/nightfall_3/blob/master/nightfall-deployer/contracts/Verifier.sol#L105) in the latest version :()) 

function verifiyProof(uint256[] memory _proof, uint256[] memory _publicInputs, uint256[] memory _vk) public returns (uint) {`

Pairing.G1Point memory sm_qpih;
// The following success variables replace require statements with corresponding functions called. Removing require statements to ensure a wrong proof verification challenge's require statement correctly works
uint256 snark_scalar_field = 21888242871839275222246405745257275088548364400416034343698204186575808495617
bool success_sm_qpih;
bool success_vkdi_sm_qpih;
for (uint i = 0; i < _publicInputs.length; i++) {
//Missing public input scalar field overflow check
// require( _proofInputs[i] < snark_scalar_field );
(sm_qpih, success_sm_qpih) = Pairing.scalar_mul(vk.gamma_abc[i+1], _publicInputs[i]);
(vk_dot_inputs, success_vkdi_sm_qpih) = Pairing.addition(
vk_dot_inputs,
sm_qpih
);
if (!success_sm_qpih || !success_vkdi_sm_qpih) {
return 2;
}
}

**Note** _proof field overflow will be checked in precompile contracts  for ecliptic curve computation(addition,multiply,pairing) according to [EIP-196 ](https://github.com/ethereum/EIPs/blob/master/EIPS/eip-196.md)



 #### Example 2 Truncating public input to fit in the scalar field modulus
  The BN128 curve has a prime order scalar field of modulus
r = 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001, which is a 254-bit number. To prevent any 256-bit input hash H, if interpreted as an integer, from exceeding the modulus r, it is sufficient to delete the first 3 bits of H to get a new digest H’, guaranteeing that the new digest H’ is smaller than r.  
  

function verifyProof(
uint256[] calldata proof,
bytes8 calldata publicInput1,
bytes8 calldata publicInput2,
bytes8 calldata publicInput3,
uint256[] memory verifyingKey
) internal {
// calculate publicInputHash
bytes32 publicInputHash = sha256(abi.encodePacked(publicInput1,publicInput2,publicInput2,publicInput3);
// verify proof with gm17 verifier
// concat hash by selecting the 1st 253 of 256 bits
require(Verifier.verify(proof, uint256(publicInputHash & 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff), verifyingKey), 'This proof and/or inputs appears to be invalid');
}

* Group member check (e.g. input point is on curve, non-zero group member ) 

* ###  Under-constraint circuit (missing constraint in the circuit) 
  ####   Example 1 Missing ERC20 check in the SNARK circuits
  
  The circuit only checks the sum of ERC-20 tokens for the token addresses included in the input notes, but not for the output notes, which could enable a malicious actor to drain funds by adding random output notes
  
  ![](https://i.imgur.com/WF8IO5u.png)

  
  
  https://github.com/zkopru-network/zkopru/issues/165
  
 * ###  Lacking formal statement for proving  
 A formal statement is a formal specification of the statement (what is to be proved). 
>  Lacking a proper statement enable a malicious prover to find valid proofs for unintended system behavior. Since zero-knowledge is involved, those proofs, that are valid but malicious, would be potentially very difficult to detect. 
> Additionally, when lacking a statement, there is no foundation to compare the implementation against. It is insufficient to have the statement implicit in the code, as this would force a circular approach for reviewers, consisting of comparing the code against a statement that is implicit in the code.     
>        -- ZKOpru audit by Least Authority


Statement example https://github.com/zkopru-network/protocol-specification/blob/main/SPEC.md

**Example** see [above](https://hackmd.io/JhriohGxQ1uZV4XthEVx3w#Example-1-Missing-ERC20-check-in-the-SNARK-circuits ) 

* ### Incomplete Fiat-Shamir transformation(Frozen Heart attack)
 Non-interactive challenge 
 Hash all public inputs into challenge 
 Trail of bits explanation
 https://blog.trailofbits.com/2022/04/15/the-frozen-heart-vulnerability-in-bulletproofs/
 
* ###  Predicatable random challenge in Plonk verification
  Failed static calls due to not enough gas if not checked may make challenge gamma, beta, alpha, zeta (values are derived from the prover’s transcript by hashing defined parameters and are supposed to be unpredictable by either the prover or the verifier) predictable. 
 https://consensys.io/diligence/audits/private/re9fdlhtjn7jfr/#gas-greifing-and-missing-return-status-check-for-staticcalls-may-lead-to-unexpected-outcomes
 
* ###  Missing paring result check in Plonk verifier
  Incorrect proof element could pass the paring check 

https://consensys.io/diligence/audits/private/re9fdlhtjn7jfr/#missing-verifying-paring-check-result

* ### Missing proof length check in Plonk verifier 
 Attacker may do some trick to forge a public input as the proof element 
   
 https://consensys.io/diligence/audits/private/re9fdlhtjn7jfr/#missing-length-check-for-proof


  
 ##  Completeness: Valid proofs should always be accepted
  
 Very few in the wild as developers tends to focus on it  
* #### DoS attack on prover 
  Malicious input to exhaust prover's resources or crashing the prover 

*   #### All programs/circuit should be corretly processed
     ####    Example 1 Merkel tree append error (ZKopru)
     Not directly related to ZKP it's an bug in withdraw Merkel tree appends  
     ![](https://i.imgur.com/kYL1zJB.png)

     https://github.com/zkopru-network/resources/blob/main/audits/v2/AUDIT-REPORT.md#major
## Livenss
* ####  Sequencer liveness and centralization risk (ZKRollup) 
  Single sequencer can go down or censor a prover, proof cannot be submitted, thus freezing state update onchain(funds are frozen)
  
## Zero knowledgeness
* Proofs leaks no secret information(Secrete input)
* Private data treated as pubic input 

### Layers in the ZKP system that could go wrong   
![](https://i.imgur.com/iuJbvW5.png)

## Security Tooling  
#### Formal Verification: Good for math heavy stuff

* [Medjai](https://github.com/Veridise/Medjai) by [Veridise](https://veridise.com): A Symbolic Execution (formal verification) tool for Cairo, found one overflow bug in MakerDAO. Based on Rosette. https://www.youtube.com/watch?v=w7UAcsptyeo&t=31919s
![](https://i.imgur.com/EvfIn6g.jpg)


#### Static analysis: Good for under-constraint circuit bugs 
* [ECNE](https://0xparc.org/blog/ecne): Automated Verification of ZK Circuit, good for finding uniqueness/under-constraint bugs in circuit to QAP/R1CS conversion  
* [Picus](https://github.com/Veridise/Picus) by Veridise: A static analysis tool for ZKP circuits implemented in Circom (or anything that compiles to R1CS). Under-constraint circuit can be expressed as SMT query. ECNE + SMT solver interacts in a loop.

 
![](https://i.imgur.com/FFjTXoJ.jpg)



#### Fuzzing 
Veridise fuzzing: Fuzzing transactions and transaction execution traces for zkEVM circuit 

####  Interactive Theorem Prover
Prove the equavalence between the specification and circuit 
Specification and circuit are translated to the language [Coda](https://github.com/Veridise/Coda)     



## Resources and reference 
* https://www.zkdocs.com/docs/zkdocs/ from ToB, limited in crytographic vulneralbility stuff, not much about zkSNARK
* Zk bug tracker: A community-maintained collection of bugs, vulnerabilities, and exploits in apps using ZK crypto https://github.com/0xPARC/zk-bug-tracker



* Coda by Veridise: Interactive Theorem prover 
* ZKOpru [first audit ](https://github.com/zkopru-network/resources/blob/main/audits/v1/Least%20Authority%20-%20Ethereum%20Foundation%20Zkopru%20zk-SNARK%20Circuits%20%2B%20Smart%20Contracts%20-%20Final%20Audit%20Report.pdf) by Least Authority
* ZKOpru [second audit](https://github.com/zkopru-network/resources/blob/main/audits/v2/AUDIT-REPORT.md) by Igor Gulamov
* Polygon Nightfall https://github.com/EYBlockchain/nightfall_3/blob/master/nightfall-deployer/
* Security of ZKP projects: same but different - JP Aumasson https://www.youtube.com/watch?v=be9pbCKNB28&t=989s
* zkEVM auditors education session https://www.notion.so/zkEVM-Audit-Education-Session-11-15-11-22-86d60daceadb438f85908817f7082611
* Awesome ZK https://github.com/ventali/awesome-zk
* ZK audit report https://github.com/nullity00/zk-security-reviews