Phase 13: Tools & Protocols

द्विआधारी विभेदन और प्रतीकात्मक निष्पादनः मिलान कार्य और इनपुट के लिए समाधान

दो कार्यों के बीच एक मेल एक गुण के साथ एक हस्ताक्षर द्वारा किया गया दावा है, और एक हल किया गया इनपुट एक पथ स्थिति का एक मॉडल है; यह पाठ दोनों का निर्माण करता है और उन्हें radiff2, Ghidra, angr, और z3 के खिलाफ जांचता है।

Type: Build

Languages: Python, C, x86-64 assembly, Java (one Ghidra script)

Prerequisites: Phase 13 · 33 (disassembly and control flow), 34 (lifting to pseudocode), 36 (rebuild and prove equal)

Time: ~150 minutes

सीखने के लक्ष्य

  • किसी वस्तु और उसकी सूची से पांच फ़ंक्शन हस्ताक्षर बनाएंः सटीक बाइट्स, स्थानांतरण क्षेत्रों के साथ बाइट्स, मनमोनिक अनुक्रम, प्रवाह-ग्राफ आकार और प्रतीक नाम।
  • बिनडीफ शैली में एक स्टेज-आधारित लोभी मैच चलाएं, जहां एक हस्ताक्षर केवल तभी मेल खाता है जब यह दोनों तरफ अद्वितीय हो, और प्रत्येक मैच के पीछे चरण और गुणवत्ता रिकॉर्ड करें।
  • ऐसे मामले को दोहराएं जहां दो बाइट-समान फ़ंक्शन लोड की गई छवियों पर बाइट-समानता को विफल कर दें और इसे मास्किंग के बाद स्थानांतरण अंकगणित के साथ पारित करें जो चार बदल गए बाइट्स की व्याख्या करता है।
  • लेवेंसटाइन दूरी से radiff2 के समानता अनुपात को पुनः प्रस्तुत करें और समझाएं कि तुलना में 82 बाइट्स रडार2 प्राप्त होने पर ही एक अनुपात क्यों दिखाई देता है।
  • एक छोटे IR पर फ़ंक्शन के पथों को सूचीबद्ध करें, प्रति पथ एक शर्त ले जाएं, और एक सीमित खोज के साथ इनपुट के लिए प्रत्येक पाना हल करें।
  • प्रतीकात्मक सीमा के साथ लूप पर पथ विस्फोट को मापें और अंक, वर्गों और मॉडल को angr 10.0.3 और z3 5.1.0 के साथ तुलना करें।

समस्या

तुमने पुनर्निर्माण किया हैledger.cपर-O2और एक एजेंट से पूछा कि क्या कुछ बदल गया है के बाद से -O1एजेंट एक अंतर चलाया और रिपोर्ट किgradeयह एक बदलाव की व्याख्या करने के लिए अपने बजट खर्च किया है जो मौजूद नहीं है।gradeदो वस्तु फ़ाइलों में समान हैं। स्थानांतरण के बाद तुलनात्मक चित्र अलग हैं, और .rodata में 0x70 बाइट्स आगे पर स्थित है-O2कार्यक्रम, तो एक विस्थापन में grade0x70 से बढ़ी।

उसी दोपहर आप पूछा कि स्कोर क्या बनाता हैgradeरिटर्न 4। एजेंट ने छद्म कोड पढ़ा और "90" का जवाब दिया। यह एक उत्तर है। फ़ंक्शन 90 से 109 तक के प्रत्येक स्कोर के लिए 4 देता है, और प्रश्न का कोई बंधन नहीं था, इसलिए एजेंट का जवाब एक नमूना था जहां आपको एक सेट की आवश्यकता थी।

दोनों विफलताएं एक ही अंतराल से आती हैं। एक मैच और एक हल किया गया इनपुट प्रत्येक एक विधि के साथ एक दावा है। यह सबक मानक पुस्तकालय पायथन में दोनों तरीकों का निर्माण करता है और उनके बगल में उत्पादन उपकरण चलाता है। जहां उपकरण और कोड सहमत हैं, आपके पास दो व्युत्पन्न हैं। जहां वे असहमत हैं, आपके पास एक पता, बाइट या एक बाध्यता है।

एक कार्य हस्ताक्षर एक गुण के साथ दावा है

फ्लेक ने 2004 में दो समान निष्पादन योग्य के फ़ंक्शन सेट के बीच एक आइसोमोर्फिज्म के निर्माण के रूप में द्विआधारी भिन्नता को फ्रेम किया। डूलिन और रोल्स ने 2005 में इसे बुनियादी ब्लॉक और निर्देशों तक बढ़ाया। बिन्डीफ़ अवधारणा पृष्ठ उस कार्य से निकली रणनीति का वर्णन करता है। दोनों तरफ प्रत्येक फ़ंक्शन के लिए एक विशेषता गणना करें। एक मूल्य जो प्रत्येक पक्ष पर एक बार दिखाई देता है वह एक मेल खाता है। एक से अधिक बार दिखाई देने वाला मान अस्पष्ट है और उस समकक्षता वर्ग के भीतर अगले विशेषता के साथ ड्रिल किया जाता है। बिना समकक्ष के कोई मूल्य अपरिवर्तनीय रहता है। प्रत्येक पास के बाद, नए मैचों के कॉलर्स और कॉलर्स छोटे सेट बनाते हैं जहां अगले विशेषता की संभावना अद्वितीय है, और प्रक्रिया अगले विशेषता के साथ दोहराई जाती है।

प्रत्येक मिलान एल्गोरिथ्म में एक गुण होता है। पृष्ठों का रेट हैश मैचिंग कच्चे फ़ंक्शन बाइट्स और नाम हैश मैचिंग बहुत अच्छा है, प्रवाह ग्राफ एमडी सूचकांक और प्राइम हस्ताक्षर मैचिंग (प्रत्येक एमनेमोनिक एक छोटा प्राइम, फ़ंक्शन पर उत्पाद) अच्छा है, स्ट्रिंग संदर्भ मध्यम के रूप में, और लूप गिनती या पता अनुक्रम खराब है। एक मैच का आत्मविश्वास उस एल्गोरिदम की औसत गुणवत्ता है जिसने इसे उत्पन्न किया, जिसका वजन सिग्मोइड द्वारा किया गया है। फ़ंक्शन समानता लगभग 25% मिलान प्रवाह ग्राफ किनारों, 15% मिलान बुनियादी ब्लॉक, 10% मिलान निर्देश, और 50% अंतर प्रवाह ग्राफ एमडी सूचकांक, विश्वसनीयता से गुणा है।

