Bersipa Ecosystem
چرا بیت کوین و دنیای ارز رمزها آینده ای نخواهند داشت ؟؟؟!!!
2 نوامبر 2020
تحلیل توکن YFI در هفته پیش رو
8 نوامبر 2020فناوری فوق امنیتی DEEPSEA چیست ؟
به گزارش برسیپا، در دنیای بلاکچین امنیت از اهمیت بالایی برخوردار است ، اما نوشتن نرم افزار صحیح و بدون نقص نیز بسیار مشکل است. زبانهای برنامه نویسی فعلی برای کار مناسب نیستند - چه رسد به اینکه با تأیید رسمی (Formal Verification) سازگار باشند. DeepSEA زبانی است که به برنامه ها امکان مدیریت کدهای بسیار پیچیده را می دهد در حالی که به زیبایی و ایمنی برای خود رمزگذاران کار می کند. این طراحی شده است تا هنگام انجام تأیید رسمی کامل در سیستم Coq ، یک دستیار اثبات ، مفید واقع شود.تأیید رسمی از نظر ریاضی ثابت می کند که یک کد همانطور که در نظر گرفته شده است تمام محسابات را انجام می دهد و به عنوان یک برنامه پیشگام فناوری تأیید رسمی در قراردادهای هوشمند و بلاک چین ، CertiK دریافت میکند. اگرچه تأیید رسمی نرم افزار تنها راه برای نشان دادن مصونیت عینی در برابر آسیب پذیری ها است؛ اما نوشتن نرم افزار کاملاً صحیح بسیار گران و چالش برانگیز است. بخشی از این مشکل به دلیل عدم پشتیبانی از زبان برنامه نویسی است. زبانهای موجود ، مانند C یا OCaml یا Solidity ، به خوبی با ابزارهای تأیید ادغام نشده اند و برای ایجاد و اثبات اثبات دستی به زمان نیاز دارند. با این حال ، زبان DeepSEA راهی برای تأیید رسمیت صحیح بودن سختی صحت در مورد قراردادهای هوشمند با استفاده از Coq Proof Assistant به روشی مقیاس پذیر و خودکار ارائه می دهد. با فرض اینکه بیشتر وقت یک توسعه دهنده برای نوشتن اثبات در یک دستیار اثبات تعاملی مانند Coq صرف می شود ، DeepSEA قصد دارد تا حد امکان مشغله کاری را حذف کند و به توسعه دهندگان کمک کند تا سیستم خود را در ماژول های جداگانه ساختار دهند تا بقیه سیستم دارای تأیید شده باشد.هنگام طراحی زبان آن، از چهار اصل استفاده شده است که بهترین ویژگی های چندین زبان برنامه نویسی دیگر را با هم ترکیب می کند:
کمک هزینه بنیاد Ethereum آخرین سری از کمک هزینه های پژوهشی با اهمیت است که به پروژه DeepSEA اعطا شده است. در اوایل سال جاری ، IBM اعطای کمک هزینه تحقیقاتی برای پروژه DeepSEA برای امکان تأیید رسمی قراردادهای هوشمند در Hyperledger Burrow را پرداخت کرد. در دسامبر 2018 ، بنیاد Qtum 400 هزار دلار به تلاش های DeepSEA آزمایشگاه پروفسور Gu در دانشگاه کلمبیا اعطا کرد. زبان DeepSEA در ابتدا در آزمایشگاه تحقیقاتی پروفسور شائو ، رئیس گروه علوم کامپیوتر در دانشگاه ییل و بنیانگذار CertiK ساخته شد و در اصل برای پیاده سازی نرم افزار سیستم پیچیده مانند هسته سیستم عامل طراحی شده است. با وجود عواقب واضح درباره آسیب پذیری های قرارداد هوشمند ، اجرای قراردادهای هوشمند به عنوان گسترش مناسبی از ویژگی های محافظتی زبان DeepSEA عمل می کند. پروفسور گو می گوید: "قراردادهای هوشمند نقش محوری در گسترش blockchain دارد." وی افزود: "از آنجا كه این قراردادها خود اجرا شده و دائمی هستند ، بسیار مهم است كه این قراردادها فقط به همان صورتی كه برای آنها در نظر گرفته شده انجام شود. زبان DeepSEA به برنامه نویسان این امکان را می دهد تا با اطمینان از مطابقت دقیق کد با مشخصات آن ، با استفاده از تأیید رسمی ، پادمان هایی را اضافه کنند. " تأیید رسمی ، فرآیند استفاده از اثبات ریاضی برای تأیید صحت اجرای کد است. با استفاده از NASA Mars Rover و سایر سیستم های سخت افزاری مهم ماموریت ، تصویب رسمی در سیستم های نرم افزاری با ظهور قراردادهای هوشمند افزایش یافته است. CertiK ، متخصص در استفاده از تأیید رسمی برای حسابرسی قراردادهای هوشمند و پروتکل های بلاکچین ، با تأیید بیش از 160 پروژه رمز از جمله BNB و TrueUSD ، بیش از 1.2 میلیارد دلار دارایی را تأمین کرده است. این شرکت در اکتبر گذشته سرمایه گذاری تحت هدایت آزمایشگاه های Binance را اعلام کرد که در آن الا ژانگ ، مدیر عامل شرکت آزمایشگاه Binance ، توانایی CertiK را در "دور زدن محدودیت های تشخیص دستی" را ستوده بود. کمک هزینه های تحقیقاتی اخیر زبان برنامه DeepSEA نشانگر رویکرد فعال محدود کردن آسیب پذیری های امنیتی با پیشرفت روش های کدگذاری و فناوری زیربنایی است.
استدلال معادله ای :
هر اصطلاح DeepSEA به مشخصات عملکردی مربوطه ترجمه می شود ، سپس می توان در دستیار اثبات Coq استدلال کرد.
مشخصات لایه ای :
فناوری DeepSEA با استفاده از لایه های انتزاعی که نمای سطح بالایی از برنامه را فراهم می کند، مدرک ها را کنترل می کند. کامپایلر ثابت می کند که اجرای bytecode خام همانگونه که در نظر گرفته شده رفتار می کند ، در حالی که برنامه نویس فقط باید نمایندگی سطح بالا را بررسی کند.
کپسوله سازی و ترکیب :
هر لایه DeepSEA از مجموعه ای از اشیا تشکیل شده است که در بالای یک لایه دیگر ساخته شده اند و می توان لایه ها را به صورت یکجا درست اثبات کرد.
تصفیه داخلی داخلی :
هر لایه DeepSEA سیستم های بزرگتر را در مراحل کاربر پسند تأیید می کند. این فرایند به عنوان مجموعه ای از اثبات تصفیه پیوند یافته است که ثابت می کند یک برنامه پیوندی با مشخصات مطابقت دارد.
اهمیت فناوری DEEPSEA چگونه آشکار می شود ؟
اکوسیستم های بلاکچین بر پایه های اعتماد بنا شده اند. در حالی که برخی معتقدند پروتکل های اجماع باعث اعتماد بلاکچین ها می شود ، اما برخی کدها به دلیل اشکالات برنامه و هکرهای مخرب هنوز قابل اعتماد نیستند. به عنوان مثال، اگر عملکرد خاصی در قرارداد هوشمند شما سرریز شود - این یک مشکل است. اگر اجرای عملکردی با مشخصات مطابقت ندارد و منجر به آسیب پذیری (غیر) عمدی می شود - این یک مشکل است. اگر اعتماد را از افراد به سمت برنامه ها سوق دهید ، برنامه باید قابل اعتماد باشد. این الزام در بلاکچین مهم است زیرا به محض اینکه یک قرارداد هوشمند به کار گرفته شد ، لغو آن هیچ راهی آسان ندارد و آسیب پذیری های غیر قابل شناسایی را برای بهره برداری باز می گذارد. تأیید رسمی تنها روش مطمئن برای اطمینان از هوای بسته و فشرده بودن کد در برابر حقایق ریاضی صریح است. با اثبات اینکه این برنامه از هر مقدار ورودی ممکن به درستی استفاده می کند ، از نظر ریاضی اطمینان حاصل می کند که کد فقط مطابق آنچه در نظر گرفته شده کار می کند. و در همه مواردی که تأیید رسمی اعمال می شود ، DeepSEA به توسعه دهندگان اجازه می دهد تعداد دلخواه قراردادهای پیچیده را ثابت کنند. قراردادها از ساده تا پیچیده و همچنین تأیید رسمی نیز وجود دارد. ابزارهای اتوماتیک موجود با قراردادهای بسیار ساده ای از جمله توکن به خوبی سر و کار دارند. با این حال ، برای تأیید قراردادهای پیچیده مانند طرح های رأی دادن یا تعاملات بین زنجیره ای ، ما نیاز به انعطاف پذیری برای تعریف مشخصات و اثبات دلخواه پیچیده داریم. این جایی است که دستیارهای اثبات تعاملی مانند Coq می درخشند. با ادغام قراردادهای هوشمند و Coq ، می توانیم تأیید رسمی را در چالش برانگیزترین کارها اعمال کنیم ، و یک سیستم کاملاً تأیید شده از پایان به پایان را فراهم می کنیم.
آیا زبان های دیگری وجود دارد که از این پشتیبانی کند؟
امروزه ، تقریباً تمام قراردادها به زبان های برنامه نویسی نوشته شده اند که بدون در نظر گرفتن تأیید رسمی طراحی شده اند. حتی هنگامی که آنها با یک سیستم تأیید رسمی ادغام می شوند ، معمولاً در جهت برخورد خودکار با موارد ساده هستند. داخلی Solidity SMT یک مثال خوب است. حل کننده SMT به برنامه نویسان اجازه می دهد تابعی را با شرایطی که صحیح فرض شده اند ، حاشیه نویسی کنند ، ادعاهایی را بنویسند که باید حفظ شوند و از کامپایلر بخواهند که آنها را به صورت خودکار ثابت کند.
منبع : موسسه برسیپا / گرافیک : فریبا باستان، بهار پورنقش بند / 11 آبان ماه 1399