بازسازی و اثبات برابری کدهای دیکامپایل‌شده: تست تفاضلی و مقایسه بایت

در پروژه‌های مهندسی معکوس و بازسازی کدهای باینری، اتکای صرف به شبه‌کد خروجی دیکامپایلرهایی مانند Ghidra یا مدل‌های زبانی فریبنده است. کدی که چند تست ساده‌ی دستی را پاس می‌کند، ممکن است در شرایط مرزی، سرریزهای عددی و رفتار پلتفرم کامپایلر کاملاً متفاوت عمل کند و خطاهای امنیتی یا منطقی پنهان بر جای بگذارد.

این درس به شما می‌آموزد که چگونه با پیاده‌سازی دو پایه‌ی اصلی اثبات یعنی «تست تفاضلی روی شبکه‌ی جامع ورودی‌ها» و «مقایسه‌ی بایت‌به‌بایت پس از ماسک‌کردن بازنشانی‌ها»، برابری دقیق کد بازسازی‌شده را تضمین کنید و شواهد تجمیعی را به‌شکل شکست‌بسته (fail-closed) در قالب پروتکل MCP و ابزار rea ثبت نمایید.

قبولی در تست‌های شما صرفاً توافق روی همان تست‌ها را ثابت می‌کند؛ بنابراین اثبات برابری نیازمند شبکه‌ای از ورودی‌هاست که به تک‌تک حالت‌های مرزی برسد، و بایت‌هایی که پس از ماسک‌کردن بازنشانی‌ها (relocations) یکسان باشند.

اهداف یادگیری

• نوشتن یک بازسازی بر اساس فهرست دستورالعمل‌ها (instruction listing) و ثبت رکورد شواهد (evidence record) مربوط به آن.
• ساخت یک شبکه‌ی ورودی (input grid) با یک دسته به‌ازای هر وضعیت بحرانی: بررسی صفر (zero guard)، مقادیر منفی، تقسیم همراه‌با هرس (truncating division)، سرریز 32 بیتی و خطای تقسیم (divide trap).
• اجرای کد اصلی و بازسازی‌شده در یک برنامه و ثبت نتیجه‌ی هر خانه از شبکه، از جمله حالت خطا.
• کامپایل مجدد بازسازی با همان پرچم‌های کامپایلر اصلی و مقایسه‌ی بایت‌های تابع پس از ماسک‌کردن فیلدهای بازنشانی.
• خواندن و مقایسه‌ی مقادیر ثابتی که بازنشانی‌ها به آن‌ها اشاره دارند، تا هیچ لیترال نادرستی پذیرفته نشود.
• هدایت سرور MCP ابزار rea از طریق یک کلاینت کوچک stdio و ثبت هر مرحله همراه‌با شناسه‌ی شواهد آن.
• صدور یک رکورد اثبات با راهبرد شکست‌بسته (fail-closed) که شناسه‌اش حاصل هش ادعاها و پیوندهای شواهد باشد.

صورت مسئله

از rea خواستید پرونده‌ی تابع (function dossier) percent_change را در فایل آزمایشی ledger-x86_64-O1.o استخراج کند. Ghidra 12.1.4 یک شبه‌کد تحویل داد و ایجنت بر اساس آن این کد C را نوشت:

int percent_change(int before, int after) {
    if (before == 0) return 0;
    return (int)(((long)after - before) * 100 / before);
}

چهار تست پاس می‌شوند: ورودی (100, 150) خروجی 50 می‌دهد، (200, 100) خروجی -50 می‌دهد، (0, 5) مقدار 0 را برمی‌گرداند و (50, 100) مقدار 100 می‌دهد. ایجنت تابع grade را هم به‌صورت چهار عبارت if روی مقادیر 90، 80، 70 و 60 بازسازی کرد. شش تست دیگر هم پاس می‌شوند. گزارش می‌گوید: «تأیید شد» (verified).

اما این گزارش به هیچ‌کدام از پرسش‌های زیر پاسخ نمی‌دهد:

• وقتی (after - before) * 100 در 32 بیت جا نشود، تابع اصلی چه برمی‌گرداند؟
• تابع اصلی برای نمره‌ی 110 چه مقداری بازمی‌گرداند؟
• آیا بازسازی دقیقاً به همان 16 بایتِ تابع اصلی کامپایل می‌شود؟
• وقتی دو تابع کامپایل‌شده بایت‌های یکسانی دارند، آیا بازنشانی‌های آن‌ها هم به مقادیر ثابت یکسانی اشاره می‌کنند؟
• بازسازی از کدام رکورد شواهد آمده و آیا ایجنت فهرست دستورالعمل‌ها را خوانده یا شبه‌کد را؟
• روی سیستمی که کامپایلر C ندارد، وضعیت این اثبات چه خواهد بود؟

تمام برنامه‌های هدف در این درس، کدهایی هستند که خودمان نوشته و کامپایل کرده‌ایم. قوانین دامنه (scope) و ضوابط درس 32 بدون تغییر در اینجا نیز اعمال می‌شوند.

شواهد چه می‌گویند؟

حلقه‌ی ایجنت (agent loop) در code/main.py شش فراخوانی با stdio به سمت rea 6.5.0 ارسال کرد. اجرای ثبت‌شده در فایل code/fixtures/runs/agent-run.json قرار دارد. سرور به درخواست initialize با نسخه‌ی پروتکل 2025-11-25 پاسخ داد. سه فراخوانی، رکوردهای شواهد بازگرداندند:

هزینه‌ی اولین فراخوانی صرف ایمپورت در Ghidra و تحلیل خودکار شد. هر رکورد دارای مقادیر confidence: "observed"، authority: "shipped-artifact" و هش SHA-256 فایل آبجکت یعنی 9a4a8082ba5e285a732552981a6935e0c5255725664f380e37c44ebfb04d803f است. Ghidra فایل آبجکتِ بازنشانی‌پذیر را طوری لود می‌کند که بخش .text در آدرس 0x100000 قرار گیرد؛ بنابراین تابع percent_change در 0x100000 و تابع grade در 0x100010 می‌نشیند.

منشأ نوع داده‌ی long در واقع شبه‌کد تولیدی برای percent_change بود:

undefined1  [16] percent_change(int param_1,int param_2,ulong param_3)
{
  long lVar1;
  undefined1 auVar3 [16];
  if (param_1 != 0) {
    lVar1 = (long)((param_2 - param_1) * 100);
    auVar3._0_8_ = lVar1 / (long)param_1 & 0xffffffff;
    auVar3._8_8_ = lVar1 % (long)param_1 & 0xffffffff;
    return auVar3;
  }
  ...
}

