Співзасновник Ethereum Віталік Бутерін не вірить, що вдосконалення штучного інтелекту зрештою зробить кібербезпеку принципово безнадійною.
Бутерін упевнений, що зрештою може статися протилежне: ШІ може дати захисникам інструменти, необхідні для створення програмного забезпечення, яке значно важче експлуатувати з самого початку.
«Дедалі поширенішою стає думка, що злам за допомогою ШІ означає, що кібербезпека приречена. Я не згоден», — написав Бутерін у довгому й характерно змістовному дописі в соціальній мережі X у середу.
На думку співзасновника Ethereum, кібербезпека природно має схилятися на користь захисників, щойно розробники почнуть повною мірою використовувати формальну верифікацію.
Бутерін також безпосередньо пов'язав це переконання з власною схильністю до криптовалюти, розкривши, що приблизно 90% його статків залишаються в криптовалюті.
Будь-хто, хто й надалі тримає значні обсяги криптовалюти, стверджував він, неявно робить ставку на те, що достатньо захищені цифрові системи можна побудувати попри дедалі витонченіших атакувальників.
«Якщо ШІ може довести рівняння Нав'є — Стокса та Велику теорему Ферма, то ШІ може довести твердження "ця програма є безпечною" як математичну теорему», — написав Бутерін, маючи на увазі проблему Нав'є — Стокса та Велику теорему Ферма.
Його аргумент ґрунтується на формальній верифікації — методі математичного доведення того, що програмне забезпечення задовольняє певні властивості.
Бутерін докладно досліджував ту саму ідею у своєму травневому есеї, в якому описав формальну верифікацію за допомогою ШІ як надзвичайно трансформаційний інструмент для програмного забезпечення, критичного для безпеки. Однак довести, що таке програмне забезпечення є безпечним, може виявитися складним завданням.
Проблема визначення
Бутерін використав застосунок для зашифрованих повідомлень Signal як приклад, щоб показати, чому це може бути складним.
Атакувальник може спробувати підробити повідомлення, перешкодити їхньому надходженню, відтворити старі повідомлення, скомпрометувати сервер, маніпулювати процесом, який використовується для виявлення відкритого ключа іншого користувача, або скористатися вразливістю в операційній системі.
Інші проблеми можуть виникати через пошкоджені бази даних, шкідливі бібліотеки, компілятори або навіть витік інформації на рівні апаратного забезпечення.
Навіть якщо вміст розмови залишається зашифрованим, атакувальник усе одно може дізнатися, хто спілкується. Як наслідок, саме математичне визначення того, що насправді означає «безпечний», може стати надзвичайно складним.
«Отже... навіть визначення можуть займати понад тисячу рядків коду, і для того, щоб їх з'ясувати, потрібні глибокі ретельні роздуми», — написав Бутерін.
Атакувальник і захисник
Без сумніву, потужніші системи ШІ могли б полегшити пошук вразливостей.
Однак те саме вдосконалення машинного міркування могло б також різко знизити вартість формального доведення того, що програмне забезпечення поводиться відповідно до ретельно побудованих специфікацій безпеки.
Обидві сторони матимуть ШІ.
