امنیت اثبات‌های ZK صاحب معیار عمومی می‌شود: better.codes پیشرفت soundness را ماشین‌پذیر می‌کند

یک چالش پژوهشی جدید از سوی Ethereum Foundation در حال تغییر روش اندازه‌گیری پیشرفت در امنیت ZK است. better.codes از پژوهشگران و عامل‌های هوش مصنوعی آن‌ها می‌خواهد کران soundnessِ ماشین‌بررسی‌شده برای koalaIRS12 را افزایش دهند؛ مسئله‌ای درباره نزدیکی Reed–Solomon که به SNARKهای هش‌محور مدرن ارتباط دارد.

این چالش در ۲۰ اوت ۲۰۲۶ توسط تیم Formal Verification بنیاد اتریوم و با همکاری Yukon و zkSecurity راه‌اندازی شد. شرکت‌کنندگان به‌جای انتشار یک ادعای غیررسمی یا تنها یک عدد بنچمارک، با گزاره قضیه، نقطه پارامتر و ابزار بررسی ازپیش‌تعیین‌شده کار می‌کنند. خروجی هر مشارکت باید دقیقاً قضیه مورد انتظار را صادر کند و سپس هسته Lean پیش از ارتقای نتیجه، اثبات را بررسی می‌کند.

این تفاوت مهم است، چون بسیاری از سیستم‌های اثبات هش‌محور به فرض‌های نظریه کد درباره آزمون نزدیکی و توافق هم‌بسته تکیه دارند. این فرض‌ها به verifier کمک می‌کنند تشخیص دهد داده به یک codeword معتبر نزدیک است یا نه. اگر مهاجم بتواند داده‌ای تولید کند که آزمون‌ها را پشت سر بگذارد اما واقعاً نامعتبر باشد، تحلیل soundness ضعیف می‌شود.

Ethereum Foundation می‌گوید سیستم‌های مستقر معمولاً هدف امنیتی ۱۲۸ بیت را دنبال می‌کنند، در حالی که برخی کران‌های زیربنایی هنوز بیشتر به‌صورت حدس ریاضی مطرح‌اند تا قضیه‌ای که با ماشین بررسی شده باشد. better.codes برای آشکار کردن همین فاصله طراحی شده است. هر بهبود پذیرفته‌شده بر اساس تعداد بیت امتیاز می‌گیرد، در یک مخزن عمومی ثبت می‌شود و با لم‌ها، روش‌های اثبات یا نتایج ناممکنی همراه است که به آن نتیجه منجر شده‌اند.

این چالش همچنین نمونه قابل‌توجهی از استفاده از هوش مصنوعی در پژوهش رمزنگاری است. شرکت‌کنندگان می‌توانند مدل‌ها و زنجیره‌ابزارهای عامل‌محور خود را روی یک مسئله رسمی مشترک به کار بگیرند، اما عامل‌ها معیار موفقیت را تعیین نمی‌کنند؛ بررسی‌کننده Lean این کار را انجام می‌دهد. این مرز مفیدی ایجاد می‌کند: هوش مصنوعی می‌تواند به دنبال tacticها، ساختارها و ایده‌های اثبات بگردد، اما یک هسته کوچک و قابل اعتماد تصمیم می‌گیرد که استدلال ارسالی از نظر نوعی معتبر است یا نه.

این formalization به ArkLib، کتابخانه متن‌باز Lean از پروژه Verified-zkEVM، متصل است. ArkLib خود را چارچوبی ماژولار برای بررسی رسمی استدلال‌های غیرتعاملی فشرده درباره دانش معرفی می‌کند. هدف‌های اعلام‌شده آن شامل مشخصات اجرایی پروتکل و اثبات‌های ماشین‌بررسی‌شده برای کامل‌بودن و knowledge-soundness اجزایی مانند sum-check، FRI و WHIR و دیگر primitives نظریه کد است.

برای سازندگان ZK، درس عملی این نیست که یک سیستم اثبات جدید آماده استفاده در تولید شده است. نکته این است که ادعاهای امنیتی به‌تدریج به artifactهای قابل ممیزی تبدیل می‌شوند. تیم پروتکل می‌تواند بپرسد کدام قضیه از سطح soundness ادعاشده پشتیبانی می‌کند، کدام فرض‌ها همچنان حدس هستند و آیا گزاره رسمی با پارامترهای پیاده‌سازی مطابقت دارد یا نه.

یک محدودیت مهم وجود دارد: عدد ۱۲۸ بیت هدف این چالش است، نه نتیجه‌ای که تاکنون گزارش شده باشد. افزایش کران رسمی برای koalaIRS12 اعتماد به یک جزء از تحلیل سیستم اثبات را بیشتر می‌کند، اما به‌تنهایی امنیت همه SNARKها، zkVMها، پیاده‌سازی مدارها، compilerها یا استقرارهایی را که از ایده‌های مشابه استفاده می‌کنند ثابت نمی‌کند. حریم خصوصی zero-knowledge نیز از soundness جداست و این بنچمارک آن را اندازه‌گیری نمی‌کند.

همین جداسازی، بخش اصلی تحول است. با ورود سیستم‌های ZK به محیط تولید، ارزشمندترین پیشرفت همیشه سریع‌تر شدن proving نیست؛ گاهی مهم‌تر، بنچمارک‌های عمومی‌ای هستند که دقیقاً نشان می‌دهند کدام بخش‌های استدلال امنیتی اثبات شده، کدام بخش‌ها فرض شده و کدام بخش‌ها هنوز نیاز به کار دارند.