evm lisa

EVMLISA: เครื่องวิเคราะห์แบบคงที่การตีความแบบนามธรรมสำหรับ EVM bytecode

EVMLISA เป็นเครื่องวิเคราะห์แบบคงที่โดยใช้การตีความแบบนามธรรมสำหรับ EVM Bytecode ของสัญญาอัจฉริยะที่นำไปใช้กับ Ethereum blockchain และสร้างขึ้นบน Lisa ด้วยสัญญาอัจฉริยะ EVM Bytecode EVMLISA จึงสร้างกราฟการควบคุมเสียงและการควบคุมที่แม่นยำของสัญญาอัจฉริยะ

Evmlisa ขึ้นอยู่กับสิ่งพิมพ์ที่ผ่านการตรวจสอบโดยเพื่อน

Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella "ไปสู่การสร้างเสียงกราฟการควบคุมการไหลของ EVM bytecode" ในการประชุมเชิงปฏิบัติการนานาชาติ ACM ครั้งที่ 26 เกี่ยวกับเทคนิคทางการสำหรับโปรแกรมที่มีลักษณะคล้าย Java (FTFJP 2024) ซึ่งตั้งอยู่ร่วมกับ ECOOP 2024

- อาคาร Evmlisa

การรวบรวม EVMLISA ต้องการ:

• jdk> = 11
• Gradle> = 6.6
• คีย์ Etherscan API

คุณต้องทำ:

• โคลนที่เก็บ:

  git clone https://github.com/lisa-analyzer/evm-lisa.git
  cd evm-lisa

• นำเข้าโครงการไปยังพื้นที่ทำงานของ Eclipse/Intellij เป็นโครงการ Gradle (ไม่บังคับ)

เรียกใช้ evmlisa

ก่อนที่จะเรียกใช้ EVMLISA ตรวจสอบให้แน่ใจว่าคุณได้ตั้งค่าตัวแปรสภาพแวดล้อมด้วยคีย์ Etherscan API ของคุณ ทำตามขั้นตอนด้านล่างเพื่อตั้งค่าตัวแปรสภาพแวดล้อม:

1. เริ่มต้นด้วยการสร้างไฟล์ชื่อ .env ในโครงการ EVMLISA
2. ภายในไฟล์ .env เพิ่มบรรทัดต่อไปนี้:

 ETHERSCAN_API_KEY=<your_etherscan_api_key>

3. แทนที่ <your_etherscan_api_key> ด้วยคีย์ Etherscan API ของคุณ

ที่นี่คุณสามารถค้นหาวิธีสร้างคีย์ Etherscan API

เมื่อคุณตั้งค่าตัวแปรสภาพแวดล้อมแล้วคุณสามารถเรียกใช้ EVMLISA ผ่าน Docker หรือผ่าน Bash

ผ่าน Docker

สร้างคอนเทนเนอร์:

 mkdir -p execution/docker &&
docker build -t evm-lisa:latest .

จากนั้นคุณสามารถเรียกใช้ evmlisa ด้วย:

 docker run --rm -it 
-v $(pwd)/.env:/app/.env 
-v $(pwd)/execution/docker:/app/execution/results 
evm-lisa:latest 
-a <smart_contract_address> [options]

• -v $(pwd)/.env:/app/.env : ติดตั้งไฟล์. .env
• -v $(pwd)/execution/docker:/app/execution/results : แบ่งปันโฟลเดอร์ 'ผลลัพธ์

แทนที่ <smart_contract_address> ด้วยที่อยู่ของสัญญาสมาร์ท Ethereum ที่คุณต้องการวิเคราะห์

ผ่านการทุบตี

สร้างโครงการ:

./gradlew build

สร้าง Zip Distribution:

./gradlew distZip

เปิดซิปการกระจาย:

unzip build/distributions/evm-lisa.zip -d execution

จากนั้นคุณสามารถเรียกใช้ evmlisa ด้วย:

./execution/evm-lisa/bin/evm-lisa 
-a < smart_contract_address > [options]

แทนที่ <smart_contract_address> ด้วยที่อยู่ของสัญญาสมาร์ท Ethereum ที่คุณต้องการวิเคราะห์

