تفاضل‌گیری باینری و اجرای نمادین: تطابق توابع و حل متغیرهای ورودی

تحلیل باینری و مهندسی معکوس زمانی که با مقایسه‌ی دو بیلد از یک برنامه یا کشف شرایط ورودی توابع سر و کار داریم، بدون ابزار دقیق بسیار گمراه‌کننده خواهد بود. تفاوت‌های ناچیزی مثل تغییر محل قرارگیری داده‌ها پس از بازآرایی (Relocation) می‌تواند ابزارهای ساده را به اشتباه بیندازد تا تصور کنند کد تابع تغییر کرده است، در حالی که منطق برنامه کاملاً دست‌نخورده باقی مانده است. همچنین بررسی دستی یا خواندن سودوکد برای استخراج دامنه‌ی ورودی‌هایی که به یک خروجی خاص منجر می‌شوند، معمولاً به ارائه‌ی تنها یک نمونه‌ی تصادفی به جای تمام ورودی‌های معتبر ختم می‌شود.

این درس به شما نشان می‌دهد چطور الگوریتم‌های تفاضل‌گیری باینری (Binary Diffing) به سبک BinDiff و موتورهای تحلیل اجرای نمادین (Symbolic Execution) را از پایه پیاده‌سازی کنید. با ساخت پنج نوع امضای تابعی و رهگیری محاسبات بازآرایی، یاد می‌گیرید که چطور خطاهای تطابق ابزارهایی مانند Ghidra یا radiff2 را ریشه‌یابی کنید و چرا نسبت‌های شباهت آن‌ها ممکن است متفاوت از آب دربیاید.

در بخش تحلیل نمادین، با مفهوم انفجار مسیر (Path Explosion) و فرمول‌بندی قیود روی یک نمایش میانی (IR) کوچک آشنا می‌شوید. تمام مراحل و محاسبات جست‌وجوی محدود با موتورهای معروفی مثل angr و حل‌کننده‌ی قید z3 اعتبارسنجی می‌شوند تا در نهایت درک شفاف و دقیقی از نحوه‌ی کارکرد این ابزارها در عمل به دست آورید.

تطابق میان دو تابع، ادعایی است که یک امضا (Signature) با کیفیتی مشخص مطرح می‌کند؛ ورودیِ حل‌شده نیز مدلی است از شرایط یک مسیر اجرایی. در این درس هر دو روش را می‌سازیم و نتایج را با radiff2، Ghidra، angr و z3 می‌سنجیم.

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

• ساخت پنج امضا برای توابع با استفاده از فایل شیء (Object file) و فهرست اسمبلی (Listing) آن: بایت‌های دقیق، بایت‌ها با فیلدهای بازآرایی (Relocation) ماسک‌شده، توالی نمادها (Mnemonics)، شکل گراف جریان کنترل (Flow-graph shape) و نام نماد (Symbol).
• اجرای یک الگوریتم تطابق حریصانه‌ی مرحله‌بندی‌شده به سبک BinDiff که در آن یک امضا فقط در صورتی تطابق می‌یابد که در هر دو طرف یکتا باشد؛ همراه با ثبت مرحله و کیفیتِ پشت هر تطابق.
• بازتولید سناریویی که در آن دو تابع با بایت‌های یکسان، در تطابق‌دهنده‌ی بایتی روی ایمیج‌های بارگذاری‌شده رد می‌شوند اما پس از ماسک کردن تأیید می‌شوند، همراه با محاسبات بازآرایی برای توجیه تغییرِ آن 4 بایت.
• بازتولید نسبت‌های شباهت ابزار radiff2 بر پایه‌ی فاصله‌ی لون‌اشتاین (Levenshtein distance) و توضیح این‌که چرا یکی از نسبت‌ها تنها هنگام مقایسه‌ی 82 بایتِ کشف‌شده توسط radare2 به دست می‌آید.
• شمارش مسیرهای یک تابع روی یک نمایش میانی (IR) کوچک، همراه داشتن شرط به ازای هر مسیر، و حل متغیرهای ورودی برای هر برگ از طریق جست‌وجوی محدود (Bounded search).
• اندازه‌گیری انفجار مسیر (Path explosion) روی حلقه‌ای با کران نمادین، و مقایسه‌ی تعداد مسیرها، دسته‌ها و مدل‌ها با نسخه‌های angr 10.0.3 و z3 5.1.0.

صورت مسئله

کد ledger.c را با بهینه‌سازی -O2 دوباره کامپایل کرده‌اید و از یک ایجنت می‌پرسید آیا نسبت به بیلد -O1 تغییری رخ داده است یا نه. ایجنت ابزار مقایسه‌گر (Differ) را اجرا می‌کند و گزارش می‌دهد که تابع grade دستکاری شده، چرا که بایت‌های آن در دو برنامه‌ی بارگذاری‌شده در حافظه متفاوت است. سپس کل بودجه‌اش را صرف توضیح تغییری می‌کند که در واقعیت اصلاً رخ نداده است. 46 بایتِ تابع grade در هر دو فایل شیء کاملاً یکسان هستند. مقایسه‌گر، ایمیج‌ها را بعد از اعمال بازآرایی مقایسه کرده بود؛ از آنجا که بخش .rodata در برنامه‌ی -O2 به اندازه‌ی 0x70 بایت جلوتر قرار گرفته، یکی از جابه‌جایی‌های (Displacements) درون grade نیز 0x70 بایت افزایش یافته است.

همان روز عصر می‌پرسید چه نمره‌ای باعث می‌شود grade مقدار 4 را برگرداند. ایجنت سودوکد را می‌خواند و جواب می‌دهد: «90». این فقط یک جواب ممکن است. این تابع به ازای هر نمره‌ای از 90 تا 109 عدد 4 را برمی‌گرداند؛ از آنجا که سؤالتان کرانی نداشت، پاسخ ایجنت تنها یک نمونه از مجموعه‌ای بود که به آن نیاز داشتید.

هر دو شکست ریشه در یک خلاء دارند. تطابق یا ورودیِ حل‌شده، هر کدام ادعایی هستند که روشی پشت آن‌ها قرار دارد. در این درس، این دو روش را با کتابخانه‌ی استاندارد Python می‌سازیم و ابزارهای محیط عملیاتی را در کنارشان اجرا می‌کنیم. هر جا ابزارها با کد هم‌نظر باشند، دو استنتاج مستقل در دست دارید؛ هر جا اختلاف داشته باشند، یک آدرس، یک بایت، یا یک کران مشخص برای بررسی دقیق‌تر در اختیارتان خواهد بود.

امضای تابع: ادعایی با یک کیفیت مشخص

فلیک (Flake) در سال 2004 تفاضل‌گیری باینری (Binary diffing) را به صورت ساخت یک یکریختی (Isomorphism) میان مجموعه‌ی توابع دو فایل اجراییِ مشابه صورت‌بندی کرد. دولین (Dullien) و رولز (Rolles) در سال 2005 این مفهوم را به بلوک‌های پایه (Basic blocks) و دستورالعمل‌ها بسط دادند. صفحه‌ی مفاهیم BinDiff استراتژی برآمده از این پژوهش‌ها را شرح می‌دهد: برای هر تابع در هر دو فایل یک ویژگی را محاسبه کنید. مقداری که در هر طرف دقیقاً یک بار دیده شود یک تطابق است. مقداری که بیش از یک بار ظاهر شود مبهم است و در رده‌ی هم‌ارزیِ مربوطه با ویژگی بعدی بررسی عمیق‌تری روی آن صورت می‌گیرد. مقداری که در طرف مقابل همتایی نداشته باشد بدون تطابق می‌ماند. پس از هر دور، فراخواننده‌ها و فراخوانده‌شده‌های تطابق‌های جدید، مجموعه‌های کوچکی می‌سازند که در آن‌ها ویژگی بعدی به احتمال زیاد یکتا خواهد بود؛ این فرآیند با ویژگی بعدی تکرار می‌شود.

هر الگوریتم تطابق، کیفیتی به همراه دارد. مستندات BinDiff تطابق هش بایت‌های خام تابع و تطابق هش نام را «بسیار خوب» (Very good)، شاخص MD گراف جریان کنترل و تطابق امضای اعداد اول (هر نماد یک عدد اول کوچک، و حاصل‌ضرب آن‌ها در کل تابع) را «خوب» (Good)، ارجاعات رشته‌ای را «متوسط» (Medium)، و تعداد حلقه‌ها یا توالی آدرس‌ها را «ضعیف» (Poor) ارزیابی می‌کند. میزان اطمینان (Confidence) به یک تطابق، میانگین کیفیت الگوریتم‌های سازنده‌ی آن است که با یک تابع سیگموئید وزن‌دهی می‌شود. شباهت توابع تقریباً از 25٪ یال‌های منطبق گراف جریان کنترل، 15٪ بلوک‌های پایه‌ی منطبق، 10٪ دستورالعمل‌های منطبق، و 50٪ اختلاف در شاخص MD گراف جریان کنترل تشکیل می‌شود که همگی در ضریب اطمینان ضرب می‌شوند.

