Верификация С-программ с помощью смешанной аксиоматической семантики

В диссертации представлены формальные семантики языков C-light и C-kernel, ориентированные на верификацию методом Хоара. Доказана теорема о корректности аксиоматической семантики языка C-kernel, исследован вопрос перехода инвариантов циклов при трансляции программ из языка С-light в язык C-kernel, приведены примеры, иллюстрирующие применение предложенных семантик.

Актуальность темы

.

Формальная верификация программ — актуальное направление современного программирования. Особый интерес представляет верификация программ, написанных на распространённых языках системного программирования таких, как С. Область применения этого языка огромна: от программного обеспечения для бытовой техники до операционных систем и авионики.

Обозримая формальная семантика является необходимой предпосылкой того, что язык удобен для верификации. Однако формальной детерминированной семантики для полного языка С, соответствующего стандарту ISO [62], не существует. Во-первых, сказывается заложенная в С возможность работать на низком уровне — обращение к памяти на уровне отдельных байтов и даже битов. Во-вторых, стандартизация С произошла намного позже его широкого распространения, поэтому многие аспекты поведения С-программ в стандарте ISO просто не специфицированы. В-третьих, сам стандарт написан большей частью на обычном английском языке, что влечёт за собой двусмысленности и неясности, характерные для любого человеческого языка.

В проекте Шармы, Дходапкара, Рамеша и др. (Bhabba Atomic Research Centre, Indian Institute of Technology) представлен метод [66] дедуктивного поиска ошибок в программах на языке MISRA С, который является индустриальным стандартом для написания безопасных программ, ориентированным в основном на встраиваемые системы. Входная С-программа моделируется в виде типизированной системы переходов в языке спецификаций автоматического доказателя теорем PVS. По спецификации автоматически генерируются леммы, направленные на поиск таких ошибок, как выход за границы массива, деление на ноль, арифметические переполнения и др. Проводилась верификация функций из библиотеки, используемой при написании программного обеспечения для атомных реакторов. Вместе с тем отметим, несмотря на то, что язык MISRA С является крайне ограниченным (например, запрещены объединения, арифметика указателей, динамическая память и рекурсия), для него отсутствует формальное синтаксическое определение. Поэтому для программ необходимо дополнительно осуществлять проверку на соответствие этому стандарту. Также метод не является дедуктивной верификацией в классическом понимании этого термина и предназначен лишь для поиска некоторых классов (см. выше) ошибок периода исполнения.

Система проверки моделей для языка ANSI-C [34] описана Кларком, Кронингом и др. (Carnegie Mellon University). Заявлена поддержка большинства особенностей языка С и высокий уровень автоматизации. Для борьбы с взрывом числа состояний используется предикатная абстракция программ и парадигма CEGAR (CounterExample Guided Abstraction Refinement). Этой же группой исследователей развивается подход к использованию языка С в качестве языка спецификаций для верификации аппаратного обеспечения, описываемого на языке Verilog [35]. Дополнительный интерес представляет набор эквивалентных трансляций в языке ANSI-C, позволяющих свести задачу проверки моделей к уравнению с битовыми векторами (SAT-решатели). Кларк также участвует в разработке аналогичного проекта MAGIC (Modular Analysis of proGrams In C) [33], в котором также строится конечная модель С программ. Отметим, что верификация в данном случае имеет характер аппроксимации, поскольку циклы и рекурсия разворачиваются в некоторых границах, к тому же пользователь должен явно сформулировать эти границы.

Система С Wolf [37] (SUNY at Stone Brook, North Carolina State University) используется для извлечения конечной размеченной системы переходов из С программы. Эта модель подается на вход системе проверки моделей NCSU Concurrency Workbench. С Wolf использовался для анализа таких приложений, как GNU i-protocol и BSD ftp daemon. Отметим ряд ограничений на низкоуровневые возможности языка С, а также то, что пользователь вынужден сам моделировать механизм параллельного взаимодействия в Concurrency Workbench.

