Ang artikulong ito ay isinumite ng komunidad. Ang may-akda ay si David Tarditi, VP ng Engineering sa CertiK, isang kumpanyang nag-o-audit ng smart contract sa Web3.
TL;DR
Tinitiyak ng pormal na pag-verify ng mga smart contract na ito ay walang bug, kahinaan, at iba pang hindi nilalayong gawi. Sangkot dito ang pagpapakita ng isang taong eksperto ng lohika ng smart contract bilang mga mathematical statement, pagkatapos ay pagsasailalim ng mga ito sa isang naka-automate na presyo na sumusuri sa aktwal na lohika laban sa mga modelo ng inaasahang gawi ng kontrata. Ang kumbinasyon ng pormal na pag-verify at manu-manong pag-audit ay nagbibigay ng komprehensibong pagsusuri sa seguridad ng isang smart contract.
Panimula
Ang mga smart contract ay mga computer program na dine-deploy sa isang blockchain na awtomatikong tumatakbo kapag natugunan ang ilang partikular na kondisyon. Ito ay puwedeng simple hanggang napakakumplikado, at kaya nitong humawak ng mga asset na nagkakahalaga ng milyon-milyon o kahit bilyon-bilyon pang dolyar.
Puwedeng magkaroon ng mga napakalalang kahihinatnan ang mga kahinaan sa seguridad sa code ng smart contract, kasama na ang pagnanakaw sa lahat ng asset na hawak ng isang smart contract. Noong 2021, nanakawan ang automated market maker (AMM) na Uranium Finance ng $50 milyon dahil sa isang typo sa isang smart contract.
Noong 2021 din, namigay ang Compound Finance ng $80 milyong halaga ng mga hindi kinitang reward dahil sa pagkakamali sa isang character. Noong 2022, $320 milyon ang nanakaw sa Wormhole Bridge dahil sa isang bug sa isa sa mga smart contract nito.
Mahalagang maitama ang programa ng smart contract sa umpisa pa lang. Open-source ang mga smart contract, ibig sabihin, available sa publiko ang code kapag na-deploy ang isang kontrata. Kung may makikitang bug ang isang hacker, masasamantala niya ito agad. Dagdag pa rito, hindi opsyon ang pag-patch sa mga kahinaan sa seguridad sa paglipas ng panahon, dahil karaniwang hindi nababago ang code ng isang smart contract pagkatapos ma-deploy.
Paano Gumagana ang Pag-verify ng Smart Contract?
Gumagana ang pormal na pag-verify ng mga smart contract sa pamamagitan ng pagpapakita ng lohika at gustong gawi ng mga smart contract bilang mga mathematical statement. Pagkatapos, gumagamit ang mga auditor ng mga naka-automate na tool para suriin kung tama ang mga statement na ito.
Kasama sa proseso ang:
Pagtukoy sa mga detalye at gustong katangian ng isang kontrata sa pormal na pananalita.
Pagsasalin ng code ng kontrata sa isang pormal na representasyon, gaya ng mga matematikal na modelo o lohika.
Paggamit ng mga naka-automate na tagapagpatunay ng theorem o tagapagsuri ng modelo para ma-validate ang mga detalye at katangian ng kontrata.
Pag-uulit ng proseso ng pag-verify para mahanap at maayos ang anumang error o deviation mula sa mga gustong property.
Bakit Mahalaga ang Pag-verify ng Smart Contract
Nakakatulong ang paggamit ng mathematical reasoning para matiyak na ang mga smart contract na pormal na na-verify ay walang bug, kahinaan, at iba pang hindi nilalayong gawi. Nakakatulong din itong madagdagan ang tiwala at kumpyansa sa kontrata, dahil mabusising napatunayan na tama ang mga katangian nito.
Nasa ibaba ang ilang halimbawa kung paano nakatulong ang pag-verify ng smart contract na pigilan ang malaking pagkalugi at iba pang mapaminsalang kahihinatnan.
Uniswap
Ang Uniswap ay isang kilalang AMM. Noong na-develop ang smart contract ng Uniswap V1, pormal itong na-verify. Bago ito ni-release, sa pormal na pag-verify na ito, may nahanap at naayos na mga error sa pag-round na naging dahilan sana para malimas ang mga pondo ng Uniswap V1.
Balancer
Ang Balancer V2 ay isa ring AMM na pormal na na-verify. Sa pamamagitan ng pormal na pag-verify, may nahanap at naayos na maling pagkalkula sa bayad na kinasasangkutan ng functionality ng mabilisang pautang sa smart contract, na nagpahina sana sa palitan laban sa pagnanakaw.
SafeMoon
Sa SafeMoon V1, may nakatagong bug na nahanap ng pormal na pag-verify pagkatapos itong ma-deploy. Posible para sa isang may-ari na isuko ang pagmamay-ari sa kontrata at pagkatapos ay kunin ito ulit, kung may ilang partikular na pagpapatakbo na isinagawa bago isinuko ang pagmamay-ari.
Napalampas ang bug na ito sa karamihan ng mga manu-manong pag-audit ng mga fork ng SafeMoon V1 dahil para mahanap ito, kailangang magsuri ng mga partikular na kumbinasyon ng mga value ng variable ng program. Isa itong bagay na madaling mapapalampas ng mga tao, at madaling makikita ng computer.
Paano Gumagana ang Pormal na Pag-verify at Manu-manong Pag-audit nang Magkasama
Nagbibigay ang pormal na pag-verify ng sistematiko at naka-automate na paraan para suriin ang lohika at gawi ng isang kontrata laban sa mga gusto nitong katangian. Mas pinapadali nitong tukuyin at ayusin ang anumang potensyal na error o bug. Partikular itong kapaki-pakinabang para sa paghahanap ng mga kumplikado at patagong isyu na posibleng mahirap makita sa pamamagitan ng manu-manong pagsisiyasat.
Sangkot sa manu-manong pag-audit ang pagsusuri ng eksperto sa code, disenyo, at pag-deploy ng isang kontrata. Ginagamit ng auditor ang kanyang karanasan at kahusayan para tumukoy ng mga panganib sa seguridad at suriin ang pangkalahatang kalagayan ng seguridad ng kontrata. Makukumpirma rin niya na tama ang pagsasagawa ng proseso ng pormal na pag-verify, at masusuri niya kung may anumang isyu na posibleng hindi nade-detect ng mga naka-automate na tool.
Ang pagsasama ng pormal na pag-verify at manu-manong pag-audit ay nagbibigay ng komprehensibo at masusing pagsusuri sa seguridad ng isang smart contract. Pinapalaki nito ang tsansang mahanap at maayos ang anumang kahinaan. Ang resulta ay isang defense-in-depth na diskarte sa seguridad na gumagamit sa mga natatanging kakayahan ng mga tao at computer.
Mga Pangwakas na Pananaw
Para matiyak ang seguridad ng mga smart contract, mahalagang gumamit ng pormal na pag-verify at manu-manong pag-audit para matiyak na magkakaroon ng komprehensibo at masusing pagsusuri ng kalagayan ng seguridad ng isang smart contract.
Bagama't posibleng malakas kumonsumo ng resource ang pormal na pag-verify, sulit itong pamumuhunan para sa mga kontratang may mataas na halaga o may mga salik na mataas ang panganib. Sa huli, napakahalagang bigyang-priyoridad ang seguridad at siguraduhin na ang mga smart contract ay walang bug, kahinaan, at hindi nilalayong gawi.
Iba pang Babasahin
Disclaimer at Babala sa Panganib: Ibinibigay sa iyo ang content na ito nang ganito para lang sa mga layunin ng pagbibigay ng pangkalahatang impormasyon at pagtuturo, nang walang kahit anong isinasaad o pinapatunayan. Hindi dapat ito ituring na pinansyal na payo, at hindi rin nito nilalayong irekomenda ang pagbili ng anumang partikular na produkto o serbisyo. Puwedeng maging volatile ang mga presyo ng digital asset. Puwedeng bumaba o tumaas ang halaga ng iyong pamumuhunan at puwedeng hindi mo mabawi ang halagang ipinuhunan. Ikaw lang ang responsable sa iyong mga desisyon sa pamumuhunan at walang pananagutan ang Binance Academy sa anumang pagkaluging puwede mong matamo. Hindi dapat ituring ang materyal na ito bilang pinansyal na payo.