این درس پنج مورد از این ویژگی‌ها و همان یک قانون حیاتی را نگه می‌دارد: یکتا در هر دو طرف، یا بدون تطابق. از شاخص MD صرف‌نظر می‌کنیم، چون صفحه‌ی مفاهیم بدون ارائه‌ی فرمول از آن نام برده است، و به جای آن از توالی ساده‌ی درجات گره‌ها (Degree sequence) استفاده می‌کنیم. برچسب‌های کیفیت باقی می‌مانند، زیرا اعتبار هر تطابق دقیقاً به اندازه‌ی ضعیف‌ترین داده‌ای است که آن را ساخته است.

پنج امضا از رکورد یک تابع

مقایسه‌گر ما به ازای هر فایل شیء، دو چیز را می‌خواند. فایل ELF بایت‌ها، اندازه‌ی نمادها و رکوردهای .rela.* را به دست می‌دهد. فهرست خروجی llvm-objdump -d مرز دستورالعمل‌ها و نمادها را مشخص می‌کند؛ درس 33 ثابت کرد که رمزگشایی (Decode) روی تک‌تک دستورالعمل‌های این فایل‌ها با این فهرست کاملاً برابری می‌کند. تابع function_record() بررسی می‌کند که بایت‌های هر دستورالعملِ فهرست‌شده دقیقاً برابر با بایت‌های فایل شیء در همان آدرس باشد و در غیر این صورت استثنا صادر می‌کند. فهرست قدیمی به معنای تغییر داده‌های آزمون (Fixture) است.

تابع grade را در فایل ledger-x86_64-O1.o در نظر بگیرید. نماد آن نشان‌دهنده‌ی آفست 0x10 و اندازه‌ی 46 بایت است؛ بنابراین رکورد بازه‌ی 0x10 تا 0x3e را پوشش می‌دهد و دستور دو بایتی nop را که تابع بعدی را تراز می‌کند، کنار می‌گذارد.

امضای بایت‌های دقیق (Exact-bytes signature)، هش SHA-256 این 46 بایت است. امضای بایت‌های ماسک‌شده (Masked-bytes signature) ابتدا تمام فیلدهای بازآرایی را صفر می‌کند. در اینجا یک فیلد وجود دارد: رکورد R_X86_64_PC32 .rodata+0x10 در آفست 0x36 به طول 4 بایت، که مقدار جابه‌جایی دستور leaq (%rip), %rcx در آدرس 0x33 است. در یک فایل شیء با فرمت RELA، این چهار بایت از قبل مقدار صفر دارند؛ بنابراین این دو امضا در تمام توابعِ تمام فایل‌های شیءِ اینجا کاملاً یکسان هستند. ماسک کردن برای بخش بعدی کاربرد دارد.

امضای نمادها، توالی 14 نماد را هش می‌کند:

movslq imulq movq sarq shrq addl addl xorl cmpl ja movl leaq movl retq

امضای شکل گراف جریان کنترل، از بلوک‌های پایه و یال‌های نوع‌دار درس 33 به دست می‌آید که به بلوک‌های در دسترس از نقطه‌ی ورود محدود شده است. تابع grade در سطح -O1 سه بلوک و سه یال دارد. بلوک 0x10 به دستور ja 0x3d با یک یال انشعاب‌یافته (Taken) و یک یال مستقیم (Fallthrough) ختم می‌شود؛ بلوک 0x31 به 0x3d سرریز می‌کند و 0x3d بازمی‌گردد. توالی درجات، جفت‌های (ورودی، خروجی) را برای هر بلوک به صورت مرتب‌شده فهرست می‌کند؛ بنابراین امضا به شکل 3b 3e [0/2,1/1,2/0] خوانده می‌شود. برای grade در سطح -O0، رکورد مربوطه پرش غیرمستقیم را از طریق پنج ورودی .rela.rodata دقیقاً مثل درس 33 حل می‌کند، که نتیجه‌اش هشت بلوک و یازده یال با چهار یال جدول (table) است.

امضای نام، همان نام نماد است. در صورت وجود، محکم‌ترین فکت است و اگر بیلد استریپ (Strip) شده باشد، هیچ ارزشی ندارد.

یک فیلد دیگر نیز برای حالت بررسی تکه (Patch) در ادامه همراه داده‌ها ذخیره می‌شود. زمانی که تابعی دارای یک بازآرایی lea به داخل .rodata، یک بررسی کران، و یک بارگذاری نمایه‌دار (Indexed load) باشد، تابع referenced_table() جدول را به همان شیوه‌ی درس 36 می‌خواند: دستور cmpl $0x4 پیش از ja نشان‌دهنده‌ی پنج ورودی است و بارگذاری movl (%rcx,%rax,4), %eax طول هر ورودی را 4 بایت تعیین می‌کند. برای grade در سطح -O1، این جدول در آدرس .rodata+0x14 به صورت 1, 2, 3, 4, 4 خوانده می‌شود.

تطابق‌دهنده‌ی حریصانه

تابع match_functions() مراحل را به ترتیب اجرا می‌کند. برای هر مرحله، توابعی از هر دو طرف را که هنوز تطابق نیافته‌اند بر اساس امضای آن مرحله گروه‌بندی می‌کند و هر مقداری را که دقیقاً یک تابع در هر طرف دارد می‌پذیرد. رکورد تطابق، مرحله، کیفیت آن مرحله، سایر امضاهای موافق، و نسبت شباهت را ثبت می‌کند.

for stage in order:
    for signature, candidates in left_groups.items():
        partners = right_groups.get(signature, [])
        if len(candidates) != 1 or len(partners) != 1:
            continue
        a, b = candidates[0], partners[0]
        agreeing = [s.id for s in STAGES if a.signatures()[s.id] == b.signatures()[s.id]]
        matches.append(Match(a, b, stage, agreeing, radare2_ratio(a.raw, b.raw), data_equal))

ترتیب مراحل در این درس ابتدا چهار مرحله‌ی ساختاری و در پایان نام‌ها است؛ به این ترتیب مراحل ساختاری سنجیده می‌شوند و نام‌ها در ادامه به آن‌ها نمره می‌دهند. برای مقایسه‌ی -O1 با -O2:

تابع total از 31 بایت و 13 دستورالعمل به 140 بایت و 41 دستورالعمل رشد کرد، چون clang حلقه‌ی آن را با SSE2 برداری کرد و یک حلقه‌ی باقی‌مانده‌ی اسکالر را نیز نگه داشت. شکل گراف آن از پنج بلوک و پنج یال به ده بلوک و سیزده یال تغییر یافت. هیچ ساختاری باقی نمانده و فقط نماد این دو را به هم پیوند می‌دهد.

برای مقایسه‌ی -O0 با -O1، همین ترتیب یک تطابق اشتباه ایجاد می‌کند:

تابع percent_change در سطح -O0 یک لوزیِ چهاربلوکی است: یک ورودی که بر اساس before == 0 شاخه می‌زند، دو بازو، و یک نقطه‌ی پیوند که مقدار را برمی‌گرداند. توالی درجات آن 0/2, 1/1, 1/1, 2/0 است. تابع grade_label در سطح -O1 کدِ grade را درون‌خطی (Inline) کرده و همان لوزی را حول بررسی کران دارد. شکل گراف در هر دو طرف یکتا است و قانون ما آن را می‌پذیرد. برچسب کیفیت «متوسط» نقش هشدار را دارد، و مرحله‌ی بررسی نام که پس از آن اجرا می‌شود این تطابق را نقض می‌کند. این تطابق کاذب همچنین grade_label را در سمت راست مصرف می‌کند؛ در نتیجه جفت‌های واقعی percent_change و grade_label بدون تطابق باقی می‌مانند.

ترتیب BinDiff، در صورت وجود نام‌های واقعی، تطابق نام را به عنوان مرحله‌ی دوم اجرا می‌کند و متغیر BINDIFF_ORDER در کد نیز همین کار را انجام می‌دهد. با این ترتیب، هر چهار تابع در -O0 بر اساس نام با نسخه‌های -O1 خود تطابق می‌یابند، یعنی همان نتیجه‌ای که Ghidra در ادامه گزارش می‌دهد. در این درس هر دو ترتیب در کد دمو نگه داشته شده‌اند تا شکست به‌وضوح دیده شود. شکل گراف جریان کنترلِ چهارگرهی، شکلِ مشترک تمام دستورات if و else است که پیش از خروج از تابع به هم می‌رسند.

بایت‌های یکسان، عملوند بازآرایی‌شده

