• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Найдены 134 публикации
Сортировка:
по названию
по году
Статья
Гетьман А. И., Маркин Ю. В., Обыденков Д. О. и др. Труды Института системного программирования РАН. 2016. Т. 28. № 6. С. 103-110.

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

Добавлено: 5 сентября 2019
Статья
Подымов В. В., Захаров В. А. Труды Института системного программирования РАН. 2014. Т. 26. № 3. С. 145-166.

В статье исследована задача проверки эквивалентности последовательных программ, некоторые операторы которых обладают свойствами перестановочности и подавления. Два оператора считаются перестановочными, если результат их последовательного выполнения не зависит от порядка, в котором эти операторы выполняются. Считается, что оператор b подавляет оператор a, если последовательное выполнение операторов a и b дает такой же результат, что и выполнение одного лишь оператора b. Разрешимость проблемы эквивалентности в исследуемой модели программ была установлена в 1971 г. А.А. Летичевским. Однако с тех пор вопрос о сложности проверки эквивалентности таких программ оставался открытым. Основной результат статьи – алгоритм, осуществляющий проверку эквивалентности программ с перестановочными и подавляемыми операторами за время, полиномиально зависящее от размеров анализируемых программ.

Добавлено: 29 сентября 2015
Статья
Захаров В. А., Новикова Т. А. Труды Института системного программирования РАН. 2012. Т. 22. С. 435-455.
Логико-термальная эквивалентность программ – это одно из наиболее слабых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности и обладающих разрешающим алгоритмом. В данной статье предложена новая модификация алгоритма проверки логико-термальной эквивалентности программ, основанная на операции вычисления точной нижней грани в решетке конечных подстановок. Показано, что трудоемкость предложенного алгоритма оценивается величиной O(n6) , где n - размер анализируемых программ. Полученная верхняя оценка сложности задачи проверки логико-термальной эквивалентности программ существенно меньше ранее известных полиномиальных оценок сложности указанной задачи.
Добавлено: 30 сентября 2015
Статья
Федотов А., Каушан В., Гайсарян С. С. и др. Труды Института системного программирования РАН. 2017. Т. 29. № 6. С. 151-162.

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

Добавлено: 12 февраля 2018
Статья
Гуськова М. С., Бараш Л. Ю., Щур Л. Н. Труды Института системного программирования РАН. 2018. Т. 30. № 1. С. 115-126.

В работе описывается применение наборов SIMD инструкций (Single Instruction Multiple Data) для параллелизации алгоритма генерации псевдослучайных чисел. Дан обзор расширений MMX, SSE, AVX2, AVX512, реализующих принцип SIMD. Приведен пример реализации генератора LFSR113 с использованием расширения AVX512. Приведен сравнительный анализ скоростей работы различных реализаций алгоритма.

Добавлено: 26 марта 2018
Статья
Захаров В. А., Новикова Т. А. Труды Института системного программирования РАН. 2011. Т. 21. С. 141-166.
Для решения многих задач системного программирования, к числу которых относятся задачи реорганизации программ, деобфускации программ, выявления уязвимостей в программном коде и др., желательно иметь инструментальное средство, позволяющее обнаруживать фрагменты программ, имеющие сходное поведение. Современные средства обнаружения программных клонов позволяют выявлять лишь фрагменты программ, имеющие сходное синтаксическое устройство, поскольку более глубокий семантический анализ программ сталкивается с алгоритмической неразрешимостью проблемы функциональной эквивалентности программ. Для того чтобы избежать алгоритмически трудных задач проверки функциональной эквивалентности, авторы настоящей статьи предлагают воспользоваться более сильным разрешимым отношением эквивалентности программ – логико-термальной эквивалентностью, – введенной в 1972 г. В.Э. Иткиным. В данной статье разработан новый алгоритм проверки логико-термальной эквивалентности программ, основанный на операции вычисления точной нижней грани в решетке конечных подстановок. На основе этого алгоритма авторам статьи удалось также решить задачу логико-термальной унификации программ, которая состоит в построении для двух заданных фрагментов программного кода такой процедуры, которая представляет собой наиболее общую специализацию этих двух фрагментов.
Добавлено: 30 сентября 2015
Статья
Захаров В. А., Подымов В. В. Труды Института системного программирования РАН. 2015. Т. 27. № 4.

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

