⚠️ परियोजना संग्रहित है ⚠️

यह परियोजना अब आंतरिक रूप से विकसित या अनुरक्षित नहीं की जा रही है।

Manticore

Manticore, स्मार्ट कॉन्ट्रैक्ट्स और बाइनरीज़ के विश्लेषण के लिए एक प्रतीकात्मक निष्पादन (symbolic execution) उपकरण है।

विशेषताएँ

• प्रोग्राम अन्वेषण: Manticore प्रोग्राम को प्रतीकात्मक इनपुट के साथ निष्पादित कर सकता है और उन सभी संभावित स्थितियों का पता लगा सकता है जिन तक वह पहुँच सकता है
• इनपुट निर्माण: Manticore स्वचालित रूप से ठोस इनपुट उत्पन्न कर सकता है जो किसी दिए गए प्रोग्राम स्थिति में परिणामित होते हैं
• त्रुटि खोज: Manticore बाइनरीज़ और स्मार्ट कॉन्ट्रैक्ट्स में क्रैश और अन्य विफलता मामलों का पता लगा सकता है
• इंस्ट्रुमेंटेशन: Manticore इवेंट कॉलबैक और इंस्ट्रक्शन हुक के माध्यम से स्थिति अन्वेषण पर सूक्ष्म-नियंत्रण प्रदान करता है
• प्रोग्रामेटिक इंटरफ़ेस: Manticore Python API के माध्यम से अपने विश्लेषण इंजन तक प्रोग्रामेटिक पहुँच प्रदान करता है

Manticore निम्नलिखित प्रकार के प्रोग्रामों का विश्लेषण कर सकता है:

• Ethereum स्मार्ट कॉन्ट्रैक्ट्स (EVM बाइटकोड)
• Linux ELF बाइनरीज़ (x86, x86_64, aarch64 और ARMv7)
• WASM मॉड्यूल

स्थापना

नोट: हम अन्य परियोजनाओं या पैकेजों के साथ विरोध को रोकने के लिए Manticore को वर्चुअल वातावरण में स्थापित करने की अनुशंसा करते हैं

विकल्प 1: PyPI से स्थापित करना:

pip install manticore

विकल्प 2: PyPI से स्थापित करना, मूल बाइनरीज़ को निष्पादित करने के लिए आवश्यक अतिरिक्त निर्भरताओं के साथ:

pip install "manticore[native]"

विकल्प 3: नाइटली डेवलपमेंट बिल्ड स्थापित करना:

pip install --pre "manticore[native]"

विकल्प 4: master शाखा से स्थापित करना:

git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"

विकल्प 5: Docker के माध्यम से स्थापित करना:

docker pull trailofbits/manticore

एक बार स्थापित होने के बाद, manticore CLI टूल और Python API उपलब्ध होंगे।

डेवलपमेंट स्थापना के लिए, हमारा विकी देखें।

उपयोग

CLI

Manticore में एक कमांड लाइन इंटरफ़ेस है जो किसी बाइनरी या स्मार्ट कॉन्ट्रैक्ट का बुनियादी प्रतीकात्मक विश्लेषण कर सकता है। विश्लेषण परिणाम mcore_ से शुरू होने वाली एक कार्यक्षेत्र निर्देशिका में रखे जाएँगे। कार्यक्षेत्र के बारे में जानकारी के लिए, विकी देखें।

EVM

Manticore CLI स्वचालित रूप से पहचान लेता है कि आप एक कॉन्ट्रैक्ट का परीक्षण करने का प्रयास कर रहे हैं यदि (उदाहरण के लिए) कॉन्ट्रैक्ट में .sol या .vy एक्सटेंशन है। एक डेमो देखें।

$ manticore examples/evm/umd_example.sol 
 [9921] m.main:INFO: Registered plugins: DetectUninitializedMemory, DetectReentrancySimple, DetectExternalCallAndLeak, ...
 [9921] m.e.manticore:INFO: Starting symbolic create contract
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 0
 [9921] m.e.manticore:INFO: 4 alive states, 6 terminated states
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 1
 [9921] m.e.manticore:INFO: 16 alive states, 22 terminated states
[13761] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
[13754] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
...
[13743] m.c.manticore:INFO: Generated testcase No. 36 - THROW(3 txs)
[13740] m.c.manticore:INFO: Generated testcase No. 37 - THROW(3 txs)
[9921] m.c.manticore:INFO: Results in ~/manticore/mcore_gsncmlgx

Manticore-verifier