इस पाठ में उन गुणों में से पांच और एक नियम को रखा गया है जो मायने रखता हैः दोनों पक्षों पर अद्वितीय या कोई मैच नहीं। यह एमडी सूचकांक को छोड़ देता है, क्योंकि अवधारणा पृष्ठ इसे सूत्र के बिना नाम देता है, और इसके स्थान पर एक सादे डिग्री अनुक्रम का उपयोग करता है। गुणवत्ता लेबल बने रहते हैं, क्योंकि एक मैच केवल सबसे कमजोर तथ्य के रूप में अच्छा है जिसने इसे उत्पन्न किया।

एक कार्य रिकॉर्ड से पांच हस्ताक्षर

भिन्न प्रति वस्तु दो चीजें पढ़ता है। ELF बाइट्स, प्रतीक आकार, और .rela.*रिकॉर्ड।llvm-objdump -dसूची निर्देश सीमाओं और mnemonics देता है, और पाठ 33 इन वस्तुओं के प्रत्येक निर्देश पर सूची के बराबर एक डिकोडर साबित हुआ। function_record()जांच करता है कि प्रत्येक सूचीबद्ध निर्देश के बाइट उस पते पर ऑब्जेक्ट के बाइट के बराबर हैं और अन्यथा बढ़ता है। एक पुराने सूची एक बदल गया फिस्ट है।

ले लोgradeमें ledger-x86_64-O1.o. प्रतीक कहते हैं 0x10 और आकार 46 ऑफसेट, तो रिकॉर्ड 0x10 से 0x3e तक कवर करता है और दो-बाइट को बाहर करता है nopजो अगले समारोह को संरेखित करता है।

सटीक बाइट्स हस्ताक्षर 46 बाइट्स में से SHA-256 है। मास्क बाइट्स हस्ताक्षर पहले प्रत्येक स्थानांतरण क्षेत्र को शून्य करता है। एक क्षेत्र हैः रिकॉर्डR_X86_64_PC32 .rodata+0x100x36 पर चौड़ाई 4 बाइट, विस्थापन leaq (%rip), %rcx0x33 पर एक RELA वस्तु में उन चार बाइट्स पहले से ही शून्य है, तो दोनों हस्ताक्षर यहाँ प्रत्येक वस्तु के प्रत्येक समारोह पर सहमत हैं. मुखौटा अगले खंड के लिए मौजूद है.

mnemonic हस्ताक्षर 14 mnemonics के अनुक्रम हैश करता हैः

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

प्रवाह ग्राफ आकार हस्ताक्षर पाठ 33 के बुनियादी ब्लॉक और टाइप किनारों से आता है, जो प्रविष्टि तक पहुंच सकते हैं। gradeपर-O1तीन ब्लॉक और तीन किनारों है. ब्लॉक 0x10 में समाप्त होता हैja 0x3dएक लिया किनारा और एक गिरावट किनारा के साथ, ब्लॉक 0x31 0x3d तक गिरता है, और 0x3d वापस आता है। डिग्री अनुक्रम क्रमबद्ध क्रम में प्रत्येक ब्लॉक को सूचीबद्ध करता है, इसलिए हस्ताक्षर पढ़ता है 3b 3e [0/2,1/1,2/0]. . के लिए .gradeपर-O0रिकॉर्ड पांच के माध्यम से अप्रत्यक्ष कूद हल करता है .rela.rodataप्रविष्टियों बिल्कुल पाठ 33 के रूप में किया, जो आठ ब्लॉक और चार के साथ ग्यारह किनारे देता है tableकिनारों.

नाम हस्ताक्षर प्रतीक नाम है यह सबसे मजबूत तथ्य है जब यह मौजूद है और जब बिल्ड को हटा दिया जाता है तो कुछ भी नहीं है।

एक और क्षेत्र पैच मामले के लिए आगे चला जाता है बाद में. जब एक समारोह एक है lea.rodata, सीमाओं की जांच, और एक सूचकांकित लोड, referenced_table()तालिका को पाठ 36 की तरह पढ़ा जाता हैः cmpl $0x4पहलेjaपांच प्रविष्टियों और लोड देता है movl (%rcx,%rax,4), %eaxप्रत्येक चार बाइट देता है।gradeपर-O1.rodata+0x14पढ़ता है 1, 2, 3, 4, 4. .

लालची डाकू

match_functions()प्रत्येक चरण के लिए यह उस चरण के हस्ताक्षर द्वारा प्रत्येक पक्ष पर अभी तक अपरिवर्तित कार्यों को समूहित करता है और प्रत्येक पक्ष पर एक कार्य के साथ प्रत्येक मान को स्वीकार करता है। मैच चरण, चरण की गुणवत्ता, प्रत्येक अन्य हस्ताक्षर को रिकॉर्ड करता है जो भी सहमत है, और समानता अनुपात।

python
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:

FunctionStageAgreeing signaturesSimilarity
percent_changeexact bytesall five1.000
gradeexact bytesall five1.000
totalnamename only0.171
grade_labelexact bytesall five1.000

totalयह 31 बाइट्स और 13 निर्देशों से 140 बाइट्स और 41 निर्देशों तक बढ़ गया, क्योंकि क्लिंग ने SSE2 के साथ लूप को वेक्टरिज़ किया और एक स्केलर शेष लूप बनाए रखा। इसका आकार पांच ब्लॉक और पांच किनारों से दस ब्लॉक और तेरह किनारों तक चला गया। कोई संरचनात्मक बचा नहीं है, और केवल प्रतीक दोनों को जोड़ता है।

के लिए-O0-O1उसी क्रम में एक गलत मैच होता हैः

Function at -O0Matched at -O1StageNames agree
percent_changegrade_labelflow-graph shapeno
gradegradenameyes
totaltotalnameyes
grade_labelunmatched

percent_changeपर-O0एक चार ब्लॉक का हीरा हैः एक प्रविष्टि जो शाखाओं पर before == 0, दो हाथों, और एक जोड़ जो वापस आता है.0/2, 1/1, 1/1, 2/0. .grade_labelपर-O1हैgradeइनलाइन और सीमाओं के चारों ओर एक ही हीरा जांचें. आकार दोनों तरफ अद्वितीय है और नियम इसे स्वीकार करता है। मध्यम गुणवत्ता लेबल चेतावनी है, और नाम चरण, बाद में चलाया, इसके विपरीत है। गलत मिलान भी खपत करता हैgrade_labelदाईं ओर, तो असली percent_changeऔर grade_labelजोड़े बेजोड़ रहते हैं।

