securify

[เลิกใช้แล้ว] Securify

นี่คือเวอร์ชันของ Securify ที่เลิกใช้แล้วและจะไม่ได้รับการสนับสนุนอีกต่อไป โปรดใช้ Securify v2.0

Securify เป็นเครื่องสแกนความปลอดภัยสำหรับสัญญา Smart Ethereum ที่สนับสนุนโดยมูลนิธิ Ethereum และความปลอดภัย การวิจัยหลักที่อยู่เบื้องหลัง Securify ได้ดำเนินการที่ศูนย์น้ำแข็งที่ ETH Zurich

มันมีรายการรูปแบบความปลอดภัยที่พบได้ทั่วไปในสัญญาอัจฉริยะ:

• บางรูปแบบของ Dao Bug (หรือที่เรียกว่า reentrancy)
• อีเธอร์ล็อค
• ขาดการตรวจสอบอินพุต
• จำนวนการสั่งซื้อที่ขึ้นอยู่กับการทำธุรกรรมตัวรับสัญญาณและการถ่ายโอน
• ข้อยกเว้นที่ไม่สามารถจัดการได้
• การไหลของอีเธอร์ที่ไม่ จำกัด

โครงการนี้มีความหมายว่าจะเป็นแพลตฟอร์มที่เป็นมิตรกับการบริจาคจากชุมชนความปลอดภัย Ethereum ทั้งหมด หากต้องการแนะนำรูปแบบใหม่เพื่อเป็นอาสาสมัครสำหรับการทดสอบหรือเพื่อมีส่วนร่วมในการพัฒนารูปแบบใหม่โปรดติดต่อผ่านกลุ่ม Discord ของเรา

เริ่มต้น

ความต้องการ

• Soufflé: https://github.com/souffle-lang/souffle/releases (Securify ควรทำงานกับแพ็คเกจล่าสุดโปรดยกปัญหาหากไม่ได้) หากคุณไม่สามารถติดตั้งsouffléให้ดูที่คอนเทนเนอร์ Docker สำหรับทางเลือกอื่น Securify จะผิดพลาดโดยไม่มี souffle Binary ในการเขียนSouffléไม่สามารถใช้งานได้บน Windows ดังนั้น Securify จึงไม่ควรคาดหวังว่าจะทำงานบน Windows เช่นกัน
• Java 8
• จำเป็นต้องใช้ไบนารี solc เพื่อให้สามารถใช้ไฟล์ความแข็งแกร่งเป็นอินพุต Securify สันนิษฐานว่ามีการติดตั้งเวอร์ชันที่เหมาะสมสำหรับไฟล์ที่กำหนด solc มีให้ที่นี่

ใช้

เพื่อสร้าง:

./gradlew jar

ในการเรียกใช้ Securify บนไฟล์ Solidity:

java -jar build/libs/securify.jar -fs src/test/resources/solidity/transaction-reordering.sol

ในการเรียกใช้ Securify บนเอาต์พุตการสลายตัวที่จัดทำโดยสคริปต์ pysolc.py (ซึ่งต้องใช้ PY-SOLC):

java -jar build/libs/securify.jar -co out.json

เพื่อเรียกใช้ความปลอดภัยใน Binary EVM บางตัว (ผลิต EG โดย solc ):

java -jar build/libs/securify.jar -fh src/test/resources/solidity/transaction-reordering.bin.hex

หากต้องการดูรายการตัวเลือกทั้งหมด:

java -jar build/libs/securify.jar -h

เพื่อเรียกใช้การทดสอบ (ซึ่งใช้ Junit4):

./gradlew test

เสื้อคลุม Python ช่วยในการจัดการกับ solc และ truffle ข้อกำหนดอยู่ในไฟล์ข้อกำหนด. txt DockerFile สามารถใช้เป็นข้อมูลอ้างอิงเพื่อตั้งค่าสภาพแวดล้อมในพื้นที่ของคุณเพื่อใช้ wrapper นี้

นักเทียบท่า

การติดตั้งควรง่ายพอสำหรับอนุพันธ์ของ Debian หรือแพลตฟอร์มอื่น ๆ ที่สนับสนุนโดยSoufflé

สำหรับการสาธิตอย่างรวดเร็วซึ่งไม่จำเป็นต้องใช้Souffléคุณสามารถใช้ Docker

สร้างภาพนักเทียบท่า:

docker build . -t securify

เรียกใช้ความปลอดภัยในตัวอย่างเล็ก ๆ :

docker run securify

คุณสามารถเปลี่ยนไฟล์ที่วิเคราะห์โดยการระบุระดับเสียงไปที่เมานต์และไฟล์ *.sol ทุกไฟล์ที่อยู่ในนั้นจะถูกประมวลผลโดย Securify:

docker run -v $( pwd ) /folder_with_solidity_files:/project securify

การเพิ่มธง --truffle ควรอนุญาตให้ Securify ทำงานผ่านโครงการ Truffle ที่ติดตั้งการพึ่งพาได้แล้ว (ดังนั้นเรียกใช้ npm install ก่อนหากจำเป็นต้องเป็น) หากไม่มีธงนี้โครงการจะถูกรวบรวมโดยใช้ solc เพิ่ม -h เพื่อรับรายการตัวเลือกทั้งหมด โดยเฉพาะอย่างยิ่งหากผู้ใช้ต้องการรับข้อมูลการรวบรวมจากทรัฟเฟิลเขาควรเพิ่มธง -v