Добавлено: 13 октября 2015
Статья
С.С.Гайсарян, Нурмухаметов А., Курмангалеев Ш. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 3. С. 113-126.

Уязвимости программного обеспечения представляют серьезную угрозу безопасности информационной системы. Любое программное обеспечение, написанное на языках C/C++, потенциально содержит в себе значительное количество уязвимостей, используя которые злоумышленник может с помощью специально подготовленных эксплойтов захватить контроль над системой. Для противодействия эксплуатации таких уязвимостей в данной работе предлагается использовать компиляторные преобразования: перестановка местами функций в модуле, добавление локальных переменных на стек функции, перемешивание локальных переменных на стеке. С помощью этих преобразований предлагается генерировать диверсифицированную популяцию исполняемых файлов компилируемого приложения. Такой подход, например, усложняет планирование ROP-атак на всю популяцию. Злоумышленник, получив в свое распоряжение один исполняемый файл, может сделать ROP-эксплойт, работающий только для этой версии приложения. Остальные исполняемые файлы популяции останутся устойчивыми к данной атаке.

Добавлено: 13 сентября 2016
Статья
С.С.Гайсарян, Курмангалеев Ш., Долгорукова К. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 315-326.

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

Добавлено: 13 сентября 2016
Статья
Массобрио Р., Несмачнов С., Черных А. и др. Труды Института системного программирования РАН. 2016. Т. 28. № 6. С. 121-140.

В этой статье рассматривается вопрос применения анализа данных большого объема с использованием облачных вычислений для решения задач анализа дорожного траффика в контексте «умных» городов. Предложенное решение базируется на модели параллельных вычислений MapReduce, реализованной на  платформе Hadoop. Анализируются два экспериментальных случая: оценка качества общественного транспорта на основе анализа истории местоположения автобусов, и оценка мобильности пассажиров при помощи анализа истории покупок билетов с транспортных карт. Оба эксперимента используют реальную базу данных системы общественного транспорта Монтевидео в Уругвае. Результаты эксперимента показали, что рассмотренная модель действительно позволяет эффективно обрабатывать большие объемы данных.

Добавлено: 28 августа 2017
Статья
Семакин А. Н. Труды Института системного программирования РАН. 2017. Т. 29. № 5. С. 311-328.

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

Добавлено: 25 декабря 2017
Статья
Кузнецов С. Д., Турдаков Д. Ю., Борисенко О. Д. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 4. С. 45-54.

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

Добавлено: 26 ноября 2017
Статья
С.Д. Кузнецов, Посконин А. В. Труды Института системного программирования РАН. 2013. Т. 24. С. 327-258.

В современном мире всё острее встает проблема работы с огромными объемами данных и большими нагрузками. Крупные Web-приложения, социальные сети, различные научные исследования, бизнес-аналитика, а также множество других областей, так или иначе, сталкиваются с проблемами управления и анализа данных большого объема («big data»). Кроме анализа уже накопленного объема данных, возникают задачи манипулирования данными под большой нагрузкой, характерные, например, для Web-приложений. В таких проектах большое количество пользователей одновременно читают и пишут информацию, что требует от системы управления данными не только большой пропускной способности и низких задержек, но и масштабируемости, надежности и определённых гарантий согласованности данных. Несмотря на большую популярность, опыт применения и универсальность, традиционные SQL-ориентированные СУБД зачастую не могут удовлетворить требования современных приложений, что привело к появлению большого числа специализированных распределённых систем, способных лучше справляться с возникающими задачами. В данной статье предлагается обзор некоторых современных решений, обеспечивающих масштабируемость при работе с большими объемами данных под высокими нагрузками.