نرم‌افزار Ghidra هنگام وارد کردن (Import) یک فایل شیء، بازآرایی‌ها را اعمال می‌کند. بنابراین تطابق‌دهنده‌ی بایتی آن ایمیج‌های بارگذاری‌شده را مقایسه می‌کند، و دلیل ماسک کردن فیلدهای بازآرایی در درس 36 نیز همین بود. تابع load_image() فرآیند وارد کردن را بازتولید می‌کند. این تابع بخش‌های تخصیص‌یافته را به ترتیبِ هدر پیمایش کرده، هر کدام را بر اساس sh_addralign تراز می‌کند و آن‌ها را از آدرس 0x100000 می‌چیند. سپس تک‌تک رکوردها را اعمال می‌کند: مقدار S + A - P به عنوان یک مقدار 32 بیتی علامت‌دار برای R_X86_64_PC32 و R_X86_64_PLT32، و S + A به صورت 64 بیتی برای R_X86_64_64.

این چیدمان با Ghidra 12.1.4 در نقطه‌ی شروع تک‌تک بخش‌ها در هر دو برنامه کاملاً مطابقت دارد؛ مجموعه‌ی تست‌ها این موضوع را در برابر خروجی ثبت‌شده‌ی Version Tracking ارزیابی می‌کند:

بخش .text در سطح -O2 به اندازه‌ی 112 بایت طولانی‌تر است که ناشی از رشد تابع total است؛ در نتیجه .rodata به اندازه‌ی 0x70 بایت جلوتر شروع می‌شود. تابع grade در هر دو برنامه در آدرس 0x100010 قرار دارد. فیلد جابه‌جایی دستور leaq آن در آفست 0x33 در آدرس 0x36 قرار گرفته و در 0x3a به پایان می‌رسد. مقدار افزودنیِ بازآرایی (Addend) که 0x10 است به‌علاوه‌ی 4 بایت معمول، جدول را در .rodata+0x14 قرار می‌دهد.

در ایمیج بیلد -O1: مقدار جابه‌جایی برابر است با 0x1000a0 + 0x14 - 0x10003a = 0x7a = 122. در ایمیج بیلد -O2: مقدار برابر است با 0x100110 + 0x14 - 0x10003a = 0xea = 234. بایت‌های این فیلد در یکی 7a 00 00 00 و در دیگری ea 00 00 00 هستند. یک بایت از 46 بایت متفاوت است، نسبت لون‌اشتاین 0.978 می‌شود، و مرحله‌ی تطابق بایت‌های دقیق شکست می‌خورد. مرحله‌ی بایت‌های ماسک‌شده این فیلد را صفر می‌کند و قبول می‌شود. تابع grade_label دقیقاً به همان اندازه‌ی 0x70 بایت همراه با جدول خود جابه‌جا شده است؛ بنابراین جابه‌جایی‌های آن مساوی مانده و در هر دو نما بر اساس بایت‌های دقیق مطابقت می‌یابد.

ابزار Ghidra نیز همین تفکیک را گزارش می‌دهد. در مقایسه‌ی -O1 با -O2، تطابق‌دهنده‌ی Exact Function Bytes Match توابع percent_change و grade_label را پیدا کرد، Exact Function Instructions Match این دو را به‌علاوه‌ی grade پیدا کرد، و Exact Function Mnemonics Match دقیقاً همان سه تابع را یافت. تطابق‌دهنده‌ی دستورالعمل‌ها عملوندها را ماسک می‌کند که مقدار جابه‌جایی را هم پوشش می‌دهد. نمای ایمیجِ این درس دقیقاً برای همان دو تابعی تطابق بایت دقیق می‌دهد که تطابق‌دهنده‌ی بایتی Ghidra پیدا کرده بود، و تطابق بایت‌های ماسک‌شده دقیقاً برای همان سه تابعی ثبت می‌شود که تطابق‌دهنده‌ی دستورالعمل Ghidra یافته بود. مجموعه‌ی تست‌ها برابری هر دوی این موارد را اثبات می‌کند.

متد compare_functions در rea 6.5.0 تفاوت‌های متنی خروجی ارائه‌دهنده را خط‌به‌خط بررسی می‌کند. در بُعد اسمبلی، این محدودیت را قید کرده است: «نرمال‌سازی بازآرایی‌ها در دسترس نیست». لودر و سیستم ماسک کردن در این درس، همان نرمال‌سازی را انجام می‌دهند.

متغیرهای اندازه‌گیری radiff2

ابزار radare2 6.2.4 همراه با radiff2 عرضه می‌شود. با آرگومان -AC هر دو فایل را تحلیل می‌کند و به ازای هر تابع یک ردیف چاپ می‌کند: اندازه و آدرس فایل سمت چپ، MATCH یا UNMATCH، نسبت شباهت، و اندازه و آدرس فایل سمت راست. ردیف‌های ثبت‌شده برای فایل‌های ما:

نسبت شباهت در سورس‌کد radare2 فرمول 1 - distance / max(len_a, len_b) است که در آن distance فاصله‌ی لون‌اشتاین بین اثر انگشت (Fingerprint) دو تابع است؛ اثر انگشت نیز از الحاق بلوک‌های پایه‌ی تابع به ترتیب آدرس به دست می‌آید. آستانه‌ی تطابق 0.7 است. تابع radare2_ratio() در فایل code/main.py همین فرمول را روی بایت‌های خام تابع پیاده‌سازی می‌کند و مقادیر 0.130435، 0.106061، 0.269841 و 0.171429 را تا شش رقم اعشار بازتولید می‌کند.

اما این فرمول عدد 0.426829 را برای تابع grade در بیلد -O0 بازتولید نمی‌کند. این نسبت روی کل 118 بایت تابع برابر با 0.296610 است. جالب اینجاست که radare2 در ستون اندازه عدد 118 را چاپ می‌کند، اما اثر انگشت آن کوتاه‌تر است. بدون اعمال بازآرایی‌ها، این ابزار نمی‌تواند جدول پرش را حل کند؛ بنابراین تحلیل آن فقط به بلوک ورودی، بلوکی که به jmpq *%rax ختم می‌شود، حالت پیش‌فرض، و دستور خروج می‌رسد: یعنی 82 بایت، دقیقاً همان 82 بایتی که الگوریتم ساده‌ی بازگشتی به پایین (Recursive descent) در درس 33 مدعی آن بود. فاصله‌ی لون‌اشتاین میان این 82 بایت و 46 بایت در -O1 برابر 47 است و 1 - 47/82 = 0.426829. با فلگ -e bin.relocs.apply=true، نرم‌افزار radare2 تمام 118 بایت را شناسایی کرده و عدد 0.288136 را چاپ می‌کند؛ این عدد برابر با نسبت شباهت کد ما روی ایمیج‌های بازآرایی‌شده است، جایی که چهار بایت جابه‌جایی با فیلدهای صفر فایل شیء تفاوت دارند. دو ابزار تنها زمانی هم‌نظر می‌شوند که بایت‌های یکسانی را مقایسه کنند، و ستون اندازه نشان نمی‌دهد چه بایت‌هایی واقعاً وارد پردازش شده‌اند.

گزینه‌ی -O اثر انگشت را به بایت‌های آپکد (Opcode) محدود می‌کند و عملوندها را صفر در نظر می‌گیرد. با این کار، نسبت‌های -O0 در برابر -O1 به 0.239130، 0.512195، 0.303030 و 0.523810 افزایش می‌یابند، و نسبت total در مقایسه‌ی -O1 با -O2 به 0.192857 می‌رسد. فواصل در سطح کل فایل نیز وجود دارند: آرگومان -s (روش مایرز / Myers) شباهت 0.956 و فاصله‌ی 162 را بین دو فایل شیء گزارش می‌کند، و -ss (لون‌اشتاین) شباهت 0.927 و فاصله‌ی 137 را نشان می‌دهد. این اعداد شامل هدرها، جداول نمادها و بخش‌های بازآرایی نیز می‌شوند و هیچ اطلاعی درباره‌ی توابع به ما نمی‌دهند.

تطابق‌دهنده‌های Ghidra Version Tracking

ابزار Version Tracking در Ghidra، برنامه‌ی مبدأ را با تطابق‌دهنده‌ها (Correlators) به برنامه‌ی مقصد جفت می‌کند. تطابق‌دهنده‌های توابع عبارت‌اند از: Exact Function Bytes Match، Exact Function Instructions Match (با ماسک کردن عملوندها)، Exact Function Mnemonics Match، و Duplicate Function Instructions Match (برای حالت‌های 1 به N و N به M). تطابق‌دهنده‌های داده شامل Exact، Duplicate و Similar Data Match هستند. تطابق‌دهنده‌های نماد، نام‌ها را به صورت دقیق، تکراری یا بر اساس شباهت مقایسه می‌کنند. تطابق‌دهنده‌های ارجاع (Reference correlators) با استفاده از تطابق‌های پذیرفته‌شده به دنبال موارد بیشتر می‌گردند. توابع باید در برنامه‌ی مقصد تعریف شده باشند، و پیش‌فرض حداقل طول تابع 10 بایت است. قابلیت Auto Version Tracking به ترتیب Exact Symbol Name، Exact Data، Exact Function Bytes، Exact Function Instructions، Exact Function Mnemonics، Duplicate Function Instructions، و سپس تطابق‌دهنده‌ی ارجاع را اجرا می‌کند و برای موارد تأییدشده تطابق‌های ضمنی می‌سازد. از نسخه‌ی 11.2 یک تطابق‌دهنده‌ی BSim نیز اضافه شده است.

