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

Методы и инструменты автоматической статической верификации позволяют выявить все ошибки искомых видов в целевых программах при выполнении определенных предположений даже в условиях отсутствия полных моделей и формальных спецификаций. Эта возможность является основой предлагаемого в работе метода инкрементального построения спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем. Данный метод был реализован в системе статической верификации Klever и применен для проверки подсистемы поддержки терминальных устройств ядра ОС Linux.

В статье авторами рассматриваются результаты дедуктивной верификации набора из 26 библиотечных функций ядра ОС Linux с помощью стека инструментов AstraVer. В набор включены преимущественно функции, работающие с данными строкового типа. Целью верификации является доказательство свойств функциональной корректности. В статье рассматриваются аналогичные работы по верификации, сравниваются полученные результаты, рассматривается ряд проблем, с которыми сталкивались авторы предыдущих работ, в том числе проблемы, с которыми удалось справится в рамках данной работы и те, которые все ещё препятствуют успешной верификации. Также предлагается методология разработки спецификаций, примененная для рассматриваемого набора функций, которая включает некоторые шаблонные приёмы разработки спецификаций. Авторам удалось доказать полную корректность двадцати пяти функций. В статье приведены результаты доказательства полученных условий верификации каждой функции с помощью нескольких современных SMT-солверов.

Разработка виртуальных устройств и машин для QEMU - трудоёмкий процесс. С целью поддержки разработчика, в данной работе был проведён анализ архитектуры QEMU и процесса разработки моделей отдельных устройств и виртуальных машин для QEMU. Предлагается подход к разработке, в рамках которого начальный этап ощутимо автоматизируется, благодаря применению декларативного описания устройств и машин, а также средств графического представления разрабатываемых устройств и машин. Подход реализован в интегрированном инструменте, позволяющем разработчику QEMU получить компилируемый набор файлов с исходным Си-кодом. Разработчик задаёт параметры генерации устройств и описывает состав машины на языке Python или в графическом редакторе, обеспечивающем визуализацию текстового описания. Результатом применения инструмента при построении машины становится фактически готовый Си-код, требующий только уточнить конфигурацию процессора и обработать параметры командной строки. В случае периферийного устройства от разработчика потребуется реализовать поведенческий аспект. Проведённые эксперименты с платформами Q35 и Cisco 2621XM показали, что количество строк в описании устройства в 11-26 раз меньше числа строк получаемой заготовки на языке Си. Такая разница в объёме достигнута за счёт генерации формального кода, реализующего служебные интерфейсы QEMU. Такой код составляет ощутимую долю кода устройства, в то время как может быть сгенерирован по сравнительно небольшому описанию. Суммарный объём сгенерированного кода заготовок составил от ¼ до ¾. Исходный код разработанного инструмента доступен по адресу https://github.com/ispras/qdt.

Работа посвящена решению задачи декомпиляции одного из разновидностей формата DCU - файлов .dcuil, создаваемых компиляторами тех версий Delphi, которые работали для платформы .NET. Разработан метод решения этой задачи, состоящий из ряда этапов: синтаксический анализ кода CIL; формирование графа потока управления; генерация промежуточного представления; структурирование графа потоков управления; анализ потоков данных с учётом семантики команд CIL; улучшение промежуточного представления с учётом особенностей работы компилятора Delphi; генерация кода.

Разработка программного обеспечения является сложным и подверженным ошибкам процессом. В целях снижения сложности разработки ПО создаются сторонние библиотеки. Примеры исходных кодов для популярных библиотек доступны в литературе и интернет-ресурсах. В данной работе представлена гипотеза о том, что большинство подобных примеров содержат повторяющиеся шаблоны. Более того, данные шаблоны могут быть использованы для построения моделей, способных предсказать наличие (либо отсутствие) недостающих вызовов определенных библиотечных функций с использование машинного обучения. В целях проверки данной гипотезы была реализована система, реализующая описанный функционал. Экспериментальные исследования, проведенные на примерах для библиотеки OpenGL, говорят в поддержку выдвинутой гипотезы. Точность результатов достигает 80%, при условии рассмотрения уже первых 4-х ответов, предлагаемых системой. Можно сделать вывод о том, что данная система при дальнейшем развитии может найти индустриальное применение.

