Preview

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

Расширенный поиск
Том 31, № 6 (2019)
Скачать выпуск PDF
7-20
Аннотация
В работе мы рассмотрим подход статической верификации исходного кода программы на предмет корректной работы с памятью. Метод основывается на использовании символьных графов для представлении памяти программы. В работе представлено расширение символьных графов памяти, позволяющее использовать предикаты над символьными значениями для повышения точности анализа. Предикаты позволяют отсекать недостижимые пути, уменьшая количество ложных сообщений об ошибках, а также находить новые ошибки за счет добавления новых проверок на символьных значениях. Метод реализован на основе инструмента CPAchecker. Практическая полезность продемонстрирована на драйверах ядра операционной системы Linux.
21-32
Аннотация

Автоматическое обнаружение ошибок в программах является крайне востребованным направлением современных исследований и разработок в области обеспечения безопасности и устойчивости программного обеспечения. В рамках проекта 17-07-00702 Российского фонда фундаментальных исследований исследовались направления применения комбинированных методов анализа программ, совмещающих динамическое символьное исполнение, рандомизированное тестирование и статический анализ программ. Разработаны методы направленного анализа программ, основанные на совмещении статического анализа и динамического символьного исполнения, совмещения рандомизированного тестирования и динамического символьного исполнения программы. В данной статье рассматривается формальная модель обнаружения ошибок в программах методом символьного исполнения программ и её реализация для обнаружения ошибок выхода за границы буфера в памяти. Приводится формальная модель символьного исполнения программ, формулируется и доказывается теорема об обнаружении ошибки в программе, основанная на нарушении области определения операции вычислительной системы. Приводится описание реализации анализатора нарушения границ буфера в памяти в процессе динамического символьного исполнения программы и результаты применения реализованного прототипа анализатора на наборе программ из поставки Debian Linux, подтверждающих применимость предложенного метода обнаружения ошибок.

33-64
Аннотация

Обнаружение недекларированных возможностей программного обеспечения является одной из основных задач анализа безопасности бинарного кода. Автоматизация решения этой задачи затруднена и требует участия эксперта информационной безопасности. Существующие решения ориентированы на ручную работу аналитика, автоматизация его действий не несет в себе системный характер. В случае отсутствия необходимого инструментария аналитик лишается необходимой поддержки и вынужден самостоятельно заниматься разработкой инструментов, что сильно отдаляет его от получения необходимых практических результатов. В данной работе представлен программный комплекс, решающий задачу выявления недекларированных возможностей в целом: от создания контролируемой среды выполнения до подготовки высокоуровневого описания интересующего алгоритма. Представлен пакет инструментов разработчика QEMU QDT, предлагающий поддержку жизненного цикла разработки виртуальных машин, включая вопросы специализированного тестирования и отладки. Представлено высокоуровневое иерархическое представление алгоритма программы на основе блок-схем, а также алгоритм его построения. Предложенное представление основано на гиперграфе и позволяет реализовать ручной анализ потока данных на различных уровнях детализации. В будущем разработанное представление может использоваться для реализации алгоритмов автоматического анализа. Предложен подход к повышению качества полученного представления алгоритма с помощью объединения отдельных потоков данных в один, связывающий логические модули алгоритма. Для оценки результата построения высокоуровневого представления алгоритма разработан набор тестов на основе реальных программ и модельных примеров.

65-88
Аннотация