نتایج این تطابق‌دهنده‌ها در این درس به صورت بدون واسط گرافیکی (Headless) استخراج شده‌اند. اسکریپت capture_ghidra_vt.sh سه فایل شیء را به یک پروژه وارد کرده و ListVersionTrackingMatches.java را اجرا می‌کند؛ این اسکریپت کوتاه که کلاس AbstractGhidraVersionTrackingScript را گسترش می‌دهد، برنامه‌های مبدأ و مقصد را با مسیر باز می‌کند، شش تطابق‌دهنده‌ی غیرارجاعی را به ترتیب Auto Version Tracking اجرا می‌کند و به ازای هر بلوک، تابع، تطابق‌دهنده و تطابق، یک خط چاپ می‌کند. تمام اعداد این بخش از همین دو فایل متنی استخراج شده‌اند.

بین بیلد -O0 و -O1 تمام توابع تغییر کرده بودند، بنابراین فقط نام‌ها تطابق یافتند؛ یعنی همان نتیجه‌ای که الگوریتم ما با ترتیب BinDiff به دست می‌آورد. به ازای هر تطابق، شباهت 1.000 و ضریب اطمینان 10.000 چاپ شد. در راهنمای برنامه، تطابق‌دهنده‌های دقیق با شباهت 1.0 و اطمینان 1.0 توصیف شده‌اند؛ مقیاس ضریب اطمینان چاپ‌شده سؤالی باز است که این درس آن را ثبت می‌کند و پاسخی به آن نمی‌دهد.

ابزار Program Differences در منوی Tools مقوله‌ی متفاوتی است. این ابزار دو برنامه با فضای آدرس یکسان را بر اساس بایت‌ها، برچسب‌ها، واحدهای کد، ارجاعات، کامنت‌ها و توابع در آدرس‌های برابر مقایسه می‌کند. این مقایسه وابسته به تراز بودن آدرس‌ها است و هر آنچه جابه‌جا شده باشد را نادیده می‌گیرد.

نرم‌افزارهای Diaphora و Binary Ninja از نگاه مستنداتشان

ابزار Diaphora یک افزونه‌ی IDA Pro است که نخستین بار در سال 2015 منتشر شد و تا تاریخ 18-08-2026 به نسخه‌ی 3.4.2 رسیده است. این ابزار از نسخه‌ی 2.0 تحت مجوز AGPL-3.0 منتشر شده و به IDAPython نیاز دارد؛ بنابراین در نسخه‌های IDA Home یا IDA Pro کار می‌کند و روی IDA Free قابل اجرا نیست. این افزونه هر پایگاه داده را به SQLite خروجی می‌گیرد و هیوریستیک‌های خود را در قالب کوئری‌های SQL اجرا می‌کند. هر هیوریستیک دارای نام، دسته‌بندیِ Best، Partial، یا Unreliable، نوع نسبت شباهت، و پرچم‌های اختیاری مانند SAME_CPU یا SLOW است. نام این الگوریتم‌ها در سورس‌کد فعلی شباهت زیادی به مراحل این درس دارد، اما با تنوع بیشتر: هش بایت‌ها، آدرس و نمادهای یکسان، اسمبلیِ پاک‌سازی‌شده‌ی یکسان، حاصل‌ضرب اعداد اول برای نمادها، گره‌ها، یال‌ها، حلقه‌ها و مؤلفه‌های قویاً همبندِ یکسان، هش مرتب‌سازی توپولوژیک (Topological sort)، و هش‌های فازی سودوکد که به دکامپایلر Hex-Rays وابسته‌اند. یادداشت‌های انتشار آن تاریخچه‌ی تنظیم دقیق را نشان می‌دهد: هیوریستیک‌های کند فقط برای کمتر از حدود 2,000 تابع اجرا می‌شوند، و «Same graph» به دسته‌ی نامطمئن (Unreliable) منتقل شده است. این تغییر وضعیت، دقیقاً حاصل دیدن مشکل لوزیِ چهارگرهی این درس در مقیاس‌های بزرگ است.

نرم‌افزار Binary Ninja 6.0 که در تاریخ 03-09-2026 منتشر شد، قابلیت Binary Similarity را به عنوان یک فریم‌ورک همراه با ارائه‌دهنده‌ها (Providers) و حل‌کننده‌ها (Resolvers) اضافه کرد. این نرم‌افزار BinDiff را به عنوان ارائه‌دهنده‌ی ساختاری و WARP را برای تطابق دقیق توابع با عملوندهای بازآرایی‌پذیر عرضه می‌کند. راهنمای آن توصیه می‌کند زمانی که توابع صرف‌نظر از دستورالعمل‌های بازآرایی‌پذیر با هم منطبق هستند از WARP استفاده شود، و هنگامی که پس از کامپایل مجدد شباهت‌های ساختاری حفظ شده‌اند از BinDiff استفاده کنید. این ویژگی منحصراً در نسخه‌ی Ultimate وجود دارد. ابزار Binary Ninja در اینجا روش نصبی از طریق مدیر بسته (Package manager) نداشت و اجرا نشد؛ بنابراین این پاراگراف صرفاً از مستندات رسمی آن نقل شده است.

پروژه‌ی BinDiff از تاریخ 25-09-2023 تحت مجوز Apache-2.0 متن‌باز شده و آخرین نسخه‌ی آن v8 است. این ابزار به یک دیس‌اسمبلر و افزونه‌ی BinExport نیاز دارد که از IDA Pro 9.4 به بعد، Binary Ninja و Ghidra پشتیبانی می‌کند. مسیر رایگان برای یک یادگیرنده، ترکیب Ghidra به‌علاوه‌ی BinExport و ابزار خط فرمانی BinDiff است. ما در این درس آن را اجرا نکردیم و تمرین عملی از شما می‌خواهد این کار را انجام دهید.

کد یکسان، ثابت متفاوت

در درس 36 یک بیلد کاندید بازسازی‌شده از grade داشتیم که آخرین ورودی جدول آن به جای 4 برابر 3 بود. فایل grade_case10_wrong.o همان 46 بایت کد تابع grade در سطح -O1 را دارد. تطابق‌دهنده‌ی ما این دو را به دلیل تطابق کامل بایت‌ها و هم‌نظری تمام امضاها جفت می‌کند. اما بررسی جدول ارجاع‌شده، از طریق یک بازآرایی مقادیر 1, 2, 3, 4, 4 و از طریق دیگری 1, 2, 3, 4, 3 را می‌خواند و dataEqual: false را گزارش می‌دهد. سه تابع دیگر بیلد -O1 در سمت چپ بدون تطابق باقی می‌مانند، چون فایل شیء کاندید تنها شامل یک تابع است.

این همان الگوی تحلیل تکه (Patch) است. اگر یک مقایسه‌گرِ تابع فقط روی بایت‌ها متوقف شود، می‌گوید هیچ تغییری رخ نداده است. تطابق Exact Data Match در Ghidra و تطابق ارجاعات رشته‌ای در BinDiff به همین دلیل طراحی شده‌اند. پیاده‌سازی این درس نسخه‌ی جمع‌وجوری از آن است: به ازای هر جفت منطبق، بایت‌هایی را که بازآرایی‌های هر تابع به آن‌ها اشاره دارند مقایسه کنید؛ تعداد ورودی‌ها از بررسی کران و عرض هر کدام از دستور بارگذاری استخراج می‌شود.

اجرای نمادین: مسیرها، شرط‌ها، حل‌کننده‌ها

کینگ (King) در سال 1976 اجرای نمادین (Symbolic execution) را شرح داد. ورودی‌ها به نماد تبدیل می‌شوند. هر دستور، یک حافظه‌ی نمادین را به‌روزرسانی می‌کند. هر انشعاب، شرطی به مسیر می‌افزاید، و یک حل‌کننده (Solver) تصمیم می‌گیرد که آیا مسیر شدنی است یا خیر، و ورودی مشخصی برای طی آن تولید می‌کند. تابعی با چندین انشعاب به درختی از مسیرها تبدیل می‌شود و هر برگ نشان‌دهنده‌ی یک خروج (Return) همراه با شرطی مشخص است.

