PolyVer: Композиционный подход к моделированию и верификации полиглотных систем

Основная информация

• ID статьи: 2503.03207
• Название: PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
• Авторы: Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
• Категория: cs.PL (Языки программирования)
• Дата публикации/Конференция: Formal Methods in Computer-Aided Design 2025
• Ссылка на статью: https://arxiv.org/abs/2503.03207

Аннотация

Полиглотные программные системы состоят из программ, реализованных на нескольких языках программирования, однако существующие верификаторы программ обычно разработаны для одного языка. Для верификации полиглотных систем обычно требуется их трансляция в универсальный язык верификации или формальное представление. В данной работе предлагается PolyVer — альтернативный подход, использующий абстракцию, композиционное рассуждение и синтез для прямой верификации полиглотных систем. PolyVer моделирует полиглотные системы как формальные модели переходных систем, где функции обновления переходов реализованы на целевых языках (таких как C или Rust). Для выполнения верификации PolyVer связывает проверку моделей переходных систем с верификаторами конкретных языков через контракты предусловия/постусловия функций обновления. Эти контракты автоматически генерируются посредством синтеза, управляемого синтаксисом, или оракулов синтеза на основе больших языковых моделей, и проверяются верификаторами конкретных языков.

Исследовательский контекст и мотивация

Определение проблемы

Современные программные системы все чаще используют многоязычную архитектуру, где фреймворки, такие как ROS2 и Lingua Franca, позволяют разработчикам выбирать наиболее подходящий язык программирования для каждого компонента. Однако эта гибкость создает проблемы верификации:

1. Различия в семантике языков: Разные языки программирования имеют различную синтаксис и семантику. Например, функция saturating_add в Rust насыщается до максимального значения при переполнении, тогда как сложение в C может привести к переносу.
2. Ограничения существующих верификаторов: Большинство верификаторов программ (таких как CBMC для C, Kani для Rust) специально разработаны для одного языка и не могут напрямую обрабатывать полиглотные системы.
3. Сложность трансляции: Трансляция всей полиглотной системы в один язык верификации требует поддержки полной синтаксиса и семантики всех языков, что является непрактичным для современных языков.

Значимость исследования

Возрастающая сложность полиглотных систем увеличивает риск программных ошибок. В критичных по безопасности областях (таких как автономные транспортные средства, аэрокосмическая промышленность) требуются строгие гарантии, обеспечиваемые формальной верификацией, а не только неполные методы, такие как тестирование.

Ограничения существующих подходов

• Монолитные методы трансляции: Требуют разработки полной инфраструктуры компилятора для каждого языка
• Сложность сохранения семантики: Трудно верно отобразить все языковые конструкции исходного языка в целевом языке верификации
• Проблемы масштабируемости: Генерируемые задачи верификации могут стать чрезмерно большими

Основные вклады

1. Формализация проблемы верификации полиглотных систем: Впервые систематически формализована проблема верификации полиглотных систем и предложено композиционное решение, интегрирующее несколько верификаторов конкретных языков.
2. Автоматизированный синтез контрактов: Предложен метод автоматического синтеза и уточнения контрактов предусловия/постусловия с использованием промежуточного языка и цикла CEGIS-CEGAR, поддерживающий синтез, управляемый синтаксисом, и оракулы синтеза на основе больших языковых моделей.
3. Реализация инструмента: Реализован инструмент PolyVer на основе UCLID5, поддерживающий C и Rust через верификаторы CBMC и Kani, демонстрирующий превосходство синтеза на основе LLM над чистыми символическими методами синтеза.
4. Тематические исследования и оценка: Разработана верификация для языка координации Lingua Franca, верифицированы полиглотные системы, содержащие процессы на C и Rust, а также фрагменты C, которые не поддерживались предыдущими работами.

Детальное описание методологии

Определение задачи

Входные данные: Полиглотная модель M = (Q,V,I₀,T,F) и свойство системы φ Выходные данные: Результат верификации (успех/отказ) и возможная контрпримерная трасса Цель: Определить, выполняется ли M ⊨ φ

Где:

• Q: множество состояний
• V: множество типизированных переменных
• I₀: множество начальных состояний
• T: множество переходов состояний
• F: множество процедур