बिनडीफ आदेश नाम मिलान दूसरे चरण के रूप में चलाता है जब असली नाम मौजूद हैं, और BINDIFF_ORDERकोड में एक ही करता है। उस क्रम के साथ सभी चार-O0कार्य उनके अनुरूप हैं -O1इस प्रकार, एक फ्लो-ग्राफ चार नोड्स का आकार है जो प्रत्येक नोड का आकार है।ifऔर elseजो वापसी से पहले जुड़ता है।

समान बाइट, स्थानांतरित ऑपरेन्ड

Ghidra वस्तु आयात करते समय स्थानांतरण लागू करता है। इसलिए इसका बाइट सहसंबंधी लोड किए गए चित्रों की तुलना करता है, और इस कारण से लक्षित स्थानांतरण फ़ील्ड का पाठ 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 के साथ लेआउट सहमत है, जिसे परीक्षण सूट कैप्चर किए गए संस्करण ट्रैकिंग आउटपुट के खिलाफ जांचता हैः

Section-O1 program-O2 program
.text0x100000, 159 bytes0x100000, 271 bytes
.rodata0x1000a00x100110
.rodata.str1.10x1000f00x100160

.text पर 112 बाइट अधिक है-O2, विकासtotal, तो .rodata0x70 बाइट आगे शुरू होता है। gradeदोनों कार्यक्रमों में 0x100010 पर बैठता है।leaq0x33 पर 0x36 पर स्थानांतरण क्षेत्र है और 0x3a पर समाप्त होता है। स्थानांतरण योग 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 से समान रूप से आगे बढ़ता है, इसलिए इसके विस्थापन समान रहते हैं और यह दोनों दृश्यों में सटीक बाइट्स पर पारित करता है।

गिदरा ने एक ही विभाजन की सूचना दी है।-O1-O2, सटीक फ़ंक्शन बाइट्स मिलान पाया percent_changeऔर grade_label, सटीक कार्य निर्देश मिलान उन दो प्लस पायाgrade, और सटीक फ़ंक्शन मेनोमिक्स मैच ने वही तीन पाए। निर्देश सहसंबंधी ऑपरेन्ड्स को कवर करता है, जो विस्थापन को कवर करता है। पाठ के छवि दृश्य में गिदरा के बाइट सहसंबंधी ने पाए गए दो कार्यों के लिए सटीक बाइट्स मिलान देता है और निर्देश सहसंबंधी ने पाए गए तीन के लिए मास्क-बाइट्स समझौते। परीक्षण सूट दोनों समानताओं का दावा करता है।

6.5.0 के लिए compare_functionsलाइन-डिफ़्स प्रदाता पाठ। विधानसभा आयाम पर यह सीमा संलग्न "परिवर्तन सामान्यीकरण अनुपलब्ध है।" लोडर और इस पाठ में मुखौटा सामान्यीकरण की आपूर्ति।

क्या उपाय

रडार2 6.2.4 जहाज radiff2. के साथ -ACयह फ़ाइलों का विश्लेषण करता है और प्रत्येक फ़ंक्शन के लिए एक पंक्ति प्रिंट करता हैः बाएं आकार और पता, MATCH या UNMATCH, एक अनुपात, और सही आकार और पता। हमारे वस्तुओं के लिए कैप्चर किए गए पंक्तियांः

Pairpercent_changegradetotalgrade_label
-O0 vs -O1UNMATCH 0.130435UNMATCH 0.426829UNMATCH 0.106061UNMATCH 0.269841
-O1 vs -O2MATCH 1.000000MATCH 1.000000UNMATCH 0.171429MATCH 1.000000
-O1 vs -O1MATCH 1.000000MATCH 1.000000MATCH 1.000000MATCH 1.000000

रडार2 स्रोत में अनुपात 1 - distance / max(len_a, len_b), जहां दो फ़ंक्शन फिंगरप्रिंट और एक फिंगरप्रिंट के बीच की दूरी लेवेंसस्टाइन दूरी है, वह फ़ंक्शन के मूल ब्लॉक का पता क्रम में संयोजन है। मिलान सीमा 0.7 है। radare2_ratio()में code/main.pyकच्चे फ़ंक्शन बाइट्स पर एक ही सूत्र लागू करता है और 0.130435, 0.106061, 0.269841, और 0.171429 को छह दशमलव तक पुनः प्रस्तुत करता है।

यह 0.426829 के लिए पुनरुत्पादित नहीं होता हैgradeपर-O0. फ़ंक्शन के 118 बाइट्स पर अनुपात 0.296610. रडार2 प्रिंट है 118आकार स्तंभ में. इसके फिंगरप्रिंट छोटा है. लागू स्थानांतरण के बिना यह कूद तालिका को हल नहीं कर सकता है, इसलिए इसके विश्लेषण प्रवेश ब्लॉक तक पहुँचता है, ब्लॉक जो समाप्त होता है jmpq *%rax, डिफ़ॉल्ट केस, और रिटर्नः 82 बाइट्स, वही 82 जो पाठ 33 की सादे पुनरावर्ती वंशावली ने दावा किया। उन 82 बाइट्स और 46 बाइट्स के बीच लेवेंसटाइन दूरी -O147 है, और 1 - 47/82 = 0.426829. के साथ -e bin.relocs.apply=trueradare2 सभी 118 बाइट्स को ढूंढता है और 0.288136 प्रिंट करता है, जो स्थानांतरित छवियों पर पाठ के अनुपात के बराबर है, जहां चार विस्थापन बाइट्स वस्तु के शून्य क्षेत्रों से भिन्न होते हैं। दो उपकरण केवल तभी सहमत होते हैं जब वे एक ही बाइट्स की तुलना करते हैं, और आकार स्तंभ नहीं कहता है कि कौन से बाइट्स गए।

-Oफिंगरप्रिंट को ऑपकोड बाइट्स तक सीमित करता है और ऑपरेन्ड को शून्य करता है।-O0बनाम -O1अनुपात 0.239130, 0.512195, 0.303030, और 0.523810 तक बढ़े, और totalपर-O1बनाम -O20.192857 तक बढ़ता है। पूरे फ़ाइल दूरी भी मौजूद हैंः -s(माइयर्स) दो वस्तुओं के बीच समानता 0.956 और दूरी 162 रिपोर्ट करता है,-ss(लेविनश्टीन) 0.927 और 137. उन संख्याओं में हेडर, प्रतीक तालिकाओं, और स्थानांतरण अनुभाग शामिल हैं और कार्यों के बारे में कुछ नहीं कहते हैं।

गिद्रा संस्करण ट्रैकिंग सहसंबंध

