ACSL cпецификации к библиотечным функциям ядра Linux
Проект по разработке спецификаций и формальному доказательству корректности библиотечных функций ядра Linux.
Актуальная информация по статусу доказательств отражена в основном README.md файле.
Спецификации разрабатываются на языке ACSL. В качестве инструментов формальной верификации используются Frama-C с плагином дедуктивной верификации AstraVer.
- Описание, как установить инструменты можно найти по ссылке. Инструменты работают на Linux, Windows, macOS.
- По ссылке можно загрузить образ виртуальной машины VirtualBox в формате ova с уже с предустановленными и настроенными инструментами. Размер образа ~3.6 гигабайт. Ос - Ubuntu. Логин - user. Пароль - 1. В директории workspace находятся два репозитория. Один соответствует данному, второй - acsl-proved (примеры с протоколами верикации).
$ frama-c -av <func>.c
$ frama-c -av check_bytes8.c
Or
$ make verify-<func>
$ make verify-check_bytes8
Каждая библиотечная функция ядра Linux располагается в отдельном *.c файле. В соответствующем *.h файле находятся объявления, типы, структуры, специфичные для данной функции.
- В kernel_definitons.h файле находятся общие для всех функции типы, макросы и прочие декларации.
- В ctype.h находятся сразу несколько функций, которые изначально в ядре были макросами. Для удобства формальной верификации данные макросы (islower,isupper,isdigit,...) были переписаны как inline функции.
В репозитории есть инструмент dismember. Он используется для того, чтобы "выцепить" код функции в отдельный файл. Пример (код для функции strim):
$ dismember -m ~/linux-stable/lib/string.c -k ~/linux-stable --double -f strim --output-dir .
Будет сформировано два файла: strim.c и strim.h
- Опция -m - путь к файлу с определением функции.
- Опция -k - путь к директории ядра.
- Опция --double - формировать два файла *.h и *.c
- Опция --f - имя функции
- Опция --output-dir - директория для вывода файлов
Контракт (предусловие и постусловие) находятся для каждой доказанной функции в соответствующем заголовочном файле (например, strlen.h). В нем же находятся леммы/аксиомы/логические функции, если они разработаны для соответствующей функции.
В *.c файле находится тело функции с инвариантами циклов, оценочными функциями и ассертами.
Для некоторых функций спецификации избыточны и фактически дважды по разному описывают то, как функций должна функционировать. Например, одна из таких функций - strlen. В её спецификации есть обычные функциональные требования и есть требование на соответствие возвращаемого результата вызову логической функции под тем же названием strlen. Чем мотивирована подобная "избыточность"? Логическую функцию strlen удобно использовать в спецификациях других функций, например, strcmp (а логическую функции, описывающую поведение функции strcmp при описании функциональных требований к strcpy). При этом все основные свойства логической функции выражаются через леммы (леммы на данном этапе не доказываются). Такие спецификации невозможно отобразить в проверки времени исполнения E-ACSL. Поэтому для тех функций, которым в спецификациях ставится в соответствие логическая функция, обязательно есть и "обычные" спецификации.
Как выбирается будет ли для функции разработана такая избыточная спецификация?
- Обычной функции можно сопоставить логическую функцию (один-в-один), только если функция на языке Си "чистая" (pure).
- Логическую функцию рационально писать в том случае, если они пригодится для разработки спецификаций в том числе и для других функций. Например, в функциональных требованиях к memcpy можно выразить "одинаковость" src и dest посредством вызова логической функции memcmp.
Протоколы доказательств (запусков солверов) на текущий момент в репозиторий не включены. Это будет сделано чуть позже, когда будет доказано большее количество функций. На текущий момент, когда спецификации ещё дорабатываются, это лишь "замусорит" репозиторий огромным количеством объемных файлов.
На данном этапе корректность лемм в спецификациях никак не доказывалась. Соответственно, в них могут быть ошибки. Леммы будут доказаны на втором этапе, когда все основные спецификации зафиксированы и будут выкладываться протоколы доказательств. Корректность лемм будет доказана посредством Coq или же лемма-функций, поддерка которых появится в одном из следующий релизов инструментария.
LibFuzzer - библиотека для фаззинга функций. Для части функций произведена соответствующая интерграция с данной библиотекой. Для того, чтобы можно было запустить фаззинг, необходио иметь в системе компилятор clang, а в корне директоии библиотеку libFuzzer.a Запуск фаззинга:
$ make fuzz-<func>
$ make fuzz-check_bytes8