Preview

Труды Института системного программирования РАН

Расширенный поиск
Том 28, № 5 (2016)
Скачать выпуск PDF
9-10 31
Аннотация
В настоящем выпуске Трудов ИСП РАН представлены статьи по одному из наиболее развитых направлений исследований и разработок в ИСП РАН - технологии анализа, моделирования и трансформации программ. Все эти статьи подготовлены по материалам докладов, представленных на Открытой конференции ИСП РАН в 2016 г.
11-26 37
Аннотация
Описанный в данной статье метод позволяет автоматически обнаруживать использование неинициализированных значений в рамках полносистемной эмуляции. Это актуально для такого низкоуровневого программного обеспечения, как, например, BIOS или начальный загрузчик, выполняющие функции инициализации оборудования и загрузки операционной системы. Ошибки в данных программных системах наиболее опасны и приводят к неработоспособности всей системы целиком. Программное обеспечение подобного рода затруднительно тестировать на реальной аппаратуре, поэтому для этих целей используются эмуляторы различных архитектур. В рамках работы был разработан метод использования теневой памяти (памяти, содержащей информацию об исходной памяти) для хранения и отслеживания состояния регистров и ячеек гостевой памяти. Также были сформулированы критерии обнаружения использования неинициализированных значений и уведомления об ошибках. Разработанный метод был реализован и протестирован на гостевой системе архитектуры x86 в полносистемном эмуляторе QEMU.
27-54 137
Аннотация
Разыменование пустого указателя - это хорошо известная ошибка, встречающаяся в объектно-ориентированных программах. Ее можно избежать путем добавления к языку, на котором пишется программа, специальных правил приложимости. Достаточно ли этих правил для гарантии отсутствия таких исключительных ситуаций? Данная статья посвящена безопасности пустых указателей во внутрипроцедурном контексте, в котором не требуются какие-либо дополнительные аннотации. Правила формализуются в системе автоматического доказательства теорем Isabelle/HOL. Затем доказывается теорема о сохранении безопасности пустых указателей в крупношаговой семантике. Наконец, демонстрируется, что при наличии таких правил семантики с безопасностью пустых указателей и без нее эквивалентны.
55-72 148
Аннотация
Основная часть уязвимостей в программах вызвана переполнением буфера. Чтобы предотвратить переполнение буфера и уменьшить ущерб от него используется безопасное программирование, аудит исходного кода, аудит бинарного кода, статические и динамические особенности кодогенерации. В современных компиляторах реализованы механизмы защиты, работающие на этапе компиляции и на этапе выполнения скомпилированной программы: переупорядочивание переменных, копирование аргументов и встраивание стековой канарейки. В статье описывается исследование, посвященное поиску недостатков в этих механизмах. Мы протестировали компиляторы MSVC, gcc и clang и обнаружили, что два из них содержат ошибки, позволяющие эксплуатировать переполнение буфера при определенных условиях.
73-92 78
Аннотация
В данной работе предложен уточненный метод автоматизированной оценки степени опасности найденных программных дефектов. На этапе тестирования промышленного программного обеспечения выявляется значительное число дефектов, приводящих к аварийному завершению. Из-за ограниченности ресурсов исправление дефектов растягивается во времени и требует расстановки приоритетов. Основным критерием для назначения высокого приоритета становится возможность использования ошибки в злонамеренных целях. На практике эта задача решается путем автоматизированного построения входных данных, подтверждающего наличие опасной уязвимости. Но в известных публикациях по данной теме не учитывают современные защитные механизмы, препятствующие действиям атакующего, что снижает качество вырабатываемых оценок. В данной статье рассматриваются современные защитные механизмы и дается оценка их распространенности и эффективности. Метод применим к бинарным файлам и не требует какой-либо отладочной информации. В основе метода лежит символьная интерпретация трасс выполнения, полученных при помощи полносистемного эмулятора. Даже в условиях одновременного функционирования DEP, ASLR и защиты стека («канарейка») метод способен демонстрировать возможность использования ошибок, сочетающих условия «write-what-where» и переполнение буфера на стеке. Возможности реализованного метода были продемонстрированы на модельных примерах и реальных программах.
93-104 72
Аннотация
Развитие методов обнаружения вредоносных приложений привело к развитию специальных технологий, которые помогают вредоносным приложениям оставаться незамеченными. Многие из них направлены на изменение сигнатуры программного кода. Для академического изучения этих методов и кода, получаемого с их помощью, необходимо разработать инфраструктуру для автоматизированного изменения сигнатуры имеющейся программы. В данной работе приводится результаты работы по разработке и реализации такого автоматизированного инструмента на базе компиляторной инфраструктуры LLVM и инфраструктуры инструментации и трансформации бинарного кода Syzygy. В рамках этих инфраструктур были реализованы диверсифицирующие и обфусцирующие преобразования, которые были направлены на изменение сигнатуры исполняемого файла. Для работы этих инструментов требуется соответственно наличие исходного кода или отладочной информации. Были разработаны и реализованы следующие преобразования: вставка мертвого кода, перестановка местами инструкций, перестановка местами базовых блоков, перестановка местами функций в модуле, замена инструкций на эквивалентные, шифрование константных буферов данных. По результатам проведенных работ была продемонстрирована работоспособность данного подхода на реальных примерах, а также выявлены недостатки предложенного подхода и пути дальнейшего развития.
105-118 41
Аннотация
Данная работа посвящена формализации понятия ошибочной ситуации при статическом анализе исходного кода, основанном на символьном выполнении. При использовании методов символьного выполнения для статического анализа необходимо пересматривать критерий выдачи ошибок, так как оригинальный критерий приводит к чрезмерному числу ложных срабатываний. Для решения этой проблемы предлагаются альтернативные определения ошибочной ситуации, сообщающие об ошибке только в том случае, когда она происходит на некотором множестве значений входных переменных. Примерами таких множеств являются, например, множество значений входных переменных, при которых управление пройдет через заданную точку программы, или множество значений, при которых управление пройдет по заданному пути в графе потока управления. В данной работе рассматриваются различные способы задания таких множеств начальных значений. Анализируются полученные таким образом определения ошибочных ситуаций. Приводятся алгоритмы, обнаруживающие данные ошибочные ситуации, а также доказывается их соответствие. Рассматривается практическое применение приведённых определений ошибочных ситуаций, а именно: классификация срабатываний инструментов статического анализа; учет неизвестных контракта вызова анализируемой функции; использование определения ошибочной ситуации в качестве запроса к SMT-решателю для поиска точного решения в соответствии с данными определением.
119-134 59
Аннотация
В данной работе рассматривается метод поиска межпроцедурных ошибок доступа к буферу с помощью статического анализа. В основе рассматриваемого подхода лежит разработанный ранее алгоритм внутрипроцедурного анализа на базе символьного исполнения с объединением состояний, который является чувствительным к путям и учитывает взаимосвязи между переменными, такие как сравнения, арифметические операции и инструкции приведения типа. В работе предложено формальное определение межпроцедурного дефекта и рассмотрены некоторые типы межпроцедурных ошибок доступа к буферу. Межпроцедурный анализ реализован с помощью метода резюме, что позволяет в некоторой степени добиться контекстной чувствительности. Показано, как можно расширить внутрипроцедурный алгоритм для отслеживания межпроцедурных связей между переменными. Кроме этого, приведен алгоритм построения двух типов достаточных условий наличия ошибки доступа к буферу в функции, которые сохраняются в резюме и проверяются при вызове этой функции. Описанный подход был реализован в инструменте статического анализа Svace. На проекте Android 5.0.2 было получено 351 предупреждение об ошибке доступа к буферу, среди которых 64% оказались истинными, при этом существенного замедления анализа не произошло.
135-144 60
Аннотация
В статье рассматривается метод поиска ошибок выхода за границы буфера в рамках метода комбинированного (статико-динамического) анализа бинарного кода. Для поиска ошибок используется символьная интерпретация последовательности машинных инструкций, выполненных за время работы программы. Рассматриваются способы увеличения точности анализа за счёт анализа циклов работы со строками, а также предварительного расширения покрытия кода. С помощью инструмента, разработанного на основе предложенных методов, были найдены как известные ошибки, так и ошибки, информация о которых ранее не была опубликована.
145-158 76
Аннотация
В статье описывается поиск недостижимого кода в исходном коде программ, написанных на языках Си и Си++. Приведена классификация видов недостижимого кода. Описаны цели, достигаемые поиском недостижимого кода: выдача предупреждений о возможных ошибках в анализируемой программе и улучшение точности других анализов. Формально поставлены три задачи анализа потока данных: анализ интервалов значений, анализ выколотой точки, предикатный анализ. Решения этих задач применены для поиска инвариантных условий ветвления программы. Показаны особенности поиска недостижимого кода в статических анализаторах, предназначенных для поиска ошибок. Отмечены общие ситуации, в которых нет необходимости сообщать пользователю о найденном недостижимом коде. Описанные алгоритмы реализованы в статическом инструменте Svace, разрабатываемом в ИСП РАН. Оценка результатов детекторов произведена для исходного кода операционных систем Android-5.02 и Tizen-2.3 в виде количественного сравнения предупреждений, выданных каждым из анализов, и их пересечения между собой.
159-174 59
Аннотация
Динамическое символьное исполнение - это хорошо известная техника, применяемая для решения различных задач анализа программ: генерация входных данных для увеличения тестового покрытия программы, для эксплуатации уязвимостей и т.д. В то же время значительное падение производительности при динамическом символьном исполнении также является хорошо известной, в общем случае NP-сложной проблемой в связи с экспоненциальным взрывом количества анализируемых путей и решением задачи SAT/SMT при разрешении предиката пути. Применение метода грубой силы при попытке анализа всех достижимых путей в программе, как правило, не имеет смысла в условиях жесткого ограничения времени решения поставленных задач. Поэтому применяются различные методы и эвристики для увеличения производительности анализа и сокращения анализируемого пространства. Мы представляем подход совмещения статического анализа исполняемого кода, основанного на использовании библиотеки binutils, и метода динамического символьного исполнения, основанного на инструменте итеративного динамического анализа Avalanche, для направленной генерации входных данных программы с целью достижения заранее определенной функции в программе. На первом шаге предлагаемого подхода строится усеченный граф вызовов программы, который содержит только те функции, вызов которых в конечном счете приводит к вызову заранее определенной функции. Далее мы дополняем граф вызовов графом потока управления внутри функций, включенных в усеченный граф вызовов. С использованием усеченного графа потока управления программы, который содержит только вызовы и условные переходы, приводящие в конечном итоге к вызову заранее определенной функции, вычисляется метрика наиболее перспективного пути для проведения дальнейшего анализа. Предложенный подход позволил значительно (до двенадцати раз для некоторых реальных программ) сократить время достижения заранее определенной функции по сравнению с методом грубой силы.
175-198 45
Аннотация
В данной статье речь идет о двух методах ускорения процесса сборки программы: распараллеливании межпроцедурной оптимизации и о легковесном методе проведения оптимизаций. Ускорение в первом случае достигается за счет горизонтального масштабирования системы оптимизации времени связывания. Во втором случае метод представляет собой работу исключительно на аннотациях, что позволяет работать с минимально необходимой информацией вместо кода всей программы целиком. Проблема горизонтальной масштабируемости системы всегда связана с необходимостью разделения большой задачи на несколько подзадач, которые могут быть выполнены независимо и параллельно. Масштабирование оптимизаций времени связывания - непростая задача, так как оптимизирующие преобразования работают последовательно на всем промежуточном представлении программы, и результат их работы зависит от предыдущих преобразований. Для оптимизации на этапе связывания необходимо разделить промежуточное представление компилируемой программы на участки, минимизируя зависимости между ними, и оптимизировать эти участки отдельно. Для анализа программы используется граф вызовов. Таким образом, задача сводится к тому, чтобы разделить граф вызовов на несколько слабо связанных друг между другом компонент. Данная задача относится к одной из сложных комбинаторных проблем, и нахождение оптимального решения - NP-полная задача. Тем не менее, качество работы алгоритма зависит от свойств графа, поэтому целесообразно исследовать свойства графа вызовов в контексте оптимизаций времени связывания и подобрать к нему приемлемый алгоритм, проверив работу на реальных программах. Основная задача данного исследования - найти легковесный и эффективный метод разбиения структуры программы таким образом, чтобы как можно меньше ухудшить производительность собираемых программ при независимой оптимизации участков кода. В статье представлен новый метод разбиения графа вызовов программ, проведено его сравнение с некоторыми другими существующими методами для графов вызовов тестовых программ. Также описана реализация предложенного метода в системе LLVM, представлены результаты сравнения производительности программ, собранных в один поток и в несколько потоков. Запуск на 4-х потоках показал ускорение процесса сборки в среднем на 31%, тогда как производительность по сравнению с собранными в один поток программами упала в среднем на 3%. Для легковесного метода оптимизаций описана реализация преобразования удаления мертвого кода. Также приведены результаты тестирования в совокупности с ленивой загрузкой кода.
199-214 41
Аннотация
Распределение регистров оказывает существенное влияние на производительность генерируемого кода. В данной статье исследуется задача распределения регистров во время динамической двоичной трансляции. Так как существующие алгоритмы распределения регистров рассчитаны на использование в компиляторах, они плохо подходят для использования во время динамической двоичной трансляции. Был разработан новый алгоритм, который определяет, какие переменные должны располагаться на каких регистрах в начале и в конце базового блока (назовем эти ограничения пред- и постусловиями данного базового блока), а затем решает задачу локального распределения регистров в данных ограничениях. Для обеспечения корректности ограничений алгоритм должен работать так, чтобы бля любого базового блока b', предшествующего блоку b, постусловия блока b' совпадали с предусловиями блока b. Этого можно достичь, если выделить в графе потока управления группы дуг, на всех концах которых ограничения должны быть неизменны. Такие дуги называются точками синхронизации. Точки синхронизации являются связными компонентами в неориентированном графе, вершинами которого являются дуги графа потока управления, а ребрами соединены те дуги-вершины, которые либо входят, либо выходят из одного базового блока. Данное утверждение позволяет эффективно находить точки синхронизации. Для определения того, сколько переменных должно находиться на регистрах в точке синхронизации, количество доступных регистров оценивается с помощью регистрового давления. Затем выбираются конкретные переменные на их частоты использования в данном фрагменте кода. Алгоритм локального распределения регистров был модифицирован, чтобы использовать предусловия и обеспечивать постусловия. В статье приводится эффективный алгоритм для приведения существующего распределения в конце базового блока к требуемым постусловиям и доказывается оптимальность этого алгоритма. Применение описанного алгоритма распределения регистров привело к сокращению времени работы синтетического примера на 29.6%.
215-226 113
Аннотация
При разработке программного обеспечения разработчики часто прибегают к копированию того или иного участка кода для достижения желаемого результата. Копирование кода может привести к появлению различных ошибок, а также к увеличению размера исходного и бинарного кода. Задача поиска семантически сходных участков кода (клонов) в бинарных файлах становится более актуальной в связи с недоступностью исходного кода многих программных средств. В данной статье обсуждаются существующие методы поиска клонов бинарного кода и приводится описание разработанного нами инструмента обнаружения клонов в бинарном коде. Работа инструмента разделена на три основных этапа. Первый этап базируется на платформе Binnavi [1] и ответственен за генерацию графов зависимостей программы для каждой функции. В качестве основы для генерации графов используется платформенно-независимый язык REIL (Reverse Engineering Intermediate Language). Использование языка REIL позволяет генерировать графы сразу для нескольких целевых архитектур (x86, x86-64, ARM, MIPD, PPC), тем самым обеспечивает независимость инструмента от целевой архитектуры. На втором этапе производится поиск клонов на основе ранее созданных графов. Для каждой пары графов строится наибольший общий подграф, на основе которого определяются клоны бинарного кода. На третьем этапе полученные клоны визуализируются для удобного анализа полученных результатов.
227-238 38
Аннотация
Занимая около половины времени разработки, тестирование остается наиболее распространенным методом контроля качества ПО, и его недостаток может приводить к финансовым потерям. При систематическом подходе тестовый набор считается полным, если он обеспечивает определенное покрытие кода. На данный момент существует большое количество систематических генераторов тестов, направленных на поиск стандартных ошибок. Подобные инструменты порождают огромное количество трудночитаемых тестов, обладающих высокой ценой проверки человеком. Представленный в данной работе метод позволяет улучшить читаемость тестов, автоматически сгенерированных при помощи символьных вычислений, обеспечивая качественное снижение данной цены. Экспериментальные исследования генератора тестов, включающего данный метод в качестве заключительной фазы работы, были проведены на 12-ти строковых функциях из репозитория Linux. Оценка степени читаемости строк, содержащихся в оптимизированных тестах, сопоставима со случаем использования слов натурального языка, что положительно сказывается на процессе верификации результатов тестирования человеком.
239-268 322
Аннотация
Язык FlexT разработан для спецификации бинарных форматов данных. Язык является декларативным, рассчитанным на хорошее восприятие человеком, его основными конструкциями являются определения типов данных, которые напоминают определения типов в императивных языках программирования, но являются более гибкими. В работе сделан обзор возможностей современных проектов, направленных на спецификацию бинарных форматов файлов. Далее рассматриваются особенности языка FlexT, отдельно описываются возможности языка, позволяющие работать с форматами кодирования машинных команд. Кратко описаны реализованные программные системы, использующие интерпретатор FlexT и некоторые новые возможности поиска информации в бинарных файлах, которые даёт использование спецификаций.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)