Разыменование нулевого указателя остаётся одной из основных проблем в современных объектно-ориентированных языках. Очевидное добавление ключевых слов, чтобы различать между всегда ненулевыми и возможно нулевыми ссылками, оказывается недостаточным во время инициализации объекта, когда некоторые поля, объявленные всегда ненулевыми, могут временно быть нулевыми до окончания инициализации. Существует несколько подходов к решению проблемы инициализации объекта. Каким образом их можно сравнить практически? Являются ли реализации обоснованными? Данная работа представляет набор примеров, выделяя сценарии использования из публикаций по теме и библиотек с открытым кодом, и объясняет стоящие за ними критерии. Затем она обсуждает ожидаемые результаты для выбранного набора инструментов, производящих проверки безопасности нулевых ссылок для Eiffel, Java и Kotlin, и завершается фактическими результатами, демонстрирующими незрелость решений.

В статье рассматриваются подходы и способы выполнения кода с использованием уязвимостей в программах. В частности, рассмотрены способы выполнения кода для переполнения буфера на стеке и в динамической памяти, для уязвимости использования памяти после освобождения и для уязвимости форматной строки. Описываются методы и подходы, позволяющие автоматически получать наборы входных данных, которые приводят к выполнению произвольного кода. В основе этих подходов лежит использование символьной интерпретации. Динамическое символьное выполнение предоставляет набор входных данных, который направляет программу по пути активации уязвимости. Предикат безопасности представляет собой дополнительные символьные уравнения и неравенства, описывающие требуемое состояние программы, наступающее при обработке пакета данных, например, передача управления на требуемый адрес. Объединив предикаты пути и безопасности, а затем решив полученную систему уравнений, можно получить набор входных данных, приводящий программу к выполнению кода. В работе представлены предикаты безопасности для перезаписи указателя, перезаписи указателя на функцию и уязвимости форматной строки, которая приводит к переполнению буфера на стеке. Описанные предикаты безопасности использовались в методе оценки критичности программных дефектов. Проверка работоспособности предикатов безопасности оценивалась на наборе тестов, который использовался в конкурсе Darpa Cyber Grand Challenge. Тестирование предиката безопасности для уязвимости форматной строки, приводящей к переполнению буфера, проводилось на программе Ollydbg, содержащей эту уязвимость. Для некоторых примеров удалось получить входные данные, приводящие к выполнению кода, что подтверждает работоспособность предикатов безопасности.

Уязвимости программного обеспечения являются серьезной угрозой безопасности. Важной задачей является развитие методов противодействия их эксплуатации. Она приобретает особую актуальность с развитием ROP-атак. Имеющиеся средства защиты обладают некоторыми недостатками, которые могут быть использованы атакующими. В данной работе предлагается метод защиты от атак такого типа, который называется мелкогранулярной рандомизацией адресного пространства программы при запуске. Приводятся результаты по разработке и реализации данного метода на базе операционной системы CentOS 7. Рандомизацию на уровне перестановки функций осуществляет динамический загрузчик с помощью дополнительной информации, сохраненной с этапа статического связывания. Описываются детали реализации и приводятся результаты тестирования производительности, изменения времени запуска и размера файла. Отдельное внимание уделяется оценке эффективности противодействия эксплуатации с помощью ROP атак. Строятся две численных метрики: процент выживших гаджетов и оценка работоспособности примеров ROP цепочек. Приводимая в статье реализация применима в масштабах всей операционной системы и не имеет проблем совместимости с точки зрения работоспособности программ. По результатам проведенных работ была продемонстрирована работоспособность данного подхода на реальных примерах, обнаружены преимущества и недостатки и намечены пути дальнейшего развития.

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

