Preview

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

Расширенный поиск

Труды Института системного программирования РАН (Труды ИСП РАН) издаются Институтом в традиционной бумажной форме с 2000 г. (с ISBN). До 2010 г. у издания отсутствовал строгий график выхода очередных выпусков, но обычно каждый год публиковались 1-2 новых "регулярных" тома, а иногда и специальные тематические тома.

С 2010 г. Труды ИСП РАН также публикуются на данном сайте в виде периодического электронного издания с одновременной публикацией небольшим тиражом в бумажной форме (ISSN 2220-6426 (Online), ISSN 2079-8156 (Print)). До начала 2014 г. ежегодно издавались два регулярных тома; по решению редакционной коллегии допускалось издание дополнительных тематических томов. С 2014 г. Труды ИСП РАН издаются в более традиционной форме: один том в год, по шесть выпусков (номеров) в каждом томе.

Это издание зарегистрировано в Федеральном агентстве по печати и массовым коммуникациям как средство массовой информации – научное электронное периодическое издание (регистрационное свидетельство Эл № ФС77-42228), а также в НТЦ "ИНФОРМРЕГИСТР" Федерального агентства по информационным технологиям как электронное научное издание (номер государственной регистрации 0421100143). Издание включено в Перечень ВАК российских рецензируемых научных журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней доктора и кандидата наук (позиция в списке 1952).

Текущий выпуск

Том 33, № 5 (2021)
Скачать выпуск PDF
7-24 74
Аннотация

В последнее время системы управления данными об изделии (PDM) широко используются в сложных междисциплинарных проектах в различных промышленных областях. PDM-системы позволяют группам проектировщиков, инженеров и менеджеров удаленно общаться в сети, обмениваться и совместно пользоваться общей информацией об изделии. Для интеграции приложений CAD/CAM/CAE с PDM-системами и обеспечения их совместимости было разработано и используется специальное семейство стандартов STEP (ISO 10303). Частью этого семейства является объектно-ориентированный язык моделирования EXPRESS, предназначенный для формального описания схем данных, а также форматы файлов для хранения и передачи данных об изделии, управляемых этими схемами. Это формат кодирования данных открытым текстом SPF и STEP-XML. В настоящее время, с развитием и широким внедрением веб-технологий, формат JSON становится все более популярным благодаря тому, что он подходит для задач обмена и хранения объектно-ориентированных данных, а также благодаря его простому и удобному для анализа синтаксису. В статье исследуется возможность применения формата JSON для представления, хранения и однозначной интерпретации данных об изделии. В предположении, что данные определяются информационными схемами на языке EXPRESS, в статье предложены и описаны формальные правила продукции объектной нотации JSON. Приводятся примеры, иллюстрирующие предложенные правила. Также обсуждаются результаты проведенных вычислительных экспериментов, которые подтверждают преимущества использования формата JSON по сравнению с SPF и STEP-XML и служат основанием для его широкого применения при интеграции программных приложений.

25-40 144
Аннотация

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

41-64 91
Аннотация

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

65-82 60
Аннотация

В статье представлены результаты разработки методов маркирования текстовых документов, представленных как растровое изображение. Важной особенностью алгоритмов является возможность обратного преобразования документа, что позволяет заменять метку на маркированном документе. Разработка относится к структурным алгоритмам маркирования на основе вертикальных сдвигов слов и изменения яркости отдельных фрагментов слов. В работе используются инструменты сегментирования для получения разметки текста в документе, БЧХ-коды для коррекции ошибок, метод максимизации правдоподобия для извлечения метки, нейронная сеть для восстановления искаженных слов. Тестирование показало практическую применимость разработанных алгоритмов маркирования при печати и сканировании текстовых документов.

83-104 76
Аннотация

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

105-116 75
Аннотация

