Развитие методов и инструментов дедуктивной верификации императивных программ

Большинство инструментов дедуктивной верификации императивных программ условно делятся на два класса: инструменты авто-активной и интерактивной верификации. Авто-активная верификация основана на использовании полностью автоматических инструментов доказательства теорем (в основном, SMT- и суперпозиционных решателей), в то время как в интерактивной верификации используются инструменты интерактивного доказательства, такие как Coq, Isabelle/HOL и Lean. Инструменты обоих классов обладают общим существенным недостатком: сложность (стоимость) их применения практически всегда является невысокой только для относительно небольшого класса достаточно специфических и небольших по размеру программ.

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

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

Ядром развиваемого в нашем отделе инструмента дедуктивной верификации PLRDF (Paths, Labels, Regions and Dynamic Frames), реализованного в виде пакета расширения системы интерактивного доказательства теорем Isabelle/HOL, является процедура элаборации, которая по сути реализует относительно простую дискретную экспертную систему для применения правил переноса и абстракции предикатов (а также разрешения возникающих при этом побочных предусловий) над конечной последовательностью состояний программы (путем выполнения) из базы знаний, представленной в виде упорядоченных наборов правил вывода, и в текущей реализации разрабатываемой пользователем инструмента. При таком подходе класс решаемых инструментом задач неявно определяется содержимым базы правил элаборации и не имеет простой строгой формулировки, однако на практике достаточно большие и практически значимые фрагменты кода программ могут покрываться относительно небольшим набором правил элаборации (сотни простых правил и десятки более сложных). При этом все выполняемые процедурой элаборации преобразования являются полностью формальными и сертифицируются логическим ядром Pure системы формального доказательства Isabelle/HOL. Система Isabelle хорошо подходит для реализации процедуры элаборации, потому что как решатель для предусловий правил, используемый процедурой элаборации, так и логическое ядро Isabelle/Pure основаны на методе резолюции (и процедуре унификации термов) правил (формул Хэрропа, обобщающих Хорновские дизъюнкты) в логике высшего порядка.

Текущее основное направление работы ─ разработка библиотеки правил элаборации (в виде набора теорий Isabelle/HOL) для верификации библиотечных функций работы с одной из базовых структур данных, таких как связные списки из ядра ОС Linux.

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

Приведем другие актуальные темы исследования, связанные с развитием инструмента верификации PLRDF:

Модель неограниченных указателей и блочно-байтовая модель памяти с переинтерпретацией

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

Моделирование функциональных указателей с помощью теории доменов

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

Реализация автоматического построения моделей кода функций из промежуточного представления Frama-C

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

Формализация семантики функций выделения памяти

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

Разработка специфического алгоритма сопоставления с образцом для правил элаборации в логике высшего порядка

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

Автоматический вывод триггеров, упорядочение и группировка лемм для их предварительного конечного инстанцирования

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

Генерация операций и соответствующих семантических правил для выделения и освобождения локальных регионов памяти

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

Генерация семантических правил для интерпретации областей памяти как объектов разных типов

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

Генерация семантических правил и правил элаборации для инициализаторов объектов композитных типов

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