6655

6655

درستي يابي صوري قراردادهاي هوشمند

كارشناسي

كامپيوتر

1398

دكتر محمد عبداللهي ازگمي

1398/11/02

كامپيوتر

Formal Verification of Smart Contracts

در سالهاي اخير، كاربران و توسعهدهندگان حوزهي زنجيرهبلوكي افزايش چشمگيري داشتهاست. يكي مهمترين بخشهاي سيستمهاي زنجيرهبلوكي قرارداد هوشمند است. قرارداد هوشمند برنامهاي كه است كه به صورت غيرمتمركز، بر روي تمامي ماشينهاي داخل يك شبكهي زنجيرهبلوكي اجرا ميشود. اين قراردادها عمدتاً مديريت رمزارزها را بر عهده دارد. لذا تا كنون مهاجمين زيادي سعي كردهاند تا با استفاده از آسيبپذيري هاي كدهاي قرارداد هوشمند، رمزارز ساير كاربران را به سرقت ببرند. درستييابي صوري قراردادهاي هوشمند، كمك بسيار زيادي به رفع قسمتهاي آسيبپذير قراردادهاي هوشمند ميكند. در اين گزارش، فعاليتهاي انجام شده در اين حوزه مرور ميشود و سپس به كمك ابزار بررسي مدل اسپين )و زبان پروملا(، چند مورد آسيبپذيري در چند قرارداد هوشمند معروف بهطور صوري توصيف و با روش بررسي مدل، درستييابي ميشود