Программный инструментарий для работы с бинарным кодом востребован не только разработчиками: невозможно добиться достаточной безопасности современных программ без изучения свойств исполняемого кода. Базовым компонентом такого инструментария является декодер машинных команд. У разных процессорных архитектур реализации декодеров разнородны, результаты разбора команд несовместимы, а сопровождение затруднительно из-за повсеместной практики реализовывать декодеры в виде каскадов ветвлений. Дальнейший анализ бинарного кода (на уровне потоков данных и управления, символьная интерпретация и др.) оказывается непереносимым между различными процессорными архитектурами из-за ограничений и особенностей реализации декодеров. В статье предлагается подход к декодированию машинных команд, основанный на внешних спецификациях. Отличительной особенностью подхода является оригинальный способ представления декодированной команды в универсальном (т.е. не отличающемся от одной архитектуры к другой) виде. Декодирование осуществляется при помощи разработанной авторами абстрактной стековой машины. Несмотря на неизбежные накладные расходы, обусловленные большей универсальностью подхода, прототип реализации показывает скорость разбора лишь в 1,5-2,5 раза уступающую традиционным декодерам, с учетом времени разбора спецификации и формирования служебных структур данных. Предлагаемый подход к организации декодирования позволит в перспективе развернуть единый стек программных средств анализа бинарного кода, применимый к различным процессорным архитектурам. В статье обсуждаются вопросы дальнейшей трансляции декодированных команд в машинно-независимое промежуточное представление для анализа их операционной семантики и проведения абстрактной интерпретации. Приведены практически полезные примеры интерпретации: конкретная интерпретация для эмуляции бинарного кода и «направляющая» интерпретация, позволяющая увязать идею абстрактной интерпретации с задачей углубленного автоматического анализа отдельных путей в программе.

89-98
Аннотация

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

99-124.
Аннотация

В работе приводится обзор существующих методов и инструментов автоматизированной генерации эксплойтов повторного использования кода. Такие эксплойты используют код, уже содержащийся в уязвимом приложении. Подход повторного использования кода (например, возвратно-ориентированное программирование) позволяет эксплуатировать уязвимости программного обеспечения при наличии защитного механизма операционной системы, который запрещает исполнение кода страниц памяти, помеченных в качестве данных. В статье дается определение базовых понятий таких, как гаджет, фрейм гаджета, каталог гаджетов. Кроме того, показывается, что гаджет по своей сути является инструкцией, а их набор задает некоторую виртуальную машину. Задача создания эксплойта сводится к задаче генерации кода для такой виртуальной машины. Набор команд виртуальной машины задается исполняемым кодом конкретной программы. В работе приводится обзор методов поиска гаджетов и определения их семантики (формирования каталога гаджетов). Они позволяют получить набор команд виртуальной машины. Если набор гаджетов в каталоге полон по Тьюрингу, то гаджеты из каталога можно использовать в качестве набора команд целевой архитектуры компилятора. Однако в каталоге гаджетов для конкретного приложения могут отсутствовать некоторые инструкции, поэтому в литературе было предложено несколько способов для замены отсутствующих инструкций несколькими гаджетами. Связывание гаджетов в цепочки может происходить как поиском гаджетов по шаблонам, задаваемым регулярными выражениями, так и с учетом семантики гаджета. Более того, существуют подходы конструирования ROP цепочек с использованием генетических алгоритмов, а также методы с использованием SMT-решателей. В статье проводится сравнение инструментов с открытым исходным кодом. Мы предлагаем тестовую систему rop-benchmark, с помощью которой была проведена экспериментальная проверка работоспособности генерируемых инструментами цепочек на специально сформированном наборе тестов.

125-144
Аннотация

Сегодня виртуализация – это ключевая технология облачных вычислений и современных центров обработки данных, обеспечивающая масштабируемость и безопасность, управление глобальной ИТ-инфраструктурой и снижение затрат. Среди методов виртуализации, наиболее популярной стала контейнеризация – изоляция связанных групп процессов, разделяющих общее ядро операционной системы. Эффективность контейнеризации в сравнении с классической аппаратной виртуализацией, проявляется в компактности контейнеров и меньших накладных затратах вычислительных ресурсов – памяти, диска, ЦПУ.  Однако в сравнении с классическими архитектурами без изоляции процессов контейнеры могут обходиться дороже, и в любом случае, индустрия ждет дополнительной оптимизации – скорости запуска, экономии памяти и дискового пространства и других ресурсов. В этом может помочь различное кеширование – старейший механизм повышения производительности программ без радикальной модификации алгоритма и оборудования. Однако при этом возникают различные архитектурно-инженерные дилеммы вида «безопасность или эффективность» и здесь мы рассмотрим современные научно-технические подходы к их решению в разных аспектах – ускорение запуска, оптимизация совместного использования, ускорение сборки образов, а также некоторые проблемы безопасности, возникшие из-за агрессивного кэширования в процессорных архитектурах. А в некоторых сценариях использования мультиконтейнерных систем наоборот, скорость и задержки не важны, важно обеспечить максимальную загрузку физических серверов – в этом случае актуальны алгоритмы планирования и размещения контейнеров, и нами приведен обзор теоретических работ на эту тему.

