Проблема «слепых зон» в верификации C-кода
Большие языковые модели (LLM) уже научились генерировать функциональные контракты и инварианты циклов, но часто игнорируют frame conditions (условия фрейма). Эти условия критически важны для формальной верификации, так как они точно указывают, какие области памяти могут быть изменены, а какие остаются нетронутыми во время выполнения функции. Отсутствие точных фреймов делает автоматическую проверку безопасности системного кода неполной.
Методология: CPG как навигатор для LLM
Авторы (Han Zhou, Yu Luo, Dianxiang Xu) предложили подход AutoFraming, который не полагается только на текст кода. Система анализирует Code Property Graphs (CPG) — структурированное представление кода, извлекая из него информацию о зависимостях данных и разделениях регионов памяти. Эти данные используются как контекст для LLM, направляя генерацию спецификаций ACSL (Annotated C Specification Language) в нужное русло.
Результаты бенчмарков
Эксперименты проводились на реальных функциях из нетривиальных систем. Метод демонстрирует статистически значимое превосходство над существующими SOTA-решениями, особенно в снижении количества ошибок в сгенерированных спецификациях.
| Бенчмарк | Количество функций | Результат AutoFraming | Результат SOTA (базовый) | Относительный прирост |
|---|---|---|---|---|
| Набор 1 (реальные системы) | 84 | 92,9% (без ошибок) | ~34,3% | +179% |
| Набор 2 (дополнительный) | 51 | 96,1% | 80,4% | +19,3% (абс.) |
Кроме того, при интеграции AutoFraming в качестве вспомогательного модуля в существующие фреймворки синтеза ACSL, производительность генерации фреймов улучшается до 61,9%.
Почему это важно
Для разработчиков критического ПО (авионика, автопилоты, embedded-системы) точная спецификация того, «что не изменилось» в памяти, так же важна, как и то, «что изменилось». AutoFraming закрывает пробел в автоматизации формальной верификации, позволяя LLM генерировать не просто «похожий» код, а математически корректные контракты для статического анализа.
Источник: arXiv cs.AI ↗