مقالات اتریوم

استحکام قراردادهای هوشمند به وسیله “درستی یابی صوری”

به زبان ساده، درستی یابی صوری روشی استدلالی و منطقی و با کمک ریاضی است که برای شناسایی و تجزیه و تحلیل اشکالات و خطاهای یک برنامه استفاده می شود. با توجه به عوامل زمان و هزینه، درستی یابی صوری بهترین انتخاب در شرایطی است که زندگی انسان و یا مبلغ زیادی پول در معرض خطر می باشد.

استحکام قراردادهای هوشمند به وسیله “درستی یابی صوری”

استحکام قراردادهای هوشمند به وسیله "درستی یابی صوری"

به عنوان راهی برای رفع اشکالات موجود در کد پر مخاطره (high risk code؛ مجموعه، برنامه، نظام نامه، رمزگذاری و یا هر چیز مشابه است که در نهاد آن احتمال ایجاد خطر زیاد و یا عدم اطمینان در اجرای آن وجود داشته باشد)، شیوه ای از برنامه نویسی نرم افزار موسوم به درستی یابی صوری  (formal verification)، راه خود را به دنیای بلاکچین باز می نماید.

به زبان ساده، درستی یابی صوری روشی استدلالی و منطقی و با کمک ریاضی است که برای شناسایی و تجزیه و تحلیل اشکالات و خطاهای یک برنامه  استفاده می شود. با توجه به عوامل زمان و هزینه، درستی یابی صوری بهترین انتخاب در شرایطی است که زندگی انسان و یا مبلغ زیادی پول در معرض خطر می باشد.

در حال حاضر این روش برای تأیید صحت کد پر مخاطره در حمل و نقل، نیرو های مسلح و رمزنگاری استفاده می شود. شرکت های تولید کننده تراشه از آن برای تقویت الگوریتم خود، پیش از تعبیه آنها در سیلیکون استفاده می کنند. بانک ها نیز از آن برای توسعه الگوریتم های مالی بهره می برند.

درستی یابی صوری با بکارگیری فناوری بلاکچین می تواند تضمین کند که معاملات خود-اجرا موسوم به قرار دادهای هوشمند به همان شکل مورد نظر کار خواهند کرد و باعث حذف برخی از اشکالات و زیان های مالی ناشی از خطاهای برنامه می شود.

تخمین زده شده که تنها در سال جاری، اشکالات موجود در کیف پول تضمین شده اتریوم موجب از دست رفتن ۱۸۰ میلیون دلار شده است. در سال گذشته نیز اشکالی در تشکیلات مجازیِ معروفِ The DAO، یک هکر را قادر به خروج ۵۰ میلیون دلار از قراردادهای هوشمند اتریوم نمود.

هم اکنون پلت فرم هایی مانند Cardano و Tezos، روی زبان های برنامه نویسی قراردادهای هوشمند که به طور خاص برای تسهیل عملکرد درستی یابی صوری طراحی شده اند، کار می کنند. اتریوم نیز در حال کار بر روی قراردادهای هوشمند خود به همین روش می باشد.

اما درستی یابی صوری چیست؟

چگونه کار می کند؟ و چرا از ابتدا درستی نرم افزار بسیار دشوار است؟

انسان جایز الخطا است!

نرم افزار ذاتا گذشت ندارد. اگر شما ساختمانی را بسازید، بدون اینکه ساختار آن از هم بپاشد قادرید یک پیچ و یا یک میخ را از ساختمانتان جدا کنید. اما هنگامی که این کار با یک نرم افزار انجام شود، چیزی ساده  مثل یک خطای چاپی یا ماشینی می تواند دلیلی برای توقف کل برنامه باشد.

Gerard Holzmann، دانشمند سرشناس سابق NASA طی مصاحبه ای با Bitcoin Magazine گفت: “زبان های برنامه نویسی بسیار قدرتمند هستند، وبه عنوان یک برنامه نویس شما باید با جزئیات زیادی دست و پنجه نرم کنید، و اگر همه جزئیات را بدرستی در نظر نگیرید، قطعا تاثیر خود را نشان خواهد داد.”