دیکامپایلر دید که دو دستور cltd و idivl روی هر دو رجیستر edx و eax می‌نویسند؛ به همین دلیل مقدار بازگشتی 16 بایتی را به‌شکل یک تقسیم 64 بیتی مدل‌سازی کرد. اما فهرست دستورالعمل‌ها در همان رکورد شواهد، بیان ساده‌تری دارد:

0x100000: TEST EDI, EDI
0x100002: JZ 0x0010000d
0x100004: SUB ESI, EDI
0x100006: IMUL EAX, ESI, 0x64
0x100009: CDQ
0x10000a: IDIV EDI
0x10000c: RET
0x10000d: XOR EAX, EAX
0x10000f: RET

تمام عملیات‌ها 32 بیتی هستند. دستور IMUL EAX, ESI, 0x64 ضرب 32 بیتی انجام می‌دهد و نیمه‌ی پایینی را نگه می‌دارد. دستور CDQ علامت رجیستر eax را در edx بسط می‌دهد و IDIV EDI این جفت 64 بیتی را بر یک مقسوم‌علیه 32 بیتی تقسیم می‌کند. بازسازی درستی که این فهرست را دنبال کند، 100 * (after - before) / before در قالب int است.

رکورد مربوط به grade نیز ساختار مشابهی دارد. شبه‌کد به یک جدول اشاره می‌کند: *(uint *)(&DAT_001000b4 + (ulong)uVar2 * 4)، همراه‌با یک عبارت پیش‌فرض ناخوانا که با 0x66666667 ساخته شده است. فهرست دستورالعمل‌ها نشان می‌دهد تقسیم بر 10 به‌صورت IMUL RAX, RAX, 0x66666667، SAR RCX, 0x22، SHR RAX, 0x3f و ADD ECX, EAX پیاده شده است. سپس دستورهای ADD ECX, -0x6، CMP ECX, 0x4 و JA دهگان‌های بین 6 تا 10 را نگه می‌دارند. دستور XOR EAX, EAX قبل از مقایسه، همان مقدار پیش‌فرض 0 است. در نهایت LEA RCX, [0x1000b4] و MOV EAX, dword ptr [RCX + RAX*0x4] جدولی شامل پنج ورودی 4 بایتی را می‌خوانند.

مرحله‌ی 4 همان 20 بایت را خواند: 01000000 02000000 03000000 04000000 04000000. این جدول شامل مقادیر 1, 2, 3, 4, 4 برای دهگان‌های 6، 7، 8، 9 و 10 است. این دقیقاً همان ساختار switch در فایل ledger.c است که در آن case 10 و case 9 در مقدار 4 مشترک‌اند.

هر دو اثبات در صفحات شواهد خودِ rea از فهرست دستورالعمل‌ها و خواندن مقادیر ثابت با read_bytes آغاز شدند. در پروژه‌ی DX-Ball، اولین شبه‌کد به‌صورت FUN_00406400(void) بدون ورودی استک بود و نمایش دستورالعمل‌ها آن را تصحیح کرد. ابتدا فهرست دستورالعمل‌ها را بخوانید، به شناسه‌ی رکورد ارجاع دهید و سپس کد C را بنویسید.

نوشتن کاندیداها

پوشه‌ی code/fixtures/candidates/ شامل هشت بازسازی است؛ هر فایل برای یک تابع. چهار فایل از فهرست دستورالعمل‌ها پیروی می‌کنند یا به همان کد کامپایل می‌شوند. چهار تای دیگر ظاهراً معقول اما نادرست‌اند، یا طوری خطا دارند که حتی یک تست دستی هم آن را پیدا می‌کند.

هر فایل با این دستور تست کامپایل می‌شود: clang -target x86_64-unknown-linux-gnu -O1 -fno-asynchronous-unwind-tables -c. فایل‌های کامپایل‌شده کنار سورس‌ها commit شده‌اند تا تست‌ها روی سیستمی بدون clang هم اجرا شوند.

پایه‌ی اول: اجرا و مقایسه

تعریف مَک‌کیمن در سال 1998 از تست تفاضلی (differential testing) نیازمند «دو یا چند سیستم مقایسه‌پذیر» است که با «تست‌کیس‌های تولیدشده به‌صورت مکانیکی» تغذیه شوند؛ در این تعریف، هرگونه نتیجه‌ی متفاوت، قفل‌کردن (hang) یا کرش، گزینه‌ی باگ تلقی می‌شود. او بخش دشوار کار را هم نام برد: «زننده‌ترین مسئله در تست، ارزیابی نتیجه‌ی یک تست است.» در اینجا تابع اصلی نقش مرجع حقیقت (oracle) را دارد. نیازی نیست جواب درست را از پیش بدانیم؛ کافی است تابع اصلی و کد بازسازی‌شده روی شبکه‌ای از ورودی‌ها که به تک‌تک وضعیت‌های بحرانی می‌رسد، در هیچ نقطه‌ای اختلاف نداشته باشند.

طراحی شبکه‌ی ورودی

تابع input_grid() در code/main.py تعداد 92 خانه ورودی می‌سازد. برای percent_change، تمام جفت‌های حاصل از ده مقدار before و هفت مقدار after را در نظر می‌گیرد:

before: 0, 1, -1, 3, -3, 7, 100, -100, 2147483647, -2147483648
after:  0, 5, -5, 105, 536870911, 2147483647, -2147483648

برای grade، تعداد 22 نمره انتخاب می‌کند: دو سمت هر مرز بازه، اعداد منفی، 0، 110 و دو حد نهایی نوع int. تابع classify() هر خانه را برچسب‌گذاری می‌کند. دسته‌ی سرریز شامل 32 خانه، منفی 17، مرزها 14، عادی 12 و بررسی صفر 7 خانه دارند. همچنین هرس منفی 5 خانه، گردکردن 2، خارج از دامنه switch تعداد 2 و خطای تقسیم 1 خانه دارد.

هر دسته تنها به‌یک دلیل وجود دارد. خانه‌های بررسی صفر، شاخه‌ی TEST EDI, EDI را ارزیابی می‌کنند. خانه‌های منفی، تقسیمِ همراه‌با هرس را می‌سنجند: C و دستور idiv به سمت صفر گرد می‌کنند؛ در نتیجه -9 / 10 برابر 0 و -10 / 10 برابر -1 می‌شود. خانه‌های گردکردن بررسی می‌کنند که ضرب پیش از تقسیم انجام شود، تا (105 - 100) * 100 / 100 برابر 5 شود نه 0. خانه‌های سرریز طوری تنظیم شده‌اند که (after - before) * 100 از 32 بیت فراتر برود. تک‌خانه‌ی خطا نیز حاصل‌ضربِ سرریز‌شده را برابر INT_MIN قرار می‌دهد، درحالی‌که before برابر -1 است.

