عهدهای بیت‌کوین رها شده: یک مدل صوری برای قراردادهای هوشمند پیشرفته

1. مقدمه

مدل خروجی تراکنش خرج‌نشده (UTXO) بیت‌کوین، اگرچه برای انتقال همزمان ارز ظریف است، به دلیل فقدان حالت مشترک تغییرپذیر، محدودیت‌های قابل توجهی برای پیاده‌سازی قراردادهای هوشمند پیچیده و حالت‌دار ایجاد می‌کند. عهدها به عنوان یک پایه زبانی حیاتی مطرح می‌شوند که برای گسترش اسکریپت بیت‌کوین پیشنهاد شده‌اند و به یک تراکنش اجازه می‌دهند محدودیت‌هایی بر روی اسکریپت‌های تراکنش‌های بازخرید آینده اعمال کند. این مقاله شکاف موجود در مدل‌های صوری و انتزاعی برای عهدها را مورد توجه قرار می‌دهد؛ عهدها عمدتاً از منظر سطح پایین و متمرکز بر پیاده‌سازی از زمان پیدایش حدود سال ۲۰۱۳ توصیف شده‌اند. با ارائه یک بنیان صوری، این کار هدف دارد تا استدلال درباره ویژگی‌های قرارداد را ساده‌سازی کند، امکان مشخص‌سازی موارد استفاده پیشرفته فراتر از قابلیت‌های فعلی بیت‌کوین را فراهم آورد و طراحی انتزاعات برنامه‌نویسی سطح بالاتر را تسهیل نماید.

2. مدل بیت‌کوین خالص

این مقاله از یک صوری‌سازی از مدل تراکنش هسته‌ای بیت‌کوین اقتباس می‌کند. در مدل UTXO، حالت بلاک‌چین توسط مجموعه‌ای از خروجی‌های تراکنش خرج‌نشده تعریف می‌شود. هر خروجی حاوی یک مقدار (مقدار بیت‌کوین) و یک scriptPubKey (اسکریپت قفل‌کننده) است که شرایط لازم برای خرج کردن آن را مشخص می‌کند. یک تراکنش خرج‌کننده یک scriptSig (اسکریپت بازکننده) ارائه می‌دهد و به UTXOای که مایل به مصرف آن است ارجاع می‌دهد. اعتبارسنجی شامل اجرای اسکریپت‌های الحاق‌شده است. نکته کلیدی این است که اسکریپت استاندارد بیت‌کوین محدود است: نمی‌تواند ساختار تراکنش خرج‌کننده را فراتر از تأیید امضا و حساب‌گری/منطق پایه، درون‌کاوی یا محدود کند و این امر از ایجاد قراردادهایی که پروتکل‌های چندمرحله‌ای را اعمال می‌کنند جلوگیری می‌نماید.

3. مدل صوری عهدها

مشارکت اصلی، یک مدل صوری است که اپ‌کدهای عهد پیشنهادی (مانند OP_CHECKTEMPLATEVERIFY) را انتزاع می‌کند.

4. مشخص‌سازی قراردادهای پیچیده بیت‌کوین

مدل صوری برای مشخص‌سازی قراردادهایی که در بیت‌کوین خالص غیرقابل بیان یا دست‌وپاگیر هستند، به کار گرفته می‌شود.

5. پایه‌های زبان سطح بالا

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

6. بینش اصلی و دیدگاه تحلیلی

بینش اصلی: بارتولتی و همکاران صرفاً یک اپ‌کد عهد دیگر را پیشنهاد نمی‌دهند؛ آنها نظریه صوری گمشده‌ای را ارائه می‌دهند که یک ترفند هوشمندانه را به یک پارادایم برنامه‌نویسی مشروع و قابل تحلیل برای بیت‌کوین تبدیل می‌کند. این کلیدی است که مهندسی سیستماتیک قراردادهای پیچیده و ایمن روی بلاک‌چین‌های UTXO را ممکن می‌سازد و فراتر از اسکریپت‌نویسی موردی حرکت می‌کند.

جریان منطقی: استدلال به طور قانع‌کننده‌ای ساده است: ۱) مدل UTXO بیت‌کوین فاقد حالت است و قراردادها را محدود می‌کند. ۲) عهدها به عنوان یک راه‌حل پیشنهاد شده‌اند اما به صورت صوری به خوبی درک نشده‌اند. ۳) بنابراین، ما یک مدل صوری می‌سازیم. ۴) با استفاده از این مدل، نشان می‌دهیم که می‌تواند موارد استفاده باارزش و پیچیده (گاوصندوق‌ها، کانال‌ها، DeFi) را بیان کند. ۵) این صوری‌سازی سپس به طور طبیعی طراحی زبان سطح بالاتر را ممکن می‌سازد. این یک خط لوله کلاسیک "نظریه، عمل را ممکن می‌سازد" است که با دقت اجرا شده است.