गिद्रा के संस्करण ट्रैकिंग टूल एक स्रोत कार्यक्रम को एक गंतव्य कार्यक्रम के साथ सहसंबंधों से मेल खाता है। फ़ंक्शन सहसंबंधी हैं सटीक फ़ंक्शन बाइट्स मैच, सटीक फ़ंक्शन निर्देश मैच (ओपरैंड्स मास्क), सटीक फ़ंक्शन मेनमोनिक मैच, और दोहरा फ़ंक्शन निर्देश मैच (1: N और N: M) । डेटा सहसंबंध सटीक, डुप्लिकेट और समान डेटा मेल खाते हैं। प्रतीक संबद्ध नामों से बिल्कुल मेल खाते हैं, जैसे दोहरे, या समानता से। अधिक जानकारी प्राप्त करने के लिए संदर्भ सहसंबंधी स्वीकार किए गए मैचों का उपयोग करते हैं। कार्य को गंतव्य कार्यक्रम में परिभाषित किया जाना चाहिए, और न्यूनतम कार्य लंबाई डिफ़ॉल्ट रूप से 10 बाइट्स तक है। ऑटो वर्जन ट्रैकिंग सटीक प्रतीक नाम, सटीक डेटा, सटीक फ़ंक्शन बाइट्स, सटीक फ़ंक्शन निर्देश, सटीक फ़ंक्शन मेमोनिक, दोहरा फ़ंक्शन निर्देश चलाता है, फिर एक संदर्भ सहसंबंधी, और स्वीकार किए गए लोगों के लिए अंतर्निहित मैच बनाता है। 11.2 में एक बीएसआईएम सहसंबंधी जोड़ा गया।

पाठ ने सहसंबंधकों को बिना सिर के पकड़ लिया।capture_ghidra_vt.shपरियोजना में तीन वस्तुओं का आयात और संचालन ListVersionTrackingMatches.java, एक छोटी सी स्क्रिप्ट जो विस्तारित होती है AbstractGhidraVersionTrackingScript, पथ द्वारा स्रोत और गंतव्य कार्यक्रमों को खोलता है, ऑटो संस्करण ट्रैकिंग क्रम में छह गैर-संदर्भात्मक सहसंबंध चलाता है, और प्रति ब्लॉक, फ़ंक्शन, सहसंबंधी और मैच एक पंक्ति प्रिंट करता है। इस खंड में प्रत्येक संख्या उन दो पाठ फ़ाइलों से आती है।

Correlator-O0 to -O1-O1 to -O2
Exact Symbol Name Match4 functions4 functions, 5 data items (labels.rel, .L.str.1 to .L.str.4)
Exact Data Match00
Exact Function Bytes Match02 (percent_change, grade_label)
Exact Function Instructions Match03 (adds grade)
Exact Function Mnemonics Match03
Duplicate Function Instructions Match00

प्रत्येक फ़ंक्शन के बीच बदल गया -O0और -O1, तो केवल नामों से मेल खाया, जो कि एक परिणाम है कि पाठ के मैच BinDiff क्रम में देता है. प्रत्येक मैच प्रिंट समानता 1.000 और विश्वास 10.000. मदद पृष्ठ सटीक सहसंबंधों को समानता 1.0 और विश्वास 1.0 के रूप में वर्णित करता है, इसलिए प्रिंट विश्वास के पैमाने एक खुला सवाल है इस पाठ रिकॉर्ड करता है और हल नहीं करता है.

कार्यक्रम अंतर, उपकरण के तहत, एक अलग बात है। यह बाइट्स, लेबल, कोड इकाइयों, संदर्भों, टिप्पणियों और कार्यों पर समान पता स्थान के साथ दो कार्यक्रमों की तुलना करता है। यह एक पता-अनुसूचित अंतर है और कुछ भी नहीं जो चला गया है, से मेल खाता है।

डायफोरा और बाइनरी निंजा, उनके दस्तावेज से

डायफोर एक आईडीए प्रो प्लगइन है, जिसे पहली बार 2015 में जारी किया गया था और 2026-08-18 के रूप में संस्करण 3.4.2 पर। यह 2.0 के बाद से AGPL-3.0 है और IDAPython की आवश्यकता है, इसलिए यह IDA होम या IDA प्रो में चलाया जाता है और IDA फ्री में नहीं। यह प्रत्येक डेटाबेस को SQLite में निर्यात करता है और SQL क्वेरी के रूप में अपनी हेरिस्टिक्स चलाता है। प्रत्येक हेरिस्टिक का नाम, बेस्ट, आंशिक या अविश्वसनीय श्रेणी, अनुपात प्रकार और वैकल्पिक ध्वज जैसे SAME_CPU या SLOW है। वर्तमान स्रोत में नाम इस पाठ के चरणों की तरह पढ़ते हैंः बाइट्स हैश, समान पता और एमनेमोनिक्स, समान साफ विधानसभा, एमनेमोनिक्स छोटे-प्रिम-उत्पाद, समान नोड्स, किनारे, लूप और दृढ़ता से जुड़े घटक, टोपोलॉजिकल सॉर्ट हैश, और छद्म कोड धुंधली हैश जिन्हें हेक्स-रेज डिकोम्पाइलर की आवश्यकता होती है। इसके रिलीज नोट्स में ट्यूनिंग इतिहास दिखाया गया हैः धीमी हेरिस्टिक्स केवल लगभग 2,000 कार्यों के नीचे चलती है, और "समान ग्राफ" अविश्वसनीय श्रेणी में स्थानांतरित हो गया है। यह कदम इस पाठ का चार ब्लॉक का हीरा है, जिसे पैमाने पर देखा जा सकता है।

2026-09-03 में जारी बाइनरी निंजा 6.0, प्रदाताओं और रिज़ॉल्वरों के साथ एक ढांचे के रूप में बाइनरी समानता को जोड़ा। यह एक संरचनात्मक प्रदाता के रूप में BinDiff और WARP को सटीक कार्य मैचों के लिए भेजता है जो स्थानांतरित करने योग्य ऑपरेन्डों को सहन करते हैं, और इसका गाइड कहता है कि WARP का उपयोग करें जब कार्य स्थानांतरित करने योग्य निर्देशों के अलावा मैच करते हैं और BinDiff जब वे पुनः संकलन के बाद संरचनात्मक रूप से संबंधित रहते हैं। यह सुविधा केवल अंतिम संस्करण में है। द्विआधारी निंजा में कोई पैकेज प्रबंधक स्थापित नहीं है और चलाया नहीं गया था, इसलिए यह पैराग्राफ इसके प्रलेखन से आता है और कुछ नहीं।