یانگ، چن، آید و رجر ابزار Csmith را ساختند تا برنامه‌هایی بدون رفتار تعریف‌نشده (undefined behaviour) تولید کنند. اختلاف با اوراکل روی رفتار تعریف‌نشده صرفاً نوفه است و هرگز گزارش باگ معتبر به حساب نمی‌آید. سرریز علامت‌دار در C تعریف‌نشده است. اما اوراکل ما یک فایل باینری کامپایل‌شده با رفتاری ثابت است؛ پس خانه‌های سرریز کاملاً در دامنه‌ی کار قرار دارند. نکته‌ی آموزنده این است که بدانید کدام خانه‌ها به استاندارد وابسته‌اند و کدام خانه‌ها به بایت‌های کامپایل‌شده.

درایور و خطای تقسیم

فایل code/driver.c هر خانه را به‌صورت یک خط از stdin می‌خواند و ورودی‌ها، نتیجه‌ی اصلی و نتیجه‌ی بازسازی را چاپ می‌کند. تابع build_harness() کاندیدا را با فلگ‌های -Dpercent_change=cand_percent_change -Dgrade=cand_grade کامپایل می‌کند تا هر دو نسخه با نام‌های متفاوت در یک برنامه لینک شوند. روی یک سیستم لینوکس x86-64، کد اصلی همان فایل آبجکت fixture است. روی هر سیستم دیگری، فایل ledger.c به‌شکل بومی کامپایل می‌شود و گزارش، مقدار original_kind: fixture-source را ثبت می‌کند.

درایور یک هندلر برای سیگنال SIGFPE به کمک sigsetjmp و siglongjmp مستقر می‌کند. برای مقادیر before = -1 و after = 536870911، اختلاف برابر 536870912 می‌شود و حاصل‌ضرب 32 بیتی پس از سرریز به -2147483648 می‌رسد. در معماری x86-64، اجرای idiv با چنین مقسوم و مقسوم‌علیهی برابر -1، استثنای خطای تقسیم را ایجاد می‌کند؛ زیرا خارج‌قسمت در 32 بیت جا نمی‌شود (راهنمای توسعه‌دهندگان اینتل، جلد 2، دستور IDIV). هندلر این رخداد را به مقدار ثبت‌شده‌ی trap تبدیل می‌کند.

در معماری AArch64، دستور sdiv چنین خطایی ندارد و برای همین عملوندها مقدار -2147483648 را برمی‌گرداند. اجرای ما روی مک با arm64 دقیقاً همین رفتار را ثبت کرد. پس اوراکل به معماری وابسته است و گزارش مشخص می‌کند کدام معماری اجرا شده است.

نتایج

فراخوانی prove_behaviour(PLAUSIBLE) بازسازی بر پایه‌ی long و بازسازی بر پایه‌ی آستانه‌ها را می‌سازد. هر ده تست ساده پاس می‌شوند؛ اما شبکه در 28 خانه شکست می‌خورد:

تمام 26 شکست در percent_change مربوط به خانه‌های سرریزی هستند که در آن‌ها |before| > 1 است. اگر before برابر 1 یا -1 باشد، خارج‌قسمت 64 بیتی دوباره پس از هرس به همان مقدار سرریز‌شده بازمی‌گردد؛ بنابراین این خانه‌ها تصادفی هم‌خوانی دارند. بازسازی آستانه‌ای grade رد می‌شود، چون ساختار switch اصلی برای دهگان‌های 11 به بالا هیچ شرطی ندارد و حاصل 110 / 10 برابر 11 است.

فراخوانی prove_behaviour(EQUAL) دو فایل percent_change_mul_first.c و grade_switch.c را بیلد می‌کند. همه‌ی 92 خانه هم‌خوانی دارند. در مقابل، فایل percent_change_div_first.c در دو مورد از چهار تست ساده شکست می‌خورد، که همان خطایی است که یک تست دستی می‌تواند کشف کند.

تابع oracle_disagreements() نکته‌ی دومی را بررسی می‌کند. توابع percent_change_model() و grade_model() پیاده‌سازی‌های پایتونی فهرست دستورالعمل‌ها هستند که از wrap32() برای ضرب 32 بیتی و از idiv32() برای قاعده‌ی معماری بهره می‌برند. گزارش، مدل را با رفتار واقعی و مشاهده‌شده‌ی کد اصلی در تمام خانه‌ها مقایسه می‌کند. صفر بودن اختلاف‌ها یعنی مدل و باینری در تمام خانه‌ها توافق دارند. مدل یک شواهد مشتق‌شده (derived evidence) و اجرا یک شواهد مشاهده‌شده (observed evidence) است. گزارش این دو را در فیلدهای جداگانه‌ای نگه می‌دارد.

پایه‌ی دوم: کامپایل مجدد و مقایسه

رفتار روی شبکه تنها یکی از پایه‌هاست. پایه‌ی دوم می‌پرسد: آیا بازسازی، اگر با همان کامپایلر و همان پرچم‌ها کامپایل شود، دقیقاً همان بایت‌ها را تولید می‌کند؟ پروژه‌ی DX-Ball برای تابع کمکی‌اش «تطابق 63 بایت» را گزارش کرد. پروژه‌ی TH04 به تطابق 2139 بایتی رسید. هرکدام از کامپایلر همان دوره‌ی زمانی استفاده کردند. خودِ rea به‌تنهایی قادر به این کار نیست. ابزار compare_functions آن صرفاً تفاوت خط‌به‌خط متن ارائه‌دهنده را نشان می‌دهد و این محدودیت را پیوست می‌کند: «اسمبلی یک متن ارائه‌دهنده‌ی مات است؛ امکان نرمال‌سازی بازنشانی وجود ندارد.»

خواندن آبجکت

کلاس ElfObject در code/main.py یک فایل آبجکت بازنشانی‌پذیر ELF64 را با struct.unpack_from می‌خواند. این کلاس مقادیر جادویی (magic)، کلاس 64 بیتی، داده‌های little-endian، مقدار e_machine برابر 62 و e_type برابر 1 را بررسی می‌کند. سپس سراغ هدر بخش‌ها، جدول رشته‌ها، .symtab و تمام بخش‌های .rela می‌رود. در فایل نمونه، percent_change در آفست 0 از بخش .text با اندازه‌ی 16 بایت، و grade در آفست 0x10 با اندازه‌ی 46 بایت شروع می‌شود. total در آفست 0x40 با اندازه‌ی 31 بایت و grade_label در 0x60 با اندازه‌ی 63 بایت قرار دارد.

