نقش هوش مصنوعی در امنیت قراردادهای هوشمند از نگاه ویتالیک بوترین
«ویتالیک بوترین» همبنیانگذار اتریوم، در جدیدترین تحلیل خود دیدگاهی متفاوت نسبت به آینده امنیت سایبری و هوش مصنوعی ارائه کرده است. در حالی که بسیاری از کارشناسان معتقدند ابزارهای مبتنی بر AI میتوانند یافتن باگها و حملات سایبری را آسانتر کنند و در نتیجه امنیت نرمافزارها را تهدید نمایند، بوترین بر این باور است که ترکیب هوش مصنوعی با «Formal Verification» یا اعتبارسنجی رسمی، میتواند عصر جدیدی از نرمافزارهای فوقامن را ایجاد کند.
او در توضیح این موضوع نوشت:
«بسیاری تصور میکنند با پیشرفت هوش مصنوعی، ساخت نرمافزار امن غیرممکن خواهد شد. اما من دیدگاه بسیار خوشبینانهتری دارم و اعتبارسنجی رسمی مبتنی بر AI دلیل اصلی آن است.»
Formal Verification چیست و چرا اهمیت دارد؟
اعتبارسنجی رسمی روشی است که در آن بهجای آزمایش سنتی نرمافزار، برای کدها اثباتهای ریاضی نوشته میشود تا ثابت شود برنامه دقیقاً همان کاری را انجام میدهد که توسعهدهنده انتظار دارد.
در این روش، سیستم بهصورت ریاضی تضمین میکند که نرمافزار تحت تمامی شرایط، رفتاری صحیح و بدون خطا خواهد داشت. اگرچه این فناوری دهههاست وجود دارد، اما به دلیل پیچیدگی بالا و زمانبر بودن فرآیند اثباتها، تاکنون تنها در پروژههای بسیار حساس استفاده میشد.
بوترین معتقد است هوش مصنوعی میتواند این معادله را تغییر دهد. به گفته او، AI قادر است هم کد و هم اثباتهای ریاضی را تولید کند و انسان تنها کافی است بررسی کند که اهداف تعریفشده با نیاز واقعی سیستم مطابقت دارند.
چرا این موضوع برای اتریوم مهم است؟
ویتالیک بوترین توضیح داد که بخشهایی از اکوسیستم اتریوم هماکنون از اعتبارسنجی رسمی استفاده میکنند. این حوزهها شامل موارد زیر هستند:
- امضاهای مقاوم در برابر رایانههای کوانتومی
- سیستمهای اثبات STARK
- الگوریتمهای اجماع
- ZK-EVMها و فناوریهای دانش صفر
او اشاره کرد که پروژههایی مانند Arklib در حال توسعه پیادهسازی کاملاً تأییدشده STARK هستند و پروژه evm-asm نیز روی نسخهای از ماشین مجازی اتریوم کار میکند که بهصورت ریاضی اعتبارسنجی شده است.
به گفته بوترین، این فناوری میتواند فاصله بین «آنچه کد انجام میدهد» و «آنچه باید انجام دهد» را تقریباً به صفر برساند.
آیا Formal Verification همه مشکلات را حل میکند؟
بوترین تأکید کرد که اعتبارسنجی رسمی راهحل جادویی نیست و محدودیتهای مهمی دارد. برای مثال:
- ممکن است تنها بخشی از سیستم اعتبارسنجی شود و باگها در بخشهای دیگر باقی بمانند
- توسعهدهندگان ممکن است برخی ویژگیهای حیاتی را در اثباتها لحاظ نکنند
- خود تعریف ریاضی سیستم میتواند اشتباه باشد
- حملات سختافزاری مانند Side-Channel همچنان ممکن است رخ دهند
او توضیح داد:
«درست بودن ریاضی یک نرمافزار الزاماً به معنی درست بودن آن از نگاه انسانها نیست.»
آیندهای که بوترین تصور میکند
بوترین آینده نرمافزارها را به دو لایه تقسیم میکند:
۱. لایه ناامن (Edge Layer)
این بخش شامل سرویسهای کماهمیتتر است که در محیطهای محدود و ایزوله اجرا میشوند و دسترسی محدودی دارند.
۲. هسته امن (Secure Core)
این لایه شامل بخشهای حیاتی مانند:
- شبکه اتریوم
- هسته سیستمعاملها
- زیرساختهای اینترنت اشیا
- و سیستمهای مالی حساس
خواهد بود و تحت سختگیرانهترین فرآیندهای اعتبارسنجی رسمی قرار میگیرد.
به اعتقاد او، هوش مصنوعی توان محاسباتی لازم را برای عملیکردن این مدل در مقیاس گسترده فراهم میکند.
تأثیر احتمالی بر آینده بلاکچین و امنیت سایبری
اظهارات بوترین میتواند اهمیت زیادی برای صنعت بلاکچین داشته باشد؛ صنعتی که امنیت قراردادهای هوشمند و زیرساختهای غیرمتمرکز در آن حیاتی است.
اگر ترکیب AI و Formal Verification به بلوغ برسد، پروژههای بلاکچینی میتوانند:
- امنیت قراردادهای هوشمند را بهشدت افزایش دهند
- احتمال هک و باگهای میلیوندلاری را کاهش دهند
- اعتماد مؤسسات مالی به دیفای را تقویت کنند
- و زیرساختهای بلاکچینی مقاومتری ایجاد نمایند
جمعبندی
ویتالیک بوترین معتقد است برخلاف نگرانیهای رایج، هوش مصنوعی لزوماً تهدیدی برای امنیت نرمافزارها نیست؛ بلکه میتواند به ابزاری برای ساخت امنترین سیستمهای تاریخ تبدیل شود.
به باور او، ترکیب AI و اعتبارسنجی رسمی میتواند آیندهای ایجاد کند که در آن نرمافزارهای حیاتی، از بلاکچین گرفته تا سیستمهای مالی و زیرساختهای اینترنت، با اطمینان ریاضی محافظت شوند؛ آیندهای که در آن «مدافعان امنیت» بالاخره شانس پیروزی قطعی خواهند داشت.