BinDiff खुद Apache 2.0 के तहत 2023-09-25 से ओपन सोर्स है, जिसमें नवीनतम संस्करण v8 है। इसके लिए एक डिसाम्बलर और BinExport प्लगइन की आवश्यकता है, जो IDA Pro 9.4 या बाद का समर्थन करता है, द्विआधारी निंजा और गिड्रा। एक सीखने के लिए मुफ्त मार्ग गिड्रा प्लस बिनएक्सपोर्ट प्लस बिनडिफ कमांड लाइन है। पाठ ने इसे नहीं चलाया, और इसकी प्रैक्टिस लैब आपसे पूछती है।

एक ही कोड, अलग-अलग निरंतर

पाठ 36 एक उम्मीदवार पुनर्निर्माण के लिए रखा gradeजिसका तालिका में अंतिम प्रविष्टि के रूप में 3 है, जहां मूल में 4 है। grade_case10_wrong.oके रूप में एक ही 46 कोड बाइट्स है gradeपर-O1. मैचर्स उन्हें प्रत्येक हस्ताक्षर के साथ सटीक बाइट पर जोड़ता है। संदर्भित तालिका चेक पढ़ता है1, 2, 3, 4, 4एक स्थानांतरण के माध्यम से और 1, 2, 3, 4, 3अन्य और रिपोर्ट के माध्यम से dataEqual: false. . . बाकी तीनों .-O1कार्यों को बाएं पर अद्वितीय हैं, क्योंकि उम्मीदवार वस्तु एक समारोह है.

यह पैच-विश्लेषण आकार है। एक फ़ंक्शन भिन्नता जो बाइट्स पर रुकती है, कहती है कि कुछ भी नहीं बदला गया है। गिदरा का सटीक डेटा मैच और बिनडिफ़ का स्ट्रिंग-रिफरेंस मैचिंग एक ही कारण से मौजूद है। पाठ का संस्करण छोटा हैः प्रत्येक मैच किए गए जोड़े के लिए, बाइट्स की तुलना करें प्रत्येक फ़ंक्शन के स्थानांतरण बिंदु पर, सीमाओं से गिनती और भार से चौड़ाई की जांच के साथ।

प्रतीकात्मक निष्पादनः पथ, शर्तें, समाधान

किंग ने 1976 में प्रतीकात्मक निष्पादन का वर्णन किया। इनपुट प्रतीक बन जाते हैं। प्रत्येक कथन एक प्रतीकात्मक भंडार को अपडेट करता है। प्रत्येक शाखा पथ में एक शर्त जोड़ती है, और एक समाधानकर्ता यह तय करता है कि पथ व्यवहार्य है या नहीं और इसके बाद एक ठोस इनपुट उत्पन्न करता है। शाखाओं के साथ एक फ़ंक्शन पथ का पेड़ बन जाता है, और एक पत्ती एक शर्त संलग्न के साथ वापसी है।

बाल्डोनी, कॉपा, डी'एलिया, डेमटेरेस्कु और फिनोची ने 2018 में क्षेत्र का सर्वेक्षण किया। उनका खंड 5 केंद्रीय लागत के रूप में पथ विस्फोट का नाम देता हैः एक निष्पादक प्रत्येक शाखा पर फोर्क कर सकता है, इसलिए शाखाओं की संख्या में राज्य संख्या तेजी से बढ़ सकती है, और एक लूप जिसका सीमा प्रतीकात्मक इनपुट पर निर्भर करती है, पथों का एक असीमित सेट देती है। वे सूचीबद्ध कम करने प्रत्येक शाखा पर हल करके अपूर्ण पथों को काट रहे हैं, कार्यों और लूप के लिए सारांश, राज्य विलय, और अंडर-अप्रोक्सिमेशन। कॉनकोलिक निष्पादन एक ही समय में प्रोग्राम को ठोस और प्रतीकात्मक रूप से चलाता है, कंक्रीट रन के साथ स्थितियों को रिकॉर्ड करता है, एक को नकारता है, और अगले इनपुट के लिए समाधानकर्ता से पूछता है। DART (2005), CUTE (2005), और SAGE (2008) नामित प्रणाली हैं।

KLEE (Cadar, Dunbar, Engler, OSDI 2008) LLVM बिटकोड पर एक प्रतीकात्मक आभासी मशीन है, इसलिए इसका इनपुट clang -emit-llvmयह एक POSIX पर्यावरण मॉडल और एक रिप्ले लाइब्रेरी भेजता है। 89 GNU कोरियूल प्रोग्राम पर यह डेवलपर्स के परीक्षणों के लिए 67.7% के खिलाफ 84.5% लाइन कवरेज तक पहुंच गया और 56 गंभीर बग पाए। KLEE 3.2 को NCSA लाइसेंस के तहत 2025-12-23 में जारी किया गया था, जिसमें LLVM 16 की सिफारिश की गई थी।

Angr बाइनरी पर काम करता है। angr.Projectएक CLE लोडर है जो वस्तु का नक्शा बनाता है और स्थानांतरण लागू करता है, एक लिफ्टर जो एक ब्लॉक को VEX IR में बदल देता है (block.vex) के विकल्प के रूप में पाइपकोड के साथ, और राज्यों के लिए एक कारखाना।SimStateरजिस्टर, स्मृति और एक हल करता है।SimulationManagerराज्यों के चरणों के भंडार नामित active,deadended,found,avoidedऔर erroredऔर explore(find=..., avoid=...)यह एक चरण के लिए इंजन क्रम में चल रहे हैंः विफलता, सिस्कल, हुक, ठोस डेटा के लिए युनिकॉर्न, और VEX के रूप में बैकअप। स्पष्टीकरण Z3 पर सॉल्वर फ्रंट एंड है, और 10.0 में यह एक स्वैच्छिक रस्ट कार्यान्वयन है जो आयात किया गया है।from angr import claripy. angr 10.0.3 को 2026-10-10 पर अपलोड किया गया था, यह BSD-2-Clause है, और Python 3.12 या बाद की आवश्यकता है। Z3 5.1.0, MIT के तहत 2026-08-16 में जारी किया गया, angr, Triton और KLEE के वैकल्पिक बैकेंड के पीछे समाधान है।

पाठ 34 IR पर एक छोटा-सा निष्पादक

code/main.pyपाठ 34 के कथन के आकार के साथ एक छोटी आईआर का उपयोग करता हैः Assign,Branch,Jump,Return, प्लस Switchपाठ 34 के अभ्यास प्रयोगशाला के लिए अनुरोध किया है कि टर्मिनटर.Const,Var,Binचौड़ाई के साथ, Cast,Loadएक नामित कंक्रीट मेज से, और Not. चार फिक्स्चर फ़ंक्शंस को सरलता के बाद स्तर 34 तक पहुंचते समय हाथ से उठाया जाता है, जहां 0x66666667गुणा हो गया है score / 10, और प्रत्येक आईआर ब्लॉक निर्देश पते सूचीबद्ध है कि यह आया था से.check_ir_against_listing()यह दावा करता है कि पते कार्य की सूची को एक बार कवर करते हैं।