Криптографические протоколы используются для установления безопасного соединения между “честными” агентами, которые общаются строго в соответствии с правилами протокола. Для того, чтобы убедиться, что спроектированный криптографический протокол является криптографически стойким, обычно используются различные программные инструменты. Однако, адекватная спецификация криптографического протокола обычно представляется в виде набора требований к последовательностям передаваемых сообщений, включая формат таких сообщений. Выполнение всех этих требований приводит к тому, что формальная спецификация для реального криптографического протокола становится громоздкой, в следствии чего её трудно анализировать формальными методами. Одним из таких стремительно развивающихся инструментов для формальной верификации криптографических протоколов является ProVerif. Отличительной особенностью инструмента ProVerif является то, что при больших протоколах он часто не справляется с их анализом, т.е. не может ни доказать безопасность протокола, ни опровергнуть её. В таких случаях прибегают либо к апроксимации задачи, либо к эквивалентным преобразованиям модели программы на языке ProVerif, упрощающих ProVerif-модель. В этой статье мы предлагаем способ для упрощения ProVerif-спецификаций для AKE-протоколов, использующих схему шифрования Эль-Гамаля. А именно, мы предлагаем эквивалентные преобразования, позволяющие построить ProVerif-спецификацию, которая упрощает анализ спецификации для инструмента ProVerif. Экспериментальные результаты для криптопротоколов Нидхема-Шрёдера и Yahalom показывают, что такой подход может быть перспективным для автоматической проверки реальных протоколов.

117-136 89
Аннотация

Применение формальных методов в разработке реализаций сетевых протоколов способствует повышению качества этих реализаций. Наибольший эффект даст изложение на формальном языке первичных спецификаций протоколов, публикуемых в документах RFC. В статье предлагается формальный язык описания криптографических протоколов, нацеленный на более полное, по сравнению с существующими языками первичных спецификаций, выполнение следующих требований: лаконичность, декларативность, выразительность, однозначность, исполнимость, возможность автоматического извлечения из спецификаций наборов тестов высокого качества. Основа языка – вычислитель, специально разработанный для предметной области криптографических протоколов, – т. н. C2-машина. В статье при изложении принципов построения и функционирования C2-машины используется метод последовательного уточнения модели: сначала вводится недетерминированный автомат, на котором в наиболее общем виде задается операционный контракт протокола, затем вводится машина C0, на которой демонстрируется предлагаемый подход к специфицированию недетерминизма протоколов, и далее – машина C1, на которой в формализованном виде задается семантика базовых инструкций C2-машины. Статья иллюстрирована примерами для протокола TLS.

137-154 59
Аннотация

Разработка для стековых процессорных архитектур обычно ведётся с использованием устаревших низкоуровневых языков программирования или языка ассемблер. Поэтому актуальна задача поддержки языков программирования высокого уровня для таких архитектур. В этой работе мы рассматриваем процесс разработки и реализации на базе инфраструктуры LLVM/Clang полноценной системы программирования для языка Си для стековой архитектуры TF16. Использование именно LLVM в качестве базовой системы программирования обусловлено большими возможностями адаптации дополнительных компонентов системы программирования, например, таких как дизассемблер, компоновщик и отладчик для использования с новыми архитектурами. Нами были разработаны две версии компилятора. В первой версии компилятора архитектура TF16 рассматривалась как классическая регистровая архитектура, и сгенерированный код не использовал стековые возможности. Эта версия была относительно проста в разработке и служила точкой сравнения для второй версии компилятора. Во второй версии компилятора был разработан и реализован платформо-независимый алгоритм планирования команд с учётом особенностей стековых архитектур. При сравнении двух версий версия компилятора с поддержкой стековых возможностей генерирует код, который в среднем на 35.7% быстрее по времени выполнения и на 50.8% меньше по размеру, чем код, генерируемый версией компилятора без поддержки стековых возможностей. Разработанный алгоритм позволяет реализовать в компиляторе LLVM поддержку других стековых процессорных архитектур.

155-166 105
Аннотация

Стремительное развитие Интернета-вещей (IoT) требует развития методов и средств анализа подобных устройств. Существенная часть таких устройств работает под управлением операционных систем (ОС) семейства Linux. Непосредственное применение существующих средств для анализа программного обеспечения (ПО) данного класса устройств не всегда возможно. В процессе исследования встраиваемых ОC Linux был создан инструмент ELF (Embedded Linux Fuzz), который и представлен в данной работе. В статье рассматривается анализ систем, построенных исключительно на базе ядер Linux. Среда ELF предназначена для динамического анализа устройств на основе полносистемной эмуляции в QEMU. В основу ELF были положены следующие аспекты: выполнение тестирования и анализа ПО реальных устройств в среде, максимально приближенной к их «родной» среде выполнения; интеграция с существующими средствами фаззинга; возможность проведенияраспределенного анализа.

