В настоящем выпуске Трудов ИСП РАН представлены статьи по одному из наиболее развитых направлений исследований и разработок в ИСП РАН - технологии анализа, моделирования и трансформации программ. Все эти статьи подготовлены по материалам докладов, представленных на Открытой конференции ИСП РАН в 2016 г.

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

Разыменование пустого указателя - это хорошо известная ошибка, встречающаяся в объектно-ориентированных программах. Ее можно избежать путем добавления к языку, на котором пишется программа, специальных правил приложимости. Достаточно ли этих правил для гарантии отсутствия таких исключительных ситуаций? Данная статья посвящена безопасности пустых указателей во внутрипроцедурном контексте, в котором не требуются какие-либо дополнительные аннотации. Правила формализуются в системе автоматического доказательства теорем Isabelle/HOL. Затем доказывается теорема о сохранении безопасности пустых указателей в крупношаговой семантике. Наконец, демонстрируется, что при наличии таких правил семантики с безопасностью пустых указателей и без нее эквивалентны.

Основная часть уязвимостей в программах вызвана переполнением буфера. Чтобы предотвратить переполнение буфера и уменьшить ущерб от него используется безопасное программирование, аудит исходного кода, аудит бинарного кода, статические и динамические особенности кодогенерации. В современных компиляторах реализованы механизмы защиты, работающие на этапе компиляции и на этапе выполнения скомпилированной программы: переупорядочивание переменных, копирование аргументов и встраивание стековой канарейки. В статье описывается исследование, посвященное поиску недостатков в этих механизмах. Мы протестировали компиляторы MSVC, gcc и clang и обнаружили, что два из них содержат ошибки, позволяющие эксплуатировать переполнение буфера при определенных условиях.

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

В статье описывается поиск недостижимого кода в исходном коде программ, написанных на языках Си и Си++. Приведена классификация видов недостижимого кода. Описаны цели, достигаемые поиском недостижимого кода: выдача предупреждений о возможных ошибках в анализируемой программе и улучшение точности других анализов. Формально поставлены три задачи анализа потока данных: анализ интервалов значений, анализ выколотой точки, предикатный анализ. Решения этих задач применены для поиска инвариантных условий ветвления программы. Показаны особенности поиска недостижимого кода в статических анализаторах, предназначенных для поиска ошибок. Отмечены общие ситуации, в которых нет необходимости сообщать пользователю о найденном недостижимом коде. Описанные алгоритмы реализованы в статическом инструменте Svace, разрабатываемом в ИСП РАН. Оценка результатов детекторов произведена для исходного кода операционных систем Android-5.02 и Tizen-2.3 в виде количественного сравнения предупреждений, выданных каждым из анализов, и их пересечения между собой.

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