gradeपर-O0उस आईआर मेंः

output
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 के समान स्थानान्तरण अंकगणित, तो आईआर फिक्स्चर पढ़ता है।

execute()एक राज्य में वर्तमान ब्लॉक, ब्लॉक के निशान, स्थिति सूची और एक वातावरण है जो इनपुट पर प्रत्येक चर को अभिव्यक्ति के लिए मैप करता है। Assignपर्यावरण को स्रोत में बदल देता है और परिणाम को संग्रहीत करता है। Branchएक तरफ समाधानकर्ता संतुष्ट नहीं कर सकता है, जो कि सर्वेक्षण का वर्णन करता है जो उत्सुक कटिंग है। Switchप्रवेश समीकरणों के विच्छेदन के साथ लक्ष्य और कांटे के आधार पर तालिका प्रविष्टियों को एक बार समूहित करता है, जो कि प्रतीकात्मक कूद लक्ष्य को भी एंगर का इलाज करता है। Returnएक निशान जो कदम सीमा से अधिक लंबा है, मार्ग को काटकर उसे रोकता है।

मार्ग पर चलो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. यह प्रत्येक इनपुट पर एक परिमित डोमेन रखता है, डोमेन के उत्पाद को सूचीबद्ध करता है, और सी अर्थशास्त्र के साथ प्रत्येक प्रतिबंध का मूल्यांकन करता हैः 32-बिट रैपरॉउंड, ट्रंकिंग डिवीजन, हस्ताक्षरित और अनसिनो किए गए तुलनाएं, और अंकगणितीय या तार्किक बदलाव। शून्य से विभाजन या तालिका से बाहर एक तालिका सूचकांक इस असाइनमेंट को प्रतिबंध से बाहर रखता है।score-200 से 1200 तक के पांच पथgradeइनपुट सेट के लिए प्रत्येक पत्ती को हल करने से यह मिलता हैः

LeafReturnsConditionScores in the bound
0x764!(q >u 4) && (q == 3 || q == 4)90 to 109, 20 inputs
0x7f3!(q >u 4) && q == 280 to 89, 10 inputs
0x882!(q >u 4) && q == 170 to 79, 10 inputs
0x911!(q >u 4) && q == 060 to 69, 10 inputs
0x9a0q >u 41,351 inputs, the rest of the bound

qscore / 10 - 6. वही कक्षाएं निकलती हैं gradeपर-O1, जहां आईआर दो पथ है, तालिका पथ लौटने lookup_14[q]और डिफ़ॉल्ट पथ 0 लौटता है, और प्रश्न लौटा मूल्य पर एक प्रतिबंध बन जाता है, क्योंकि वहाँ कोई मामला ब्लॉक तक पहुँचने के लिए नहीं है। तालिका lookup_14वस्तु के से पढ़ी जाती है .rodata0x14 पर।

सीमा विधि की सीमा है। सीमा खोज अपने डोमेन के अंदर पूरी होती है और इसके बाहर चुप रहती है। -200 से 1200 के भीतर 60 से 109 में कोई स्कोर 0 देता है और कोई स्कोर 110 या उससे अधिक का कोई स्कोर शून्य से बाहर का मान देता है। z3 सभी 2^32 स्कोर के लिए दोनों साबित करता है, और अगले खंड में दिखाया गया है कि दोनों विधियां अलग-अलग गवाहों को कहां लौटाती हैं।

पथ विस्फोट मापा गया

totalपर-O1पाठ 33 की लूप है: एक परीक्षण पर count, एक लूप शरीर जो जोड़ता है values[rdx]और वृद्धि rdx, और एक jneशरीर में वापस जबकि rdx != rcx. IR में rcxहै zext64(count)और rdx0 से शुरू होता है। प्रत्येक पीछे के किनारे के माध्यम से गुजरता है फोरक्स पर rdx != countके साथrdxएक स्थिर, तो पथ के लिए count = cशरीर चलाता है cसमय और बाहर निकलने के साथ।count0 से 2 तक सीमित, निष्पादक 3 पथ पाता है। 0 से 4 तक यह 5 पाता है, और 0 से 8 तक यह 9 पाता है। प्रत्येक पथ अपनी गिनती का त्रिकोणात्मक योग लौटाता हैः (0, 0), (1, 1), (2, 3), तक (8, 36). angr रिपोर्ट 3, 5 और 9 मृत राज्यों और समान नौ गिनती और योग जोड़े सभी तीन अनुकूलन स्तरों पर, सहित-O2, जिसका वेक्टर लूप को कम से कम 8 की गिनती की आवश्यकता होती है और इसलिए इस सीमा में पथ की गिनती कभी नहीं बदलती है।

बिना किसी बंधन के निष्पादक कभी खत्म नहीं होता है, क्योंकि प्रत्येक पुनरावृत्ति गणना एक और व्यवहार्य पथ है। पाठ की सीमा 24 ब्लॉक प्रति पथ, के साथ चलें count64, 22 पथ वापस करता है, 2 को छोटा करता है, और 65 में से अन्य 41 को कभी शुरू नहीं करता है जो मौजूद हैं। रिपोर्ट उन तीन संख्याओं को देता है। समाधान लागत भी बढ़ जाती हैः 33 मूल्यांकन लाइन 2, 115 पर 4, 531 पर 8, और 6,900 के लिए सीमित रन।

angr और z3 पर समान प्रश्न

capture_angr.pyतीन वस्तुओं पर 10.0.3 angr चलाया। CLE प्रत्येक स्थानांतरित करने योग्य वस्तु को 0x400000 पर ELF बैकेंड के साथ लोड किया, 13 स्थानांतरण लागू किए गए।-O0और अन्य के लिए 8 और चार प्रतीकों को हल किया।gradeएक प्रतीकात्मक 64-बिट तर्क के साथ, run()5 राज्यों के साथ समाप्त हो गया।-O0और 2 पर -O1और -O2, 0.475, 0.408, और 0.318 सेकंड में। जोड़ना eax == vप्रत्येक स्थगित राज्य के लिए और हल करने वाले से हस्ताक्षरित न्यूनतम और अधिकतम के लिए पूछने के लिए 60 से 69, 70 से 79, 80 से 89, और 90 से 109 के लिए दिया vप्रत्येक स्तर पर 1 से 4 तक, और -2147483648 से 2147483647 तक 0. दोनों क्रॉस चेक पूरा नहीं हुए।