एक वैकल्पिक CLI टूल प्रदान किया गया है जो कॉन्ट्रैक्ट परीक्षण को सरल बनाता है और गुण विधियों को उसी उच्च-स्तरीय भाषा में लिखने की अनुमति देता है जिसका कॉन्ट्रैक्ट उपयोग करता है। Manticore-verifier दस्तावेज़ीकरण देखें। एक डेमो देखें

Native

$ manticore examples/linux/basic
[9507] m.n.manticore:INFO: Loading program examples/linux/basic
[9507] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Results in ~/manticore/mcore_7u7hgfay
[9507] m.n.manticore:INFO: Total time: 2.8029580116271973

API

Manticore एक Python प्रोग्रामिंग इंटरफ़ेस प्रदान करता है जिसका उपयोग शक्तिशाली कस्टम विश्लेषणों को लागू करने के लिए किया जा सकता है।

EVM

Ethereum स्मार्ट कॉन्ट्रैक्ट्स के लिए, API का उपयोग स्वेच्छ कॉन्ट्रैक्ट गुणों के विस्तृत सत्यापन के लिए किया जा सकता है। उपयोगकर्ता प्रारंभिक स्थितियाँ निर्धारित कर सकते हैं, प्रतीकात्मक लेन-देन निष्पादित कर सकते हैं, और फिर एक कॉन्ट्रैक्ट के लिए अपरिवर्तनीयताएँ सुनिश्चित करने के लिए खोजी गई स्थितियों की समीक्षा कर सकते हैं।

from manticore.ethereum import ManticoreEVM
contract_src="""
contract Adder {
    function incremented(uint value) public returns (uint){
        if (value == 1)
            revert();
        return value + 1;
    }
}
"""
m = ManticoreEVM()

user_account = m.create_account(balance=10000000)
contract_account = m.solidity_create_contract(contract_src,
                                              owner=user_account,
                                              balance=0)
value = m.make_symbolic_value()

contract_account.incremented(value)

for state in m.ready_states:
    print("can value be 1? {}".format(state.can_be_true(value == 1)))
    print("can value be 200? {}".format(state.can_be_true(value == 200)))

Native

API का उपयोग Linux बाइनरीज़ के लिए कस्टम विश्लेषण उपकरण बनाने के लिए भी संभव है। प्रारंभिक स्थिति को अनुकूलित करने से स्थिति विस्फोट समस्याओं से बचने में मदद मिलती है जो अक्सर CLI का उपयोग करते समय होती हैं।

# example Manticore script
from manticore.native import Manticore

m = Manticore.linux('./example')

@m.hook(0x400ca0)
def hook(state):
  cpu = state.cpu
  print('eax', cpu.EAX)
  print(cpu.read_int(cpu.ESP))

  m.kill()  # tell Manticore to stop

m.run()

WASM

Manticore प्रतीकात्मक इनपुट पर WebAssembly फ़ंक्शनों का मूल्यांकन भी गुण सत्यापन या सामान्य विश्लेषण के लिए कर सकता है।

from manticore.wasm import ManticoreWASM

m = ManticoreWASM("collatz.wasm")

def arg_gen(state):
    # Generate a symbolic argument to pass to the collatz function.
    # Possible values: 4, 6, 8
    arg = state.new_symbolic_value(32, "collatz_arg")
    state.constrain(arg > 3)
    state.constrain(arg < 9)
    state.constrain(arg % 2 == 0)
    return [arg]


# Run the collatz function with the given argument generator.
m.collatz(arg_gen)

# Manually collect return values
# Prints 2, 3, 8
for idx, val_list in enumerate(m.collect_returns()):
    print("State", idx, "::", val_list[0])

आवश्यकताएँ

• Manticore को Python 3.7 या उससे अधिक की आवश्यकता है
• Manticore आधिकारिक तौर पर Github Actions द्वारा प्रदान किए गए Ubuntu के नवीनतम LTS संस्करण का समर्थन करता है
  • Manticore में MacOS पर EVM और WASM (लेकिन मूल Linux बाइनरी नहीं) के लिए प्रायोगिक समर्थन है
• हम बढ़ी हुई स्टैक आकार के साथ चलाने की अनुशंसा करते हैं। यह ulimit -s 100000 चलाकर या docker run पर --ulimit stack=100000000:100000000 पास करके किया जा सकता है

स्मार्ट कॉन्ट्रैक्ट्स संकलित करना

