SiMBA

SiMBA रैखिक मिश्रित बूलियन-अंकगणितीय व्यंजकों (MBAs) के सरलीकरण के लिए एक उपकरण है। MBA-Blast और MBA-Solver की तरह, यह पूरी तरह से बीजगणितीय दृष्टिकोण का उपयोग करता है जो इस विचार पर आधारित है कि एक रैखिक MBA अपने मानों द्वारा शून्य और एक के सेट पर पूरी तरह से निर्धारित होता है, लेकिन नई अंतर्दृष्टि का लाभ उठाते हुए कि इसके लिए 1-बिट-स्पेस में परिवर्तन आवश्यक नहीं है।

यह निम्नलिखित पेपर पर आधारित है:

@inproceedings{simba2022,
    author = {Reichenwallner, Benjamin and Meerwald-Stadler, Peter},
    title = {Efficient deobfuscation of linear mixed Boolean-arithmetic expressions},
    year = {2022},
    month = nov,
    address = {Los Angeles, CA, USA},
    date = {November 7 - 11, 2022},
    booktitle = {Proceedings of the CheckMATE 2022 workshop, co-located with the ACM Conference on Computer and Communication Security, CCS'22},
    pages = {19--28},
    doi = {10.1145/3560831.3564256},
    publisher = {ACM},
    howpublished = {\url{https://arxiv.org/abs/2209.06335}}
}

प्रस्तुति की स्लाइड्स और एक वीडियो रिकॉर्डिंग खोजें। ACM के माध्यम से भी उपलब्ध।

सामग्री

दो मुख्य प्रोग्राम (Python 3) प्रदान किए गए हैं:

• एकल रैखिक MBAs के सरलीकरण के लिए simplify.py
• एक फ़ाइल में निहित रैखिक MBAs के एक सेट के सरलीकरण और उनके सत्यापन के लिए simplify_dataset.py, जो इस फ़ाइल में भी निहित संबंधित सरल व्यंजकों के साथ तुलना द्वारा किया जाता है

इसके अतिरिक्त, प्रोग्राम check_linear_mba.py का उपयोग यह जांचने के लिए किया जा सकता है कि व्यंजक रैखिक MBAs का प्रतिनिधित्व करते हैं या नहीं।

उपयोग

एकल व्यंजकों का सरलीकरण

एक एकल व्यंजक expr को सरल बनाने के लिए, उपयोग करें:

python3 src/simplify.py "expr"

वैकल्पिक रूप से, एक बार में कई व्यंजकों को सरल किया जा सकता है, जैसे:

python3 src/simplify.py "x+x" "a&a"

वास्तव में, प्रत्येक कमांड लाइन तर्क जो कोई विकल्प नहीं है, उसे सरल किए जाने वाले व्यंजक के रूप में माना जाता है। ध्यान दें कि उद्धरण चिह्नों को छोड़ने से अवांछित व्यवहार हो सकता है। सरलीकरण परिणाम कमांड लाइन पर निम्नानुसार मुद्रित होते हैं:

*** Expression x+x
*** ... simplified to 2*x
*** Expression a
*** ... simplified to a

डिफ़ॉल्ट रूप से, यह जांच नहीं की जाती कि इनपुट व्यंजक एक रैखिक MBA है या नहीं। इस जांच को वैकल्पिक रूप से विकल्प -l के माध्यम से सक्षम किया जा सकता है:

python3 src/simplify.py "x*x" -l

चूँकि $x*x$ कोई रैखिक MBA नहीं है, इस मामले में निम्नलिखित आउटपुट दिखाई देगा:

*** Expression x*x
Error: Input expression may be no linear MBA: x*x

यदि विकल्प -z का उपयोग किया जाता है, तो सरलीकरण परिणामों को अंततः Z3 का उपयोग करके मूल व्यंजकों के बराबर होने की पुष्टि की जाती है। इसका कमांड लाइन आउटपुट पर कोई प्रभाव नहीं पड़ता है, जब तक कि एल्गोरिदम सही ढंग से काम करता है और इनपुट व्यंजक एक रैखिक MBA है:

python3 src/simplify.py "x*x" -z

यह निम्नलिखित त्रुटि उत्पन्न करेगा:

*** Expression x*x
Error in simplification! Simplified expression is not equivalent to original one!

चूँकि SiMBA के आउटपुट व्यंजकों में होने वाले स्थिरांक हमेशा गैर-ऋणात्मक होते हैं, वे स्थिरांकों के साथ-साथ चरों के लिए उपयोग किए जाने वाले बिट्स की संख्या पर निर्भर हो सकते हैं। यह संख्या डिफ़ॉल्ट रूप से $64$ है और इसे विकल्प -b का उपयोग करके सेट किया जा सकता है:

python3 src/simplify.py "-x" -b 32

बिट्स की संख्या $b$ के लिए, आउटपुट में होने वाले स्थिरांक हमेशा $0$ और $2^b-1$ के बीच होते हैं। इसलिए उपरोक्त कॉल निम्नलिखित आउटपुट देगा:

*** Expression -x
*** ... simplified to 4294967295*x

फ़ाइल से व्यंजकों का सरलीकरण और सत्यापन

पथ path_to_file वाली फ़ाइल में संग्रहीत व्यंजकों को सरल बनाने के लिए, उपयोग करें:

python3 src/simplify_dataset.py -f path_to_file

अर्थात, फ़ाइल को विकल्प -f का उपयोग करके निर्दिष्ट करना होगा। फ़ाइल की प्रत्येक पंक्ति में एक जटिल व्यंजक और एक समतुल्य सरल व्यंजक होना चाहिए, जो अल्पविराम द्वारा अलग किए गए हों, उदाहरण:

example-expressions.txt:

(x&y)+(x|y), x+y
(x|y)-(~x&y)-(x&~y), x&y
-(a|~b)+(~b)+(a&~b)+b, a^b
2*(s&~t)+2*(s^t)-(s|t)+2*~(s^t)-~t-~(s&t), s

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

simplify.py की तरह, रैखिकता जांच के साथ-साथ सही सरलीकरण की जांच को विकल्प -l और -z का उपयोग करके सक्षम किया जा सकता है, और बिट्स की संख्या को विकल्प -b का उपयोग करके निर्दिष्ट किया जा सकता है। यदि कोई निर्दिष्ट फ़ाइल में निहित व्यंजकों की केवल एक निश्चित अधिकतम संख्या पर SiMBA चलाना चाहता है, तो इस अधिकतम संख्या को विकल्प -r के माध्यम से निर्दिष्ट किया जा सकता है:

python3 src/simplify_dataset.py -f some_file.txt -r 2

यदि some_file.txt में ऊपर सूचीबद्ध व्यंजक होंगे, तो उनमें से केवल पहले दो को सरल किया जाएगा:

Simplify expressions from data/some_file.txt ...
  * total count: 2
  * verified: 2
  * equal: 2
  * average duration: 0.00014788552653044462

किसी भी स्थिति में, आउटपुट इसके बारे में जानकारी देता है:

• इनपुट में व्यंजकों की कुल संख्या,
• उन व्यंजकों की संख्या जिन्हें सरलीकरण के बाद Z3 का उपयोग करके संबंधित सरल व्यंजक के समतुल्य सत्यापित किया जा सकता है (जब तक कि सरलीकरण परिणाम में पहले से ही बिल्कुल समान स्ट्रिंग प्रतिनिधित्व न हो),
• उन व्यंजकों की संख्या जो संबंधित सरल व्यंजक के समान ही सरलीकृत होते हैं, और
• सेकंड में औसत रनटाइम।

कृपया ध्यान दें कि Z3 का उपयोग करके सही सरलीकरण का एक वैकल्पिक सत्यापन रनटाइम में योगदान देता है, जबकि जटिल और सरल व्यंजकों के जोड़ों के सरलीकरण परिणामों की तुलना के मामले में ऐसा नहीं है।

डिफ़ॉल्ट रूप से सरलीकरण परिणाम मुद्रित नहीं होते हैं, बल्कि केवल ये आँकड़े प्रस्तुत किए जाते हैं। यदि पूर्व के बारे में जानकारी चाहिए, तो विकल्प -v का उपयोग किया जा सकता है:

python3 src/simplify_dataset.py -f some_file.txt -v

तब निम्नलिखित आउटपुट दिखाया जाएगा:

Simplify expressions from data/some_file.txt ...

    *** 1 groundtruth x+y, simplified x+y => equal: True, verified: True
    *** 2 groundtruth x&y, simplified x&y => equal: True, verified: True
    *** 3 groundtruth a^b, simplified a^b => equal: True, verified: True
    *** 4 groundtruth s, simplified s => equal: True, verified: True

  * total count: 4
  * verified: 4
  * equal: 4
  * average duration: 0.00016793253598734736

एक अन्य विकल्प -e सभी व्यंजकों के आउटपुट को affine फलनों $f(x) = ax+b$ द्वारा यादृच्छिक पूर्णांक $a,b$ के साथ $1$ और $2^b-1$ के बीच एन्कोड करने की संभावना प्रदान करता है, यदि $b$ बिट्स की संख्या है:

python3 src/simplify_dataset.py -f some_file.txt -v -e

बेशक एक ही फलन को एक ही पंक्ति में व्यंजकों के जोड़े पर लागू किया जाता है। यह निम्नलिखित के समान आउटपुट देगा:

Simplify expressions from data/some_file.txt ...

    *** 1 groundtruth 10623056950310032687+5038261596809828791*x+5038261596809828791*y, simplified 10623056950310032687+5038261596809828791*x+5038261596809828791*y => equal: True, verified: True
    *** 2 groundtruth 15181401701264988765+3962868592131193124*(x&y), simplified 15181401701264988765+3962868592131193124*(x&y) => equal: True, verified: True
    *** 3 groundtruth 6812440940417974076+11894131080657788315*(a^b), simplified 6812440940417974076+11894131080657788315*(a^b) => equal: True, verified: True
    *** 4 groundtruth 4558303267887122851+10271005790757592209*s, simplified 4558303267887122851+10271005790757592209*s => equal: True, verified: True

  * total count: 4
  * verified: 4
  * equal: 4
  * average duration: 0.00019435951253399253

पुनरुत्पादन क्षमता

पेपर में बताए गए प्रयोगों के एक भाग के पुनरुत्पादन के लिए, कोई निर्देशिका data/ में निहित किसी भी डेटासेट फ़ाइल का उपयोग कर सकता है। निम्नलिखित प्रत्येक फलन $e_1,\ldots, e_5$ के लिए, $2$, $3$ या $4$ चरों का उपयोग करके $1,000$ समतुल्य रैखिक MBAs के डेटासेट प्रदान किए गए हैं:

• $e_1(x,y) = x+y$
• $e_2 = 49,374$
• $e_3(x) = 3,735,936,685, x + 49,374$
• $e_4(x,y) = 3,735,936,685, (x\mathbin{^\wedge}y) + 49,374$
• $e_5(x) = 3,735,936,685\cdot \mathord{\sim} x$

$e_1$ के लिए, $5$ से $7$ चरों के लिए अतिरिक्त डेटासेट प्रदान किए गए हैं। ये MBAs Zhou et al. द्वारा 2007 में वर्णित विधि के आधार पर एक एल्गोरिदम का उपयोग करके उत्पन्न किए गए हैं और पेपर में वर्णित हैं।

कृपया ध्यान दें कि ये डेटासेट $b=64$ बिट्स के लिए उत्पन्न किए गए हैं। बिट्स की विभिन्न संख्याओं के लिए, $e_i$'s के साथ उनकी समतुल्यता की गारंटी नहीं दी जा सकती है।

आगे के प्रयोगों के पुनरुत्पादन के लिए, हम क्रमशः MBA-Solver रिपॉजिटरी और NeuReduce रिपॉजिटरी द्वारा प्रदान किए गए डेटासेट का संदर्भ लेते हैं।

रैखिकता की जाँच

फ़ाइल check_linear_mba.py का उपयोग सरलीकरणकर्ता द्वारा किया जाता है, लेकिन यह अपना स्वयं का इंटरफ़ेस भी प्रदान करता है, उदाहरण:

python3 src/check_linear_mba.py "x+x" "x*x"

यह कमांड लाइन तर्कों के माध्यम से पारित सभी व्यंजकों की जाँच करता है। इस मामले में यह निम्नलिखित आउटपुट देगा:

*** Expression x+x
*** +++ valid
*** Expression x*x
*** --- not valid

MBAs का प्रारूप

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

• $a$, $b$, $c$, ..., $x$, $y$, $z$, ...
• $v0$, $v1$, $v2$, ...
• $v_0$, $v_1$, $v_2$, ...
• $X0$, $X1$, $X2$, ...
• $var0$, $var1$, $var2$, ...
• $var1a$, $var1b$, $var1c$, ...
• ...

निम्नलिखित ऑपरेटर समर्थित हैं, जो Python में उनकी प्राथमिकता के क्रम में व्यवस्थित हैं:

• $\mathord{\sim}$, $-$: बिटवाइज़ नेगेशन और यूनरी माइनस
• $*$: गुणन
• $+$, $-$: योग और अंतर
• &: संयोजन (conjunction)
• $\mathbin{^\wedge}$: एक्सक्लूसिव विसंयोजन (exclusive disjunction)
• $|$: समावेशी विसंयोजन (inclusive disjunction)

इनपुट व्यंजकों में व्हाइटस्पेस का उपयोग किया जा सकता है। उदाहरण के लिए, व्यंजक "x+y" को वैकल्पिक रूप से "x + y" के रूप में लिखा जा सकता है।

कृपया ऑपरेटरों की प्राथमिकता का सम्मान करें और यदि आवश्यक हो तो कोष्ठक का उपयोग करें! उदाहरण के लिए, व्यंजक $1 + (x|y)$ और $1 + x|y$ समतुल्य नहीं हैं क्योंकि $+$ की प्राथमिकता $|$ से अधिक है। ध्यान दें कि बाद वाला एक रैखिक MBA भी नहीं है।

निर्भरताएँ

SMT सॉल्वर Z3 आवश्यक है:

• simplify_dataset.py द्वारा जहाँ सरलीकृत व्यंजकों को संबंधित सरल व्यंजकों के समतुल्य सत्यापित किया जाता है, और
• simplify.py द्वारा यदि सरलीकृत व्यंजकों का वैकल्पिक सत्यापन उपयोग किया जाता है। यदि इस विकल्प का उपयोग नहीं किया जाता है, तो Z3 स्थापित न होने पर भी कोई त्रुटि नहीं फेंकी जाती है।

Z3 स्थापित करना:

• Github रिपॉजिटरी से: https://github.com/Z3Prover/z3, या
• Debian पर: sudo apt-get install python3-z3

लाइसेंस

कॉपीराइट (c) 2022 Denuvo GmbH, GPLv3 के तहत जारी।

संपर्क

• Benjamin Reichenwallner: benjamin(dot)reichenwallner(at)denuvo(dot)com
• Peter Meerwald-Stadler: peter(dot)meerwald(at)denuvo(dot)com