Тази статия е предоставена от общността. Авторът е Дейвид Тардити, вицепрезидент по инженерството в CertiK, фирма за одит на Web3 смарт договори.
Резюме
Официалната проверка на смарт договори гарантира, че те не съдържат грешки, уязвимости и друго нежелано поведение. Това включва човешки експерт, който представя логиката на смарт договор като математически изявления, след което ги пуска през автоматизиран процес, който проверява действителната логика спрямо модели на очакваното поведение на договора. Комбинацията от официална проверка и ръчен одит предоставя цялостна оценка на сигурността на смарт договора.
Въведение
Смарт договорите са програми, съхранявани в блокчейн, които изпълняват действие при изпълнението на определени условия. Те могат да варират от прости до изключително сложни и могат да съдържат активи на стойност милиони или дори милиарди долари.
Уязвимостите на сигурността в кода на смарт договора могат да имат опустошителни последици, включително кражба на всички активи, държани от смарт договор. През 2021 г. автоматизираният маркет мейкър (AMM) Uranium Finance открадна $50 млн. поради една печатна грешка в смарт договор.
Също през 2021 г. Compound Finance раздаде $80 млн. неспечелени награди поради грешка в един знак. През 2022 г. $320 млн. бяха откраднати от Wormhole Bridge поради грешка в един от смарт договорите му.
Важно е програмата за смарт договори да бъде правилна от първия път. Смарт договорите са с отворен код, което означава, че кодът е публично достъпен, след като договорът бъде внедрен. Ако хакер открие грешка, той може да се възползва незабавно от нея. Освен това коригирането на уязвимости в сигурността с течение на времето не е опция, тъй като кодът на смарт договора обикновено не може да бъде модифициран след внедряването.
Как работи проверката на смарт договора?
Официалната проверка на смарт договори работи, като представя логиката и желаното поведение на смарт договори като математически изявления. След това одиторите използват автоматизирани инструменти, за да проверят дали тези твърдения са верни.
Процесът включва:
Дефиниране на спецификациите и желаните свойства на договор на официален език.
Превеждане на кода на договора във формално представяне, като математически модели или логика.
Използване на автоматизирани програми за доказване на теореми или проверки на модели за валидиране на спецификациите и свойствата на договора.
Повтаряне на процеса на проверка за намиране и коригиране на грешки или отклонения от желаните свойства.
Защо проверката на смарт договор е важна
Използването на математически разсъждения помага да се гарантира, че официално проверените смарт договори са свободни от грешки, уязвимости и друго нежелано поведение. Той също така помага за увеличаване на доверието и увереността в договора, тъй като свойствата му са стриктно доказани като правилни.
По-долу са дадени някои примери за това как проверката на смарт договора е помогнала за предотвратяване на значителни финансови загуби и други катастрофални резултати.
Uniswap
Uniswap е добре познат AMM. Когато беше разработен смарт договорът Uniswap V1, той беше официално проверен. Преди пускането му, тази официална проверка откри и поправи грешки при закръгляване, които можеха да доведат до източване на средства от Uniswap V1.
Balancer
Balancer V2 също е AMM, който беше официално проверен. Официалната проверка откри и поправи неправилно изчисление на таксата, включващо функционалност за бърз заем в смарт договора, което можеше да направи борсата уязвима за кражба.
SafeMoon
SafeMoon V1 съдържаше фина грешка, открита чрез официална проверка след внедряването му. Възможно е собственикът да се откаже от собствеността върху договора и след това да го придобие отново, ако са извършени определени операции преди да се откаже от собствеността.
Тази грешка беше пропусната при повечето ръчни одити на разклоненията на SafeMoon V1, тъй като намирането ѝ изискваше анализиране на специфични комбинации от стойности на програмни променливи. Това е нещо, което лесно би могло да се пропусне от хората, но пък машината лесно улавя.
Как официалната проверка и ръчният одит работят заедно
Официалната проверка осигурява систематичен и автоматизиран начин за проверка на логиката и поведението на договор спрямо желаните свойства. Това улеснява идентифицирането и коригирането на потенциални грешки. Това е особено полезно за намиране на сложни и фини проблеми, които може да са трудни за откриване чрез ръчна проверка.
Ръчният одит включва експертен преглед на кода, дизайна и внедряването на договора. Одиторът използва своя опит и експертиза, за да идентифицира рисковете за сигурността и да оцени цялостното състояние на сигурността на договора. Те могат също да потвърдят, че официалният процес на проверка е извършен правилно и да проверят за проблеми, които може да не бъдат открити от автоматизирани инструменти.
Комбинирането на формална проверка и ръчен одит предоставя цялостна и задълбочена оценка на сигурността на смарт договора. Това увеличава шансовете за намиране и коригиране на всякакви уязвимости. Резултатът е подход към сигурността, насочен в дълбочина на защитата, който използва уникалните способности както на хората, така и на машините.
Заключителни мисли
За да се гарантира сигурността на смарт договорите, от съществено значение е да се използва както официална проверка, така и ръчен одит, за да се осигури цялостна и задълбочена оценка на състоянието на сигурността на смарт договора.
Въпреки че формалната проверка може да изисква много ресурси, тя е полезна инвестиция за договори с висока стойност или фактори с висок риск. В крайна сметка приоритизирането на сигурността и гарантирането, че смарт договорите не съдържат грешки, уязвимости и нежелано поведение е жизненоважно.
Допълнителни статии
Отказ от отговорност и предупреждение за риск: Това съдържание ви се представя на база „както е“ само за обща информация и образователни цели, без твърдения или гаранция от какъвто и да е вид. Не трябва да се тълкува като финансов съвет, нито има за цел да препоръча покупката на конкретен продукт или услуга. Цените на цифровите активи могат да бъдат нестабилни. Стойността на вашата инвестиция може да намалее или да се повиши и може да не си върнете инвестираната сума. Вие носите цялата отговорност за вашите инвестиционни решения и Binance Academy не носи отговорност за каквито и да било загуби, които може да понесете. Този материал не трябва да се тълкува като финансов съвет.