رویکرد متعارف در درست کار کردن یک نرم افزار، صحت آزمایی آن است. پس از نوشتن یک الگوریتم، یک متغیر را وارد می کنید و به بررسی خروجی صحیح توسط آن می پردازید. اما چگونه همه ورودی های مستقل را می توانید آزمایش کنید؟  نمی توانید!  تعداد دفعاتِ آزمایش باید بسیار زیاد باشند، و موارد آزمایش نشده می توانند در کمین ایجاد خطا بمانند.

به تعبیری دیگر، آزمایش تنها به دنبال وجود اشکالات یا باگ ها است و نه عدم وجود آنها، و در نتیجه یک اشتباه کوچک می تواند نتایج ویرانگری داشته باشد.

در مقابل، به جای آزمایش یک وضعیت در هر بار، درستی یابی صوری راهی برای آزمایش یک برنامه در هر شرایطی می باشد. آنچه که اهمیت دارد، درست عمل کردن این منطق است، و بهترین راه برای بررسی آن، استفاده از کامپیوتر خواهد بود.

Holzmann گفت: یک هدف رسمی و انتزاعی، توانمندی در استدلال و اثبات مسائل است. و کاراترین روش آن، برنامه ریزی یک ماشین به همین منظور و بجای شماست.

طرح و برنامه ریزی

عموما اولین گام در درستی یابی صوری، ایجاد یک مدل مبتنی بر ریاضیات است. ریاضیات مورد نیاز پیچیده نیست؛ فقط یک منطق بنیادی ست که به اصطلاح با زبان رسمی(formal) نوشته شده و قابل بررسی توسط ماشین می باشد.

به طور معمول، فرآیند تعیین یک مدل با یک متولی یا ذی نفع شروع می شود که آگاه به آنچه که این سیستم باید انجام دهد، می باشد. مثلا در مورد یک دستگاه پزشکی، ممکن است متولی یک پزشک و در مورد یک قرار داد هوشمند این متولی می تواند یک وکیل، یک بانکدار و یا هردو باشد.

کار یک متولی یا ذی نفع، انتقال اطلاعاتی است که یک مهندس در زمینه مورد نظر به آن نیاز دارد. مهندسی که این اطلاعات را گردآوری و مدل را ایجاد می کند. این فرآیند با بحث ها و انتزاعات غیر رسمی آغاز می شود، اما به صورت محض و با مشخصات دقیق مبتنی بر ریاضیات به پایان می رسد.

این امر ساده و آسان نیست. فرآیندی زمان بر است، فرآیندی چند باره که بسته  به شرایط می تواند ماه ها به طول انجامد. اما اغلب به وضعیتی که پیش از این وجود نداشته، روشنی می بخشد. زیرا برنامه نویسان را عمیقا مجبوربه اندیشیدن در مورد رفتار یک نرم افزار می کند.

Andreas Zeller، پروفسور و استاد مهندسی نرم افزار دانشگاه Saarland University واقع در شهر Saarbruecken آلمان، که به ایجاد یک مشخصات رسمی(formal specification) برای توسعه یک طرح برای یک ساختمان می پردازد، گفت: “شما می توانید آن نرم افزار را به مثابه قوانین و مقررات در نظر بگیرید.”

او به Bitcoin Magazine گفت: “شما این قوانین و مقررات را اصلاح می کنید، اما اگر در ابتدای امر قانونمندی نداشته باشید، ساختمان شما فرو می ریزد، و این زمانی ست که متوجه می شوید که بهتر بود یک طرح  و برنامه می داشتید.”

بررسی منطق مدل

هنگامی که یک مدل مشخص می گردد، گام بعدی تأیید منطق این مدل با دلایل ومستندات است. این امر گام مهمی در این فرآیند می باشد. Zeller توضیح داد: “اگر اثبات و استدلالی نداشته باشید، شما تضمینی برای کارکرد این مدل به همین شکلی که هست را در اختیار نخواهید داشت.”

از آنجا که باید هرگام منطقی خود را آشکار و روشن کنید، دلایل و مستندات آن می تواند بی اندازه طولانی و پیچیده باشد. در گذشته این مسئله، درستی یابی صوری را مشکل می کرد. حتی ساده ترین اظهار نیز نیازمند ده ها فرمول و قضیه و صغرا و کبرا چیدن بود.