คำสั่งนี้จะเริ่มต้นกระบวนการวิเคราะห์สำหรับสัญญาอัจฉริยะที่ระบุโดยให้ข้อมูลเชิงลึกและผลลัพธ์ตามรหัส Bytecode EVM ของสัญญา

 Options:
 -a,--address <arg>          address of an Ethereum smart contract
 -b,--benchmark <arg>        filepath of the benchmark suite (i.e., a list of smart contract addresses)
 -C,--cores <arg>            number of cores to use
 -c,--dump-cfg               dump the CFG
 -d,--dump-analysis <arg>    dump the analysis (html, dot)
 -D,--download-bytecode      download the bytecode, without analyzing it
 -f,--filepath <arg>         filepath of an EVM bytecode smart contract
 -o,--output <arg>           output directory path
 -q,--stack-size <arg>       maximal height of stack
 -s,--dump-stats             dump statistics
 -S,--use-live-storage       use the live storage in SLOAD
 -w,--stack-set-size <arg>   maximal size of stack sets

- โดเมนชุดบทคัดย่อสแต็ก

ในการวิเคราะห์โปรแกรม Bytecode EVM EVMLISA ใช้โดเมนของชุดของสแต็คนามธรรมเพื่อเพิ่มความแม่นยำโดยเฉพาะอย่างยิ่งเมื่อพบลูปในซอร์สโค้ด

Evmlisa แนะนำโดเมนนามธรรมสแต็ค PowerSet $ texttt {setst} _ {k, h, l} $ ซึ่งประกอบด้วยชุดของสแต็คนามธรรมที่มากที่สุด $ l $ องค์ประกอบและความสูงมากที่สุด $ h $ - โดเมนนี้ช่วยให้เครื่องวิเคราะห์สามารถรักษาคอลเลกชันของสแต็คนามธรรมหลีกเลี่ยงความจำเป็นในการคำนวณ lub และอนุญาตให้แต่ละองค์ประกอบของสแต็คนามธรรมเป็น A $ k $ ชุดจำนวนเต็ม

- ตัวอย่างการรัน

นี่คือตัวอย่างของวิธีการเรียกใช้ EVMLISA ในตัวอย่างนี้เราจะวิเคราะห์สัญญาอัจฉริยะตามที่อยู่ 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B พร้อมตัวเลือกเฉพาะสำหรับขนาดสแต็กขนาดสแต็ก

• ทุบตี:

./execution/evm-lisa/bin/evm-lisa 
-a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B 
--stack-size 64 
--stack-set-size 10 
--dump-stats 
--use-live-storage

• นักเทียบท่า:

docker run --rm -it 
-v $( pwd ) /.env:/app/.env 
-v $( pwd ) /execution/docker:/app/execution/results 
evm-lisa:latest 
-a 0x7c21C4Bbd63D05Fa9F788e38d14e18FC52E9557B 
--stack-size 64 
--stack-set-size 10 
--dump-stats 
--use-live-storage

ใช้ docker run -a stderr เพื่อทิ้งรายงาน JSON เป็นเอาต์พุตมาตรฐาน

ผลลัพธ์ที่คาดหวังมีดังนี้:

 # #############
Total opcodes : 344
Total jumps : 45
Resolved jumps : 44
Definitely unreachable jumps : 1
Maybe unreachable jumps : 0
Unsound jumps : 0
Maybe unsound jumps : 0
# #############

การจำแนกประเภท

• ได้รับการแก้ไข : จุดหมายปลายทางทั้งหมดของโหนดกระโดดได้รับการแก้ไขแล้ว
• ไม่สามารถเข้าถึงได้อย่างแน่นอน : โหนดกระโดดไม่สามารถเข้าถึงได้ (เช่นสามารถเข้าถึงได้ด้วยสถานะนามธรรมด้านล่าง);
• อาจจะไม่สามารถเข้าถึงได้ : โหนดกระโดดไม่สามารถเข้าถึงได้ใน CFG เริ่มต้นจากจุดเริ่มต้นของมัน แต่อาจเข้าถึงได้ผ่านโหนดกระโดดที่ไม่มั่นคง (อาจ) (ถ้ามี);
• unsound : โหนดกระโดดถึงอย่างน้อยก็มีสแต็คที่มีค่าตัวเลขที่ไม่รู้จักซึ่งอาจสอดคล้องกับปลายทางกระโดดที่ถูกต้องเป็นองค์ประกอบด้านบน;
• อาจจะ unsound : ชุดสแต็กเกินขนาดสแต็กสูงสุด

---

ผู้มีส่วนร่วม