دیپ سی (DeepSEA) و دنیای بلاک چین

در دنیای بلاک چین، امنیت در درجه اول اهمیت قرار دارد، اما نوشتن نرم‌افزار سیستمی که به‌طور کامل قابل‌تأیید رسمی باشد، کار بسیار دشوار و پیچیده‌ای است.

در این مطلب از وبلاگ خط دید می‌خواهیم با دیپ سی (DeepSEA) آشنا شویم. DeepSEA زبان جدید برای نوشتن قراردادهای هوشمند تأیید شده است.

DeepSEA چیست و چرا ساخته شد؟

DeepSEA زبانی است که به برنامه‌ها اجازه می‌دهد تا کدهای بسیار پیچیده را مدیریت کنند و در عین حال برای خود کدنویس‌ها به زیبایی و  با امنیت بالا عمل می‌کند. دیپ سی طراحی شده است تا هنگام انجام تأیید رسمی کامل در سیستم Coq، یک دستیار اثبات صحت عملکرد، مفید باشد.

تأیید رسمی از نظر ریاضی ثابت می‌کند که کد همانطور که در نظر گرفته شده عمل می‌نماید و همه سناریوهای ممکن را محاسبه  و در نظر گرفته است و به عنوان پیشگام فناوری تأیید رسمی در قراردادهای هوشمند و بلاک چین به کار می‌رود.

اگرچه تأیید رسمی نرم افزار تنها راه برای نشان دادن مصونیت عینی در برابر آسیب پذیری‌ها است، اما همچنان نوشتن نرم افزار کاملاً صحیح بسیار گران و چالش برانگیز است که این با عملکرد و درجه اهمیت و ایجاد امنیت آن قابل قیاس است.

بخشی از این مشکل به دلیل عدم پشتیبانی از زبان برنامه نویسی است. زبان های موجود، مانند C یا OCaml  یاSolidity ، به خوبی با ابزارهای تأیید یکپارچه نیستند و برای ایجاد و اثبات دستی به زمان نیاز دارند. با این حال، زبان DeepSEA راهی برای تأیید رسمی ویژگی‌های صحت دشوار قراردادهای هوشمند با استفاده از Coq Proof Assistant به روشی مقیاس‌پذیر و خودکار فراهم می‌کند.

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

DeepSEA چگونه ساخته شده است؟

هنگام طراحی این زبان، عموما از چهار اصل استفاده می‌گردد که بهترین ویژگی های چندین زبان برنامه نویسی دیگر را ترکیب می‌کند:

استدلال معادله

هر عبارت DeepSEA به یک مشخصات عملکردی متناظر ترجمه می‌شود، که سپس می‌توان در مورد آن در دستیار اثبات Coq استدلال کرد.

مشخصات لایه ای  DeepSEA

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

کپسوله سازی و ترکیب

هر لایه DeepSEA از مجموعه ای از اشیاء تشکیل شده است که روی لایه دیگری ساخته شده‌اند و می‌توان درستی لایه‌ها را تک تک اثبات نمود.

پالایش چکیده داخلی  DeepSEA

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

اهمیت DeepSEA در دنیای بلاک چین

اکوسیستم‌های بلاک چین بر پایه‌های اعتماد ساخته شده اند. در حالی که برخی استدلال می‌کنند که پروتکل‌های متمرکز سازی چیزی است که بلاک چین‌ها را قابل اعتماد می‌کند، برخی از کدها به دلیل اشکالات برنامه و هکرهای مخرب هنوز واقعاً قابل اعتماد نیستند.

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

امنیت در بلاک چین

اگر دربرنامه‌ها بحث امنیت به میان می‌آید، مسلماٌ برنامه باید قابل اعتماد باشد. این الزام در بلاک چین مهم است زیرا هنگامی که یک قرارداد هوشمند اجرا می‌شود، هیچ راه آسانی برای خنثی سازی آن وجود ندارد.

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

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

امروزه تقریباً تمام قراردادها به زبان‌های برنامه نویسی نوشته می‌شوند که بدون در نظر گرفتن تأیید رسمی طراحی شده‌اند. حتی زمانی که آنها با یک سیستم تأیید رسمی ادغام می‌شوند، معمولاً در جهت رسیدگی خودکار به موارد ساده هستند.

اگرچه دستیارهای اثبات تعاملی دارای زبان‌های برنامه نویسی داخلی هستند، اما آنها از طریق زبان‌های برنامه نویسی کاربردی که از جمع کننده زباله (جمع آوری کننده حافظه خودکار) استفاده می‌کنند، کامپایل می‌کنند.

در زمینه بلاک چین، داشتن زباله جمع کن قراردادهای هوشمند را کند و گران می‌کند. بنابراین زبان داخلی Coq مستقیماً برای اتریوم قابل استفاده نیست. خوشبختانه، کامپایلر DeepSEA این شکاف را با تولید کد اجرایی کارآمد (که می‌تواند بدون جمع کننده زباله اجرا شود) و یک مدل رسمی که می‌تواند در Coq  بارگذاری شود، پر می‌کند.

DeepSEA  یک زبان منعطف و سازگار است که می تواند با استفاده از Coq طراحی اساسی و شهودی با سطح بالایی از انتزاع و استدلال ایجاد کند.  DeepSEA راه حلی زیبا، واضح، قوی و کارآمد برای ایمن کردن کد ارائه می‌دهد.

 ما در تیم خط دید بر این باوریم که، با فناوری نسل بعدی در بستر بلاک چین، امنیت نسل بعدی نیز تامین می‌گردد.

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