نقاط قوت و ضعف: نقطه قوت اصلی، پل زدن بین شکاف نظریه رمزنگاری/زبان‌های برنامه‌نویسی و مهندسی بیت‌کوین است - شکافی که منجر به باگ‌های پرهزینه در مدل مبتنی بر حساب اتریوم شده است. معناشناسی صوری امکان تأیید ویژگی‌ها را فراهم می‌کند که یک دستاورد بزرگ است. نقطه ضعف، که به طور ضمنی تصدیق شده، اقتصاد سیاسی بیت‌کوین است. همانطور که مقاله اشاره می‌کند، "رویکرد بسیار محتاطانه" بیت‌کوین، استقرار اپ‌کدهای جدید مانند عهدها را - صرف نظر از ظرافت صوری آنها - به کاری عظیم تبدیل می‌کند. موفقیت لایه‌های دوم مانند لایتنینگ بدون عهدهای بومی نیز سؤالاتی درباره ضرورت در مقابل مطلوبیت مطرح می‌کند. علاوه بر این، امنیت مدل بر این فرض استوار است که فیلدهای محدودشده (مانند هش‌های اسکریپت) کافی هستند؛ اثرات تعامل پیش‌بینی‌نشده با اپ‌کدهای دیگر ممکن است باقی بماند.

بینش‌های عملی: برای پژوهشگران، این مقاله یک نقشه راه است: از روش‌های صوری برای کاهش ریسک و روشن‌سازی ارتقاءهای بلاک‌چین استفاده کنید. برای توسعه‌دهندگان، از همین حالا طراحی چارچوب‌های قرارداد را با فرض وجود عهدها آغاز کنید (همانطور که در لیکوئید یا استکس مشاهده می‌شود). برای توسعه‌دهندگان پروتکل بیت‌کوین، مقاله بنیان دقیقی را ارائه می‌دهد که برای استدلال به نفع BIP 119 (OP_CTV) یا پیشنهادهای مشابه لازم است - یک درخواست ویژگی را به یک مشخصه فنی تبدیل می‌کند. بزرگ‌ترین برداشت: آینده قراردادهای هوشمند بیت‌کوین درباره تقلید از اتریوم نیست، بلکه درباره بهره‌گیری از پارادایم منحصر به فرد UTXO+عهدها برای ایجاد یک کلاس جدید، بالقوه ایمن‌تر و مقیاس‌پذیرتر از برنامه‌های غیرمتمرکز است.

7. جزئیات فنی و صوری‌سازی

مدل صوری، تراکنش‌ها، اسکریپت‌ها و اعتبارسنجی را به صورت بافتاری تعریف می‌کند. یک جزئیات فنی کلیدی، نمایش محدودیت عهد است. اجازه دهید $\texttt{tx}$ نشان‌دهنده یک تراکنش باشد. یک عهد را می‌توان به عنوان یک تابع دید:

$\text{Covenant}_{\text{cond}} : \texttt{tx}_{\text{current}} \times \texttt{tx}_{\text{next}} \times \sigma \rightarrow \{\text{True}, \text{False}\}$

جایی که $\sigma$ نشان‌دهنده بافتار اعتبارسنجی (ارتفاع بلاک و غیره) است. گزاره $\text{cond}$ می‌تواند یک ربط از بررسی‌ها روی فیلدهای $\texttt{tx}_{\text{next}}$ باشد:

$\text{cond} \equiv (\texttt{hashOutputs}(\texttt{tx}_{\text{next}}) = H) \land (\texttt{nLockTime}(\texttt{tx}_{\text{next}}) > T) \land ...$

این با پیشنهادهایی مانند OP_CHECKTEMPLATEVERIFY همسو است که یک هش از بخش‌های مشخص‌شده تراکنش خرج‌کننده را برای مقایسه روی پشته می‌گذارد. ویژگی بازگشتی با اطمینان از اینکه یک خروجی از $\texttt{tx}_{\text{next}}$ حاوی یک اسکریپت $S'$ است که خودش یک عهد $\text{Covenant}_{\text{cond}'}$ را اعمال می‌کند، صوری‌سازی می‌شود.

8. چارچوب تحلیل و نمونه موردی

