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

پروتکل سیگنال یکی از فناوری‌های شناخته‌شده در حوزه ارتباطات رمزنگاری‌شده است و در سرویس‌هایی مانند پیام‌رسان سیگنال، گوگل مسیجز و واتس‌اپ مورد استفاده قرار می‌گیرد. به همین دلیل، بررسی مستقل ویژگی‌های امنیتی این پروتکل اهمیت زیادی دارد. پژوهشگران دیپ‌مایند در این پروژه از ابزار AlphaProof Code برای ارزیابی ریاضی برخی از تضمین‌های رمزنگاری آن استفاده کردند.

اعتبارسنجی رسمی امنیت با کمک هوش مصنوعی

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

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

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

 AlphaProof Code توانست این ضعف‌ها را شناسایی کند و نشان دهد نسخه‌های قدیمی در برخی الزامات امنیتی موفق نیستند.

آیا امنیت کامل سیگنال تأیید شده است؟

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

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

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

آینده امنیت نرم‌افزار با هوش مصنوعی

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

هدف نهایی ایجاد فرایندی است که در آن هوش مصنوعی بتواند بخش عمده کارهای فنی را انجام دهد و انسان همچنان بر تعریف الزامات و ارزیابی نتایج نظارت داشته باشد . این پروژه در مجموع نشان می‌دهد هوش مصنوعی می‌تواند به ابزاری مؤثر برای بررسی امنیت نرم‌افزار، اعتبارسنجی پروتکل‌های رمزنگاری و شناسایی برخی آسیب‌پذیری‌ها تبدیل شود؛ هرچند اثبات امنیت کامل سامانه‌های پیچیده همچنان به بررسی‌های گسترده‌تر نیاز دارد.