автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Верификация С-программ с помощью смешанной аксиоматической семантики

На правах рукописи

005018979

МАРЬЯСОВ Илья Владимирович

ВЕРИФИКАЦИЯ С-ПРОГРАММ С ПОМОЩЬЮ СМЕШАННОЙ АКСИОМАТИЧЕСКОЙ СЕМАНТИКИ

Специальность 05.13.11 —Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

3 МАЙ 2012

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата физико-математических наук

Новосибирск — 2012

005018979

Работа выполнена в Институте систем информатики им. А. П. Ершова Сибирского отделения Российской академии наук

Научный руководитель: Непомнящий Валерий Александрович,

кандидат физико-математических наук

Официальные оппоненты: Сафонов Владимир Олегович,

доктор физико-математических наук, профессор

Защита состоится 14 мая 2012 г. в 16 ч 00 мин. на заседании диссертационного совета ДМ003.032.01 в Институте систем информатики им. А. П. Ершова Сибирского отделения РАН по адресу:

630090, г. Новосибирск, пр. ак. Лаврентьева, 6.

С диссертацией можно ознакомиться в читальном зале ИСИ СО РАН (пр. ак. Лаврентьева, 6).

Автореферат разослан 12 апреля 2012 г.

Учёный секретарь диссертационного совета

Скопин Игорь Николаевич, кандидат физико-математических наук

Ведущая организация:

Ярославский государственный университет имени П. Г. Демидова

к. ф.-м. н.

Мурзин Ф. А.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

Обозримая формальная семантика является необходимой предпосылкой того, что язык удобен для верификации. Значительный вклад в эту область внесли работы Д. Гриса, Э. Дейкстры, Р. Флойда, Ч. Э. Р. Хоара, Г. Плоткина. Среди отечественных авторов можно отметить А. П. Ершова, А. В. Замулина, С. С. Лаврова, А. А. Летичевского, В. А. Серебрякова и др. Из языков, для которых известны успешные результаты по формализации семантики, можно назвать языки Pascal, SML, Euclid, Eiffel. Однако формальной детерминированной семантики для языка С, полностью соответствующего стандарту ISO, не существует. Во-первых, сказывается заложенная в С возможность работать на низком уровне — обращение к памяти на уровне отдельных байтов и даже битов. Во-вторых, стандартизация С произошла намного позже его широкого распространения, поэтому многие аспекты поведения С-программ в стандарте ISO не специфицированы. В-третьих, сам стандарт написан на естественном языке, что влечёт за собой двусмысленности и неясности.

Актуальность формальной верификации подтверждается и современными работами зарубежных специалистов по верификации С программ, таких как Шармы, Дходапкара, Рамеша, Кларка, Кронинга, Хольцмана, Ле-руа. При общем сравнении известных проектов их можно разделить на два класса. К первой группе относятся проекты, ориентированные на максимальный охват языка С, но пригодные для поиска лишь некоторых классов ошибок, либо использующие трудно формализуемые методы, что усложняет доказательство их корректности. Во второй группе находятся проекты, использующие классические формальные подходы, но при этом исследователи вынуждены вводить ограничения на целевой язык.

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

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

используют аксиоматическую семантику, базирующуюся на логике Хоара, которая определяется как система вывода утверждений о свойствах программ. Однако аксиоматическая семантика для языка С-1щЫ: была бы очень громоздкой.

