Security & testing

Act

Formal verification

शिक्षण · विश्लेषण · औपचारिक पडताळणी · प्रतीकात्मक अंमलबजावणी

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

Related resources

K Semantics of the Ethereum Virtual Machine (EVM)

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

Kontrol - formal verification tool based on Foundry and KEVM

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

hax

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

Verifereum

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