145-162
Аннотация

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

163-176
Аннотация
Ветроэнергетика – одно из важнейших направлений в развитии возобновляемых источников энергии в РФ. Наиболее важными направлениями в ветроэнергетике являются задачи проектирования новых ветропарков, задачи  эксплуатации и мониторинга ветропарков, задачи проектирования ветроэлектрических установок (ВЭУ), разработка тематического российского программного обеспечения и т.п. В связи со строительством новых ветропарков на территории РФ возникает ряд актуальных фундаментальных и прикладных задач. В данной работе рассматривается одна из таких задач: исследование ветровой обстановки в районе поселка Тикси, ввиду установки там ветроэлектростанции. Прогнозирование ветровой обстановки производится на основе мезомасштабной модели Advanced Research WRF (Weather Research and Forecasting) с использованием данных Global Forecast System (GFS) модели.  Представленные расчеты производились на серии вложенных сеток с пространственным разрешением 1, 3 и 9 км. Предлагается методика для исследования и мониторинга ветропарка вблизи поселка Тикси, которая основана на интерполяции результатов, полученных из Advanced Research WRF, на модель меньшего масштаба в рамках библиотеки Simulator fOr Wind Farm Applications (SOWFA) открытого пакета OpenFOAM.
177-186
Аннотация
В настоящее время в РФ активно ведется строительство новых ветропарков. Вопросы изучения физических процессов являются актуальными, так как действующие ветропарки оказывают влияние на микроклимат и экологию. В ветропарках возможно появление и движение жидких и твердых частиц. При исследовании двухфазных потоков, содержащих взвесь аэрозольных частиц (дисперсная фаза) в несущей среде (дисперсионная среда) в атмосфере важно правильно выбирать основные параметры, определяющие систему, и адекватно описать реальный процесс при помощи сформулированной математической модели. Работа посвящена разработке новых решателей на базе библиотеки SOWFA в составе открытого пакета OpenFOAM 2.4.0 для изучения моделирования динамики частиц в планетарном (атмосферном) пограничном слое и в модельном ветропарке. Для описания динамики частиц используется эйлер-лагранжев подход. Разработаны два новых решателя на базе ABLSolverи pisoTurbineFoam.ALM для моделирования динамики частиц. Представлены результаты расчета для случая нейтрального пограничного слоя и модельного ветропарка с 14 модельными ветроустановками. Приведены графики для распределения частиц с разным диаметром по высоте. Для расчета одного примера было использовано от 72 до 96 вычислительных ядер.
187-194
Аннотация
В данной работе систематически исследуется влияние численной диссипации на расчетную точность метода моделирования крупных вихрей с пристенным моделированием. С этой целью в свободном программном обеспечении OpenFOAM® было проведено шестнадцать расчетов развитого турбулентного течения в канале. Расчеты проведены на сетках четырех разных плотностей, по четыре расчета на каждой сетке, в каждом из которых, в свою очередь, установлен разный уровень численной диссипации посредством изменения интерполяционной схемы для конвективного переноса. Проведено сравнение результатов расчетов с данными прямого численного моделирования, находящимися в открытом доступе. Показано, что профили ошибки всех рассмотренных величин находятся в монотонной зависимости от объема численной диссипации. Диссипация предсказуемо приводит к подавлению высокочастотных флуктуаций скорости. Кроме этого, она также приводит к увеличению энергии крупномасштабных флуктуаций и существенной переоценке уровня кинетической энергии турбулентности во внутреннем слое. Однако повышенный уровень диссипации приводит и к улучшению точности расчета средней скорости течения, что, в свою очередь, обеспечивает более точную оценку касательного напряжения на стенке пристенной моделью. Таким образом, оптимальный уровень диссипации может зависеть от основной цели расчета. Эффект плотности расчетной сетки на точность расчета трудно предсказуем, и оптимальное значение плотности зависит как от рассматриваемой физической величины, так и от уровня диссипативности интерполяционных схем.
195-202
Аннотация

