Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

सुरक्षा · शिक्षण · विश्लेषण · औपचारिक पडताळणी · प्रतीकात्मक अंमलबजावणी · डीबगिंग टूल्स · रनटाइम पडताळणी · Vyper

सोशल runtimeverification/evm-semantics(586 ☆)

KEVM हे EVM चे K-framework एक्झिक्युटेबल सिमेंटिक्स आहे: जेव्हा तुम्हाला कन्फॉर्मन्स-चेक्ड एक्झिक्युशन, सिम्बॉलिक एक्सप्लोरेशन, गॅस रिझनिंग, किंवा इथेरियमच्या नियमांचा बारकाईने मागोवा घेणाऱ्या पुराव्यांची आवश्यकता असते, तेव्हा त्याला बाइटकोडवर निर्देशित करा.

Related resources

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol Foundry प्रॉपर्टी चाचण्यांना KEVM-समर्थित पुराव्यांमध्ये रूपांतरित करते, जेणेकरून तुम्ही केवळ रॉ KEVM च्या तुलनेत कमी हाताने लिहिलेल्या स्पेसिफिकेशनच्या कामासह औपचारिक हमी मिळवू शकाल.

hax

hax हे Rust च्या मोठ्या उपसंचाचे F* किंवा Rocq सारख्या फॉर्मल लँग्वेजेसमध्ये हाय ॲश्युरन्स ट्रान्सलेशन्स करण्यासाठी एक टूल आहे.

Act

Act ही इथेरियमची डिक्लेरेटिव्ह स्पेसिफिकेशन भाषा आणि टूलचेन आहे जी EVM प्रोग्रॅमच्या सर्व वर्तनांचे वर्णन करते, जेणेकरून SMT सॉल्व्हर्स, थिअरम प्रूव्हर्स किंवा आर्थिक विश्लेषण साधने बाइटकोड-स्तरीय अचूकता आणि इन्सेंटिव्ह कम्पॅटिबिलिटीबद्दल तर्क करू शकतील, ज्यामध्ये काँक्रीट इम्प्लिमेंटेशन्सच्या विरुद्ध स्वयंचलित रिफाइनमेंट प्रूफ्स्चा समावेश आहे.

Verifereum

Verifereum इथेरियम स्मार्ट कॉन्ट्रॅक्ट्सना HOL4-समर्थित थिअरम प्रूव्हिंगशी जोडते, जेणेकरून जेव्हा स्वयंचलित SMT दृष्टिकोन पुरेसे नसतात तेव्हा तुम्ही अत्यंत भक्कम अचूकतेचे दावे साध्य करू शकता.