В данной работе рассматриваются проблемы масштабируемости проекта Keystone - центрального сервиса авторизации и аутентификации облачной платформы Openstack и новый принцип построения сервиса, позволяющий избегать этих проблем. В более ранних работах был предложен подход к масштабированию Openstack Keystone путем отказа от использования СУБД MySQL/MariaDB и PostgreSQL в качестве хранилища данных сервиса в пользу распределенных NoSQL решений. Данная работа представляет полноценную реализацию сервиса, обеспечивающего полную функциональность Openstack Keystone API V3, на базе API Gateway и использования Apache Cassandra.

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

В 2012 году М. А. Трушников предложил принципиально новый онлайновый алгоритм упаковки прямоугольников в полосу, а в 2013 году в [3] была получена оценка точности алгоритма в среднем, равной математическому ожиданию незаполненной прямоугольниками площади, равная . Ранее известная оценка была существенно улучшена. В настоящей работе данная оценка улучшена до , а также алгоритм Трушникова обобщён на случай упаковки прямоугольников в полос, , с сохранением оценки .

MPI - это хорошо зарекомендовавшая себя технология, которая широко используется в высокопроизводительной вычислительной среде. Однако настройка кластера MPI может быть сложной задачей. Контейнеры - это новый подход к виртуализации и простой упаковке приложений, который становится популярным инструментом для высокопроизводительных задач (HPC). Именно этот подход рассматривается в данной статье. Упаковка MPI-приложения в виде контейнера решает проблему конфликтных зависимостей, упрощает конфигурацию и управление запущенными приложениями. Для управления ресурсами кластера может использоваться обычная система очередей (например SLURM) или системы управления контейнерами (Docker Swarm, Kubernetes, Mesos и др.). Контейнеры также дают больше возможностей для гибкого управления запущенными приложениями (остановка, повторный запуск, пауза, в некоторых случаях миграция между узлами), что позволяет получить преимущество при оптимизации размещения задач по узлам кластера по сравнению с классической схемой работы планировщика. В статье рассматриваются различные способы оптимизации размещения контейнеров при работе с HPC-приложениями. Предлагается вариант запуска MPI приложений в системе Fanlight, упрощающий работу пользователей. Рассматривается связанная с данным способом запуска задача оптимизации.

Смешанная конвекция над нагреваемой горизонтальной пластиной была смоделирована с использованием четырех численных моделей на базе рейнольдсовых, вихревых и вязкостных моделей турбулентности. Основным критерием оценки адекватности моделей было распределение температуры на поверхности пластины и в слое жидкости над ней. В расчетах использовалась трехмерная расчетная область с условиями симметрии. Моделирование проводилось с использованием программного пакета Code_Saturne в нестационарной постановке. Для оценки сеточной сходимости решения были использованы три ортогональные сетки. Вязкостная модель u2-f и вихревая модель Смагоринского показали наиболее адекватные результаты. Однако наиболее точные распределения температуры в области преимущественного действия архимедовой силы были получены при использовании вихревой k-модели и эллиптической рейнольдсовой модели EBRSM. Разработанные модели пригодны для промышленного использования (например, для проектирования охлаждающих рубашек) и могут быть использованы в качестве основы для дальнейших исследований смешанной конвекции.

В связи с развитием ветроэнергетики и строительством новых ветропарков в РФ возникает потребность в решении ряда прикладных задач и разработке эффективных методик расчета элементов ветроустановок. Одно из направлений в задачах механики сплошной среды связано с задачами аэроупругости. В данной статье показана возможность решения связанной задачи аэроупругости с использованием программного комплекса на базе свободного программного обеспечения OpenFOAM и Code_Aster. На примере лопасти ветроустановки длиной 61.5 метра рассмотрены методики решения задач статической и динамической аэроупругости, в которых расчет обтекания лопасти дозвуковым набегающим потоком воздуха производится в пакете OpenFOAM (решатели simpleFOAM и pimpleFOAM), а расчет напряженно-деформированного состояния лопасти производится в пакете Code_Aster. В статье приводятся блок-схемы для трех различных подходов решения задачи аэроупругости, примеры скриптов и командных файлов для передачи данных между пакетами в процессе расчета. Контрольно-объемная сетка, состоящая их гексаэдральных элементов, для расчета обтекания лопасти построена в пакете OpenFOAM, конечно-элементная сетка, состоящая из треугольных оболочечных элементов первого порядка, для расчета напряженно-деформированного состояния построена в пакете Salome-Meca. Результаты расчета представлены в форме полей для давления и скорости; зависимостей для невязкок давления, скорости, турбулентной вязкости; проекций аэродинамической силы от времени; эпюр перемещения и напряжения; значений давления и перемещения для двух точек на поверхности лопасти от времени. Расчеты выполнены с использованием ресурсов web-лаборатории UniHUB ИСП РАН.