В связи с этим был применён двухуровневый подход: в языке С-Н{*Ы: выделяется подмножество — язык С-кегпе1, для которого разработана аксиоматическая семантика, и в этот язык транслируются исходные программы на языке С-Н{*1И. По сравнению с языком С-Н^ в языке С-кегпе1 более простые выражения с минимальным числом побочных эффектов и ограниченный набор операторов. Это позволило упростить аксиоматическую семантику для языка С-кегпе1. При разработке метода верификации С-^^ программ была доказана теорема о непротиворечивости аксиоматической семантики языка С-кегпе1 относительно операционной, а также описаны формальные правила перевода из языка С-^Ы в язык С-кегпе1 с обоснованием их корректности. Стоит отметить, что использование промежуточного этапа трансляции входных программ характерно для некоторых проектов указанных выше авторов. Но трансляция осуществляется в языки, отличные от С, что ставит под вопрос её корректность.

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

Цель и задачи диссертации. Целью диссертационной работы является разработка непротиворечивой формальной аксиоматической семантики языка позволяющей существенно упрощать как сами условия кор-

ректности, так и процесс их генерации. Для достижения цели были поставлены и решены следующие задачи:

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

2. Разработана соответствующая смешанная операционная семантика языка С-И^.

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

4. Доказана непротиворечивость смешанной аксиоматической семантики языка С-кегпе1 относительно операционной семантики языка С-НцЬЬ

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

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

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

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

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

По материалам диссертации опубликовано 11 работ, включая 2 работы в журнале из списка ВАК.

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

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

В главе 1 даются предварительные понятия, используемые в работе.

В разд. 1.1 дано определение языка C-light. Подробно рассматриваются допустимые типы, декларации, выражения, операторы, а так же накладываемые на них ограничения по сравнению со стандартом ISO С99.

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

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

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

Составные литералы в C-light разрешены только в качестве инициализаторов в декларациях. Операция приведения типа для составного инициализатора запрещена.

Приведения типов указателей ограничены случаем приведения от типа void к произвольному х.

На операторы накладывается два ограничения: все case-метки и метка default в операторе switch должны находиться на одном уровне вложенности; запрещён переход по оператору goto внутрь блока.

Исходный текст программы есть последовательность внешних деклараций. На внешнем уровне можно объявить тип (typedef-декларации), функцию (прототип или определение), структуру и данные.

В языке C-light препроцессор отсутствует, поскольку исходная программа препроцессируется до начала её верификации. Модульность не поддерживается, поэтому с точки зрения семантики любая исходная программа состоит из одного файла.

Язык C-kernel рассмотрен в разд. 1.2: описываются различия по сравнению с языком C-light.

Язык C-kernel — это промежуточный язык двухуровневой схемы верификации программ, в который транслируются программы на языке C-light.

Число побочных эффектов в выражениях языка C-kernel сведено до минимума, а операции, содержащие контрольные точки (например, логические && и 11), отсутствуют.

Нормализованным выражением называется выражение, не содержащее условных операций, операций последовательного вычисления, логических операций && и 11, простых и составных присваиваний, операций инкремента и декремента.

Пусть е (возможно с индексами) обозначает нормализованное выражение, т — его тип. Оператор-выражение языка C-kernel имеет вид:

• е = е';

• e'(ei,..., еп);

• е = e'(ei,..., еп).

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

В языке C-kernel допустимыми являются следующие операторы:

1. Оператор вычисления выражения (возможно, пустой).

2. Условный оператор if с обязательной ветвью else (возможно, пустой) и нормализованным условием.

3. Оператор цикла while с нормализованным условием.

4. Оператор передачи управления goto с теми же ограничениями, что и в C-light.

5. Оператор возврата значения return, причём возвращаемым выражением может быть только нормализованное выражение.

6. Составной оператор (блок).

Разд. 1.3 подробно описывает язык утверждений, используемый для спецификации программ, его типы и алфавит (п. 1.3.1), выражения (п. 1.3.2), в п. 1.3.3 вводится понятие подстановки и формулируется лемма о подстановке. П. 1.3.4 даёт определение интерпретации выражений, необходимое для формального определения операционной семантики языка C-light. В п. 1.3.5 вводится понятие истинности логического утверждения, формулируется лемма о свойствах стандартных булевских операций и лемма о свойствах подстановки.

Глава 2 представляет разработанную операционную семантику языка C-light. Данная семантика рассматривает процесс выполнения программы в терминах изменения состояний абстрактной машины. Её определение вводится в разд. 2.1. Прежде всего даётся определение состояния:

Состояние абстрактной машины языка C-light — это отображение, означивающее следующие переменные:

1. MD — переменная типа Locations —* CTypes (где Locdtions — множество адресов, CTypes — объединение всех допустимых типов языка C-light) определяет значения, хранимые в памяти.

2. Val — переменная типа CTypes х LogTypeSpecs, где LogTypeSpecs — множество логических имён типов данных языка C-light. В этой переменной хранится значение вычисленного выражения и его тип.

3. Переменные типа Names, к значениям которых нет доступа через указатели (далее такие переменные называем неразделяемыми, остальные переменные — разделяемыми).

Для описания работы абстрактной машины языка C-light требуются специальные функции, называемые абстрактными. Их определение даётся в разд. 2.2, перечислим основные:

1. UnOpSem(«, V, т) — функция, которая возвращает результат применения унарной операции • к значению V типа т.

2. BinOpSem(*, Vi, ti, V2, Т2) — функция, которая возвращает результат применения бинарной операции • к значениям Vi и V2 типов Ti и tj соответственно.

3. mb(e, id) — функция, вычисляющая адрес элемента массива e[id] или поля структуры е.id.

4. Функция upd(A, е, с) осуществляет обновление отображения А в точке е на значение С и определяется стандартным образом.

5. Функция retype(t) получает в качестве аргумента логический тип т и возвращает тип То, если т имеет вид Ti х ... х тп —> То и т в противном случае.

6. Семейство функций type(n) возвращает тип конструкции П (константы, переменной, выражения) языка C-light.

7. Функция addr(e, MD) вычисляет адрес выражения е в соответствии со значением MD.

8. Функция \/а1(е, МО) возвращает значение выражения е в соответствии со значением МО.

9. Функция саэ^е, т, т') преобразует значение е типа т к значению типа т'.

Разд. 2.3 посвящен аксиомам и правила вывода операционной семантики Вначале даётся определение конфигурации абстрактной машины — это пара (Р, о): программа Р и состояние СТ.

Произвольная аксиома операционной семантики имеет вид

(А, а) -> (В, а1).

Эта запись означает, что один шаг исполнения программного фрагмента А, начинающийся в состоянии СТ, приводит в состояние СТ1 и В — тот фрагмент исходной программы, который остаётся для исполнения. Произвольное правило семантики имеет вид

Рь • ■■, Рп

(А, ст> - <В, а')

Это означает, что при выполнении условий Р1, ..., Р„ можно перейти от первой конфигурации ко второй.

Таким образом, исполнение программ в операционной семантике приводит к цепочками конфигураций, которые в общем случае могут быть и бесконечными:

<51, аО -» <Б2, а2) -» ... -» ф, Ст|> -» ...

Конфигурация (Б!, СТ1) называется начальной. Если же цепочка конечна и (Бп, СТП) — последняя конфигурация в этой цепочке, то говорим, что исполнение фрагмента Бь начинающееся в состоянии СТ1 приводит в заключительную конфигурацию (Бп, СТП). Если обозначить транзитивное рефлексивное замыкание отношения -> как -> , то в общем случае такое исполнение можно обозначить как

<Б1, СТ1) <БП, стп).

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