Добавлено: 30 января 2018
Статья
Иванников В. П., Курмангалеев Ш. Ф., Белеванцев А. А. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 327-342.

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

Добавлено: 22 марта 2017
Статья
S. Kuznetsov, Борисенко О. Д., Алексиянц А. В. et al. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 5. P. 35-48.
Добавлено: 23 января 2018
Статья
Твардовский А. С., Евтушенко Н. В. Труды Института системного программирования РАН. 2019. Т. 31. № 4. С. 175-188.

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

Добавлено: 13 марта 2020
Статья
Захаров В. А., Варновский Н. П., Кузюрин Н. Н. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 3. С. 167-198.
Обфускацией программ называется такое эквивалентное преобразование программ, которое придает программе форму, затрудняющую понимание алгоритмов и структур данных, реализуемых программой, и препятствующую извлечению из текста программы определенной секретной информации, содержащейся в ней. Поскольку обфускация программ может найти широкое применение при решении многих задач криптографии и компьютерной безопасности, задаче оценки стойкости обфускации придается очень большое значение, начиная с самых первых работ в этой области. В этой статье приводится обзор различных определений стойкости обфускации программ и результатов, устанавливающих возможность или невозможность построения стойкой обфускации программ в тех или иных криптографических предположениях
Добавлено: 30 сентября 2015
Статья
Борисенко О. Д., Пастухов Р. К., С.Д. Кузнецов Труды Института системного программирования РАН. 2016. Т. 28. № 6. С. 111-120.

Apache Spark является одним из наиболее производительных распределенных фреймворков для обработки больших данных в парадигме Map-Reduce. С распространением облачных технологий и предоставления ресурсов по запросу все более актуальной становится задача построения виртуальных вычислительных кластеров для конкретной задачи. В работе представлен краткий обзор разработанного решения для создания виртуальных кластеров Apache Spark в облачной среде Openstack и подведение итогов исследования о способах создания виртуальных кластеров Apache Spark в открытых облачных средах. Решение построено с использованием системы оркестрации Ansible. В работе будет проведено качественное сравнение разработанных в ИСП РАН подходов к решению задачи.

Добавлено: 25 января 2018
Статья
Татарников А. Д., Камкин А. С., Чупилко М. М. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 149-200.

Обеспечение корректности микропроцессоров и другой микроэлектронной аппаратуры является фундаментальной проблемой, для решения которой применяют разнообразные средства функциональной верификации. В отличие от программ, ошибки в которых исправляются сравнительно просто, дефекты в интегральных схемах (конструктивные и производственные) не могут быть устранены. Несмотря на то, что постоянно совершенствуются системы автоматизированного проектирования (САПР), инструменты генерации тестов и методы анализа схем, верификация остается самым узким местом процесса разработки (на нее тратится около 70% всех ресурсов проектирования). В работе делается краткий обзор средств верификации микропроцессоров, рассматриваются проблемы, возникающие в промышленной практике, анализируются возможные пути их решения. Значительная часть статьи посвящена исследованиям по верификации аппаратуры, проводимым в ИСП РАН: подводятся итоги выполненных работ, описываются текущие разработки, формулируются направления дальнейших исследований.

Добавлено: 11 декабря 2017
Статья
Иванников В. П., Белеванцев А. А., Бородин А. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 231-250.

В работе описывается разрабатываемый в ИСП РАН инструмент автоматического статического анализа Svace. Инструмент позволяет находить ошибки и потенциальные уязвимости в исходном коде программ на языках Си/Си++. Особенностью инструмента являются простота использования, широкий набор поддерживаемых типов предупреждений, масштабируемость до программ в миллионы строк кода и приемлемое качество анализа (30-80% истинных предупреждений).

Добавлено: 22 марта 2017
Статья
Ильин Д., Фокина Н., Семенов В. А. Труды Института системного программирования РАН. 2018. Т. 30. № 3. С. 271-284.

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

Добавлено: 12 декабря 2018