В статье предложен метод для анализа полного сопротивления движению судна на скоростях хода, соответствующих числу Фруда по длине от 0,14 до 0,41. Основная идея метода состоит в разделении корпуса судна на составляющие поверхности. Данный подход позволяет рассчитать распределение силы сопротивления по длине судна. На основании полученных данных могут быть выбраны зоны для корректировки обводов, а также может быть выполнено более качественное сравнение нескольких вариантов корпуса. Перед примером применения предложенного метода были выполнены постановка задачи расчета сопротивления в программном комплексе OpenFOAM, валидация расчетной схемы и проверка сеточной сходимости. Для выполнения расчетов использовались стандартный решатель interDyMFoam и модель корпуса DTMB 5415. Для реализации предложенного метода корпус DTMB 5415 был разделен на 22 поверхности по длине судна. По результатам расчетов были получены кривые распределения силы сопротивления по длине корпуса для рассматриваемых скоростей хода. По результатам анализа кривых были разработаны два варианта обводов носовой оконечности корпуса DTMB 5415: без бульба и с обтекаемым бульбом. Оба варианта обводов обладают меньшим сопротивлением на всех скоростях хода по сравнению с базовым корпусом DTMB 5415. По результатам анализа кривых распределения силы сопротивления трех корпусов получено, что в районе средней и кормовой частей корпуса (~3/4 длины судна) распределенная сила сопротивления практически не зависит от скорости хода и обводов носовой оконечности. Носовая оконечность при этом играет первостепенную роль в формировании значении полного сопротивления корпуса.

203-214
Аннотация

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

215-224
Аннотация
В настоящее время практически не вызывает сомнений наличие крупномасштабных магнитных полей в спиральных галактиках. Их эволюция описывается с помощью механизма динамо. Динамо основано на совместном действии дифференциального вращение и альфа-эффекта. В случае галактик, как правило, используется планарное приближение, связанное с тем, что галактический диск достаточно тонкий. Отдельный интерес представляют так называемые внешние кольца галактик. Исследование магнитных полей в них имеет некоторые существенные трудности. Во-первых, полагать, что внешнее кольцо является тонким по сравнению с радиальными размерами, уже нельзя. Во-вторых, необходим учет влияния магнитного поля на турбулентные движения межзвездной среды. В настоящей работе представлены результаты моделирования магнитных полей, а также продемонстрировано влияние магнитного поля на турбулентные движения межзвездной  среды.
225-236
Аннотация
Возможности численного моделирования движения гидродинамических потоков около объектов сложной формы позволяют рассматривать результаты вычислений, как один из способов понимания механизмов ветрового выноса песчаных частиц. Для исследования условий возникновения микрорельефа проводится ряд численных экспериментов с использованием открытого пакета Open OpenFOAM. Над неоднородностями поверхности, определяемыми особенностями взаимного расположения частиц, возникают области понижения давления, вблизи которых более вероятен ветровой вынос частиц. Причиной такого понижения давления являются различного рода разрежения структуры пространственного расположения элементов поверхности: изменение расстояния, изменение ориентации структуры в пространстве, изменение угла между плоскостями, содержащими частицы. За счет понижения давления происходит увеличение скорости воздушного потока у поверхности и возникновение микровихрей.
237-252
Аннотация

 

В работе рассматривается применение различных современных технологий высокопроизводительных вычислений для ускорения численного решения задач распространения динамических волновых возмущений с использованием сеточно-характеристического метода. Рассматриваются технологии как для центральных процессоров (CPU), так и для графических процессоров (GPU). Приведены сравнительные результаты применения технологий MPI, OpenMP, CUDA. В качестве примеров работы разработанного программного комплекса приводится ряд примеров расчета задач сейсмики и геофизики. Отдельно рассмотрен вопрос распараллеливания задач с наличием контактов многих сеток и топографии дневной поверхности, используя криволинейные сетки.


 



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


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