30.05.2017: Компонент AstraVer был представлен на международном семинаре Frama-C & SPARK Day 2017
В презентации на международном семинаре Frama-C & SPARK Day 2017, который состоялся 30 мая в университете Париж Дидро, мы представили наш опыт дедуктивной верификации модулей ядра Linux с помощью платформы Frama-C, Why3 и компонента AstraVer, а также реализованную в нем комбинированную модель ограниченных целых. Мы также представили нашу новую модель памяти на основе регионов, разработанную для компонента AstraVer на семинаре команды TOCCATA в лаборатории LRI, где разрабатывается платформа дедуктивной верификации Why3.
AstraVer — это компонент для платформы статического анализа Frama-C, предназначенный для дедуктивной верификации низкоуровневого C-кода. AstraVer использует платформу дедуктивной верификации Why3 и наследует реализацию Jessie, компонента Frama-C для поддержки верификации C-программ с помощью платформы Why. AstraVer разрабатывается в рамках проекта Linux Deductive Verification с целью улучшить применимость инструментов автоматизированной дедуктивной верификации, использующих SMT-решатели, для доказательства свойств корректности фрагментов кода ядра Linux. По сравнению с Jessie, в AstraVer реализована комбинированная модель ограниченных целых на основе битовых векторов и линейной арифметики, а также базовая поддержка доказательств в модельном (ghost) коде. Разрабатывается новая модель памяти на основе регионов, поддерживающая произвольные приведения типов указателей и произвольную адресную арифметику.
При верификации непрерывно разрабатываемого низкоуровневого кода ядер операционных систем возникает ряд специфических трудностей, осложняющих применение средств автоматизированной дедуктивной верификации. Повсеместное использование таких возможностей языка C, как адресная арифметика с вложенными структурами (в частности, макрос container_of), непрефиксные приведения типов указателей, объединения, побитовые операции и преднамеренные арифметических переполнения, предполагает использование соответствующих низкоуровневых и точных моделей памяти и ограниченных целых, например, теории битовых веторов и модели памяти с поддержкой произвольной переинтерпретации типов. Но использование таких моделей значительно снижает производительность автоматических решателей. В компоненте AstraVer мы реализуем подходы, основанные на многоуровневых, но не полностью автоматических моделях, требующих поддержки со стороны пользователя в виде специальных дополнительных аннотаций.
В докладе "Specifying and Proving Correctness of Linux Kernel Components with ACSL" на Frama-C & SPARK Day 2017 (30-го мая) мы рассказали о нашем опыте дедуктивной верификации модулей ядра Linux с использованием платформы Frama-C и компонента AstraVer с комбинированной моделью ограниченных целых чисел, позволяющей доказывать свойства фрагментов кода, манипулирующего побитовым представлением целых, с помощью дополнительных аннотаций, модельного (ghost) кода и лемма-функций.
Днем ранее, 29 мая, мы представили доклад на семинаре команды TOCCATA в лаборатории Laboratoire de recherche en informatique (LRI) в INRIA Сакле, где разрабатывается платформа дедуктивной верификации Why3. В этом докладе "A Memory Model and Other Extensions of ACSL Made for Deductive Verification of Linux Kernel Modules" мы представили нашу модель памяти на основе регионов с поддержкой переинтерпретации, которая отличается тем, что использует некорректный в общем случае оптимистичный анализ регионов, результаты работы которого затем проверяются вместе с остальными условиями верификации. В случаях, когда результат работы анализа регионов оказывается некорректным, доказательство условий верификации оказывается невозможным. В таких случаях пользователь может предоставить дополнительные аннотации для уточнения анализа регионов. Это позволяет эффективно поддерживать произвольную адресную арифметику, объединения и произвольные приведения типов указателей.