167-180 68
Аннотация

Современные графические ускорители (GPU) позволяют существенно ускорить выполнение численных задач. Однако перенос программ на графические ускорители является непростой задачей. Иногда перенос программ на такие ускорители осуществляется путём практически полного их переписывания (например, при использовании технологии OpenCL). При этом возникает непростая задача поддержки двух независимых исходных кодов. Однако, графические ускорители CUDA, благодаря разработанной компанией NVIDIA технологии, позволяют иметь единый исходный код как для обычных процессоров (CPU), так и для CUDA. Машинный код, генерируемый при компиляции этого единого текста, зависит от того, каким компилятором он компилируется (обычным, таким, как gcc, icc и msvc, или компилятором для CUDA, nvcc). Однако, в этом едином исходном коде нужно каким-то образом указать компилятору, какие части этого кода нужно распараллеливать на общей памяти. Для CPU это обычно делается с помощью OpenMP и специальных прагм компилятору. Для CUDA распараллеливание делается совершенно по-другому. Применение разработанной авторами библиотеки функционального программирования позволяет скрыть использование того или иного механизма распараллеливания на общей памяти внутри библиотеки и сделать пользовательский исходный код полностью независимым от используемого вычислительного устройства (CPU или CUDA). В настоящей статье показывается, как это можно сделать.

181-204 88
Аннотация

Предлагается новый высокоуровневый подход к разработке приложений на GPU на основе Vulkan API. Цель работы – снижение трудоемкости разработки и отладки приложений, реализующих сложные алгоритмы на GPU при помощи Vulkan. Предлагаемый подход использует технологию генерации кода путем трансляции программы на языке C++ в оптимизированную реализацию на Vulkan, включающую автоматически генерацию шейдеров, привязывание ресурсов и использование механизмов синхронизации. Предлагаемое решение не является технологией программирования общего назначения, а специализируется на конкретных задачах, но обладает при этом расширяемостью, позволяющей адаптировать решение под новые задачи. Для одной входной программы на языке C++, мы можем сгенерировать несколько реализаций для разных случаев (опций транслятора) или разного аппаратного обеспечения. Например, вызов виртуальных функций может быть реализован либо через конструкцию switch в одном вычислительном ядре, либо через сортировку потоков и непрямой вызов в разных ядрах, либо через т. н. callable shaders в Vulkan. Таким образом, предлагаемая технология позволяет обеспечить кроссплатформенность решения за счёт генерации разных реализаций одного и того же алгоритма под разные GPU. В то же время за счёт этого она позволяет обеспечить доступ к специфической аппаратной функциональности, необходимой в приложениях компьютерной графики.

205-218 74
Аннотация

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

219-236 83
Аннотация

19 сентября 2017 года в Мексике произошло землетрясение с эпицентром в пределах штатов Пуэбла и Морелос. Оно имело интенсивность в 7,1 баллов по шкале Рихтера. Пострадало 31 090 домов, из них 1659 были полностью разрушены. Для принятия мер в условиях чрезвычайной ситуации правительство Морелоса в первые же часы сформировало межведомственный комитет для проведения первоначальной диагностики ущерба и оказания экстренной помощи. В этой статье представлены тематическое исследование и уроки, извлеченные из поддержки разработки программного обеспечения для разработки платформы на основе данных на различных этапах реагирования на чрезвычайные ситуации: перепись поврежденных домов, выявление получателей помощи, определение пакетов помощи в соответствии с оценкой ущерба, логистика и отслеживание доставки пакетов помощи, принятие решений на основе данных, а также общедоступный портал для открытых данных и прозрачности бюджета..

237-248 69
Аннотация

Исследование режимов обледенения ЛА, при которых необходимо учитывать эффект дробления капель, представляет большой интерес при расчетах обледенения летательных аппаратов, оптимизации гидрофобных и противообледенительных свойств покрытий и актуально в ряде других практических приложении. Большой практической значимостью является разработка высокопроизводительных методов расчета взаимодействия аэрозольных течений с твердым телом. Данная работа посвящена развитию модели динамики частиц, а также модели дробления переохлажденных капель аэрозольного потока при его взаимодействии с поверхностью обтекаемого тела. Развитые физико-математические модели могут быть использованы в программных комплексах численного моделирования обледенения летательных аппаратов.

