وقتی حریم خصوصی به اثبات نیاز دارد: حرکت STRK20 استارکنت بهسوی راستیآزمایی صوری
استارکور رسماً مدل Lean 4 مربوط به استخر حریم خصوصی STRK20 را متنباز کرده است؛ اقدامی که بحث حریم خصوصی ZK را از پنهانکردن موجودیها به اثبات درستی گذارهای حالت، حسابداری، مالکیت، بازیابی و انطباق منتقل میکند.
سامانههای حریم خصوصی یک مسئله دشوار برای راستیآزمایی ایجاد میکنند: دفترکل دقیقاً در جایی جزئیات تراکنش را پنهان میکند که توسعهدهندگان به اطمینان از درستی قواعد نیاز دارند. آخرین انتشار STRK20 از سوی استارکور، منتشرشده در ۲۳ ژوئیه ۲۰۲۶، با یک مدل بررسیشده توسط ماشین برای استخر حریم خصوصی به این مسئله پاسخ میدهد.
ایده اصلی این است که استخر بهعنوان یک ماشین حالت مدل شود. در STRK20، موجودیهای رمزگذاریشده در قالب note نمایش داده میشوند و nullifierها مانع خرجکردن دوباره یک note میشوند. توسعه Lean 4 اقداماتی مانند ثبتنام، ایجاد کانال، ایجاد زیرکانال و ایجاد note را مدل میکند و سپس ویژگیهای سامانه را برای هر حالتی که از دنبالهای معتبر از اقدامات قابل دستیابی است، اثبات میکند.
استارکور میگوید این پروژه بیش از ۲۳۰ قضیه دارد و هیچ گام اثباتنشدهای در آن باقی نمانده است. همچنین، ابزارها و کتابخانههای نسخهبندیشده امکان بازسازی و بررسی مستقل اثباتها را فراهم میکنند. تضمینهای ادعاشده کاربردیاند: noteها قابل جعل نیستند، nullifierها از دوبارهخرجکردن جلوگیری میکنند، ارزش نمیتواند بدون پشتوانه ایجاد یا افزایش یابد، مالکان میتوانند noteهای خود را پیدا کنند و noteهای خرجنشده همچنان قابل خرجکردن باقی میمانند. مدل همچنین مسیر انطباقی را پوشش میدهد که در آن یک کلید انطباق میتواند noteها را بازیابی و مسیر حرکت آنها را دنبال کند.
این موضوع از آن جهت اهمیت دارد که STRK20 بهعنوان زیرساخت داراییهای خصوصی طراحی شده، نه یک mixer منزوی. اطلاعیه توسعهدهندگان استارکنت از Privacy SDK و Wallet API متنباز خبر میدهد. SDK کنترل سطح پایین کلیدهای مشاهده، noteها، اثباتسازی و ارسال روی زنجیره را در اختیار توسعهدهندگان میگذارد؛ Wallet API نیز به برنامههای عادی اجازه میدهد عملیات shield، transfer، unshield یا swap را از طریق یک کیف پول دارای قابلیت حریم خصوصی درخواست کنند. هر تراکنش خصوصی یک اثبات ZK-STARK حمل میکند که معتبر و خرجنشدهبودن noteها و حفظ ارزش را تأیید میکند، درحالیکه فرستنده، گیرنده و مبلغ درون استخر پنهان میمانند.
این لایه جدید راستیآزمایی، فهرست بررسی توسعهدهندگان را تغییر میدهد. تیمی که کیف پول خصوصی یا جریان DeFi را یکپارچه میکند، نباید فقط بررسی کند که آیا اثبات پذیرفته میشود یا نه. باید بپرسد سیستم اثبات دقیقاً چه چیزی را درباره ماشین حالت ثابت میکند، آیا کشف note پس از هر گذار کامل باقی میماند، دامنه nullifierها چگونه تعریف شده و کلید مشاهده یا کلید انطباق چه اطلاعاتی را میتواند آشکار کند. این پرسشها حریم خصوصی را از یک قابلیت رابط کاربری به یک مرز پروتکلی قابل ممیزی تبدیل میکنند.
یک محدودیت مهم وجود دارد. ادعاهای راستیآزمایی صوری مطرحشده در این مقاله از اطلاعیه دستاول استارکور گرفته شدهاند و پیش از آنکه نتیجه یک ممیزی مستقل تلقی شوند، باید بهطور مستقل بازسازی شوند. اثباتهای منتشرشده مدل پروتکل و برخی اجزای زیربنایی را پوشش میدهند؛ استارکور میگوید قرارداد Cairo مستقر بهصورت جداگانه توسط OpenZeppelin ممیزی شده است. بنابراین راستیآزمایی صوری اعتماد به ویژگیهای مشخصشده را افزایش میدهد، اما بهطور خودکار همه پیادهسازیها، یکپارچهسازیها، فرایندهای مدیریت کلید یا فرضهای عملیاتی را تأیید نمیکند.
درس بزرگتر برای توسعهدهندگان ZK این است که حریم خصوصی به دو اثبات نیاز دارد: یک اثبات رمزنگاری که نشان دهد تراکنش بدون افشای داده خصوصی از قواعد پیروی میکند، و یک اثبات صوری که نشان دهد خود قواعد، داراییها و تضمینهایی را که برنامه وعده میدهد حفظ میکنند. توسعه Lean متنباز STRK20 گامی مشخص برای قابلبررسیکردن هر دو لایه است.
خبرخوان را در ایمیل بگیرید
هر سیگنال تازه، مستقیم از خط تولید. بدون مزاحمت، لغو عضویت در هر زمان.