Другая система, для извлечения моделей из С программ, названная АХ (Automation extractor) и работающая в комбинации с системой проверки моделей SPIN, представлена Хольцманом (Bell Laboratories, Lucent Technologies) [45]. Предназначена система для верификации таких приложений как обеспечение телефонных АТС, распределённые операционные системы, протоколы и приложений архитектуры «клиент-сервер». Отмечалась поддержка полного языка С, но также указывалось на невозможность во многих случаях формально доказать непротиворечивость порождаемых абстракций.

Примером узкоспециализированного проекта по верификации является проект VERISOFT (University of Saarlandes, German Research Center for Artificial Intelligence) [28], ориентированного в основном на встраиваемые системы. Одна из целей проекта — верификация ядра операционной системы для простого, но верифицированного процессора. Используется очень простое подмножество языка С — язык СО, семантика которого моделируется в системе доказательства теорем Isabelle/HOL. В силу ограниченности СО в программах приходится использовать язык ассемблера, что усложняет верификацию. Вместе с тем, на языке СО были написаны верифицированные библиотеки обработки строк и списков.

Перспективный подход к верификации С программ предложен в рамках проекта Why (Франция, INRIA) [38]. Отметим, что Why — это платформа, пригодная для верификации многих императивных языков. В ней определён одноимённый промежуточный язык, в который можно транслировать входные программы. Цель трансляции — генерация условий корректности в виде, не зависящем от системы доказательства теорем. На основе Why построен инструментарий Frama-C, предлагающий статический анализ для полного языка С и дедуктивную верификацию для ограниченного подмножества. Из ограничений отметим запреты на goto «назад» и внутрь блока, указатели на функции, приведения типов между числами и указателями, объединения, функции с переменными списками параметров, вещественные вычисления. Также с помощью языка спецификаций ACSL было аннотировано подмножество стандартной библиотеки, включающее важные функции работы с памятью и файлами. Список верифицированных программ включает довольно простые программ поиска и сортировки.

Наконец, рассмотрим проект разработки компилятора CompCert (Франция, INRI А) для языка Clight, предложенного Jlepya [32]. Этот язык представляет собой довольно большое подмножество языка С, поддерживает работу с динамической памятью (в том числе указатели на функции), объединения. Однако в выражениях Clight запрещены побочные эффекты (в частности, в выражениях запрещены операции инкремента, декремента и составного присваивания), type-декларации и оператор goto не поддерживаются. Переменные могут объявляться либо на уровне всей программы, либо в начале тела функции, т. е. это означает запрет на использование блоков. Программа на языке Clight транслируется в язык Cminor, являющийся внутренним для всей системы CompCert: в нём уменьшено число операторов и наложены дополнительные ограничения на выражения. Доказательство корректности перевода из Clight в Cminor было проведено в системе доказательства Coq и заняло 6000 строк. На выходе система генерирует ассемблерный код для процессоров PowerPC, ARM и х86, сохраняющий семантику исходного Clight кода. В сентябре 2010 года вышла версия 1.8 компилятора CompCert, которая, как заявлено на веб-сайте проекта, поддерживает оператор goto и побочные эффекты в выражениях. Однако ссылки на печатные работы отсутствуют.

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

В лаборатории теоретического программирования ИСИ СО РАН был разработан язык С-Н^, являющийся представительным подмножеством языка С.

Формально этот язык был определён с помощью структурной операционной семантики в стиле Плоткина [59]. Хотя операционная семантика удобна для формального определения языка, для верификации она имеет слишком низкий уровень, что приводит к громоздким доказательствам условий корректности. Поэтому обычно используют аксиоматическую семантику, базирующуюся на логике Хоара [41], которая определяется как система вывода утверждений о свойствах программ. Однако аксиоматическая семантика для языка С-^М также была бы громоздкой. В связи с этим был применён двухуровневый подход: в языке С-И^ выделяется ядро — язык С-кегпе1, для которого разработана аксиоматическая семантика, и в этот язык транслируются исходные программы на языке С-Н§ М. По сравнению с языком С-Н^ в языке С-кеше1 более простые выражения и более ограниченный набор операторов, что упростило аксиоматическую семантику. Стоит отметить, что использование промежуточного этапа трансляции входных программ характерно для некоторых из перечисленных выше проектов. Но трансляция осуществляется в языки, отличные от С, что ставит под вопрос её корректность. В [22] была доказана важная теорема о непротиворечивости аксиоматической семантики языка С-кегпе1 относительно операционной, а также были описаны формальные правила перевода из языка С-Н^ в язык С-кегпе1 и дано доказательство их корректности. При верификации реальных программ (особенно среднего и большого объёма) ручной генерации условий корректности очень трудоёмкий, поэтому его целесообразно автоматизировать. Предложенная в [22] аксиоматическая семантика языка С-кегпе1 удобна для теоретических исследований, но не ориентирована на автоматическую генерацию условий корректности. Цель и задачи диссертации.