หากต้องการรับเอาต์พุต JSON นักเทียบท่าจะรองรับธง --json ที่จะระงับเอาต์พุตสวยและส่งคืน JSON แทน ตรวจสอบให้แน่ใจว่าได้เพิ่มค่าสถานะ -q หากไม่ควรแสดงข้อมูลความคืบหน้าดังนั้นจึงส่งผลให้เอาต์พุต JSON บริสุทธิ์ ดัชนีของบรรทัดที่ตรงกันนั้นใช้ 0 ซึ่งหมายความว่าการจับคู่กับบรรทัด i หมายความว่าบรรทัด i+1 th นั้นตรงกัน โดยเฉพาะอย่างยิ่งบรรทัดแรกมีดัชนี 0

การทดสอบ

การทดสอบขั้นพื้นฐานถึงจุดสิ้นสุดสามารถเรียกใช้ผ่านไฟล์ทดสอบไฟล์:

 python3 test . py

ข้อกำหนดสามารถติดตั้งได้โดยใช้ PIPENV:

pipenv install

หรือใช้ pip :

pip install -r requirements.txt

การทดสอบเหล่านี้เปรียบเทียบเอาต์พุต JSON ปัจจุบันที่ได้รับจาก Securify กับผลลัพธ์ที่ผ่านมาและรายงานความแตกต่างระหว่างทั้งสอง

การรวมเทรวิส

คุณสามารถเพิ่ม .travis.yml ต่อไปนี้ลงในโครงการของคุณเพื่อเรียกใช้ความปลอดภัยใน New Commits:

 services:
  - docker

before_install:
  - docker pull chainsecurity/securify

script:
- docker run -v $(pwd):/project chainsecurity/securify

สิ่งนี้ควรอนุญาตให้ Securify ทำงานผ่านโครงการ Truffle ที่ติดตั้งการพึ่งพาได้แล้ว (ดังนั้นเรียกใช้ npm install ก่อนหากจำเป็น)

เอาท์พุท

เอาท์พุทติดตามสไตล์เสียงดังอย่างหลวม ๆ มีการรายงานคำเตือนและช่องโหว่เท่านั้น หากมีความประสงค์ที่จะได้รับข้อมูลการปฏิบัติตามกฎระเบียบโปรดใช้ --json Flag ใน Docker หรือ -co Flag บน Java Consenable เพื่อรับข้อมูลการวิเคราะห์ทั้งหมดในรูปแบบ JSON

การบริจาค

ดูการสนับสนุน.

เข้าร่วม Discord ของเราเพื่อหารือกับผู้ใช้รายอื่น

ข้อ จำกัด ที่รู้จัก

แม้ว่า Securify จะใช้เป็นประจำเพื่อช่วยในการตรวจสอบที่ chainsecurity แต่ก็ยังมีข้อบกพร่องรวมถึง:

• รหัสในฟังก์ชั่นทางเลือกไม่ได้ทำการวิเคราะห์ วิธีแก้ปัญหาคือการตั้งชื่อฟังก์ชันนี้แทน
• ในบางกรณีข้อยกเว้น Stackoverflowerror ถูกโยนลงเนื่องจาก computeBranches ที่ถูกเรียกซ้ำ ในกรณีส่วนใหญ่มันก็เพียงพอที่จะเพิ่มขนาดสแต็กโดยใช้ตัวเลือก -Xss ของ java เช่น java -Xss1G -jar ...
• ไม่ได้รับการสนับสนุนห้องสมุดอย่างเหมาะสม
• สัญญานามธรรม (ซึ่งไม่สามารถรับไบนารีได้ผ่าน solc ) ไม่ได้รับการสนับสนุน

การนำเสนอการวิจัยและบล็อกเกี่ยวกับ Securify

• Securify Research Paper นำเสนอที่ ACM CCS'18 ในโตรอนโตแคนาดา
• บทสรุปของรายงานการวิจัย Securify ในกระดาษตอนเช้า
• TechCrunch: สแกนเนอร์สัญญาอัจฉริยะนี้จะทำให้แน่ใจว่าโทเค็นของคุณเป็นทิปด้านบน
• พูดคุยที่ EPFL ใน Lausanne
• พูดคุยที่ DevCon3 ในCancún
• พูดคุยที่ D10E ใน Davos
• นักวิจัยจาก ETH Zürichเปิดตัวเครื่องสแกนความปลอดภัยที่ทันสมัยสำหรับสัญญา Smart Ethereum
• การวิเคราะห์ความปลอดภัยอัตโนมัติของสัญญา Smart Ethereum
• ตรวจจับข้อผิดพลาดที่กระเป๋าเงินของ Parity แข็งตัวโดยอัตโนมัติ

รายละเอียดทางเทคนิค

Securify การวิเคราะห์รหัส EVM ของสัญญาอัจฉริยะเพื่ออนุมานข้อมูลความหมายที่สำคัญ (รวมถึงข้อเท็จจริงเกี่ยวกับการควบคุมการไหลและการไหลของข้อมูล) เกี่ยวกับสัญญา ขั้นตอนนี้เป็นไปโดยอัตโนมัติโดยใช้Souffléซึ่งเป็นตัวแก้ดาต้าล็อกที่ปรับขนาดได้ จากนั้นตรวจสอบข้อเท็จจริงที่อนุมานเพื่อค้นหาการละเมิดความปลอดภัยหรือพิสูจน์การปฏิบัติตามคำแนะนำที่เกี่ยวข้องกับความปลอดภัย

รายละเอียดทางเทคนิคทั้งหมดที่อยู่เบื้องหลังเครื่องสแกน Securify มีอยู่ในรายงานการวิจัย