Алгоритм зміг виявити недоліки, які залишалися непоміченими попри мільйони автоматизованих запусків Anthropic заявила, що модель Claude офіційно перевірила властивості безпеки 123 бібліотек з відкритим кодом і виявила сотні прихованих помилок завдяки використанню математичних доказів.Про це пише РБК-Україна з посиланням на Interesting Engineering.Штучний інтелект успішно впорався із завданням перевірки безпеки ПЗ.У межах спільного проєкту з фірмою Theorem, що спеціалізується на верифікації програм, розробники Anthropic застосували математичні докази безпосередньо до скомпільованого машинного коду.Цей підхід дозволяє зробити ретельну перевірку доступною для набагато ширшого кола технологічних проєктів.Розробники зазначили: традиційні інструменти тестування та фаззингу генерують велику кількість вхідних даних, проте фізично не здатні вичерпати всі можливі комбінації. Не пропустіть: Запобігти ядерній катастрофі: GPT і Claude дозволили пожертвувати чоловікамиЯк Claude створює математичні докази?Для аналізу Anthropic використала модель Claude, яка перетворила наявні фаз-тести на чіткі математичні специфікації. Після цього ШІ згенерував докази того, що 239 точок входу у 123 бібліотеках не спричинять збоїв за визначених умов.Під час роботи досліджувався асемблерний код архітектури RISC-V, який відображає інструкції процесора:Claude згенерував приблизно 180 мільйонів рядків коду доказуТиповий сформований доказ охоплює близько 600000 рядківОкремий незалежний інструмент під назвою Rocq перевірив згенеровані докази на відповідність специфікаціям.Це звільнило розробників від необхідності вручну перевіряти кожен рядок коду. Більше того, модель самостійно виправляла знайдені помилки та генерувала нові докази для оновленого програмного забезпечення. Читайте більше: ШІ самостійно зламав понад 100 сайтів: одна атака коштувала хакеру лише 50 доларівВразливості, які витримали роки випробуваньЗавдяки новому методу вдалося виявити дефекти, які роками залишалися поза увагою звичайних тестувальників:Лічильник недоповнення, що міг спровокувати запис за межі допустимих значень під час декомпресії.Помилка у декодері зображень, для виявлення якої знадобилося ввести майже 64 МБ даних та понад 2 ГБ оперативної пам'яті.Зчитування за межами дозволеного діапазону залежно від послідовності операцій з дескрипторами файлів.Вразливість у популярному XML-парсері libexpat.Логічна помилка, яка дозволяла обійти функцію обмеження завантаження файлів. Цікаво дізнатися: Контроль замість безпеки: OpenAI та Anthropic приховують звіти про ризики ШІОбмеження методу та плани на майбутнєНезважаючи на виняткові результати, в Anthropic наголошують, що формально перевірене ПЗ не стає повністю безпомилковим. Отримані гарантії поширюються лише на конкретні властивості, вхідні дані та припущення, описані в кожному окремому доказі.Поточні тести охоплюють лише однопотокові та статично зв'язані програми RISC-V у змодельованому середовищі Linux.З усім тим, компанія очікує, що вдосконалення моделей та можливість повторного використання доказів дозволять суттєво знизити вартість перевірки критичних компонентів у майбутньому.Ще більше цікавого:Працює навіть із вимкненим ПК: Anthropic випустила проактивного агента Claude DuetСмерть 50 людей чи мільярд збитків: Anthropic вигадала критерії бану ШІ