Американский стартап создал алгоритм для верификации ПО при помощи математики
Американский стартап &Truth представил инструмент для автоматизированной формальной верификации программного обеспечения. Компания привлекла $70 млн инвестиций для развития технологий математического доказательства корректности кода.
Главный научный сотрудник компании Илья Сергей сравнивает этот процесс с проектированием мостов. Он утверждает, что предварительные математические расчеты гарантируют надежность конструкции. По его словам, технологии для математического обоснования кода существовали давно, однако разработчики испытывали трудности с масштабным применением таких инструментов.
Толчком к развитию отрасли стали успехи в применении искусственного интеллекта для проверки систем шифрования. Исследовательница одного из американских университетов Чуэ Сунь вместе с коллегами создала инструмент на базе нейросетей. Этот алгоритм за полдня выполнил проект по верификации протокола мессенджера Signal, потратив при этом менее $500.
Ранее аналогичная задача требовала пяти месяцев ручной работы трех специалистов. В августе специалистка присоединилась к команде &Truth. Эта компания ставит целью автоматизировать проверку любого языка программирования.
Индустрия формальной верификации привлекает значительные капиталы и крупных игроков. Другая профильная компания Harmonic ранее получила $295 млн финансирования. Соучредителем этого бизнеса выступил глава Robinhood Влад Тенев.
Разработчики представили агента Aristotle с поддержкой языков C и Verilog. Продукт уже тестируют производители чипов, в том числе Nvidia. На прошлой неделе компании Anthropic и Theorem также сообщили об успешном применении нейросетей для поиска уязвимостей в открытых проектах.
Несмотря на приток инвестиций, эксперты отрасли сохраняют скепсис относительно универсальности метода. Глава компании Antithesis Уилл Уилсон отмечает, что математическое доказательство не гарантирует защиты от сбоев оборудования или ошибок пользователей. Его бизнес потратил миллионы долларов на формальную верификацию, но собственные тесты выявили дополнительные недочеты в коде после проверки.
Создатель криптовалюты Ethereum Виталик Бутерин также признает, что этот подход не решит всех проблем, хотя и считает его важным рубежом защиты от кибератак.
Крупные технологические компании пока осторожно внедряют формальную верификацию из-за высокой стоимости и длительных сроков. Корпорация Apple успешно использовала этот метод для проверки криптографической библиотеки. Однако специалистам компании приходится консервативно подходить к обновлениям из-за длительности аудитов.
Руководители стартапов Proofcraft Джун Андроник и Гервин Кляйн предупреждают об одной проблеме: при автоматизации спецификаций с помощью ИИ у разработчиков может возникать ложное чувство безопасности. На данный момент ни одна система формальной верификации не может заменить собой ручную проверку.
Подпишитесь на «Инк» в Telegram. Там мы пишем нескучным языком о самом важном для предпринимателей. Подписаться.