16 بایتِ تابع percent_change عبارت‌اند از 85 ff 74 09 29 fe 6b c6 64 99 f7 ff c3 31 c0 c3. این تابع هیچ بازنشانی‌ای ندارد. اما grade یک بازنشانی دارد: در آفست 0x26 درون تابع، از نوع R_X86_64_PC32، نماد .rodata و مقدار الحاقی (addend) برابر 0x10. این بازنشانی متعلق به دستور 7 بایتی leaq در آفست 0x23 است که چهار بایت آخر آن فیلد جابه‌جایی (displacement) هستند.

ماسک‌کردن و سپس مقایسه‌ی رکوردها

در یک آبجکت RELA، مقدار الحاقی در رکورد بازنشانی نگهداری می‌شود و چهار بایتِ فیلد صفر هستند. فایل کاندیدای grade_switch.o هم در آنجا مقدار صفر دارد. مقایسه‌ی ساده‌ی بایت‌ها در شرایطی که دو بازنشانی به جاهای متفاوتی اشاره دارند موفقیت‌آمیز خواهد بود. تابع mask_relocations() درهرصورت این فیلد را در هر دو طرف صفر می‌کند؛ بنابراین همین روش برای آبجکت‌های REL و همچنین Mach-O (که فیلد، حاوی مقدار الحاقی است) نیز کار می‌کند.

سپس prove_bytes() رکوردهای بازنشانی را بر اساس آفست، نوع و بخش مقصد مقایسه می‌کند. کد اصلی مقدار .rodata+0x10 و کد کاندیدا مقدار .rodata-0x4 را نشان می‌دهد. دلیل تفاوت مقدار الحاقی این است که در آبجکت کاندیدا، جدول labels.rel پیش از جدول switch نیامده است. تفاوت مقدار الحاقی نشانه‌ی آفست متفاوت است، نه یک تابع متفاوت.

خواندن مقادیر ثابتی که بازنشانی به آن‌ها اشاره دارد

در فیلدهای وابسته به PC که در انتهای دستورالعمل قرار می‌گیرند، پردازنده آدرس دستور بعدی را اضافه می‌کند؛ بنابراین هدف برابر است با: نماد به‌علاوه‌ی مقدار الحاقی به‌علاوه‌ی 4. در کد اصلی این مقدار .rodata+0x14 و در کاندیدا .rodata+0x0 است. تابع read_table() پنج ورودی 4 بایتی را از آنجا می‌خواند. هر دو نسخه شامل مقادیر 1, 2, 3, 4, 4 هستند.

تعداد پنج ورودی مستقیماً از فهرست دستورالعمل‌ها می‌آید: دستور CMP ECX, 0x4 همراه‌با JA اندیس‌های 0 تا 4 را مجاز می‌شمارد، و [RCX + RAX*0x4] برای هر اندیس 4 بایت می‌خواند. دیکشنری CLAIMS در code/main.py این ساختار را برای grade و عدم وجود بازنشانی را برای percent_change ثبت می‌کند.

این مرحله به‌خاطر باگی است که در پروژه‌ی TH08 مستند شد. در مقایسه‌ی قدیمی‌تر آن پروژه: «آدرس مقصد مجدداً در فیلد بازنشانی دستورالعمل قرار داده می‌شد و سپس بایت‌های دستورالعمل بدون بررسی مقادیر اعشاریِ (floating-literal) آن آدرس مقایسه می‌شدند. به همین دلیل سورسِ 0.0 می‌توانست در برابر هدفِ 128.0 کاملاً یکسان به نظر برسد.» در اصلاحیه‌ای که اعمال کردند، 1548 ارجاع به مقادیر اعشاری بازبینی و دوازده مورد دیگر تصحیح شد. فایل grade_case10_wrong.c نسخه‌ی ما از همان باگ است. 46 بایت کد آن دقیقاً با کد اصلی برابر است، رکورد بازنشانی آن ساختار یکسانی دارد، اما مقادیر جدول آن 1, 2, 3, 4, 3 است. فقط بررسی مقادیر ثابت می‌تواند این خطا را رد کند.

نتایج

دو نتیجه نیاز به دقت بیشتری دارند. فایل percent_change_split.c سورس متفاوتی دارد اما بایت‌های خروجی آن کاملاً یکسان است؛ زیرا clang سرریز علامت‌دار را تعریف‌نشده در نظر می‌گیرد و عبارت after * 100 - before * 100 را در قالب یک ضرب ساده می‌کند. فایل grade_table.c هم بایت‌به‌بایت منطبق است؛ یعنی کامپایلر چه از طریق اندیس آرایه و چه از طریق ساختار switch، به همان جدول نهایی رسیده است. انطباق بایت‌ها ثابت می‌کند که این کامپایلر با این پرچم‌ها، از این کاندیدا همان کد را تولید کرده است؛ اما ثابت نمی‌کند که کاندیدا دقیقاً همان متن سورس اصلی است.

اندازه صرفاً یک شاخص تشخیصی است نه شرط پذیرش. صفحات شواهد در rea رکوردی از یک کاندیدای 1825 بایتی با اندازه‌ی درست دارند که 467 بایتِ متفاوت داشته است. بازسازی wide اندازه‌ی 26 بایتی دارد چون دستورهای movslq، imulq، cqto و idivq جایگزین حالت‌های 32 بیتی شده‌اند. فهرست دستورالعمل‌ها حتی پیش از هرگونه کامپایلی، اندازه‌ی عملوندها را مشخص کرده بود.

حلقه‌ی ایجنت روی rea

شصت‌وپنج ابزار MCP در rea دستور خط فرمانی ندارند و verify_reconstruction یکی از آن‌هاست. کلاس McpStdioClient در code/main.py کوچک‌ترین کلاینتی است که به این ابزارها دسترسی پیدا می‌کند. این کلاینت دستور npx -y rea-agents@6.5.0 mcp را اجرا می‌کند، در هر خط یک درخواست JSON-RPC به stdin می‌فرستد و پاسخ‌ها را در قالب یک شیء JSON در هر خط روی یک ریسه (thread) از stdout می‌خواند. ابتدا پیام initialize را با نسخه‌ی پروتکل 2025-11-25 ارسال می‌کند، سپس notifications/initialized و در نهایت tools/call. ضرب‌الاجل (deadline) پیش‌فرض برای هر فراخوانی 330 ثانیه است؛ همان زمانی که rea برای شروع سرد (cold start) به Ghidra می‌دهد.