خوشبختانه امروزه بسیاری از سیستم های محض یا رسمی از محک زننده های خودکار قاعده و فرمول همچون Coq، Isabelle و یا Metamath استفاده می کنند که می توانند یک اثبات و دلیل  رسمی (formal) را بررسی کرده و یا حتی خود در اثبات آن، دلیل بیاورند.

هنگامی که کارکرد یک مدل به اثبات می رسد، قدم بعدی ساخت برنامه شما است. اما هنوز باید از انطباق برنامه خودتان با مشخصات تعریف شده، اطمینان حاصل کنید.

حالا این جایی ست که زبان های برنامه نویسی کاربردی مثل: ML، Haskell، OCaml یا #F وارد عرصه می شوند. از آنجایی که این زبان ها به بیان جبری (بخشی از ریاضیات) نزدیک ترند، برای درستی یابی صوری بهتر از زبان هایی مانند C، Java، یا JavaScript هستند.

به همین دلیل Tezos به زبان OCaml و Cardano در Haskell نوشته شده است، زیرا تغییرات در پروتکل آنها به صورت رسمی آسان تر تأیید می شود. (در حال حاضر آنها بر روی مشخصات رسمی برای  Ouroboros Praos، نسل بعدی الگوریتمِ اجماعِ نیروبخشِ Cardano، مشغول به کار هستند.) به همان ترتیب، Michelson زبان قرارداد هوشمند Tezos مبتنی بر OCaml بوده؛ و Plutus، زبان قرارداد هوشمند Cardano هم مبتنی بر Haskell می باشد.

مزایا و معایب

جنبه مثبت اینکه با  درستی یابی صوری، دانشمندان کامپیوتر اطمینان خاطر بیشتری در توسعه نرم افزار خود دارند.
از جنبه منفی، به دلیل سخت گیری و دقت زیاد، روش های محض یا فرمال می توانند باعث تحمیل زمان و هزینه بالا برای پروژه های توسعه کد باشند.

از این رو، متد های صوری بهترین کاربرد در تضمین بلاک های سازنده کوچک تر کد، که بارها و بارها مورد استفاده قرار می گیرند را دارند. به عنوان مثال، شما نمی توانید ازآن برای کل یک سیستم عامل استفاده کنید، اما می توانید برای بخشهایی از سیستم که نیاز به بالاترین سطح تضمین های ایمنی و امنیتی دارند، بهره مند گردید.

به طور طبیعی، هرگونه ای از امنیت، با هزینه همراه است. حال سؤال این است که توسعه دهندگان بلاکچین وقرارداد هوشمند برای چه مقدار امنیت و به چه میزان مایل به پرداخت هزینه خواهند بود؟

Zeller هشدار می دهد: اگر خواستار چیزی عاری از خطا هستید، “بهتر است آماده خرج کردن ده ها تا صدها هزار دلار برای افرادی که یک اثبات و گواه کامل را ارائه می دهند، باشید.”

از سوی دیگر، برای قراردادهای هوشمندی که حافظ ده ها میلیون دلار سرمایه هستند، ممکن است صرف این هزینه ها ارزشش را داشته باشد. با نگاه از زاویه دیگر، در یک محیط رقابتی، درستی یابی صوری می تواند قراردادهای هوشمند را برای مصرف کننده جذاب تر کند.

 اگر بخواهید به عنوان مثال، سرمایه خود را به یک قرارداد هوشمند که به صورت رسمی یا صوری تأیید شده اختصاص  دهید، در مقایسه با یک قرارداد رسمی تأیید نشده، انتخاب شما کدام یک از این دو خواهد بود؟

 

https://coiniran.com/?p=16590
0 0 رای ها
امتیازدهی به مقاله
اشتراک در
اطلاع از
guest
0 نظرات
بازخورد (Feedback) های اینلاین
مشاهده همه دیدگاه ها
دکمه بازگشت به بالا
0
دیدگاه خود را با کوین ایران به اشتراک بگذارید!x