مثال: یک قرارداد گاوصندوق ساده
هدف: ایجاد یک UTXO که بتواند به دو روش خرج شود: ۱) فوری، اما فقط به یک آدرس خاص "ذخیره‌سازی سرد". ۲) به هر آدرسی، اما فقط پس از یک تأخیر ۳۰ روزه (اجازه لغو سرقت).
کاربرد چارچوب با استفاده از مدل صوری:
1. اسکریپت قفل‌کننده اولیه (scriptPubKey): حاوی یک شرط عهد $C_1$ است.
2. عهد $C_1(T_{vault}, T_{spend})$: باید به درست ارزیابی شود. بررسی می‌کند:
    الف) مسیر A (فوری): $\texttt{hashOutputs}(T_{spend}) = H_{cold}$ // هش خروجی باید با آدرس ذخیره‌سازی سرد از پیش متعهد شده برابر باشد.
    ب) مسیر B (تأخیری): $\texttt{nLockTime}(T_{spend}) \geq \text{currentBlock} + 4320$ (۳۰ روز به بلوک) و $\texttt{hashOutputs}(T_{spend})$ می‌تواند هر چیزی باشد.
3. اعتبارسنجی: هنگام خرج کردن UTXO گاوصندوق با $T_{spend}$، نود بیت‌کوین اسکریپت را اجرا می‌کند. نیاز به یک امضا از مالک گاوصندوق و تأیید می‌کند که $C_1$ برای جفت تراکنش برقرار است.
این مثال نشان می‌دهد که چگونه گزاره $C(T_x, T_{next})$ مدل صوری با بررسی‌های عینی روی فیلدهای تراکنش بعدی نمونه‌سازی می‌شود و یک ویژگی امنیتی (بازیابی سرقت) را ممکن می‌سازد که در بیت‌کوین پایه غیرممکن است.

9. کاربردها و جهت‌های آینده

صوری‌سازی چندین مسیر آینده را باز می‌کند:

• کامپایلرهای تأییدشده: ساخت کامپایلر از زبان‌های سطح بالا (مانند گسترش‌های سیمپلیسیتی یا مینی‌اسکریپت) به اسکریپت بیت‌کوین جاسازی‌شده با عهد، همراه با اثبات‌های صوری صحت.
• عهدهای فرازنج‌چینی: کاوش عهدهایی که خرج کردن را مشروط به رویدادهایی از بلاک‌چین‌های دیگر یا اوراکل‌ها می‌کنند، با استفاده از اثبات‌های رمزنگاری مانند SPV، همانطور که توسط کارهای قبلی روی "پل‌ها" و پژوهش‌های اخیر روی رول‌آپ‌ها اشاره شده است.
• عهدهای حفظ‌کننده حریم خصوصی: ادغام بررسی‌های عهد با اثبات‌های دانش صفر (مانند استفاده از امضاهای تاپ‌روت/شنور) برای پنهان کردن منطق قرارداد در حالی که هنوز آن را اعمال می‌کند، جهتی که در پروژه‌هایی مانند آرک در حال کاوش است.
• تحلیل امنیتی صوری: استفاده از مدل برای تحلیل سیستماتیک امنیت سازه‌های عهد پیشنهادی در برابر حملات اقتصادی و رمزنگاری، مشابه کاری که توسط جامعه سمپوزیوم امنیت و حریم خصوصی IEEE روی قراردادهای هوشمند اتریوم انجام شده است.
• ساده‌سازی پروتکل لایه دوم: بازطراحی پروتکل‌هایی مانند شبکه لایتنینگ یا سایدچین‌ها (لیکوئید) برای کارآمدتر و کم‌اعتمادتر شدن با بهره‌گیری از عهدهای بومی، کاهش نیاز به برج‌های نگهبانی پیچیده یا فدراسیون‌ها.

10. منابع

1. M. Bartoletti, S. Lande, R. Zunino. Bitcoin covenants unchained. arXiv:2006.03918v2 [cs.PL]. 2020.
2. S. Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System. 2008.
3. J. Poon, T. Dryja. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. 2016.
4. M. Moser, I. Eyal, E. G. Sirer. Bitcoin Covenants. Financial Cryptography 2016 Workshops.
5. Bitcoin Improvement Proposal 119 (BIP 119). OP_CHECKTEMPLATEVERIFY.
6. G. Wood. Ethereum: A Secure Decentralised Generalised Transaction Ledger. Ethereum Yellow Paper. 2014.
7. A. Miller, et al. Hashed Timelock Contracts (HTLCs). 2017.
8. R. O'Connor. Simplicity: A New Language for Blockchains. Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security.
9. Blockstream. Liquid Network. https://blockstream.com/liquid/
10. IEEE Symposium on Security and Privacy. Multiple papers on smart contract security analysis. Various years.