تابع agent_loop() این شش فراخوانی را انجام می‌دهد و هرکدام را ثبت می‌کند:

{
  "step": 2,
  "tool": "analyze_function",
  "arguments": {"procedure": "percent_change"},
  "seconds": 6.31,
  "is_error": false,
  "evidence_id": "ev_e88b10dc0c6400e51bb6f7fdc3eaea8d2c97cc02463f0db3e6afeefc273197cd",
  "confidence": "observed",
  "authority": "shipped-artifact",
  "limitations": ["Resolved reference metadata identifies computed, indirect, external, call, jump, and data edges; unresolved targetless flows remain unknown, and function classifications distinguish thunks and externals.", "..."],
  "result_sha256": "..."
}

رکوردهای کامل شواهد تحت شناسه‌های خودشان در همان فایل ذخیره می‌شوند. شبه‌کد و فهرست دستورالعمل‌هایی که بازسازی بر اساس آن‌ها انجام شد، بخشی از فایل نمونه هستند. تابع table_address() عملوند دستور LEA را در فهرست مربوط به grade پیدا کرده و آن را به read_bytes تحویل می‌دهد. ابزارهای open_binary، get_evidence_bundle و close_binary هیچ رکورد شواهدی بازنمی‌گردانند و با شناسه‌ی null ثبت می‌شوند.

تابع run_agent(live=True) در صورتی که npx در دسترس باشد و GHIDRA_INSTALL_DIR به یک دایرکتوری اشاره کند، rea را اجرا می‌کند. در غیر این صورت، اجرای ثبت‌شده‌ی قبلی را بازخوانی کرده و موضوع را در stderr اطلاع می‌دهد. تست‌ها یک گام فراتر می‌روند: code/tests/fake_rea_server.py یک سرور جایگزین است که به هر tools/call بر اساس همان ابزار و آرگومان‌ها، پاسخِ ضبط‌شده را برمی‌گرداند. کلاینت و حلقه در تمام تست‌ها روی این سرور اجرا می‌شوند، بدون اینکه به نصب بودن rea، Ghidra یا Java نیازی باشد.

اعتبارسنج rea چه چیزی را می‌تواند بگوید و چه چیزی را نه؟

ابزار verify_reconstruction در rea ادعاهایی را که به شواهد مقایسه‌ای اشاره دارند دریافت کرده و برای هر ادعا وضعیت pass، fail یا unknown برمی‌گرداند. در متن محدودیت‌های ثابت آن آمده است: «قبولی (Pass) یعنی تمام ادعاهای اعلام‌شده پاس شده‌اند؛ این ابزار برابری همگانی پیاده‌سازی را ثابت نمی‌کند.» یک ادعا درباره‌ی یک تابع، متن ارائه‌دهنده را از طریق compare_functions مقایسه می‌کند. یک ادعای رفتاری، دو فرآیند ثبت‌شده را از طریق compare_process_captures می‌سنجد. اگر رکورد مبدأ پوشش کاملی روی فراخوانی‌ها نداشته باشد، ادعای مربوط به فراخوانی‌ها وضعیت unknown می‌گیرد. در داخل rea هیچ امکانی برای کامپایل مجدد یک تابع بازسازی‌شده یا اجرای آن روی شبکه‌ی ورودی شما وجود ندارد. دو پایه‌ای که در این درس بررسی کردیم، بخش‌هایی هستند که rea بر عهده‌ی خود شما می‌گذارد.

دفتر کل تعهدات در rea انتظار یک رکورد اثبات با مشخصات زیر دارد: predicate_type: "rea.reconstruction-proof"، operation: "verify_reconstruction_obligations"، confidence: "observed" و normalized_result.passed === true. هیچ‌کدام از ابزارهای عمومی rea چنین رکوردی صادر نمی‌کنند. تابع build_proof() در code/main.py آن را می‌سازد:

{
  "predicate_type": "rea.reconstruction-proof",
  "operation": "verify_reconstruction_obligations",
  "confidence": "observed",
  "authority": "controlled-replay",
  "normalized_result": {
    "passed": true,
    "status": "pass",
    "claims": [
      {"claim_id": "percent_change.behaviour", "kind": "behavioral", "status": "pass", "evidence_ids": ["ev_e88b10dc..."]},
      {"claim_id": "grade.behaviour", "kind": "behavioral", "status": "pass", "evidence_ids": ["ev_67b6d3f9..."]},
      {"claim_id": "percent_change.bytes", "kind": "structural-function", "status": "pass", "evidence_ids": ["ev_e88b10dc..."]},
      {"claim_id": "grade.bytes", "kind": "structural-function", "status": "pass", "evidence_ids": ["ev_67b6d3f9..."]},
      {"claim_id": "grade.referenced-constants", "kind": "structural-function", "status": "pass", "evidence_ids": ["ev_67b6d3f9..."]}
    ]
  },
  "evidence_links": ["ev_e88b10dc...", "ev_67b6d3f9..."],
  "evidence_id": "ev_..."
}

شناسه‌ی این رکورد از پیشوند ev_ به‌علاوه‌ی هش SHA-256 محتوای رکورد (بدون احتساب خود فیلد id)، روی JSON فشرده با کلیدهای مرتب‌شده ساخته می‌شود. تابع aggregate() رفتار شکست‌بسته دارد: اولویت اول با fail است، بعد unknown، و یک لیست خالی از ادعاها نیز وضعیت unknown می‌گیرد. روی سیستمی بدون کامپایلر C، دو ادعای رفتاری در حالت unknown قرار می‌گیرند؛ بنابراین حتی اگر هر دو ادعای مربوط به بایت‌ها پاس شوند، کل رکورد وضعیت unknown خواهد داشت. مقدار authority برابر controlled-replay است؛ زیرا این اثبات حاصل اجرای درایور خودمان است، نه برآمده از فایل آبجکت به‌تنهایی.

پژوهش‌ها چه می‌گویند؟