पहुँच-ए-ब्लॉक फॉर्म में CFGFast पर इस्तेमाल किया गया था gradeपर-O0, जो आठ ब्लॉक पाठ 33 पाया सूचीबद्ध करता है, तो explore(find=0x400076)यह एक स्थिति मिली जिसमें तीन अभी भी 0.47 सेकंड में सक्रिय हैं, तर्क और नमूने 91, 93, 94, 97 और 101 पर न्यूनतम 90 और अधिकतम 109 के साथ।

के लिएpercent_change, दो अस्थिर राज्यों के साथ प्रतिबंधोंbefore[31:0] != 0और before[31:0] == 0. शून्य राज्य के लिए पूछना eax == 50दिया before = 21055744, after = 332315210पर-O0,40566804, 834296877पर-O1और -24484867, 993934694पर-O2- 16 से 16 के बीच सीमित खोज उत्तरों मेंbefore = -10, after = -15. z3, पाठ 34 सूचीबद्ध करने पर एक ही प्रश्न पूछा, उत्तर before = -25092599, after = 305712160. परीक्षण सूट आईआर मूल्यांकनकर्ता के साथ सभी पांच जोड़े का मूल्यांकन करता है और प्रत्येक 50 देता है। एक मॉडल साबित करता है कि एक इनपुट मौजूद है। यह इनपुट नहीं है, और तीन सही उपकरण तीन अलग-अलग दिए।

capture_z3.py-O1grade32 बिट बिट वेक्टर में गुणा, दो शिफ्ट, और तालिका के साथ, और चार और प्रश्न पूछता है। सूची स्रोत से अलग है switchकुछ 32-बिट स्कोर के लिएः 0.068 सेकंड में सेट नहीं किया गया, इसलिए संकलित फ़ंक्शन सभी 2^32 इनपुट पर स्रोत के बराबर है। सूची पाठ 36 की सीमा पुनर्निर्माण से भिन्न हैः स्कोर 706346536 पर सेट किया गया, जहां score / 10यह 70634653 है और स्विच डिफ़ॉल्ट में गिर जाता है जबकि सीमाएं वापस आती हैं 4. 0 से 109 तक सीमित एक ही अंतरः अनसेट, यही कारण है कि पाठ 36 के ग्रिड इसे नहीं देख सका।percent_change,before == 3परिणाम -133 के साथ बैठता है after = 1073741823, पाठ 36 के ओवरफ्लो सेल, और सीमित खोज अपने डोमेन के भीतर एक दूसरे गवाह पाता है,after = -1, जहां (-1 - 3) * 100 / 3-133 तक कम हो जाता है, बिना किसी अतिप्रवाह के।

इसे बनाओ

डेमो चलाएँः

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

आउटपुट एक JSON रिपोर्ट है। diffsऑब्जेक्ट फ़ाइल और लोड छवि के लिए मैच रखता है -O0-O1और -O1-O2, प्लस -O0BinDiff क्रम में जोड़ी। toolComparisonप्रत्येक कार्य के लिए रेडिफ2 निर्णय और अनुपात और गिद्रा सहसंबंध के साथ पाठ का चरण रखता है। patchgrade_case10_wrong.oमामला।radare2Ratiosरडफ़2 संख्याओं को पुनः प्रस्तुत करता है, 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. नाम चरण चलाएं और तुलना करें। जब बिल्ड में प्रतीक हैं, तो बिनडीफ क्रम चलाएं और केवल चरणों को ग्रेड करने के लिए संरचनात्मक परिणाम का उपयोग करें।
  6. जब कोई उपकरण अनुपात रिपोर्ट करता है, तो आप अपनी तुलना करने से पहले पता करें कि इसमें कौन से बाइट्स गए हैं।
  7. फ़ंक्शन के लिए जिसका इनपुट आप चाहते हैं, प्रति कथन एक पता के साथ आईआर लिखें, चलाएँ execute()प्रत्येक प्रतीकात्मक लूप काउंटर पर एक सीमा के साथ, और प्रत्येक पत्ती हल. परिणाम के साथ सीमा की रिपोर्ट.
  8. जब वे उपलब्ध हों तो एक ही क्वेरी को angr या z3 के माध्यम से चलाएं और कक्षा सीमाओं की तुलना करें। एक नमूना एक मॉडल है।

इंटरैक्टिव लैब

लैब ए: हाथ से पांच हस्ताक्षर

codeनिर्देशिका, खुला पायथनः

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

दौड़ें:

python
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()

आप प्रिंट करने से पहले फ़ंक्शन के 0x26 ऑफसेट पर चार बाइट्स लिखें grade.raw. फिर वही पंक्तियाँ चलाएँ gradeसेledger-x86_64-O0.oऔर गिनती tableकगार में grade.edges. .

लैब बीः स्थानांतरण को बाइट हैश तोड़ने के लिए देखो

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

गणना 0x100110 + 0x14 - 0x10003aपढ़ने से पहले कागज परdisplacements. फिर आधार में बदल load_image()0x400000 पर और पुष्टि करें कि विस्थापन नहीं बदलते हैं, क्योंकि दोनों ऑपरेन्ड एक साथ चलते हैं।

लैब सी: गलत मिलान और क्रम जो इससे बचा है

python
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और दो डिग्री अनुक्रमों को पढ़ें. फिर एक छठा चरण लिखें जो क्रमबद्ध mnemonics हैश करता है, तो आदेश अब मायने नहीं रखता है, और देखें कि यह उन्हें अलग करता है या नहीं.

लैब डी: पथ और सीमा

python
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_DOMAINrange(0, 110)और फिर से चला grade_paths("O0"). 0 के लिए वर्ग 60 इनपुट तक छोटा हो जाता है और दो क्रॉस चेक अभी भी बरकरार है. फिर डोमेन सेट करने के लिएrange(90, 100)और पढ़ें कि किन पत्तियों में कोई मॉडल नहीं है।

अभ्यास प्रयोगशाला

BinDiff को फिक्स्चर पर चलाएं और इसे पहले से ही आपके पास तीन परिणामों के साथ तुलना करें।

आवश्यकताएँः

  • Ghidra 12.1.4 में BinExport एक्सटेंशन स्थापित करें और तीन लेजर प्रोग्राम निर्यात करें। BinExport रिलीज टैग और Ghidra संस्करण रिकॉर्ड करें।
  • BinDiff 8 कमांड लाइन स्थापित करें और उत्पादन -O0बनाम -O1और -O1बनाम -O2केवल समानता विकल्प के साथ परिणाम।
  • प्रति फ़ंक्शन समानता और विश्वास को कैप्चर करें code/fixtures/में सटीक आदेश के साथ build_fixtures.sh. .
  • विस्तार tool_comparison()एक के साथ bindiffस्तंभ और एक परीक्षण जोड़े जो BinDiff के पर मिलान सेट तुलना करता है -O1बनाम -O2सबक के मास्क-बाइट सेट के साथ।
  • एक पैराग्राफ लिखें जिसमें बिनडिफ़ एल्गोरिथ्म का नाम दिया गया हो।gradeऔर क्या यह लोड छवियों की तुलना की।