• Ethereum स्मार्ट कॉन्ट्रैक्ट विश्लेषण के लिए आपके $PATH में solc प्रोग्राम की आवश्यकता है।
• Manticore स्मार्ट कॉन्ट्रैक्ट बनाने के लिए crytic-compile का उपयोग करता है। यदि आपको संकलन संबंधी समस्याएँ आ रही हैं, तो किसी भी समस्या की पहचान करना आसान बनाने के लिए अपने कोड पर सीधे crytic-compile चलाने पर विचार करें।
• हम अभी भी EVM Istanbul निर्देश शब्दार्थ के लिए पूर्ण समर्थन लागू करने की प्रक्रिया में हैं, इसलिए कुछ ऑपकोड समर्थित नहीं हो सकते हैं। मुश्किल में, आप उन निर्देशों को उत्पन्न करने से बचने के लिए Solidity 0.4.x के साथ संकलित करने का प्रयास कर सकते हैं।

एक अलग सॉल्वर का उपयोग करना (Yices, Z3, CVC4)

Manticore smtlib2 का समर्थन करने वाले बाहरी सॉल्वर पर निर्भर करता है। वर्तमान में Z3, Yices और CVC4 समर्थित हैं और उन्हें कमांड-लाइन या कॉन्फ़िगरेशन सेटिंग्स के माध्यम से चुना जा सकता है। यदि Yices उपलब्ध है, तो Manticore डिफ़ॉल्ट रूप से इसका उपयोग करेगा। यदि नहीं, तो यह Z3 या CVC4 पर वापस आ जाएगा। यदि आप मैन्युअल रूप से चुनना चाहते हैं कि किस सॉल्वर का उपयोग करना है, तो आप इसे इस तरह कर सकते हैं: manticore --smt.solver Z3

CVC4 स्थापित करना

अधिक विवरण के लिए https://cvc4.github.io/ पर जाएँ। अन्यथा, बस बाइनरी प्राप्त करें और इसका उपयोग करें।

    sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
    sudo chmod +x /usr/bin/cvc4

Yices स्थापित करना

Yices अविश्वसनीय रूप से तेज़ है। अधिक विवरण यहाँ https://yices.csl.sri.com/

    sudo add-apt-repository ppa:sri-csl/formal-methods
    sudo apt-get update
    sudo apt-get install yices2

सहायता प्राप्त करना

Manticore का उपयोग करने या विस्तारित करने में सहायता के लिए कृपया Empire Hacking में हमारे #manticore स्लैक चैनल पर आएँ।

दस्तावेज़ीकरण कई स्थानों पर उपलब्ध है:

• विकी में Manticore के साथ शुरुआत करने और योगदान देने के बारे में जानकारी है

• API संदर्भ में हमारे API पर अधिक गहन और गहन दस्तावेज़ीकरण है

• उदाहरण निर्देशिका में कुछ छोटे उदाहरण हैं जो API सुविधाओं को प्रदर्शित करते हैं

• manticore-examples रिपॉजिटरी में कुछ अधिक जटिल उदाहरण हैं, जिनमें कुछ वास्तविक CTF समस्याएँ शामिल हैं

यदि आप बग रिपोर्ट या फीचर अनुरोध दर्ज करना चाहते हैं, तो कृपया हमारे मुद्दे पृष्ठ का उपयोग करें।

प्रश्नों और स्पष्टीकरण के लिए, कृपया चर्चा पृष्ठ पर जाएँ।

लाइसेंस

Manticore AGPLv3 लाइसेंस के तहत लाइसेंस प्राप्त और वितरित है। यदि आप शर्तों के अपवाद की तलाश में हैं तो हमसे संपर्क करें।

प्रकाशन

• Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts, Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, Artem Dinaburg - ASE 19

यदि आप अकादमिक कार्य में Manticore का उपयोग कर रहे हैं, तो Crytic $10k Research Prize के लिए आवेदन करने पर विचार करें।

ASE 2019 से डेमो वीडियो

टूल एकीकरण

• MATE: Merged Analysis To prevent Exploits
  • Mantiserve: Manticore इंस्टेंस को शुरू करने, मारने और जाँचने के लिए REST API के साथ इंटरैक्शन
  • Dwarfcore: अन्वेषण के दौरान Mantiserve इंजन के भीतर उपयोग के लिए प्लगइन्स और डिटेक्टर
  • अंडर-कॉन्स्ट्रेंड प्रतीकात्मक निष्पादन Manticore के साथ एकल फ़ंक्शनों का प्रतीकात्मक रूप से अन्वेषण करने के लिए इंटरफ़ेस