لیو، رف و میسینسکی در سال 2026 هشت سیستم دیکامپایل را در نه پیکربندی مختلف ارزیابی کردند. کاندیداهایی که در تمام تست‌های بنچ‌مارک پاس شده بودند، روی ورودی‌های فازینگ (fuzzed) دچار انحراف عملکرد شدند. نرخ این انحراف به‌طور میانگین 4.9 درصد و در یک سیستم تا 13 درصد بود. روی 300 تابع از کتابخانه‌های گیت‌هاب و 287 تابع مرتبط با آسیب‌پذیری‌های CVE، قدرتمندترین مدل اصلاح توانست نرخ بیلد Ghidra را از 75 درصد به 90 درصد برساند. با این حال، در همان توابع، نرخ تطابق رفتاری از 74 درصد به 62 درصد کاهش یافت. آن‌ها ریشه‌ی مشکل را در اختراع فیلدها، نوع‌ها، توابع فراخوانی‌شده و شرط‌های بررسی دیدند؛ مواردی که جای مجهولاتِ آشکارِ دیکامپایلرهای سنتی را می‌گرفتند.

فایل percent_change_wide.c ما یکی از همین نوع‌های ساختگی است. شبه‌کد یک نوع long ارائه داد، بازسازی همان را حفظ کرد، نتیجه هم کامپایل شد و ده تست را پاس کرد، اما در 26 خانه‌ی مربوط به سرریز به خطا خورد. بازسازی آستانه‌ای grade هم یک شرط بررسی ساختگی بود. بر اساس معیار ارزیابی LLM4Decompile (که خروجی را مجدداً کامپایل کرده و assertionهای بنچ‌مارک را می‌سنجد)، هر دوی این‌ها «قابل اجرای مجدد» شناخته می‌شدند. شبه‌کد C تولیدی Ghidra در بنچ‌مارک HumanEval-Decompile توانسته بود 20.12 درصد از این assertionها را پاس کند.

بنچ‌مارک DecompileBench تعداد 23,400 تابع از 130 برنامه‌ی واقعی را بررسی کرد. نتایج نشان داد که روش‌های مبتنی بر مدل‌های زبانی از نظر درستی عملکرد 52.2 درصد پایین‌تر از دیکامپایلرهای صنعتی عمل می‌کنند، هرچند امتیاز خوانایی بالاتری دارند.

سه روش اثباتی که در این حوزه به کار می‌روند، همان سه پایه‌ای هستند که می‌توانید بسازید. ابزارهای Phoenix و DREAM خروجی را مجدداً کامپایل کرده و تست‌های برنامه‌ی اصلی را اجرا می‌کنند. مَک‌کیمن و پروژه Csmith ورودی‌های تولیدشده را در چارچوب رفتارهای تعریف‌شده در برابر کد اصلی می‌سنجند. راموس و انگلر دو تابع C را با اجرای نمادین کران‌دار (bounded symbolic execution) بررسی می‌کنند؛ روشی که برابری را در تمام مسیرهای پیمایش‌شده تا یک اندازه‌ی مشخص از ورودی اثبات می‌کند. در این درس ما دو مورد اول را پیاده‌سازی می‌کنیم. سومی آزمایش عملی در دفتر کل شواهدِ درس 35 است؛ برای مواقعی که شبکه‌ی ورودی‌ها آن‌قدر کوچک است که نمی‌توان کاملاً به آن اعتماد کرد.

پیاده‌سازی از صفر

اجرای درایور با کتابخانه‌ی استاندارد:

cd phases/13-tools-and-protocols/36-rebuild-and-prove-equal
python3 code/main.py

اگر دستور clang در دسترس باشد، این دمو هر دو جفت کاندیدا را کامپایل کرده و 92 خانه را برای هرکدام می‌سنجد. همچنین هشت کاندیدا را مجدداً کامپایل می‌کند، اجرای ایجنت را بازخوانی کرده و رکورد نهایی اثبات را می‌سازد. در صورت نبود clang، فایل‌های آبجکتِ commitشده را می‌خواند و ادعاهای رفتاری را در وضعیت unknown گزارش می‌کند.

خروجی مورد انتظار روی مک با arm64:

{
  "host": "aarch64 Darwin",
  "originalKind": "fixture-source",
  "gridCells": 92,
  "plausible": {"naivePassed": true, "gridMismatches": 28, "oracleDisagreements": 0},
  "equal": {"naivePassed": true, "gridMismatches": 0, "oracleDisagreements": 0},
  "legTwo": {
    "percent_change_mul_first": {"status": "pass", "reasons": []},
    "percent_change_wide": {"status": "fail", "reasons": ["size 16 vs 26 bytes"]},
    "grade_case10_wrong": {"status": "fail", "reasons": ["referenced constants differ: [1, 2, 3, 4, 4] vs [1, 2, 3, 4, 3]"]}
  },
  "agentRun": {"mode": "replayed fixture", "server": {"name": "rea", "version": "6.5.0", "protocolVersion": "2025-11-25"}},
  "proof": {"status": "pass", "evidence_id": "ev_..."}
}

کد code/main.py را به این ترتیب بخوانید:

1. توابع wrap32()، c_div()، idiv32() و دو تابع *_model() که معناشناسی محاسبات صحیح در فهرست دستورالعمل‌ها را پیاده می‌کنند.
2. توابع input_grid() و classify() که 92 خانه را ساخته و برچسب‌گذاری می‌کنند.
3. توابع build_harness() و execute() که از کد اصلی، کاندیداهای تغییرنام‌یافته و فایل driver.c یک برنامه‌ی واحد می‌سازند و خانه‌ها را اجرا می‌کنند.
4. تابع prove_behaviour() که گزارش پایه‌ی اول را همراه‌با موارد عدم تطابق و اختلاف‌های مدل بازمی‌گرداند.
5. کلاس ElfObject که هدرها، نمادها و رکوردهای .rela را می‌خواند. توابع mask_relocations() و read_table() داده‌ها را برای مقایسه آماده می‌کنند.
6. تابع prove_bytes() که گزارش پایه‌ی دوم شامل اندازه‌ها، بازه‌های ماسک‌شده، ساختار بازنشانی‌ها و جداول را بازمی‌گرداند.
7. کلاس McpStdioClient و تابع agent_loop() که تعامل با rea را مدیریت و هر مرحله را ثبت می‌کنند.
8. توابع build_proof() و aggregate() که رکورد اثبات را با رویکرد شکست‌بسته تولید می‌کنند.

استفاده از ابزارهای واقعی

برای اثبات برابری یک تابع جدید، این مراحل را تکرار کنید:

1. دستور analyze_function را برای تابع فراخوانی کرده و شناسه‌ی شواهد را ثبت کنید. قبل از شبه‌کد، فهرست دستورالعمل‌ها را بخوانید.
2. کد کاندیدا را بر اساس اندازه‌ی عملوندهای موجود در فهرست دستورالعمل‌ها بنویسید. نام تابع اصلی را تغییر ندهید.
3. تمام ضرب‌ها، جمع‌ها، تفریق‌ها و تقسیم‌های داخل فهرست را بنویسید. ورودی‌هایی به شبکه اضافه کنید که هر عمل را در پهنای خودش سرریز کنند.
4. هر دو سمت تمام مقادیر ثابتِ مقایسه را به شبکه اضافه کنید. در تابع grade، این مقادیر پس از تفریق، 6 و 4 بودند.
5. هر مقسوم‌علیهی را که ممکن است روی پلتفرم هدف به خطا منجر شود در شبکه بیاورید و ثبت کنید کدام معماری شبکه را اجرا کرده است.
6. هر دو پایه را اجرا کنید و پیش از بررسی وضعیت، دلایل شکست‌ها را بخوانید.
7. رکورد اثبات را کنار فایل کاندیدا نگه دارید. بخش evidence_links به خواننده نشان می‌دهد که این ادعا بر پایه‌ی کدام اسناد و شواهد است.

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

آزمایشگاه تعاملی

بخش اول: مدل و اجرا

از داخل پوشه‌ی code، مفسر Python را باز کنید:

cd phases/13-tools-and-protocols/36-rebuild-and-prove-equal/code
python3 -q

این کدها را اجرا کنید:

from main import *
percent_change_model(3, INT_MAX)
percent_change_model(-1, 536870911, "x86_64")
percent_change_model(-1, 536870911, "aarch64")
report = prove_behaviour(PLAUSIBLE)
report.naive_passed, len(report.mismatches), report.mismatches[0]

اولین فراخوانی مقدار -133 را برمی‌گرداند؛ یعنی همان مقدار سرریز‌شده که بر 3 تقسیم شده است. دومی مقدار 'trap' و سومی مقدار -2147483648 را می‌دهد. گزارش نشان می‌دهد که هر ده تست ساده پاس شده‌اند، اما 28 خانه از شبکه‌ی ورودی شکست خورده‌اند. report.oracle_disagreements را با یک لیست خالی مقایسه کنید.

بخش دوم: خواندن فایل آبجکت

obj = ElfObject(ORIGINAL_OBJECT)
grade = obj.function("grade")
grade.size, grade.data[0x26:0x2a].hex(), grade.relocations
read_table(obj, grade.relocations[0], 5, 4)

بایت‌های این فیلد برابر 00000000 هستند. بازنشانی، بخش .rodata را با مقدار الحاقی 0x10 مشخص می‌کند و جدول حاوی مقادیر [1, 2, 3, 4, 4] است.

بخش سوم: دست‌کاری یک مقدار ثابت

report = prove_bytes("grade", CANDIDATES / "grade_case10_wrong.o")
report.masked_equal, report.relocations_match, report.tables_equal, report.reasons()

بایت‌ها انطباق دارند، رکوردها هم‌خوانی دارند، ولی جداول متفاوت‌اند. حالا فایل grade_case10_wrong.c را تغییر دهید تا case 10 دوباره مقدار 4 را برگرداند، سپس با همان دستورات نمونه آن را کامپایل کنید و ببینید که چگونه وضعیت به pass تغییر می‌کند.

بخش چهارم: هدایت rea

اگر rea 6.5.0 و Ghidra 12.1.4 نصب باشند:

GHIDRA_INSTALL_DIR=/opt/homebrew/Cellar/ghidra/12.1.4/libexec \
JAVA_HOME=/opt/homebrew/opt/openjdk@21 \
python3 code/main.py --live

اولین اجرای analyze_function به‌دلیل ایمپورت فایل در Ghidra چند ثانیه طول می‌کشد. شناسه‌های شواهد جدید را با مقادیر ثبت‌شده‌ی قبلی تطبیق دهید. بایت‌های یکسان تحت یک پروفایل تحلیلی مشابه، شناسه‌های یکسانی تولید می‌کنند؛ زیرا شناسه بر پایه‌ی هش محتوا ساخته می‌شود و ربطی به مسیر فایل ندارد.

تمرین عملی

هر دو پایه را برای دو تابع total و grade_label از همان فایل آبجکت پیاده کنید.

نیازمندی‌ها:

• ورودی تابع total یک آرایه و یک متغیر تعداد است. خانه‌هایی برای تعداد 0، تعداد منفی، یک عنصر، و مجموع‌هایی که در 32 بیت سرریز می‌شوند طراحی کنید.
• تابع grade_label، تابع grade را به‌صورت درون‌خطی صدا می‌زند و جدول labels.rel را می‌خواند؛ جدولی با پنج آفست نسبی برای رشته‌ها که هرکدام بازنشانی‌های اختصاصی خود را در بخش .rela.rodata دارند.
• یک ورودی در CLAIMS برای grade_label با دو بازنشانی و یک جدول شامل پنج ورودی 4 بایتی بسازید، و رشته‌هایی را که این ورودی‌ها به آن‌ها اشاره می‌کنند مقایسه کنید.
• در صورت وجود هرگونه اختلاف بین مدل و اجرا، خانه‌های مربوطه را ثبت و بر اساس فهرست دستورالعمل‌ها تبیین کنید.
• به‌ازای هر پایه و هر تابع، یک ادعا به رکورد اثبات اضافه کنید و وضعیت کلی را به‌صورت شکست‌بسته نگه دارید.

معیار موفقیت این است که رکورد نهایی چهار تابع را پوشش دهد، هر ادعا شناسه‌ی شواهد معتبر داشته باشد، و در صورت تغییر حتی یک حرف در رشته‌های برچسب grade_label، تست رد شود.

تمرین امتیازی

پنج پرسش درباره‌ی فایل‌های نمونه‌ی این درس مطرح شده است. پاسخ‌ها را با کدی که توسعه داده‌اید بیابید و درون فایل code/lab_answers.json بنویسید. اعداد را به‌صورت عددی یا رشته‌های هگزادسیمال مانند "0x40"، و لیست‌ها را در قالب لیست‌های JSON ثبت کنید.

1. t1: مقدار percent_change_model(3, 105) در معماری x86_64.
2. t2: مقدار percent_change_model(0, 5) در معماری x86_64.
3. t3: مقدار grade_model(100).
4. t4: تعداد کل خانه‌ها در input_grid().
5. t5: تعداد خانه‌های شبکه که مدل x86_64 در آن‌ها خطای تقسیم می‌دهد.

بررسی صحت پاسخ‌ها:

cd phases/13-tools-and-protocols/36-rebuild-and-prove-equal
python3 code/lab.py