249-258 69
Аннотация

В работе рассматривается возможность библиотеки ICELIB, разработанной в ИСП РАН, для моделирования процессов ледообразования на поверхности летательных аппаратов. В качестве тестового примера для сравнения точности моделирования физических процессов, возникающих при эксплуатации самолета, исследовалась поверхность стреловидного крыла с профилем GLC-305. В статье обсуждаются возможности эффективного алгоритма распараллеливания с использованием модели жидкой пленки, динамической сетки и геометрического метода биссектрис. Разработанная библиотека ICELIB это совокупность трех решателей. Первый решатель iceFoam1 предназначен для предварительной оценки зон обледенения поверхности фюзеляжа и крыла летательного аппарата. Изменением геометрической формы исследуемого тела пренебрегаем, толщина образования льда пренебрежимо мала. Данная версия решателя не имеет ограничений на количестве вычислительных ядер при распараллеливании. Вторая версия решателя iceDyMFoam2 предназначена для моделирования образования двух типов наледи гладкой (“Glaze ice”), так и рыхлой (“Rime ice”) для которой зачастую форма льда принимает сложный и причудливый вид. Учитывается влияние изменения формы тела на процесс обледенения. Ограничения связаны с особенностями построением сетки вблизи пограничного слоя обтекаемого тела. Для движения передней и задней границ пленки используются разные алгоритмы, которые оптимизированы для своих случаев. Прирост производительности ограничен и достигается при фиксированном числе ядер. Третья версия решателя iceDyMFoam3 также позволяет учитывать влияние изменения поверхности твердого тела при образовании наледи на сам процесс обледенения. Для случая образования наледи гладкого типа последняя версия решателя пока уступает по своим возможностям второй при сложных формах поверхности льда. В третьей версии пока используется несколько упрощенный и более единообразный подход для расчета движения обеих границ пленки наледи. Проведена оценка результатов расчета с данными эксперимента M. Papadakis для различных профилей и стреловидного крыла для случая “Rime ice”. Получено хорошее согласование с результатами эксперимента.

259-270 84
Аннотация

Работа посвящена численному исследованию микроклимата жилого помещения, оборудованного системой управления микроклиматом, обозначаемой термином «умный дом». Численное моделирование микроклимата помещений является актуальной задачей, поскольку эффективное проектирование систем «умный дом» предполагает необходимость прогнозирования теплофизических параметров помещения с целью обеспечения возможности своевременного изменения этих параметров. Математическое моделирование было произведено на базе уравнения сохранения массы (уравнение неразрывности), уравнения сохранения количества движения (уравнение Навье-Стокса) и уравнения энергии. Замыкание системы уравнений осуществлено на основе использования ksst модели турбулентности. Численное решение было получено методом конечных объемов с помощью программного кода Code_Saturne, относящегося к свободному программному обеспечению (СПО). Построение сетки выполнено в программном комплексе Salome, также имеющем свободную лицензию. В работе проведена проверка адекватности получаемого численного решения. Для разрешения поля скорости применена схема второго порядка (SOLU), для поля давления – схема (Multigrid), для кинетической энергии турбулентности, ее диссипации и для поля температур использованы автоматические настройки, максимальное количество итераций по каждому циклу задано равным 10000, точность решателя (Solver Precision) принята 10-8. Для получения связанного решения уравнений баланса импульса и неразрывности использован алгоритм SIMPLEC. Верификация математической модели показала, что относительное отклонение температур от значений, полученных другими авторами, составило не более 0,8-1,2%. Таким образом, представленную математическую модель можно признать адекватной. На базе выполненного математического моделирования была получена оценка теплофизических параметров микроклимата в жилом помещении, которое оборудовано системой управления «умный дом». Математическое моделирование поля температур жилого помещения показало, что при использовании систем управления микроклимата значения температур в помещениях, имеющих различное назначение, не выходят за рамки требований комфортности. Математическое моделирование скоростей движения воздуха в различных жилых помещениях не нарушают требований комфортности для таких типов помещений и принимают значения от 0,12 до 0,15 м/с.

271-282 102
Аннотация

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



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