Целью диссертационной работы является разработка формальной семантики языка С-Б^^, позволяющей автоматически получать условия корректности и упрощать их. Для достижения цели были поставлены и решены следующие задачи:

1. Разработана новая версия операционной семантики языка С-И^.

2. Разработана смешанная аксиоматическая семантика языка С-кегпе1, позволяющая автоматически получать условия корректности и упрощать их.

3. Описан и обоснован алгоритм перевода инвариантов циклов при трансляции программ из в С-кегпе1.

4. Сформулирована и доказана теорема о корректности смешанной аксиоматической семантики языка С-кегпе1.

5. Разработан набор примеров с целью использования предложенной смешанной аксиоматической семантики С-кегпе1 для упрощения верификации.

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

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

Научная и практическая ценность.

Полученные результаты являются теоретической основной для разработки генератора условий корректности C-light программ, являющегося составной частью системы верификации СПЕКТР-2, разрабатываемой в настоящее время в лаборатории теоретического программирования ИСИ СО РАН.

Доклады и печатные работы.

Основные результаты работы были представлены на конференции-конкурсе «Технологии Microsoft в теории и практике программирования» (Новосибирск, 2007 г.), VIII Всероссийской конференции молодых учёных по математическому моделированию и информационным технологиям (Новосибирск, 2007 г.), на международном семинаре «Program Understanding» (Алтай, 2009 г.), проводившемся в рамках международной конференции «Perspectives of System Informatics», международном семинаре «Program Semantics, Specif!-cation and Verification: Theory and Applications» в рамках «5 International Computer Science Symposium in Russia» (докладчик А. В. Промский), прошедшем в 2010 г. в Казани и международной Ершовской конференции по информатике PSI’l 1 (стендовый доклад, Новосибирск, 2011 г.).

Полученные результаты обсуждались на семинаре «Теоретическое и экспериментальное программирование» ИСИ СО РАН.

По материалам диссертации опубликовано 11 работ [1, 6, 7, 8, 10, 11, 15,24,29,46,47].

Структура и объём диссертации.

Диссертация состоит из введения, пяти глав и заключения. Объём работы (за исключением библиографии) составляет 110 страниц в формате машинописного текста.

Список литературы

содержит 66 наименований. Краткое содержание работы.

Заключение

.

В рамках диссертации были получены следующие результаты:

1. Разработана новая версия операционной семантики языка.

2. Разработана смешанная аксиоматическая семантика языка С-кегпе1, позволяющая автоматически получать условия корректности и упрощать их.

3. Описан и обоснован алгоритм перевода инвариантов циклов при трансляции программ из С-^Ыв С-кегпе1.

4. Сформулирована и доказана теорема о непротиворечивости смешанной аксиоматической семантики языка С-кегпе1.

5. Разработан набор примеров с целью использования предложенной смешанной аксиоматической семантики С-кегпе1 для упрощения верификации.

В настоящее время в лаборатории теоретического программирования ведётся разработка мультиязыковой автоматизированной системы верификации СПЕКТР-2 [15, 24], которая поддерживает и язык С-%111 Предложенная в настоящей работе смешанная аксиоматическая семантика языка С-кегпе1 является основной автоматического генератора условий корректности, являющегося одним из модулей системы СПЕКТР-2.

Первые эксперименты по верификации в данной системе подтвердили полученные теоретические результаты.