
«ویتالیک بوترین» همبنیانگذار اتریوم، در جدیدترین تحلیل خود دیدگاهی متفاوت نسبت به آینده امنیت سایبری و هوش مصنوعی ارائه کرده است. در حالی که بسیاری از کارشناسان معتقدند ابزارهای مبتنی بر AI میتوانند یافتن باگها و حملات سایبری را آسانتر کنند و در نتیجه امنیت نرمافزارها را تهدید نمایند، بوترین بر این باور است که ترکیب هوش مصنوعی با «Formal Verification» یا اعتبارسنجی رسمی، میتواند عصر جدیدی از نرمافزارهای فوقامن را ایجاد کند.
او در توضیح این موضوع نوشت:
«بسیاری تصور میکنند با پیشرفت هوش مصنوعی، ساخت نرمافزار امن غیرممکن خواهد شد. اما من دیدگاه بسیار خوشبینانهتری دارم و اعتبارسنجی رسمی مبتنی بر AI دلیل اصلی آن است.»
اعتبارسنجی رسمی روشی است که در آن بهجای آزمایش سنتی نرمافزار، برای کدها اثباتهای ریاضی نوشته میشود تا ثابت شود برنامه دقیقاً همان کاری را انجام میدهد که توسعهدهنده انتظار دارد.
در این روش، سیستم بهصورت ریاضی تضمین میکند که نرمافزار تحت تمامی شرایط، رفتاری صحیح و بدون خطا خواهد داشت. اگرچه این فناوری دهههاست وجود دارد، اما به دلیل پیچیدگی بالا و زمانبر بودن فرآیند اثباتها، تاکنون تنها در پروژههای بسیار حساس استفاده میشد.
بوترین معتقد است هوش مصنوعی میتواند این معادله را تغییر دهد. به گفته او، AI قادر است هم کد و هم اثباتهای ریاضی را تولید کند و انسان تنها کافی است بررسی کند که اهداف تعریفشده با نیاز واقعی سیستم مطابقت دارند.
ویتالیک بوترین توضیح داد که بخشهایی از اکوسیستم اتریوم هماکنون از اعتبارسنجی رسمی استفاده میکنند. این حوزهها شامل موارد زیر هستند:
او اشاره کرد که پروژههایی مانند Arklib در حال توسعه پیادهسازی کاملاً تأییدشده STARK هستند و پروژه evm-asm نیز روی نسخهای از ماشین مجازی اتریوم کار میکند که بهصورت ریاضی اعتبارسنجی شده است.
به گفته بوترین، این فناوری میتواند فاصله بین «آنچه کد انجام میدهد» و «آنچه باید انجام دهد» را تقریباً به صفر برساند.
بوترین تأکید کرد که اعتبارسنجی رسمی راهحل جادویی نیست و محدودیتهای مهمی دارد. برای مثال:
او توضیح داد:
«درست بودن ریاضی یک نرمافزار الزاماً به معنی درست بودن آن از نگاه انسانها نیست.»
بوترین آینده نرمافزارها را به دو لایه تقسیم میکند:
این بخش شامل سرویسهای کماهمیتتر است که در محیطهای محدود و ایزوله اجرا میشوند و دسترسی محدودی دارند.
این لایه شامل بخشهای حیاتی مانند:
خواهد بود و تحت سختگیرانهترین فرآیندهای اعتبارسنجی رسمی قرار میگیرد.
به اعتقاد او، هوش مصنوعی توان محاسباتی لازم را برای عملیکردن این مدل در مقیاس گسترده فراهم میکند.
اظهارات بوترین میتواند اهمیت زیادی برای صنعت بلاکچین داشته باشد؛ صنعتی که امنیت قراردادهای هوشمند و زیرساختهای غیرمتمرکز در آن حیاتی است.
اگر ترکیب AI و Formal Verification به بلوغ برسد، پروژههای بلاکچینی میتوانند:
ویتالیک بوترین معتقد است برخلاف نگرانیهای رایج، هوش مصنوعی لزوماً تهدیدی برای امنیت نرمافزارها نیست؛ بلکه میتواند به ابزاری برای ساخت امنترین سیستمهای تاریخ تبدیل شود.
به باور او، ترکیب AI و اعتبارسنجی رسمی میتواند آیندهای ایجاد کند که در آن نرمافزارهای حیاتی، از بلاکچین گرفته تا سیستمهای مالی و زیرساختهای اینترنت، با اطمینان ریاضی محافظت شوند؛ آیندهای که در آن «مدافعان امنیت» بالاخره شانس پیروزی قطعی خواهند داشت.


