• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Найдены 124 публикации
Сортировка:
по названию
по году
Статья
Петренко А. К., Кулямин В. В., Хорошилов А. В. Труды Института системного программирования РАН. 2015. Т. 27. № 5. С. 175-190.

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

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

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

Добавлено: 12 декабря 2018
Статья
Аничкин А., Семенов В. А. Труды Института системного программирования РАН. 2017. Т. 29. № 3. С. 247-296.

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

Добавлено: 12 декабря 2018
Статья
С.Д. Кузнецов Труды Института системного программирования РАН. 2015. Т. 27. № 1. С. 173-192.

В 2005 г. я написал статью, в которой приводил наиболее существенные черты стандартов ODMG 3.0 (объектная модель ODMG) и SQL:2003 (модель данных SQL) и убедительно (как мне тогда казалось) доказывал, что сходство между объектной моделью и объектными расширениями SQL является чисто внешним, что за близкими на вид синтаксическими конструкциями скрываются глубинные различия модельного уровня. Примерами таких различий являются фоннеймановское разыменование объектных идентификаторов в модели ODMG по сравнению с ассоциативным разыменованием ссылочных значений в модели SQL, раздельное и независимое хранение объектов одного объектного типа в модели ODMG по сравнению с хранением всех строк типизированной таблицы в одной этой таблице в модели SQL, хранение объектных идентификаторов в экстенте в модели ODMG и хранение в аналоге экстента самих объектов в модели SQL и т.д. С тех пор прошло много лет, за которые я понял многие вещи, неправильно или недостаточно правильно понимавшиеся мной тогда, и постепенно пришел к выводам, что: 1.    различия, которые мне казались глубинными, таковыми не являются, да и вообще не являются различиями уровня модели; 2.    объектные расширения SQL обеспечивают не меньшие (а скорее большие) возможности, чем объектная модель ODMG; 3.    при разумном (с позиций сообщества баз данных) использовании СУБД, основанной на модели ODMG, будут создаваться базы данных и средства манипулирования ими, близкие к тем, которые предписывает модель данных SQL.

Добавлено: 23 января 2018
Статья
Дворянский Л. В. Труды Института системного программирования РАН. 2011. № 20. С. 71-94.

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

Добавлено: 20 сентября 2012
Статья
Кудряшов Е. А., Мельник Д. М., Монаков А. В. Труды Института системного программирования РАН. 2016. Т. 28. № 1. С. 63-80.

В статье рассматривается подход к оптимизации вызовов внешних функций в позиционно-независимом коде, основанный на выдаче вызовов непосредственно через глобальную таблицу смещений (GOT), минуя таблицу компоновки процедур (PLT). Стандартные механизмы кодогенерации на операционной системе Linux предполагают создание PLT не только для основного модуля (который является позиционно-зависимым и полагается на механизм PLT для вызовов внешних процедур), но и для динамических библиотек, где PLT используется также для организации ленивого связывания; однако, использование PLT требует дополнительной инструкции перехода, может иметь низкую локальность по кешу и на некоторых архитектурах накладывает дополнительные ограничения на работу компилятора в месте вызова. Реализация вызовов внешних функций в виде косвенных переходов на адреса, загруженные непосредственно из GOT в месте вызова, позволяет избежать недостатков вызовов через PLT, ценой отказа от возможности ленивого связывания и, возможно, увеличением размера кода. Была исследована реализация этой оптимизации для архитектур x86 и ARM в компиляторе GCC. Было обнаружено, что на архитектуре ARM отсутствуют типы релокаций, которые позволили бы генерировать оптимальный код для загрузок из GOT. Для решения этой проблемы в GCC и Binutils (в ассемблере и компоновщике) были реализованы недостающие типы релокаций, позволяющие построить адрес позиции в GOT относительно счетчика команд, используя инструкции movt, movw. Проведенное тестирование свидетельствует, что предложенная оптимизация позволяет получить увеличение производительности, несмотря на увеличение размеров динамических библиотек.

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

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

Добавлено: 22 марта 2017
Статья
Емеленко А., Маллачиев К., Пакулин Н. В. Труды Института системного программирования РАН. 2017. Т. 29. № 4. С. 295-302.

В этой статье мы расскажем о проекте по разработке отладчика для мультиплатформенной операционной системы реального времени JetOS, созданной для гражданских авиационных систем. Она предназначена для работы в рамках архитектуры Интегрированной Модульной Авионики (ИМА) и реализует ARINC 653 спецификацию API. Эта операционная система разрабатывается в институте системного программирования РАН, и важным шагом в ее создании является разработка инструмента для отладки пользовательских приложений. В этой статье будут рассмотрены проблемы особенностей отладчика для операционной системы реального времени и показаны методы, которыми достигается его мультиплатформенность, а также легкая переносимость на новую платформу. Более того, были рассмотрены другие отладчики для встраиваемых операционных систем, такие как CodeWarrior, отладчики для WxWorks и L4Ka::Pistachio, а также был изучен их функционал.  В заключение мы представим наш отладчик, который может работать как в эмуляторе QEMU, используемом для эмуляции окружения для  JetOS, так и на целевой машине на всех поддерживаемых платформах. Представленный отладчик является удаленным и построен с использованием структуры GDB, но содержит ряд расширений, специфичных для отладки встроенных приложений. Сама структура отладчика была разделена на архитектурно зависимые и независимые части, что помогает облегчить перенос отладчика на новую платформу. В то же время наш отладчик удовлетворяет большинству требований, налагаемых к отладчику операционной системы реального времени, а также уже используется разработчиками приложений для Jet OS.

Добавлено: 12 февраля 2018
Статья
С.Д, Кузнецов, Мендкович Н. А. Труды Института системного программирования РАН. 2013. Т. 25. С. 113-130.

Эта статья описывает усовершенствованные алгоритмы лексической оптимизации запросов. Алгоритмы обнаруживают и удаляют избыточные условия из ограничения запроса, чтобы упростить его. Cтатья также представляет результаты применения этих оптимизационных техник и их влияние на скорость обработки запроса.

Добавлено: 30 января 2018
Статья
С.Д. Кузнецов, Мендкович Н. А. Труды Института системного программирования РАН. 2013. Т. 25. С. 113-130.

Эта статья описывает усовершенствованные алгоритмы лексической оптимизации запросов. Алгоритмы обнаруживают и удаляют избыточные условия из ограничения запроса, чтобы упростить его. Cтатья также представляет результаты применения этих оптимизационных техник и их влияние на скорость обработки запроса.

Добавлено: 6 ноября 2017
Статья
Дробышевский М., Коршунов А., Turdakov D. Y. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 6. P. 153-170.

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

Добавлено: 28 августа 2017
Статья
Трофимович Ю., Козлов И., Турдаков Д. Ю. Труды Института системного программирования РАН. 2016. Т. 28. № 6. С. 185-196.

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

Добавлено: 28 августа 2017
Статья
Гетьман А. И., Маркин Ю. В., Обыденков Д. О. и др. Труды Института системного программирования РАН. 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