Архитектура модели

1. Расширенный конечный автомат (ESM)

PolyVer моделирует полиглотные системы как расширенные конечные автоматы, где:

• Состояния состоят из режимов и назначений переменных
• Переходы связаны с условиями охраны и отношениями обновления
• Отношения обновления специализированы как последовательности вызовов процедур

2. Промежуточный язык контрактов L*

Ключевым нововведением является введение промежуточного языка L* как "клея" между разными языками:

• Контракты записываются на L*
• Преобразуются в конкретные языки через семантически сохраняющую компиляцию compL
• Избегает сложности полной трансляции языка

3. Гибридный метод CEGIS-CEGAR

Ядро алгоритма представляет собой двухуровневый итеративный цикл:

Внешний цикл CEGAR:

1. Построение абстрактной модели M' с использованием текущих контрактов
2. Проверка моделей верифицирует M' ⊨ φ
3. При отказе проверяется, является ли контрпример ложным
4. При ложности уточняется контракт; в противном случае сообщается истинный контрпример

Внутренний цикл CEGIS:

1. Оракул синтеза генерирует кандидатные контракты
2. Верификатор проверяет корректность контрактов
3. При некорректности добавляются положительные примеры и повторяется синтез

Технические инновации

1. Стратегия композиционной верификации

В отличие от монолитной трансляции, PolyVer использует стратегию "разделяй и властвуй":

• Использует абстракцию контрактов для отдельных процедур
• Верификаторы конкретных языков проверяют корректность контрактов
• Проверка моделей верифицирует свойства уровня системы

2. Автоматизированное генерирование контрактов

Поддерживает несколько оракулов синтеза:

• Синтезатор на основе LLM: Использует подсказки цепочки мышления и Python DSL
• Синтезатор SyGuS/SyMO: Кодирует задачу как задачу синтеза на основе примеров

3. Проверка ложности

Проверяет достижимость контрпримерной трассы через верификацию {V = d} C {V' ≠ d'}, различая истинные и ложные контрпримеры.

Экспериментальная установка

Набор данных

1. Тестовый набор LFVerifier: 22 программы Lingua Franca с ограниченным синтаксисом C
2. Полные примеры LF: Контроллер светодиодов, робот-альпинист, контроллер ориентации спутника и другие встроенные системы
3. Полиглотные системы: Программы LF на C/Rust, приложения ROS2, программы с вызовами FFI

Метрики оценки

• Количество итераций синтеза (IS: итерации CEGIS, AR: итерации CEGAR)
• Время выполнения (SOT: время оракула синтеза, VOT: время верификации оракула, UT: время UCLID5)
• Процент успешной верификации

Методы сравнения

Сравнение с LFVerifier15, единственным известным инструментом для автоматизированной верификации программ LF от конца к концу.

Детали реализации

• Использование OpenAI o1-mini в качестве синтезатора LLM с 3 параллельными запросами на процедуру
• CBMC-6.3.1, Kani-0.56.0, z3-4.8.7 в качестве верификационных бэкендов
• Машина Intel Core i9 3.7GHz с 62GB оперативной памяти

Результаты экспериментов

Основные результаты

RQ1: Сравнение с существующей работой по верификации LF

На 22 тестовых примерах:

• PolyVer успешно верифицирует все примеры, LFVerifier не может верифицировать пример TrafficLight
• 18 примеров корректно синтезируют контракты за один цикл CEGIS, среднее время 37 секунд
• Хотя общее время выполнения медленнее (в основном из-за времени синтеза контрактов), обеспечивает значительные качественные улучшения

RQ2: Обработка полных примеров LF

Успешная верификация встроенных систем с полным кодом на C:

• Контроллер светодиодов: 1 процедура, 123 строки кода C, 31.0 секунд синтеза
• Робот-альпинист: 12 процедур, 75 строк кода C/Rust, 685.4 секунд синтеза
• Контроллер спутника: 6 процедур, 424 строки кода C, 729.0 секунд синтеза

RQ3: Верификация полиглотных систем

Верификация истинно полиглотных систем:

• Программы LF на смеси C/Rust
• Приложения сервисов ROS2
• Программы с кросс-языковыми вызовами FFI