सफलता का अर्थ है कि डेमो प्रति फ़ंक्शन चार उपकरण स्तंभों को प्रिंट करता है और नए परीक्षण में एक समानता या एक स्पष्ट अंतर का उल्लेख होता है।

पाठ कलाकृतियाँ

इस सबक में शामिल है outputs/skill-binary-diffing-and-symbolic-execution.md. इसका उपयोग दो बिल्ड और एक फ़ंक्शन को स्टेज डिफर में बदलने के लिए प्रति मैच एक घोषित गुणवत्ता के साथ, प्रत्येक असमान या बदलते फ़ंक्शन की व्याख्या, और प्रति पाना और इसे उत्पन्न करने वाली सीमा के साथ एक हल इनपुट सेट के साथ पथ रिपोर्ट के साथ करें।

जाँचें

डेमो और सूट चलाएंः

bash
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पांच ब्लॉक, पांच किनारे, और एक स्वयं लूप है, और इसकी आकार स्ट्रिंग निर्धारक है
  • 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जहां गिदरा ने उन्हें दोनों कार्यक्रमों में रखा
  • R_X86_64_PC32लिखा है S + A - Pऔर विस्थापन देता है 122, और R_X86_64_64 में प्रविष्टियाँ.dataप्राप्त स्ट्रिंग पते
  • gradeबाइट वस्तुओं में सहमत हैं और 0x70 शिफ्ट द्वारा छवियों में भिन्न होते हैं, और मास्किंग मैच को बहाल करता है
  • -O1बनाम -O2सटीक बाइट पर तीन कार्यों से मेल खाता है और totalनाम से; छवि दृश्य मेल खाता है grade1 - 1/46 समानता वाले छिपे बाइट्स द्वारा
  • पाठ क्रम पर एक झूठी प्रवाह ग्राफ आकार मैच उत्पन्न करता है -O0बनाम -O1, और BinDiff आदेश सभी चार नाम से मेल खाता है
  • पैच उम्मीदवार बाइट्स पर मेल खाता है और संदर्भित डेटा पर विफल रहता है
  • लेवेंसस्टाइन अनुपात 0.130435, 0.106061, 0.269841, 0.171429, 0.426829 पर 82 बाइट्स, और स्थानांतरित-बाइट्स अनुपात को पुनः प्राप्त करता है
  • radiff2 का MATCH सेट exact-byte चरण के बराबर है, और Ghidra के byte और निर्देश सहसंबंधी चित्र दृश्य के सटीक और मास्क सेट के बराबर है
  • गिदरा ने केवल नाम पाया।-O0बनाम -O1, प्रत्येक मैच पर समानता 1.0 और विश्वास 10.0 के साथ
  • हाथ से उठाए गए आईआर सूचीबद्ध प्रत्येक निर्देश को एक बार कवर करता है, और मूल्यांकनकर्ता सी अर्थशास्त्र का पालन करता है
  • grade-O0स्विच की स्थिति के साथ और दो पर -O1समान वर्गों के साथ
  • सीमावर्ती वर्ग 60 से 69, 70 से 79, 80 से 89, 90 से 109 सभी तीन स्तरों और z3 पर समान angr's, 5 और 2 सीमावर्ती राज्यों और 90 से 109 तक पहुंच-एक ब्लॉक रेंज के साथ
  • दो क्रॉस चेक में बॉन्ड, एंग्र या z3 में कोई मॉडल नहीं है, और z3 सूचकांक स्रोत स्विच के बराबर साबित करता है
  • हर percent_changeसीमांत खोज, एएनजीआर, और जेड 3 से मॉडल अनुरोधित मान तक मूल्यांकन करता है
  • total3, 5, 9 मार्गों के साथ त्रिकोणात्मक योगों, angr के समान देता है, और कदम टोपी 22 वापस आता है और 2 ट्रंक करता है
  • आंकड़ा डेटा दोनों दृश्यों, स्थानांतरण संख्याओं और पांच पत्तियों के साथ उनके इनपुट सेटों को रखता है, और साइट मॉड्यूल में समान डेटा शामिल हैं

उत्पादन विफलता मोड

FailureWhat the weak tool reportsWhat the analysis must prove
Byte hash on a loaded image"grade modified" between two builds with identical codeThe field offset, the two displacements, and the section shift; the masked hash matches
Masked hash on a relocatable object"masking made no difference"The fields were already zero; the relocation records and the referenced constants carry the change
Flow-graph shape aloneA confident pair of unrelated functionsA second signature agrees, or the names contradict and the match is dropped
Names before structure on a stripped buildNothing matchesThe structural stages with their qualities, and the unmatched list
A ratio compared across tools"radiff2 says 0.43 and the lesson says 0.30"Which bytes each side fingerprinted; 82 bytes without relocations, 118 with
Same code, different constant"exact match"The table read through the relocation and the bounds check
One model reported as the input"the score is 90"The class 90 to 109 with its count, and the bound it was found in
Bounded search reported as unsat"no input gives -133"Unsat inside the bound only; z3 finds 1073741823 outside it
Symbolic loop without a boundA timeoutThe bound or the cap, the paths returned, truncated, and never started
Closed tool described as runNumbers with no captureA capture file with the command and version, or a sentence saying documentation only

परिचालन नियम

एक बार में एक हस्ताक्षर पर मैच करें, दोनों तरफ केवल अद्वितीय मान स्वीकार करें, और मैच के साथ मंच और इसकी गुणवत्ता बनाए रखें। वस्तुओं और लोड की गई छवियों को अलग करें और दोनों के बीच चरण बदलने वाले प्रत्येक फ़ंक्शन की व्याख्या करें। प्रत्येक शाखा पर एक हलकर्ता के साथ पथों को सूचीबद्ध करें, प्रत्येक प्रतीकात्मक लूप को बांटें, और इसके बॉन्ड के साथ एक इनपुट सेट की रिपोर्ट करें। एक सीमा के बिना एक एकल मॉडल एक नमूना है।

आगे पढ़ना

This free lesson is part of the AI Engineering from Scratch curriculum. Read the full explanation, run the lesson code, and verify the result in the interactive reader or from the repository source.

Browse the complete course catalog or open this lesson on GitHub.