بالدونی (Baldoni)، کوپا (Coppa)، دلیا (D'Elia)، دمتریسکو (Demetrescu) و فینوکی (Finocchi) در سال 2018 مرور جامعی بر این حوزه ارائه دادند. در بخش 5 مقاله‌شان، انفجار مسیر به عنوان هزینه‌ی اصلی معرفی شده است: موتور اجرا ممکن است در هر انشعاب fork کند، بنابراین تعداد وضعیت‌ها می‌تواند به صورت نمایی بر اساس تعداد انشعاب‌ها رشد کند؛ همچنین حلقه‌ای که کران آن وابسته به ورودیِ نمادین باشد، مجموعه‌ای نامحدود از مسیرها ایجاد می‌کند. راهکارهایی که برمی‌شمارند عبارت‌اند از: هرس کردن مسیرهای غیرقابل تحقق با حل شرط‌ها در هر انشعاب، خلاصه‌سازی توابع و حلقه‌ها، ادغام وضعیت‌ها، و تقریبِ کمتر از واقعیت (Under-approximation). در اجرای هم‌زمان نمادین و عینی (Concolic execution)، برنامه به طور هم‌زمان به شکل عینی و نمادین اجرا می‌شود، شرایط در طول اجرای عینی ثبت می‌گردد، یکی از شرط‌ها نقیض می‌شود و از حل‌کننده خواسته می‌شود ورودی بعدی را تولید کند. سیستم‌های DART (سال 2005)، CUTE (سال 2005) و SAGE (سال 2008) نمونه‌های شاخص این رویکرد هستند.

سیستم KLEE (توسعه‌داده‌شده توسط Cadar، Dunbar و Engler در OSDI 2008) یک ماشین مجازی نمادین روی بایت‌کد LLVM است؛ ورودی آن خروجی clang -emit-llvm است نه فایل باینری. این سیستم دارای مدلی از محیط POSIX و کتابخانه‌ای برای بازپخش (Replay) است. روی 89 ابزار موجود در GNU coreutils، این ابزار به 84.5٪ پوشش خطوط در مقایسه با 67.7٪ آزمون‌های خود توسعه‌دهندگان دست یافت و 56 باگ جدی کشف کرد. نسخه‌ی KLEE 3.2 در تاریخ 23-12-2025 تحت مجوز NCSA منتشر شد و نسخه‌ی توصیه‌شده‌ی آن LLVM 16 است.

فریم‌ورک angr مستقیماً روی فایل‌های باینری کار می‌کند. بخش angr.Project شامل لودر CLE (برای نگاشت فایل شیء و اعمال بازآرایی‌ها)، یک لیفتر (Lifter) که بلوک را به VEX IR (block.vex) یا به عنوان جایگزین به pypcode تبدیل می‌کند، و کارخانه‌ای برای ساخت وضعیت‌ها است. یک SimState شامل رجیسترها، حافظه و یک حل‌کننده است. بخش SimulationManager استش‌های (Stashes) وضعیت‌ها را با نام‌های active، deadended، found، avoided و errored گام‌به‌گام پیش می‌برد و متد explore(find=..., avoid=...) آن را می‌پوشاند. در هر گام، موتورها به این ترتیب اجرا می‌شوند: failure، syscall، hook، unicorn برای داده‌های عینی، و VEX به عنوان گزینه‌ی نهایی. رابط claripy فرانت‌اندِ حل‌کننده روی Z3 است که در angr 10.0 به عنوان یک پیاده‌سازی مستقل Rust تعبیه شده و با from angr import claripy ایمپورت می‌شود. نسخه‌ی angr 10.0.3 در تاریخ 10-10-2026 تحت مجوز BSD-2-Clause آپلود شد و به Python 3.12 یا بالاتر نیاز دارد. Z3 5.1.0 که در 16-08-2026 با مجوز MIT منتشر شد، حل‌کننده‌ی پشت angr، Triton و بک‌اندِ اختیاری KLEE است.

یک موتور اجرای نمادین کوچک روی نمایش میانیِ درس 34

موتور اجرای نمادین در code/main.py از یک نمایش میانی (IR) ساده با ساختار عبارت‌های درس 34 بهره می‌برد: Assign، Branch، Jump، Return و پایان‌دهنده‌ی Switch که در تمرین عملی درس 34 درخواست شده بود. عبارت‌ها شامل Const، Var، Bin با یک عرض، Cast، دستور Load از یک جدول مشخص عینی، و Not هستند. چهار تابع آزمایشی به صورت دستی در سطحی معادل خروجی بهینه‌سازی‌شده‌ی درس 34 بازنویسی شده‌اند؛ جایی که ضرب در 0x66666667 به score / 10 تبدیل شده و هر بلوک IR آدرس دستورالعمل‌های منشأ خود را فهرست می‌کند. تابع check_ir_against_listing() بررسی می‌کند که آدرس‌ها تک‌تک دستورالعمل‌های فهرست اسمبلی تابع را دقیقاً یک بار پوشش داده باشند.

کد grade در سطح -O0 در این ساختار IR:

0x30: local_8 = score; local_10 = score / 10 - 6; if (local_10 >u 4) goto 0x9a else 0x62
0x62: switch local_10 -> 0x91, 0x88, 0x7f, 0x76, 0x76
0x76: local_4 = 4; goto 0xa1        0x7f: local_4 = 3; goto 0xa1
0x88: local_4 = 2; goto 0xa1        0x91: local_4 = 1; goto 0xa1
0x9a: local_4 = 0                    0xa1: return local_4

مقصدهای سوییچ از خروجی jump_table_targets() استخراج می‌شوند، یعنی با همان محاسبات بازآرایی درس 33؛ بنابراین IR داده‌های آزمایشی را می‌خواند.

تابع execute() یک لیست کار (Worklist) از وضعیت‌های مسیر نگه می‌دارد. هر وضعیت شامل بلوک جاری، ردپای بلوک‌ها، فهرست شرط‌ها و محیطی است که هر متغیر را به عبارتی بر حسب ورودی‌ها نگاشت می‌دهد. دستور Assign متغیرهای محیط را در مبدأ جایگزین کرده و نتیجه را ذخیره می‌کند. دستور Branch متغیرها را در شرط جایگزین می‌کند و دو بار از حل‌کننده استعلام می‌گیرد: یک بار با اضافه‌کردن شرط، و یک بار با نقیض آن. هر شاخه‌ای که حل‌کننده نتواند آن را ارضا کند کنار گذاشته می‌شود؛ این همان هرس حریصانه‌ای است که در مقاله‌ی مروری به آن اشاره شد. دستور Switch ورودی‌های جدول را بر اساس مقصد دسته‌بندی می‌کند و به ازای هر مقصدِ متمایز با فصل (Disjunction) تساوی‌های ورودی‌ها یک fork انجام می‌دهد؛ این رفتاری است که angr نیز با مقصدهای پرش نمادین در پیش می‌گیرد. دستور Return مقادیر را در متغیر خروجی جایگزین کرده و برگ مسیر را می‌بندد. ردپایی طولانی‌تر از حد مجاز گام‌ها، مسیر را به عنوان قطع‌شده (Truncated) علامت زده و متوقف می‌کند.

مسیر رسیدن به return 4 را دستی دنبال کنید. نقطه‌ی ورود عبارت local_10 = score / 10 - 6 را مقداردهی می‌کند. شرط انشعاب local_10 >u 4 در این مسیر نادرست است؛ بنابراین فهرست شرط‌ها شامل !(score / 10 - 6 >u 4) می‌شود. ورودی‌های 3 و 4 سوییچ هر دو به 0x76 اشاره می‌کنند؛ پس انشعاب به 0x76 شرط score / 10 - 6 == 3 || score / 10 - 6 == 4 را اضافه می‌کند. بلوک 0x76 مقدار local_4 = 4 را تعیین کرده، به 0xa1 پرش می‌کند، و خروجی با مقدار 4 جایگزین می‌شود. برگ نهایی ترکیب این شرط و این مقدار بازگشتی است.

حل‌کننده در اینجا BoundedSearch است. این حل‌کننده یک دامنه‌ی محدود برای هر ورودی در نظر می‌گیرد، حاصل‌ضرب دامنه‌ها را می‌پیماید و هر قید را با معناشناسی زبان C ارزیابی می‌کند: سرریز 32 بیتی، تقسیم با قطع اعشار، مقایسه‌های علامت‌دار و بدون علامت، و شیفت‌های حسابی یا منطقی. تقسیم بر صفر یا اندیس خارج از جدول باعث می‌شود آن انتساب در ارضای قید مردود شود. برای مقادیر score بین -200 تا 1200، پنج مسیر تابع grade نیازمند 44,460 ارزیابی هستند که چند میلی‌ثانیه زمان می‌برند. حل هر برگ برای مجموعه‌ی ورودی‌ها این نتایج را می‌دهد:

نماد q معادل عبارت score / 10 - 6 است. همین دسته‌ها از grade در سطح -O1 نیز به دست می‌آید؛ جایی که IR دو مسیر دارد: مسیر جدول که lookup_14[q] را برمی‌گرداند و مسیر پیش‌فرض که 0 را بازمی‌گرداند. در اینجا چون بلوکِ case مجزایی برای رسیدن به آن وجود ندارد، پرسش به یک قید روی مقدار بازگشتی تبدیل می‌شود. جدول lookup_14 از بخش .rodata در آفست 0x14 فایل شیء خوانده می‌شود.

کران، محدودیت این روش را نشان می‌دهد. یک جست‌وجوی محدود درون دامنه‌ی خود کامل است و بیرون آن ساکت. در بازه‌ی -200 تا 1200، هیچ نمره‌ای بین 60 تا 109 خروجی 0 نمی‌دهد و هیچ نمره‌ی 110 به بالایی مقداری غیر از صفر برنمی‌گرداند. ابزار z3 هر دوی این موارد را برای تمام 2^32 نمره‌ی ممکن اثبات می‌کند؛ بخش بعدی نشان می‌دهد این دو روش در کجاها شواهد (Witnesses) متفاوتی برمی‌گردانند.

اندازه‌گیری انفجار مسیر

تابع total در سطح -O1 همان حلقه‌ی درس 33 است: بررسی روی count، بدنه‌ی حلقه که values[rdx] را جمع کرده و rdx را یکی زیاد می‌کند، و دستور jne به ابتدای بدنه مادامی که rdx != rcx باشد. در نمایش میانی، rcx برابر با zext64(count) است و rdx از 0 شروع می‌شود. در هر بار عبور از یال بازگشتی، انشعاب روی rdx != count شاخه می‌زند در حالی که rdx یک مقدار ثابت است؛ بنابراین مسیر به ازای count = c، بدنه‌ی حلقه را c بار اجرا می‌کند و سپس خارج می‌شود. با محدود کردن count به بازه‌ی 0 تا 2، موتور اجرا 3 مسیر می‌یابد. با بازه‌ی 0 تا 4 تعداد مسیرها 5، و با 0 تا 8 تعداد 9 مسیر پیدا می‌شود. هر مسیر مجموع مثلثی مقدار شمارنده‌ی خود را برمی‌گرداند: (0, 0)، (1, 1)، (2, 3)، تا (8, 36). نرم‌افزار angr در تمام سطوح سه‌گانه‌ی بهینه‌سازی (از جمله -O2 که حلقه‌ی برداری آن به حداقل شمارنده‌ی 8 نیاز دارد و بنابراین در این بازه تعداد مسیرها را تغییر نمی‌دهد) دقیقاً 3، 5 و 9 وضعیت به بن‌بست رسیده (Deadended states) و همان جفت‌های نُه‌گانه‌ی شمارنده و مجموع را گزارش می‌دهد.

بدون تعیین کران، موتور اجرا هرگز پایان نمی‌یابد، چرا که هر تعداد تکرار بیشتر، یک مسیر شدنیِ دیگر است. سقف 24 بلوک برای هر مسیر در این درس، با ورودی count تا 64، تعداد 22 مسیر برمی‌گرداند، 2 مسیر را متوقف می‌کند، و 41 مسیر دیگر از مجموع 65 مسیر موجود را اصلاً شروع نمی‌کند. گزارش خروجی این سه عدد را نشان می‌دهد. هزینه‌ی حل نیز رشد می‌کند: 33 ارزیابی در کران 2، 115 ارزیابی در کران 4، 531 ارزیابی در کران 8، و 6,900 ارزیابی برای اجرای دارای سقف.

مقایسه‌ی angr و z3 روی پرسش‌های یکسان

اسکریپت capture_angr.py نسخه‌ی angr 10.0.3 را روی هر سه فایل شیء اجرا کرد. موتور CLE هر فایل بازآرایی‌پذیر را با بک‌اند ELF در آدرس 0x400000 بارگذاری کرد، 13 بازآرایی برای بیلد -O0 و 8 بازآرایی برای بقیه‌ی سطوح اعمال کرد، و چهار نماد را حل نمود. برای تابع grade با یک ورودی نمادین 64 بیتی، اجرای متد run() با 5 وضعیت به بن‌بست رسیده در سطح -O0 و 2 وضعیت در -O1 و -O2 پایان یافت؛ این کار به ترتیب در زمان‌های 0.475، 0.408 و 0.318 ثانیه انجام شد. افزودن قید eax == v به هر وضعیت به بن‌بست رسیده و درخواست حداقل و حداکثر علامت‌دار از حل‌کننده، به ازای v از 1 تا 4 در تمام سطوح، بازه‌های 60 تا 69، 70 تا 79، 80 تا 89 و 90 تا 109 را داد، و برای 0 بازه‌ی -2147483648 تا 2147483647 به دست آمد. هر دو بررسی متقابل وضعیت غیرقابل ارضا (Unsat) داشتند.

حالت رسیدن به یک بلوک خاص (Reach-a-block) از CFGFast روی grade در سطح -O0 استفاده کرد که هشت بلوک کشف‌شده در درس 33 را فهرست می‌کند؛ سپس دستور explore(find=0x400076) برای بلوکی که مقدار 4 را ذخیره می‌کند اجرا شد. این دستور در 0.47 ثانیه یک وضعیت پیدا کرد (در حالی که سه وضعیت دیگر فعال بودند)؛ ورودی حداقل 90 و حداکثر 109 را نشان داد و نمونه‌های 91، 93، 94، 97 و 101 تولید شدند.

برای percent_change، دو وضعیت به بن‌بست رسیده با قیدهای before[31:0] != 0 و before[31:0] == 0 به دست آمد. درخواست مقدار eax == 50 از وضعیت غیرصفر مقادیر زیر را به دست داد: در بیلد -O0 مقدار before = 21055744, after = 332315210، در بیلد -O1 مقادیر 40566804, 834296877 و در بیلد -O2 مقادیر -24484867, 993934694. جست‌وجوی محدود در بازه‌ی -16 تا 16 پاسخ before = -10, after = -15 را می‌دهد. موتور z3 روی فهرست اسمبلی درس 34 به همین سؤال پاسخ before = -25092599, after = 305712160 را می‌دهد. مجموعه‌ی تست‌ها هر پنج جفت را با ارزیاب IR می‌سنجد و همگی مقدار 50 را برمی‌گردانند. یک مدل ثابت می‌کند ورودیِ معتبری وجود دارد؛ آن ورودی لزوماً تنها ورودی نیست، و سه ابزارِ درست، سه پاسخ کاملاً متفاوت دادند.

اسکریپت capture_z3.py فهرست اسمبلی تابع grade در سطح -O1 را در قالب بردارهای بیتی 32 بیتی همراه با ضرب، دو شیفت و جدول مدل‌سازی می‌کند و چهار سؤال دیگر می‌پرسد. آیا این فهرست با ساختار switch کد مبدأ برای یک نمره‌ی 32 بیتی تفاوتی دارد؟ پاسخ در 0.068 ثانیه unsat شد؛ بنابراین تابع کامپایل‌شده روی تمام 2^32 ورودیِ ممکن با کد منبع برابر است. آیا این فهرست با بازسازیِ آستانه‌محور درس 36 تفاوت دارد؟ در نمره‌ی 706346536 پاسخ sat شد؛ جایی که score / 10 برابر 70634653 می‌شود و سوییچ به حالت پیش‌فرض می‌رود، در حالی که کد آستانه‌محور مقدار 4 را برمی‌گرداند. همان مقایسه اگر به بازه‌ی 0 تا 109 محدود شود: پاسخ unsat شد، و به همین دلیل ماتریس آزمون درس 36 متوجه این باگ نشده بود. در مورد percent_change، قید before == 3 با نتیجه‌ی 133- با مقدار after = 1073741823 ارضا می‌شود که همان خانه‌ی سرریز درس 36 است؛ جست‌وجوی محدود نیز شاهد دومی در دامنه‌ی خود می‌یابد: after = -1، جایی که عبارت (-1 - 3) * 100 / 3 بدون هیچ سرریزی به 133- رند می‌شود.

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

کد دمو را اجرا کنید:

cd phases/13-tools-and-protocols/44-binary-diffing-and-symbolic-execution
python3 code/main.py

خروجی یک گزارش JSON است. بخش diffs تطابق‌های فایل شیء و ایمیج بارگذاری‌شده را برای -O0 در برابر -O1 و -O1 در برابر -O2، به‌علاوه‌ی جفت -O0 با ترتیب BinDiff نگه می‌دارد. بخش toolComparison مراحل پیاده‌سازی این درس را در کنار رأی و نسبت شباهت radiff2 و تطابق‌دهنده‌های Ghidra برای تک‌تک توابع قرار می‌دهد. بخش patch مربوط به سناریوی grade_case10_wrong.o است. بخش radare2Ratios اعداد radiff2 را بازتولید می‌کند، gradeRelocationCase چیدمان حافظه و دو مقدار جابه‌جایی را نشان می‌دهد، و بخش symbolic شامل مسیرها، دسته‌ها و آمارهای انفجار مسیر است.

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

1. کلاس ElfObject بخش‌ها، نمادها و رکوردهای .rela.* را می‌خواند. تابع parse_listing() خروجی متنی llvm-objdump را می‌خواند.
2. توابع jump_table_targets() و build_cfg() بلوک‌های در دسترس و یال‌های نوع‌دار را برمی‌گردانند. متد FunctionRecord.signatures() پنج امضا را می‌سازد.
3. تابع load_image() بخش‌های تخصیص‌یافته را می‌چیند و فرمول‌های S + A - P و S + A را اعمال می‌کند.
4. متد match_functions() همان تطابق‌دهنده‌ی مرحله‌ای است. توابع levenshtein() و radare2_ratio() شباهت را به دست می‌دهند.
5. توابع parse_radiff2() و parse_ghidra_vt() خروجی‌های ثبت‌شده‌ی ابزارها را برای مقایسه می‌خوانند.
6. توابع evaluate()، substitute() و کلاس BoundedSearch معناشناسی عبارت‌ها و حل‌کننده هستند.
7. تابع execute() مسیرها را می‌شمارد. تابع solve_returns() برای هر برگ، یک مجموعه‌ی ورودی استخراج می‌کند.
8. توابع grade_ir_o0()، grade_ir_o1()، percent_change_ir_o1() و total_ir_o1() نمایش میانیِ دستی همراه با آدرس دستورالعمل‌ها هستند.

سه دستور دیگر نیز وجود دارند. دستور python3 code/main.py diff A.o B.o دو فایل شیء را که لیست اسمبلی آن‌ها کنارشان باشد مقایسه می‌کند، و سوییچ --image ایمیج بارگذاری‌شده‌ی آن‌ها را مقایسه می‌کند. دستور python3 code/main.py paths grade O0 مسیرها و دسته‌های یک تابع را چاپ می‌کند، و paths total 8 حلقه را با یک کران مشخص نشان می‌دهد. دستور python3 code/main.py figure-data داده‌هایی را چاپ می‌کند که نمودار تعاملی در خود دارد.

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

روی دو بیلد از برنامه‌ی خود، مقایسه‌گر و موتور اجرای نمادین را به این ترتیب اجرا کنید:

1. از هر فایل شیء یک فهرست اسمبلی بگیرید و بگذارید function_record() درستی آن را با بایت‌ها بررسی کند. پیش از هر کاری ابتدا فهرست اسمبلی را اصلاح کنید.
2. ابتدا فایل‌های شیء را مقایسه کنید. به مرحله‌ی هر تطابق دقت کنید و تطابق‌های ناشی از شکل گراف جریان کنترل را تا زمانی که امضای دومی تأییدشان نکرده فقط در حد پیشنهاد در نظر بگیرید.
3. ایمیج‌های بارگذاری‌شده را مقایسه کنید. تابعی که از سطح بایت‌های دقیق به بایت‌های ماسک‌شده سقوط می‌کند، جایگاهش نسبت به داده‌هایش جابه‌جا شده است؛ محاسبات جابه‌جایی دقیقاً نام بخشی را که جابه‌جا شده مشخص می‌کند.
4. به ازای هر تطابق، جداول ارجاع‌شده را مقایسه کنید. کد یکسان با ثابت‌های متفاوت یعنی تابع دستکاری شده است.
5. مرحله‌ی نام‌ها را اجرا و مقایسه کنید. اگر بیلد شامل نمادها است، ترتیب BinDiff را اجرا کنید و از نتایج ساختاری صرفاً برای ارزیابی مراحل استفاده کنید.
6. وقتی ابزاری یک نسبت شباهت را گزارش می‌دهد، پیش از مقایسه‌ی آن با نتایج خود دقیقاً بفهمید چه بایت‌هایی وارد محاسبه شده‌اند.
7. برای تابعی که به دنبال ورودی‌هایش هستید، نمایش میانی را با یک آدرس به ازای هر عبارت بنویسید، execute() را با تعیین کران روی هر شمارنده‌ی نمادین حلقه اجرا کنید، و مقدار هر برگ را حل کنید. کران را حتماً در کنار نتیجه گزارش دهید.
8. در صورت دسترسی به angr یا z3، همان پرسش را با آن‌ها نیز اجرا کنید و کران دسته‌ها را بسنجید. یک نمونه فقط یک مدل است.

کارگاه تعاملی

بخش اول: پنج امضا به صورت دستی

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

cd phases/13-tools-and-protocols/44-binary-diffing-and-symbolic-execution/code
python3 -q

اجرا کنید:

from main import *
grade = {r.name: r for r in fixture_records("ledger-x86_64-O1.o")}["grade"]
grade.raw.hex(" ")
grade.masked_bytes() == grade.raw
grade.mnemonics
grade.cfg_shape()
grade.signatures()

پیش از چاپ grade.raw، چهار بایتِ موجود در آفست 0x26 تابع را یادداشت کنید. سپس همین خطوط را روی grade از فایل ledger-x86_64-O0.o اجرا کنید و تعداد یال‌های table را در grade.edges بشمارید.

بخش دوم: مشاهده‌ی تخریب هش بایت بر اثر بازآرایی

case = grade_relocation_case()
case["layout"]
case["displacements"], case["rodataShift"]
case["objectBytesEqual"], case["imageBytesEqual"], case["maskedImageBytesEqual"]

پیش از خواندن displacements، حاصل 0x100110 + 0x14 - 0x10003a را روی کاغذ حساب کنید. سپس آدرس پایه در load_image() را به 0x400000 تغییر دهید و مطمئن شوید مقادیر جابه‌جایی تغییر نمی‌کنند، چرا که هر دو عملوند با هم جابه‌جا می‌شوند.

بخش سوم: تطابق کاذب و ترتیبی که جلوی آن را می‌گیرد

report = diff_fixtures("ledger-x86_64-O1.o", "ledger-x86_64-O2.o")
[(m.left.name, m.right.name, m.stage) for m in report.matches]
report = diff_fixtures("ledger-x86_64-O0.o", "ledger-x86_64-O1.o")
[(m.left.name, m.right.name, m.stage, m.names_agree) for m in report.matches]
report = diff_fixtures("ledger-x86_64-O0.o", "ledger-x86_64-O1.o", stages=BINDIFF_ORDER)
[(m.left.name, m.right.name, m.stage) for m in report.matches]

خروجی متد records(...)["percent_change"].cfg_shape() را برای -O0 و grade_label را برای -O1 چاپ کنید و دو توالی درجات را بخوانید. سپس مرحله‌ی ششمی بنویسید که نمادهای مرتب‌شده را هش کند (تا ترتیب دستورات دیگر اهمیتی نداشته باشد) و ببینید آیا این مرحله می‌تواند آن‌ها را از هم تفکیک کند یا نه.

بخش چهارم: مسیرها و محدوده‌ی کران

report = grade_paths("O0")
[(p["trace"], p["condition"], p["returns"]) for p in report["paths"]]
report["returns"]["4"]
total_paths(2), total_paths(4), total_paths(8)
total_paths(64, step_limit=24)["truncated"]

مقدار SCORE_DOMAIN را به range(0, 110) تغییر دهید و دوباره grade_paths("O0") را اجرا کنید. دسته‌ی مربوط به 0 به 60 ورودی کاهش می‌یابد و هر دو بررسی متقابل کماکان پابرجا می‌مانند. سپس دامنه را روی range(90, 100) بگذارید و بخوانید کدام برگ‌ها اصلاً مدلی نخواهند داشت.

تمرین عملی

ابزار BinDiff را روی داده‌های این پروژه اجرا کنید و خروجی آن را با سه نتیجه‌ای که هم‌اکنون در اختیار دارید بسنجید.

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

• افزونه‌ی BinExport را روی Ghidra 12.1.4 نصب کنید و هر سه برنامه‌ی ledger را اکسپورت بگیرید. تگ نسخه‌ی BinExport و نسخه‌ی Ghidra را ثبت کنید.
• نسخه‌ی خط فرمانی BinDiff 8 را نصب کنید و نتایج مقایسه‌ی -O0 در برابر -O1 و -O1 در برابر -O2 را با گزینه‌ی similarity-only تولید کنید.
• شباهت و ضریب اطمینان به ازای هر تابع را با دستورات دقیق در build_fixtures.sh داخل پوشه‌ی code/fixtures/ ذخیره کنید.
• تابع tool_comparison() را با یک ستون bindiff گسترش دهید و تستی اضافه کنید که مجموعه‌ی تطابق‌های BinDiff در مقایسه‌ی -O1 با -O2 را با مجموعه‌ی بایت‌های ماسک‌شده‌ی این درس مقایسه کند.
• یک پاراگراف بنویسید که در آن نام الگوریتم مورد استفاده‌ی BinDiff برای تابع grade قید شده باشد و مشخص کند آیا این ابزار ایمیج‌های بارگذاری‌شده را مقایسه کرده است یا نه.

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

خروجی این درس

این درس شامل فایل outputs/skill-binary-diffing-and-symbolic-execution.md است. با استفاده از آن می‌توانید دو بیلد و یک تابع را به یک تفاضل مرحله‌ای همراه با کیفیتِ تصریح‌شده برای هر تطابق، توضیحِ دلایل تمام توابع نامنطبق یا تغییریافته، و گزارشی از مسیرها همراه با مجموعه‌ی ورودی‌های حل‌شده برای هر برگ و کران سازنده‌ی آن تبدیل کنید.

اعتبارسنجی

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

cd phases/13-tools-and-protocols/44-binary-diffing-and-symbolic-execution
python3 code/main.py
python3 -m unittest discover -s code/tests -v

اعتبارسنجی باید موارد زیر را اثبات کند:

• جداول نمادها، چهار تابع را با اندازه‌های 46، 118، 66 و 39 در سطح -O0، اندازه‌های 16، 46، 31 و 63 در سطح -O1، و اندازه‌های 16، 46، 140 و 63 در سطح -O2 مشخص می‌کنند.
• رکوردهای .rela.text در فایل شیءِ بیلد -O1 دقیقاً همان چیزی هستند که دستور llvm-objdump -r چاپ می‌کند.
• تمام دستورالعمل‌های فهرست‌شده درون محدوده‌ی نماد خود قرار دارند و بایت‌هایشان با فایل شیء برابر است؛ همچنین تغییر یک بایت باعث بروز خطا می‌شود.
• تابع total در سطح -O1 دارای پنج بلوک، پنج یال و یک حلقه‌ی به خود (Self loop) است، و رشته‌ی شکل گراف آن قطعی است.
• تابع grade در سطح -O0 پنج مقصد جدول پرش را از .rela.rodata بازیابی می‌کند و هشت بلوک و یازده یال دارد.
• بدون این جدول، تابع grade در سطح -O0 به 82 بایت در قالب چهار بلوک می‌رسد.
• تابع percent_change در سطح -O0 و تابع grade_label در سطح -O1 شکل چهاربلوکی یکسانی دارند.
• هش‌های دقیق و ماسک‌شده در تمام توابع یک فایل شیءِ بازآرایی‌پذیر هم‌نظرند.
• بیلدهای -O1 و -O2 در سه تابع بایت‌های مشترک دارند؛ بیلدهای -O0 و -O1 هیچ بایت مشترکی ندارند.
• جدول ارجاع‌شده در grade مقادیر 1, 2, 3, 4, 4 و در کاندید مقادیر 1, 2, 3, 4, 3 را می‌خواند.
• لودر، بخش‌های .text، .rodata و .rodata.str1.1 را در هر دو برنامه همان‌جایی قرار می‌دهد که Ghidra چیده است.
• نوع R_X86_64_PC32 بر اساس فرمول S + A - P نوشته شده و جابه‌جایی 122 را به دست می‌دهد؛ ورودی‌های R_X86_64_64 در .data آدرس‌های رشته‌ای را دریافت می‌کنند.
• بایت‌های grade در فایل‌های شیء یکی هستند و در ایمیج‌ها با 0x70 شیفت تفاوت دارند؛ عمل ماسک کردن تطابق را بازمی‌گرداند.
• مقایسه‌ی -O1 با -O2 سه تابع را بر اساس بایت‌های دقیق و total را بر اساس نام تطابق می‌دهد؛ نمای ایمیج، grade را بر اساس بایت‌های ماسک‌شده با نسبت شباهت 1 - 1/46 تطابق می‌دهد.
• ترتیب مراحل این درس یک تطابق کاذب بر اساس شکل گراف در مقایسه‌ی -O0 با -O1 ایجاد می‌کند؛ ترتیب BinDiff هر چهار تابع را با نام تطابق می‌دهد.
• تکه‌ی کاندید بر اساس بایت‌ها مطابقت می‌یابد اما در ارزیابی داده‌های ارجاع‌شده رد می‌شود.
• فرمول نسبت لون‌اشتاین مقادیر 0.130435، 0.106061، 0.269841، 0.171429، و 0.426829 (روی 82 بایت) و نسبت‌های بایت‌های بازآرایی‌شده را در radiff2 پس از اعمال بازآرایی‌ها بازتولید می‌کند.
• مجموعه‌ی MATCH در radiff2 برابر با مرحله‌ی بایت‌های دقیق است؛ تطابق‌دهنده‌های بایت و دستورالعمل Ghidra نیز با مجموعه‌های بایت‌های دقیق و ماسک‌شده در نمای ایمیج برابرند.
• نرم‌افزار Ghidra در مقایسه‌ی -O0 با -O1 فقط نام‌ها را پیدا کرد، با شباهت 1.0 و اطمینان 10.0 برای تمام تطابق‌ها.
• نمایش میانیِ دستی، تمام دستورالعمل‌های فهرست‌شده را یک بار پوشش می‌دهد و ارزیاب آن از معناشناسی C تبعیت می‌کند.
• تابع grade پنج مسیر در بیلد -O0 با شرط‌های سوییچ و دو مسیر در -O1 با همان دسته‌ها دارد.
• دسته‌های محدودشده‌ی 60 تا 69، 70 تا 79، 80 تا 89 و 90 تا 109 در تمام سطوح سه‌گانه با نتایج angr و z3 برابرند (با 5 و 2 وضعیت به بن‌بست رسیده و بازه‌ی رسیدن به بلوک 90 تا 109).
• دو بررسی متقابل هیچ مدلی در دامنه‌ی کران، در angr و در z3 ندارند؛ همچنین z3 اثبات می‌کند که فهرست اسمبلی با سوییچ کد مبدأ برابر است.
• تمام مدل‌های percent_change از جست‌وجوی محدود، angr و z3 به مقدار خواسته‌شده ارزیابی می‌شوند.
• تابع total به تعداد 3، 5 و 9 مسیر با مجموع‌های مثلثی به دست می‌دهد (مشابه خروجی angr)، و سقف گام‌ها تعداد 22 مسیر را بازگردانده و 2 مسیر را متوقف می‌کند.
• داده‌های نمودار شامل هر دو نما، محاسبات بازآرایی، و پنج برگ همراه با مجموعه‌ی ورودی‌های آن‌ها است؛ ماژول وب‌سایت نیز همین داده‌ها را درون‌گذاری می‌کند.

حالت‌های شکست در محیط عملیاتی

روال اجرایی

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

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

• مفاهیم BinDiff: استراتژی تطابق، الگوریتم‌ها و رتبه‌بندی‌های کیفی
• مخزن BinDiff و نسخه‌ی متن‌باز v8
• فایل README ابزار BinExport: صادرکننده‌های IDA Pro، Binary Ninja و Ghidra
• مقالات فلیک (DIMVA 2004) و دولین، رولز (SSTIC 2005) درباره‌ی مقایسه‌ی ساختاری فایل‌های باینری، موجود در مخزن BinDiff
• فایل README ابزار Diaphora و سورس‌کد هیوریستیک‌های آن
• صفحه‌ی راهنمای تطابق‌دهنده‌های Ghidra Version Tracking
• صفحه‌ی راهنمای قابلیت Auto Version Tracking در Ghidra
• انتشار Ghidra 12.1.4
• یادداشت‌های انتشار Binary Ninja 6.0 "Krypton" و راهنمای کاربری Binary Similarity
• کتاب radare2: بخش radiff2 و سورس‌کد radare2 6.2.4
• کینگ، «اجرای نمادین و آزمون نرم‌افزار» (CACM 1976)
• بالدونی و همکاران، «مروری بر تکنیک‌های اجرای نمادین» (ACM Computing Surveys 2018)
• کادار، سن، «اجرای نمادین برای آزمون نرم‌افزار: سه دهه بعد» (CACM 2013)
• کادار، دانبار، انگلر، «KLEE: تولید خودکار تست‌های با پوشش بالا برای برنامه‌های سیستمی پیچیده» (OSDI 2008) و انتشار KLEE 3.2
• شوشتایشویلی و همکاران، «بررسی وضعیت تکنیک‌های تهاجمی در تحلیل باینری» (IEEE S&P 2016)
• مستندات angr: بارگذاری، مدیران شبیه‌سازی و پایپ‌لاین شبیه‌سازی و angr 10.0.3 روی PyPI
• انتشار Z3 5.1.0
• کتابخانه‌ی تحلیل باینری پویای Triton
• رابط باینری کاربردی System V برای معماری AMD64، جدول 4.9: انواع بازآرایی