برنامه‌ی ارزیابی، مقادیر مورد انتظار را بر اساس کدهای code/main.py روی فایل‌های نمونه محاسبه می‌کند. این برنامه برای هر بخش وضعیت PASS، FAIL یا TODO را همراه‌با امتیاز چاپ می‌کند، و تنها زمانی کد خروجی 0 می‌دهد که هر پنج مورد تأیید شوند. دستور python3 code/lab.py my-answers.json می‌تواند فایل‌های دیگر را ارزیابی کند. فایل code/tests/test_lab.py نیز تضمین می‌کند که سیستم ارزیابی پاسخ‌های صحیح را بپذیرد و پاسخ غلط را رد کند.

بررسی روند اجرا

نمونه‌ی ارائه‌شده در صفحه‌ی Inside a Decompiler کار خود را با تولید شبه‌کد به پایان می‌برد و آن را در قالب استنباط بایگانی می‌کند: صفحه اثباتی برای آن ارائه نمی‌دهد. مراحلی که در این درس پیاده کردیم، دقیقاً همان گامی است که چنین ادعایی را به یک گزاره‌ی اثبات‌شده تبدیل می‌کند.

مهارت خروجی

حاصل این درس فایل outputs/skill-rebuild-and-prove-equal.md است. از آن برای تبدیل شواهد تابع و کاندیدای بازسازی به یک اثبات دوپایه‌ای و یک رکورد اثبات استفاده کنید. پیش‌نیازهای این مهارت عبارت‌اند از: بررسی فهرست دستورالعمل‌ها پیش از شبه‌کد، ساخت شبکه‌ای با پوشش کامل تمام حالات بحرانی، ماسک‌کردن بازنشانی‌ها همراه‌با ارزیابی مقادیر ثابت، و تجمیع نتایج بر اساس الگوی شکست‌بسته.

اعتبارسنجی

اجرای دمو و مجموعه‌ی تست‌ها:

cd phases/13-tools-and-protocols/36-rebuild-and-prove-equal
python3 code/main.py
python3 -m unittest discover -s code/tests -v

این 35 تست موارد زیر را اثبات می‌کنند:

• تابع c_div() به سمت صفر گرد می‌کند و wrap32() از منطق مکمل دو پیروی می‌کند
• مدل محاسباتی برای ورودی (3, INT_MAX) مقدار -133، برای خانه‌ی خطا در x86-64 مقدار trap، و روی AArch64 مقدار -2147483648 را بازمی‌گرداند
• شبکه‌ی ورودی 92 خانه دارد و تمامی حالات بحرانی را پوشش می‌دهد، درحالی‌که تست‌های ساده از همه‌ی حالت‌های دشوار دوری می‌کنند
• خواننده‌ی ELF هر چهار تابع را با آفست‌ها و اندازه‌های دقیقِ ثبت‌شده پیدا می‌کند
• تابع percent_change دارای 16 بایت بدون بازنشانی است و grade یک بازنشانی از نوع R_X86_64_PC32 در آفست 0x26 دارد
• بایت‌های فیلد بازنشانی برابر صفر هستند و ماسک‌کردن چیزی را در این آبجکت RELA تغییر نمی‌دهد
• هر هشت کاندیدای commitشده به وضعیت مورد انتظار خود می‌رسند و دلایل ثبت‌شده تأیید می‌شوند
• کاندیدای grade_case10_wrong در مرحله‌ی بایت‌های ماسک‌شده تأیید می‌شود و تنها در بررسی مقادیر ثابت رد می‌شود
• اجرای ثبت‌شده‌ی پایه‌ی اول، ده قبولی ساده، 28 مورد عدم تطابق و صفر اختلاف با مدل را نشان می‌دهد
• در صورت وجود کامپایلر، هر دو جفت کاندیدا مجدداً بیلد شده و نتایج یکسانی بازتولید می‌کنند
• اجرای ایجنت، آبجکت مرجع را بر اساس SHA-256 و به‌ترتیب بررسی کرده و شناسه‌های ev_ را برای تمام مراحل Evidence ثبت می‌کند
• خروجی رکورد read_bytes با جدولی که خواننده‌ی ELF پیدا می‌کند مطابقت دارد
• کلاینت سرور ماک را هدایت می‌کند و دقیقاً همان شناسه‌های شواهدِ اجرای واقعی را ثبت می‌کند
• نتایج خطای سرور در گزارش اجرای ایجنت ثبت می‌شوند
• تجمیع نتایج در aggregate() به‌صورت شکست‌بسته انجام می‌شود و شناسه‌ی اثبات بر اساس محتوای آن بازتولید می‌شود

حالت‌های شکست

دستورالعمل اجرایی

کد بازسازی را بر اساس فهرست دستورالعمل‌ها بنویسید و شناسه‌ی رکوردی را که از آن استخراج شده است ثبت کنید. آن را در برابر تابع اصلی با شبکه‌ای از ورودی‌ها اجرا کنید که تمام متغیرهای میانی را سرریز کند و از تمام مرزهای مقایسه‌ی شرطی بگذرد. سپس آن را با پرچم‌های کامپایلر اصلی کامپایل کنید، فیلدهای بازنشانی را ماسک کنید، رکوردهای بازنشانی را بسنجید و مقادیر ثابتی را که به آن‌ها اشاره دارند بخوانید. هر ادعا را با شناسه‌ی شواهد مربوطه‌اش ثبت کنید و اگر ادعایی تأیید نشد، وضعیت آن را در حالت unknown باقی بگذارید.

برای مطالعه‌ی بیشتر

• McKeeman, Differential Testing for Software, Digital Technical Journal 10(1), 1998
• Yang, Chen, Eide, Regehr, Finding and Understanding Bugs in C Compilers, PLDI 2011
• Ramos, Engler, Practical, Low-Effort Equivalence Verification of Real Code, CAV 2011
• Schwartz, Lee, Woo, Brumley, Native x86 Decompilation Using Semantics-Preserving Structural Analysis, USENIX Security 2013
• Liu, Raff, Micinski, When LLM Decompilers Recompile More and Preserve Less, arXiv 2609.05370, 2026
• Gao et al., DecompileBench, Findings of ACL 2025
• Tan et al., LLM4Decompile, arXiv 2403.05286, 2024
• System V gABI, Chapter 4, Relocation
• x86-64 psABI repository, relocation types
• Intel 64 and IA-32 Architectures Software Developer's Manual, Volume 2, IDIV
• Arm Architecture Reference Manual for A-profile, DDI 0487, SDIV
• rea 6.5.0 MCP contracts
• rea 6.5.0 reconstruction obligation ledgers