Институт системного программирования им. В.П. Иванникова РАН


Текущие проекты

Asperitas

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

AstraVer Toolset: инструменты дедуктивной верификации моделей и механизмов защиты ОС

Сбои в программном обеспечении (ПО) ответственных систем, таких как, системы защиты информацией, системы управления самолётом или опасным производством, могут привести к неприятным и даже катастрофическим последствиям. По этой причине разработка такого ПО находится под контролем сертифицирующих органов, которые требуют применения лучших практик, закреплённых в международных стандартах (DO-178С, ISO/IEC 15408 и т.д.).

BinSide: статический анализатор бинарного кода

Бинарный статический анализ необходим в тех случаях, когда нет доступа к исходному коду, например, при анализе библиотек. Статический анализатор бинарного кода разрабатывается на основе фреймворка BinNavi. Для удобства пользователя анализатор интегрирован в IDA PRO. Поддерживается анализ бинарных файлов и библиотек архитектур x86, x64, ARM, PowerPC и MIPS.

Casr: инструмент формирования отчётов об ошибках

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

Constructivity. Технология индексирования, поиска и анализа больших пространственно-временных данных

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

DEDOC: Система извлечения структуры документов

Dedoc – универсальная открытая система для приведения документов к единому формату. Автоматически извлекает логическую структуру, таблицы и метаинформацию. Содержимое документов представляется в виде дерева, кодирующего заголовки и списки различного уровня вложенности. Dedoc может встраиваться как отдельный компонент в системы анализа структуры и содержимого документов.

Docmarking: система маркирования текстовых документов

Docmarking – уникальная система внедрения цифровых водяных знаков (меток) в текстовые документы. Позволяет создавать едва отличимые от оригинала цифровые и физические копии документов, однозначно идентифицирующие пользователей и их устройства.

LDV. Технология статической верификации драйверов ядра ОС Linux

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

MASIW. Программные средства поддержки проектирования комплексов бортового оборудования

Автоматизированное рабочее место архитектора и интегратора системы интегрированной модульной авионики (ИМА) предназначено для автоматизации процесса проектирования комплексов бортового оборудования (КБО).

MicroTESK: среда генерации тестовых программ для микропроцессоров

MicroTESK (Microprocessor TEsting and Specification Kit) — это среда генерации тестовых программ на языке ассемблера для функциональной верификации микропроцессоров. В качестве источника знания о конфигурации верифицируемого микропроцессора выступают формальные спецификации. Задачи генерации описываются на специальном языке, основанном на Ruby, который позволяет формулировать цели верификации в терминах тестовых ситуаций, извлеченных из формальных спецификаций. Такой подход позволяет упростить настройку среды и повысить уровень тестового покрытия. MicroTESK успешно применяется в промышленных проектах по верификации микропроцессоров ARMv8 и MIPS64.

ProtoSphere. Программная инфраструктура для проведения углубленного анализа сетевого трафика с возможностью разбора заголовков произвольного стека протоколов

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

Retrascope: инструмент обратной инженерии HDL-описаний

HDL Retrascope — это инструмент обратной инженерии (reverse engineering) и трансформаций (transformation) описаний цифровой аппаратуры, выполненных на таких HDL-языках (hardware description languages), как Verilog и VHDL. Инструмент позволяет анализировать HDL-описания, реконструировать, лежащие в их основе модели (расширенные конечные автоматы), и использовать полученные модели для генерации тестов, проверки свойств и других задач.

Talisman. Технология анализа социальных медиа-сервисов

Для анализа социальных медиа в ИСП РАН был разработан ряд оригинальных методов, которые были объединены в технологию, получившую название TALISMAN. В отличие от большинства существующих решений для социальной аналитики, технология TALISMAN изначально была нацелена на работу с большими данными, и использует наиболее перспективные открытые решения из стека технологий Big Data: Apache Spark, GraphX, MLLib и др.

Texterra. Технология автоматического построения онтологий и семантического анализа текста

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

Верификация функций безопасности и мобильности протоколов IP.

Целями этого проекта были исследование и развитие методов формального моделирования телекоммуникационных протоколов применительно к функциям безопасности и мобильности, а также разработка новых методов и программных средств автоматизации построения тестовых наборов для проверки соответствия реализаций этих функций стандартам Интернета.

Следует отметить, что проект выполнялся в тесном взаимодействии с отделом «Технологий программирования».

Верификация функций безопасности протокола нового поколения IPsec v2.

Проведенный анализ изменений, внесенных в спецификации функций безопасности уровня IP при переходе с версии IPsec v1 на версию IPsec v2, показал, что разработанные в предыдущем проекте формальные спецификации протоколов и тестовые сценарии практически невозможно использовать. Новая версия функций безопасности по существу представляет собой новый набор протоколов, который не совместим с протоколами защиты передачи данных первой версии IPsec. По этой причине, основная цель проекта заключается в полной переработке, как формальных спецификаций, так и тестовых сценариев, обеспечивающих автоматизированную верификацию функций безопасности в реализациях нового семейства протоколов. Проект выполнялся в тесном взаимодействии с отделом «Технологий программирования».

ИСП Crusher: комплекс динамического анализа программ

ИСП Crusher – программный комплекс, комбинирующий несколько методов динамического анализа. Состоит из двух инструментов: ИСП Fuzzer для проведения фаззинг-тестирования и Sydr, отвечающий за автоматическую генерацию тестов для сложных программных систем. В ближайшие 1-2 года в комплекс планируется включить ещё две технологии ИСП РАН: BinSide и Casr. ИСП Crusher позволяет построить процесс разработки в соответствии с ГОСТ Р 56939-2016 и «Методикой выявления уязвимостей и недекларированных возможностей в программном обеспечении» ФСТЭК России.

ИСП Обфускатор. Технология запутывания кода для защиты от эксплуатации уязвимостей

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

Обеспечение высокоскоростной внешней связи Института системного программирования РАН.

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

Завершенные проекты

GNU SQL Server

Начало проекта – 1996 год. Окончание проекта - 1999 год.

GNU SQL Server — это бесплатная переносимая многопользовательская реляционная система управления базами данных. Она поддерживает полную версию диалекта SQL89 и имеет некоторые расширения относительно SQL92. GNU SQL Server реализует высокий уровень изолированности транзакций и статическую и динамическую компиляцию запросов. И серверная, и клиентская стороны системы работают на Unix-подобных системах. Клиент-серверное взаимодействие основано на механизме RPC. Взаимодействие серверных процессов основано на механизмах посылки сообщений и разделяемой памяти.


1 2 3 4 5