Представлен программный пакет для расчета параметров трехмерных стационарных и нестационарных потоков газа в сложных устройствах. Модель математического потока, используемая в пакете, основана на усредненных по Рейнольдсу уравнениях Навье-Стокса для двухкомпонентной равновесной турбулентной среды и двухпараметрической полуэмпирической модели турбулентности. Описана численная реализация программного пакета для моделирования трех сложных потоков в современных устройствах.

В этой статье мы представляем методы Surface Flow Image Velocimetry (SFIV), являюшиеся практическим расширением метода Velocimetry Image Particle Image (PIV). В частности, этот метод позволяет оценивать поведение поверхностного потока для комплексного течения. SFIVпозволяет измерять сложные поля поверхностной скорости для инженерных приложений. Целью этой работы было применение метода SFIV для определения полей скоростей и гидравлической эффективности решетчатого водоприемника. Сравнивались результаты программ Digiflow и PIVlab, способных коррелировать изображения.

Статья описывает разработку и тестирование модификации решателя для гиперзвукового реагирующего течения в среде численного моделирования OpenFOAM. Модификация создается для моделирования взаимодействия между течением и приложенным постоянным магнитным полем. Цель разработки - создать численный инструментарий для исследования концепции магнитогидродинамического управления потоком и его возможных применений. Создаваемое приложение использует математическую модель на основе уравнений Навье-Стокса, дополненных необходимыми вспомогательными моделями для описания сопряженных процессов. Тестирования решателя проводилось на задачах, демонстрирующих основные возможности созданного приложения в моделировании высокоскоростных МГД-течений различных режимов. Тестовые примеры представляют собой задачи обтекания двумерных плоско и цилиндрически симметричных тел, имеющих форму, характерную для аппаратов, для которых известны потенциальные способы применения МГД управления. Исследовалось влияние выбора модели электропроводимости на результаты численного моделирования. Сравнение результатов показало зависимость важности выбора модели электропроводимости от разреженности рассматриваемого газового потока.

В статье представлен трехмерный численный анализ структуры поля течения при прорыве плотины в масштабах лаборатории путем. Численные вычисления основывались на методе конечных объемов (Finite Volume Method, FVM), OpenFOAM. В численной модели турбулентность обрабатывается с применением методологии RANS, а метод жидких объёмов (VOF, Volume of Fluid) используется для отслеживания свободной поверхности воды. Результаты вычислений оцениваются на основе экспериментальных данных. Для валидации численной модели используются измерения глубины и давления воды. Результаты показывают, что численные вычисления удовлетворительно воспроизводят изменения этих переменных во времени.

В этой статье мы описываем метод, который представляет собой композицию метода конечных объемов (finite volume method, FVM) и метода адаптивного измельчения расчётной сетки (adaptive mesh refinement, AMR). Мы используем его для решения проблемы масляной смазки объема внутренней полости главной передачи автомобиля. Вычислительный алгоритм реализован с использованием параллельной библиотеки OpenFOAM, которая предоставляет структуры данных и подпрограммы для работы с методами конечных объемов и адаптивной сетки. Эта библиотека поддерживает параллелизм на основе OpenMPI. В статье представлены результаты численного моделирования.