Исследователи представили Frame — фреймворк для повышения точности обнаружения уязвимостей в коде с помощью LLM. Система объединяет возможности генеративных моделей с формальной логикой разделения (separation logic), что позволяет верифицировать найденные ошибки и минимизировать количество ложноположительных срабатываний, характерных для стандартных нейросетевых анализаторов кода.
Основная проблема существующих ИИ-инструментов для поиска уязвимостей заключается в их склонности к «галлюцинациям» и неспособности глубоко понимать семантику управления памятью. Frame решает эту задачу, используя LLM для генерации потенциальных векторов атак, которые затем проходят строгую проверку через формальный движок. Такой гибридный подход обеспечивает математическую обоснованность выводов, делая процесс аудита безопасности более надежным и предсказуемым.
Интеграция формальных методов в агентные системы анализа кода позволяет автоматизировать сложные проверки, требующие понимания состояния кучи и указателей. Это значительно снижает нагрузку на специалистов по безопасности, так как система не просто подсвечивает подозрительные участки, но и предоставляет логическое обоснование того, почему конкретный фрагмент кода является уязвимым.
Ключевые факты
- Frame использует логику разделения (separation logic) для формальной верификации результатов, полученных от LLM.
- Метод направлен на устранение ложноположительных срабатываний, которые часто возникают при использовании чисто статистических моделей.
- Фреймворк позволяет эффективно отслеживать ошибки управления памятью, такие как утечки или некорректное освобождение ресурсов.
- Система ориентирована на автоматизацию аудита безопасности в сложных программных проектах, где ручной анализ кода затруднен из-за большого объема данных.