Важные выводы

1. LLM превосходит символические методы: Решатели SyGuS/SyMO требуют большого количества итераций CEGAR и часто не завершаются
2. Вызовы синтеза контрактов: Процедуры со сложным потоком управления и зависимостями данных требуют больше итераций
3. Проверка практичности: Способность обрабатывать реальный код реализации, а не только игрушечные примеры

Связанные работы

Верификация полиглотных систем

• Методы ручной трансляции: Cook и др. транслировали код ассемблера в C для верификации гипервизора Xen
• Автоматическая трансляция фрагментов: LFVerifier автоматически транслирует фрагменты C в язык верификации
• Методы черного ящика: Вывод резюме из поведения входа-выхода

Композиционная верификация

• Композиционная верификация на основе логики Хоара широко применяется к крупномасштабным однояычным программам
• Использование абстрактной интерпретации и CEGAR для автоматизации обучения предусловиям/постусловиям

Вывод контрактов

• Методы вывода контрактов, управляемые свойствами
• Решатели ограничивающих предложений Horn
• Недавние приложения LLM в изучении спецификаций

Заключение и обсуждение

Основные выводы

1. PolyVer успешно решает ключевые проблемы верификации полиглотных систем
2. Композиционный подход избегает сложности полной трансляции языка
3. Автоматизированный синтез контрактов делает метод практичным
4. Синтезаторы на основе LLM превосходят традиционные символические методы

Ограничения

1. Завершаемость: Алгоритм не гарантирует завершение, зависит от качества оракула синтеза
2. Поддержка языков: В настоящее время поддерживает только C и Rust, требуется разработка оракулов верификации для других языков
3. Выразительность контрактов: Выразительная способность промежуточного языка L* ограничивает сложность верифицируемых свойств
4. Масштабируемость: Время синтеза контрактов для крупных систем может стать узким местом

Направления будущих исследований

1. Расширение на другие полиглотные распределенные программные системы и робототехнические системы
2. Применение к формальной верификации трансляции кода (например, трансляция C в Rust)
3. Улучшение эффективности и точности синтеза контрактов
4. Поддержка более сложных свойств временной логики

Глубокая оценка

Преимущества

1. Значимость проблемы: Верификация полиглотных систем — это практическая и важная проблема
2. Инновационность метода: Комбинация композиционной верификации и автоматизированного синтеза контрактов является новой
3. Теоретическая основа: Четкая формализация определений, явные гарантии корректности
4. Практическая ценность: Способность обрабатывать реальные системы, а не только игрушечные примеры
5. Реализация инструмента: Предоставляется практически применимая реализация инструмента

Недостатки

1. Производительность: Время синтеза контрактов значительно, может ограничить практическое применение
2. Охват языков: В настоящее время поддерживает только C и Rust, расширяемость требует проверки
3. Ограниченные тестовые примеры: Хотя включены реальные примеры, их масштаб относительно небольшой
4. Зависимость от LLM: Зависимость от коммерческих сервисов LLM может повлиять на воспроизводимость

Влияние

1. Академический вклад: Открывает новое направление исследований в верификации полиглотных систем
2. Практическая ценность: Предоставляет инструмент верификации для критичных по безопасности полиглотных систем
3. Техническое вдохновение: Идея использования контрактов как интерфейса между языками имеет универсальную ценность

Применимые сценарии

1. Встроенные системы: Системы реального времени на смеси C/Rust
2. Распределенные системы: Фреймворки ROS2, gRPC и другие многоязычные платформы
3. Критичные по безопасности приложения: Системы, требующие гарантий формальной верификации
4. Интеграция унаследованных систем: Системы со смешанным старым и новым кодом

Библиография

Статья цитирует 50 связанных работ, охватывающих полиглотные системы, формальную верификацию, вывод контрактов, синтез, управляемый синтаксисом, и другие области, обеспечивая прочную теоретическую основу для исследования.

Общая оценка: Это высококачественная системная исследовательская работа, решающая важную и практическую проблему. Метод инновационен, эксперименты полны, реализация инструмента завершена. Хотя есть место для улучшения в производительности и масштабируемости, работа вносит значительный вклад в область верификации полиглотных систем.