В качестве примера типичного правила вывода модифицированной операционной семантики языка C-light приведём правило вывода для операции присваивания. Пусть т" — тип, отличный от массива, а е — разделяемая переменная. Правило для простого присваивания имеет вид

<е0, ст> <Val(v', -г1), а1), <е, а1) <Val(v", -с"), а">,

_у = castCv', т', т"), с - addrCv")_

<е = е0, а> -»<Val(v, т"), a"(MD <- upd(MD, с, v))>

В случае, когда е — неразделяемая переменная, правило имеет вид

<е0, а) V <yal(v', т'), а'), <е, а1) -»' <Val(e, т"), а"), v = cast(v', т', т") <е = е0, а> - <Val(v, т"), ст"(е - v)>

Вычисление присваивания состоит из следующих этапов: вычисление правой части во и сохранение результата (значения и его типа) в метапере-менной Val; вычисление левой части е; вычисление адреса выражения левой части присваивания С; приведение типа значения правой части т' присваивания к типу значения левой части т". Полученное значение объявляется результатом операции присваивания, при этом состоянием абстрактной машины объявляется состояние о", в которое перешла машина после вычисления левой части, модифицированное в точке MD(c).

Случай неразделяемой переменной, находящейся в левой части присваивания, отличается тем, что нет необходимости вычислять её адрес.

На основе введённых в предыдущих разделах понятий в разд. 2.4 даётся определение семантики частичной корректности. Семантика программы S есть отображение из множества состояний абстрактной машины в множество подмножеств этих состояний, т. е. семантика рассматривает все возможные исполнения программы S, начинающиеся в состоянии СТ, при которых программа завершается нормальным образом:

М[[S]](o) = {СТ1 I (S, СТ> -V <£, СТ1)} и {a'(Val <- (v, т)) | <S, ст> ->* <Val(v, т), а1».

Отображение JVf называется семантикой частичной корректности для языка C-light.

Разд. 2.5 посвящен трансляции программ из C-light в C-kernel. В п. 2.5.1 рассмотрены правила для операторов и деклараций, п. 2.5.2 даёт правила для выражений. В заключение раздела приводится теорема о корректности и завершимости процесса перевода.

В главе 3 описана смешанная аксиоматическая семантика языка С-kemel. В разд. 3.1 вводятся необходимые понятия. Для формализации операторов перехода и функций вводится понятие окружения — это пятёрка (f, т, В, bid, lab), где f — имя текущей функции, т — тип значения, возвращаемого этой функцией, В — её тело, bid — уникальный идентификатор текущего обрабатываемого блока, lab — метка, на которую осуществляется переход по встреченному в процессе вывода оператору goto, либо идентификатор блока тела функции, иначе lab = (ú. Функция main является текущей функцией не только для программных конструкций, входящих в её тело, но и для всей программы, поскольку в силу специфики этой функции выполнение программы начинается с её вызова.

Информация о пред- и постусловиях функции и об инвариантах помеченных операторов задаётся спецификацией SP = (SPfun/ SP|ab), включающей спецификацию функций SPfun и спецификацию меток SP|at,.

Спецификация функций SPfu„ — это пара (SPpre, SPpost) отображений SPpre и SPp0St, называемых спецификациями пред- и постусловий функций соответственно.

Спецификация предусловий функции SPpre — это отображение из имён функций f в функции Pf от метапеременных. Утверждение Pf(MD) называется предусловием функции f.

Спецификация постусловий функции SPpost — это отображение из имён функций f в функции Qf от метапеременных. Утверждение Qf(MD) называется постусловием функции f.

Спецификация меток 5Р|аь — это отображение из меток в утверждения. Утверждение SP|ab(L) называется инвариантом метки L.

Пусть символы Р, Q обозначают аннотации, S — последовательность операторов, окружение Е имеет вид (f, т, В, сиг, ш).

Теперь мы можем определить смешанную аксиоматическую семантику MHSC языка С-kemel как исчисление троек Хоара с окружениями. Выводимость тройки {Р} S {Q} в системе MHSC в окружении Е относительно

спецификации SP обозначим как Е, SP I-mhsc {Р} S {Q}. Термин «смешанная» означает то, что правила вывода с участием неразделяемых переменных могут иметь специальный (более простой) вид.

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

Символы ' и " стоящие рядом с именем переменной означают введение новой переменной (т. е. не встречавшейся в аннотациях до применения правила, в котором она вводится).

Далее подробно рассмотрены правила вывода для выражений (разд. 3.2), деклараций (разд. 3.3), операторов (разд. 3.4) и другие (разд. 3.5). В качестве примера рассмотрим правило вывода для операции присваивания. Пусть выражение Бо не содержит вызовов функций и операторов приведения.

Е, SP h {3MD1 P(MD MD') л MD = upd(MD', addr(val(e, MD'), MD'), __cast(val(e0, MP'), type(en). type(e)))} A; {Q>_

E, SP h {P> e = e0; A; {Q}

где e является разделяемой переменной.

Правило представляет собой модификацию правила классической системы Хоара: подстановка осуществляется на метапеременной MD, и происходит приведение типа выражения во к типу е.

В случае, когда е — простая неразделяемая переменная, правило имеет

вид:

Е, SP I- {Зе' Р(е <- е') л е - cast(val(e0(e <- е')), type(e0), type(e))} A; {Q>

Е, SP h {Р} е = е0; A; {Q>

При переводе программы на языке C-light в программу на языке C-kernel возникает проблема вычисления инвариантов циклов и меток полученной программы: при элиминации операторов break и Continue внутри циклов и оператора switch, а также самого оператора switch возникают новые метки, каждой из которых в соответствии с правилами смешанной аксиоматической семантики языка C-kernel для помеченного оператора должен быть сопоставлен некоторый инвариант, который отсутствует в исходной программе. Решение данной проблемы рассмотрено в разд. 3.6. Если

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

Применение данного подхода проиллюстрировано примером.

Глава 4 посвящена обоснованию корректности смешанной аксиоматической семантики относительно операционной: сформулирована и доказана теорема о непротиворечивости.

В разд. 4.1 вводятся необходимые дополнительные понятия. Для программы prg истинность тройки Хоара {Р} prg {Q} определяется следующим образом: тройка Хоара {Р} prg {Q} истинна в смысле частичной корректности (обозначение 1= {Р} prg {Q}), если Ж[[prg]](| |Р| |) с ||Q|| (то есть если утверждение Q истинно во всех заключительных состояниях всех возможных исполнений программы prg, начавшихся в тех состояниях, в которых истинно Р).

Семантика частичной корректности относительно спецификации SP определяется для произвольной конструкции S языка C-light как отображение ЖSP[[S]] из States в 2statES:

•M"sp[[S]](ct) = {ст' | <S gotoStop(S), а) V <е, а'» и {o'(Val «- (v, т)) | <S gotoStop(S), а> <Val(v, х), ст')} и {а' | (gotoStart(L) S gotoStop(S), о") -»* <е, а') для некоторой метки L,

входящей в S, и состояния СТ", такого что СТ" \= SP|ab}

То есть семантика рассматривает все возможные исполнения программной конструкции S, при которых эта конструкция завершается нормальным образом, при условии, что выполнение конструкции начинается либо в состоянии а, либо в состоянии, в котором происходит переход на эту конструкцию по оператору goto L. В последнем случае состояние должно удовлетворять инварианту SP|ab(L) метки L. Добавление конструкции

gotoStop(S), использующейся в операционной семантике для обработки оператора goto позволяет учесть циклы, образованные с его помощью.

Для доказательства, что спецификации SP|3b(L) действительно является инвариантами меток, нам потребуется ещё один вид семантики. Семантика выхода по метке L относительно спецификации SP определяется для произвольной конструкции S языка C-light как отображение -M"¿> [[S]] из States в 2states:

•MspUS]](o) = {о' I <S gotoStop(S), a) <gotoStart(L), a') для некоторой метки L} U {a' I <gotoStart(L') S gotoStop(S), a") -»* (gotoStart(L), о') для некоторых

меток L' и состояния СТ", таких что L' входит в S и a" 1= SP|ab}

То есть семантика рассматривает все возможные исполнения программной конструкции S, при которых эта конструкция завершается переходом на метку L при условии, что выполнение конструкции начинается либо в состоянии СТ, либо в состоянии, в котором происходит переход на эту конструкцию по оператору goto L. В последнем случае состояние должно удовлетворять инварианту SP|ab(L) метки L. Добавление конструкции gotoStop(S) позволяет участь циклы, образованные с помощью оператора goto.

Пусть окружение Е имеет вид (f, tf, {S}, bid, lab). Пусть Dom(E) обозначает формулу

{retType(type(&f)) = xf л snd(MD(&f)) = S, если f Ф main, true, в противном случае.

Тройка Хоара {Р} S {Q} истинна в смысле частичной корректности в окружении Е относительно спецификации SP (обозначим этот факт Е, SP t= {Р> S {Q}), если

• Р => Dom(E);

• *f[[S]](||P||)E||Q||.

Разд. 4.2 посвящён доказательству теоремы о непротиворечивости смешанной аксиоматической семантики.

Теорема 1. Система вывода MHSC непротиворечива для свойства частичной корректности, т. е. Е hMHsc {Р} prg {Q} влечёт Е t= {Р} prg {Q}.

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

Заключительная глава 5 иллюстрирует применение смешанной операционной семантики. Рассмотрена верификация программ вычисления факториала (разд. 5.1), поиска в линейном односвязном списке (разд. 5.2) и топологической сортировки (разд. 5.3).

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

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

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

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

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

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

В настоящее время в лаборатории теоретического программирования ведётся разработка мультиязыковой автоматизированной системы верификации СПЕКТР-2 [7], которая поддерживает и язык C-light. Предложенная в настоящей работе смешанная аксиоматическая семантика языка C-kernel является основой автоматического генератора условий корректности — одного из модулей системы СПЕКТР-2.

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Ануреев И. С., Марьясов И. В., Непомнящий В. А. Верификация С-программ на основе смешанной аксиоматической семантики. // Моделирование и анализ информационных систем. — 2010. — Т. 17. — № 3. — С. 5 — 28. — URL: http://mais.uniyar.ac.ru/sites/default/files/journal/private/ 173_5-28.pdf.

2. Марьясов И. В. Автоматическая верификация программ на языке С-light. // Тезисы докладов VIII Всероссийской конференции молодых учёных по математическому моделированию и информационным технологиям. — Новосибирск, 2007. — С. 103.

3. Марьясов И. В. Автоматическая верификация программ на языке С-light. // Тезисы докладов конференции-конкурса «Технологии Microsoft в теории и практике программирования». — Новосибирск, 2007. — С. 25 —• 27.

4. Марьясов И. В. Автоматическая генерация условий корректности в системе верификации C-light программ. // Материалы XLIV Международной научной студенческой конференции «Студент и научно-технический прогресс». — Новосибирск, 2006. — С. 253 — 254.

5. Марьясов И. В. На пути к автоматической верификации C-light программ. Смешанная аксиоматическая семантика языка C-kernel. — Новосибирск, 2008. — 32 с. — (Препринт / РАН Сибирское отделение. ИСИ; № 150). —URL: http://www.iis.nsk.su/files/preprints/150.pdf.

6. Марьясов И. В. Применение смешанной аксиоматической семантики языка C-kernel к верификации программы топологической сортировки.

— Новосибирск, 2010. — 36 с. — (Препринт / РАН Сибирское отделение. ИСИ; № 155). —URL: http://www.iis.nsk.su/files/preprints/155.pdf.

7. Непомнящий В. А., Ануреев И. С., Атучин М. М., Марьясов И. В., Петров А. А., Промскнй А. В. Верификация С-программ в мультиязыко-вой системе СПЕКТР. // Моделирование и анализ информационных систем.

— 2010. — Т. 17. — № 4. — С. 88 — 100. — URL: http://mais.uniyar.ac.ru/sites/default/files/journal/private/17_4_88-100.pdf.

8. Непомнящий В. А., Атучин М. М., Марьясов И. В., Петров А. А., Промский А. В. Система анализа и верификации С-программ СПЕКТР-2. // Труды семинара «Program Semantics, Specification and Verification». — 5th International Computer Science Symposium in Russia. — Казань, 2010. — С. 76 — 81.

9. Anureev I., Maryasov I., Nepomniaschy V. The Mixed Axiomatic Semantics Method for C-program Verification. // Ershov Informatics Conference: PSI Series, 8th Edition (Preliminary Proceedings). — Novosibirsk: A. P. Ershov Institute of Informatics Systems, 2011. — P. 261 — 266.

10.Maryasov I. V. The mixed axiomatic semantics method. —Novosibirsk, 2011. — 43 p. — (Preprint / Siberian Division of RAS. IIS; # 160). — URL: http://www.iis.nsk.su/files/preprints/160.pdf.

11.Maryasov I. V. Towards automatic verification of C-light programs. Mixed axiomatic semantics of C-kernel language. // Perspectives of Systems In-

fonnatics (PSI): A. Ershov 7th Int. Conf.: Int. workshop on Program Understanding. — Novosibirsk, 2009. — P. 44 — 52.

Личный вклад автора. Описанные в диссертации модифицированная операционная семантика языка C-light и смешанная аксиоматическая семантика языка C-kemel разработаны автором самостоятельно на основе работ В. А. Непомнящего, И. С. Ануреева и А. В. Промского по языкам C-light и C-kernel. Доказательство теоремы о непротиворечивости и верификация приведённых в работе примеров проведены автором самостоятельно.

Марьясов И. В.

ВЕРИФИКАЦИЯ С-ПРОГРАММ С ПОМОЩЬЮ СМЕШАННОЙ АКСИОМАТИЧЕСКОЙ СЕМАНТИКИ

Автореферат

Подписано в печать 09.04.2012 Объём 1,13 уч.-изд. л.

Формат бумаги 60 х 90 1/16_Тираж 100 экз.

Отпечатано в ЗАО РИЦ «Прайс-курьер»

630128, г. Новосибирск, ул. Кутателадзе, 4г, 310 к., тел. (383) 330-72-02 Заказ №_167

61 12-1/879

РОССИЙСКАЯ АКАДЕМИЯ НАУК СИБИРСКОЕ ОТДЕЛЕНИЕ

ИНСТИТУТ СИСТЕМ ИНФОРМАТИКИ ИМ. А. П. ЕРШОВА

На правах рукописи

Марьясов Илья Владимирович

ВЕРИФИКАЦИЯ С-ПРОГРАММ С ПОМОЩЬЮ СМЕШАННОЙ АКСИОМАТИЧЕСКОЙ СЕМАНТИКИ

05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Диссертация на соискание учёной степени кандидата физико-математических наук

Научный руководитель к. ф.-м. н., с. н. с. Непомнящий В. А.

Новосибирск, 2012

Оглавление

Введение.......................................................................................................................4

Глава 1

Языки программ и спецификаций............................................................................12

1.1 Язык С-Н .......................................................................................................12

1.2 Язык С-кегпе1....................................................................................................15

1.3 Язык утверждений............................................................................................16

1.3.1 Типы и алфавит.....................................................................................17

1.3.2 Выражения............................................................................................17

1.3.3 Подстановка..........................................................................................18

1.3.4 Интерпретация выражений..................................................................19

1.3.5 Логические утверждения.....................................................................21

Глава 2

Модифицированная операционная семантика языка С-Н^................................23

2.1 Абстрактная машина языка С-Н^................................................................23

2.2 Параметры и абстрактные функции...............................................................24

2.3 Аксиомы и правила вывода.............................................................................31

2.4 Семантика частичной корректности..............................................................42

2.5 Трансляция языка в С-кегпе1...............................................................43

2.5.1 Перевод операторов и деклараций.....................................................43

2.5.2 Перевод выражений.............................................................................45

Глава 3

Смешанная аксиоматическая семантика языка С-кегпе1.......................................49

3.1 Предварительные понятия...............................................................................50

3.2 Выражения........................................................................................................52

3.3 Декларации........................................................................................................54

3.4 Операторы.........................................................................................................56

3.5 Другие правила.................................................................................................59

3.6 Перевод инвариантов из С-Н^ в С-кегпе1....................................................60

Глава 4

Непротиворечивость смешанной аксиоматической семантики...........................68

4.1 Предварительные понятия...............................................................................68

4.2 Теорема о непротиворечивости......................................................................70

Глава 5

Примеры применения смешанной аксиоматической семантики..........................78

5.1 Вычисление факториала..................................................................................78

5.2 Поиск в линейном односвязном списке.........................................................80

5.3 Топологическая сортировка............................................................................85

Заключение...............................................................................................................103

Литература................................................................................................................104

Введение

В диссертации представлены формальные семантики языков 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 даются предварительные понятия, используемые в работе. В разд. 1.1 дано определение языка C-light. Язык C-kernel рассмотрен в разд.

1.2. Разд. 1.3 подробно описывает язык утверждений, используемый для спецификации программ, его алфавит (п. 1.3.1), выражения (п. 1.3.2) и др.

Глава 2 представляет модифицированную операционную семантику языка С-П§М. В разд. 2.1 вводится понятие абстрактной машины языка С-разд. 2.2 посвящён параметрам абстрактной машины и абстрактным функциям. В разд. 2.3 даются аксиомы и правила вывода операционной семантики С-Н^. На основе введённых в предыдущих разделах понятий в разд. 2.4 даётся определение частичной корректности. Разд. 2.5 посвящён трансляции программ из С-П^Ы в С-кегпе1: отдельно рассмотрены правила для операторов и деклараций (п. 2.5.1) и для выражений (п. 2.5.2).

В главе 3 описана смешанная аксиоматическая семантика языка С-кегпе1. В разд. 3.1 вводятся необходимые понятия. Далее подробно рассмотрены правила вывода для выражений (разд. 3.2), деклараций (разд. 3.3), операторов (разд. 3.4) и другие (разд. 3.5). Проблема перехода инвариантов циклов из в С-кегпе1 исследована в разд. 3.6.

Глава 4 полностью посвящена обоснованию корректности смешанной аксиоматической семантики относительно операционной: сформулирована и доказана теорема о непротиворечивости.

Заключительная глава 5 иллюстрирует при