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

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

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")