Институт системного программирования Роcсийской академии наук


Инновации

Собственные технологии

Статический анализатор Svace. Промышленный поиск критических ошибок в безопасном цикле разработки программ

Институтом системного программирования РАН разработан инструмент статического анализа Svace, удовлетворяющий всем требованиям для анализатора промышленного качества. Инструмент Svace поддерживает языки программирования C/C++, Java, C# (C# может также предоставляться как отдельный инструмент), операционные системы Linux, Windows, а также анализ программ, собираемых на платформах Intel x86/x86-64 Linux/Windows, ARM/ARM64. Для языков C/C++ поддерживаются популярные компиляторы ОС Linux/Windows и множество компиляторов для встраиваемых систем.

SharpChecker. Инструмент статического анализа для поиска ошибок в исходном коде программ на языке С#

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

Облачная инфраструктура поддержки жизненного цикла операционной системы Tizen

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

BINSIDE. Инструмент обнаружения дефектов в программе методами статического анализа исполняемого кода

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

Anxtiety. Инструмент обнаружения дефектов в программе методами динамического анализа программ

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

Платформа для анализа программ на основе эмулятора QEMU

Платформа для анализа программ на основе эмулятора QEMU Среди эмуляторов с открытым исходным кодом QEMU занимает особое место, поскольку в практике промышленного программирования именно ему отдают предпочтение, когда требуется вести кросс-разработку (различные процессорные архитектуры целевого устройства и компьютера, на котором ведется разработка). На основе Qemu крупные IT-компании, такие как Google и Samsung, разрабатывают специализированные эмуляторы для мобильных устройств. Qemu в режиме полносистемной эмуляции поддерживает более 10 семейств процессоров, в число которых входят x86, PowerPC, Sparc, MIPS, ARM.

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

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

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

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

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

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

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

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

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

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

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

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

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

MASIW – Modular Avionics System Integrator Workplace – «рабочее пространство»/«рабочее место» системного интегратора. Набор инструментов, позволяющий: описывать модели комплекса бортового оборудования воздушного судна, производить анализ моделей на соответствие требованиям и генерировать конфигурационные данные и бинарные образы программного кода на основе моделей.

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

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

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

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

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

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

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

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

Динамическая компиляция SQL-запросов для СУБД

В рамках данного проекта был разработан метод динамической компиляции запросов с применением альтернативной модели выполнения запроса в СУБД. Также был разработан метод автоматической трансляции исходного кода PostgreSQL во внутреннее представление LLVM IR для использования в динамическом компиляторе, что позволило использовать один и тот же исходный код как для JIT-компилятора, так и для имеющегося интерпретатора.

LLV8: экспериментальный компилятор третьего уровня для JavaScript-движка V8

LLV8 – экспериментальный динамический (just-in-time) компилятор, задуманный в качестве третьего уровня компиляции и выполнения программ для популярного JavaScript-движка V8. В сравнении с имеющимися в V8 двумя уровнями, упор делается на максимальную эффективность производимого им машинного кода для пользовательской программы. Для этого используется LLVM MCJIT – набор библиотек для оптимизации программ и генерации кода на лету.

UniTESK

UniTESK - это технология тестирования программных интерфейсов (API), которая в первую очередь предназначена для модульного тестирования. Унифицированная архитектура UniTESK позволяет на ее основе реализовать инструменты для тестирования модулей на практически всех и языках программирования. В настоящее время имеются реализации UniTESK для C (CTESK), C++ (C++TESK), Java (JavaTESK и Summer), Python (PyTESK).

Поддержка переноса вычислений на акселераторы NVIDIA в реализации OpenMP 4 в компиляторе GCC

Начиная с версии 4.0, стандарт OpenMP, предоставляющий набор расширений-прагм для написания параллельных программ, содержит поддержку для переноса части вычислений из основной программы на специализированные акселераторы, которые обычно имеют отдельную оперативную память и оптимизированную для массивно-параллельных расчетов архитектуру. Для поддержки всего многообразия функциональности OpenMP на NVIDIA-акселераторах была портирована библиотека libgomp, добавлена новая модель кодогенерации для архитектуры NVPTX в GCC, и добавлены новые стратегии преобразования OpenMP SIMD-прагм для SIMT-архитектур.

C++TESK

C++TESK Testing ToolKit является инструментом, реализованном на C++, с открытым исходным кодом, предназначенным для автоматизированного тестирования программ (в основном, написанных на C/C++) и RTL (HDL) моделей цифровой аппаратуры (написанных на языках Verilog и VHDL).

CTESK

CTESK - инструмент для тестирования программного обеспечения, реализованного на языке C. CTESK реализует технологию UniTESK автоматизированного тестирования, основанного на спецификациях. Инструмент позволяет использовать формальное описание требований для генерации тестов.

KEDR

Система KEDR предназначена для динамического (runtime и post factum) анализа модулей ядра Linux, в том числе драйверов устройств, модулей файловых систем и т.д.

RaceHound

RaceHound - система для выявления состояний гонки в модулях ядра Linux.

OTK

OTK (Optimizer Testing Kit) - инструмент для тестирования программных систем, работающих с данными, имеющими сложную структуру.

SemaTESK

SemaTESK (Semantics Testing Kit) – метод автоматической генерации множеств тестов для фронт-эндов в трансляторах.

SynTESK

SynTESK (Syntax Testing Kit), инструмент для тестирования синтаксических анализаторов (парсеров) формальных языков.

JavaTESK

JavaTESK - инструмент для тестирования программного обеспечения, реализованного на языке Java. JavaTESK реализует технологии UniTESK автоматизированного тестирования, основанного на спецификациях. Инструмент позволяет использовать формальное описание требований для генерации тестов.

Requality

Система управления требованиями Requality – это инструмент для работы с требованиями, в первую очередь к программным системам. Requality автоматизирует основные процессы работы с требованиями.

PyTESK

PyTESK - инструмент для автоматизации тестирования программного обеспечения. PyTESK представляет собой реализацию на языке Python технологии UniTESK и некоторых дополнительных средств тестирования.

KAST - Декларативный язык поиска дефектов по синтаксическим деревьям

Декларативный язык, для поиска поддеревьев в синтаксическом дереве, построенном по исходному коду на языках C/C++, Java и C#.

Инструмент итеративного динамического анализа программ Avalanche

Инструмент Avalanche построен на основе среды динамической инструментации программ Valgrind и реализует итеративный автоматический анализ исполняемого кода программ с целью обнаружения критических ошибок времени выполнения.

API Gateway - платформа для эффективной балансировки нагрузки

API Gateway представляет платформу, предназначенную для эффективной балансировки нагрузки между вычислительными узлами и защиты от злоупотребления ресурсами.

Noon - инфраструктура для семантического поиска и исследования предметно-специфичной информации

Noon - набор инструментов для быстрой разработки предметно-ориентированных семантических поисковых и навигационных систем.

Sedna - прирожденная XML-СУБД

Полнофункциональная система управления базами данных, спроектированная специально для работы с XML-данными, с поддержкой языка W3C XQuery. XML — стандарт для хранения и обмена информацией в Вебе.

Технологии на основе свободного ПО

Apache Spark - платформа для обработки больших данных

Большинство организаций, сталкивающихся с необходимостью обработки больших объемов данных, используют для этих целей свободные проекты экосистемы Apache Hadoop. Основой для создания Apache Hadoop послужила разработанная компанией Google парадигма параллельного программирования MapReduce. Основные достоинства MapReduce - масштабируемость, простота использования, устойчивость к сбоям. Однако реализация MapReduce в Hadoop обладает рядом недостатков, основным из которых является низкая производительность при решении итеративных алгоритмов (например, машинного обучения). Для решения этой проблемы в университете Беркли была разработана модель для организации распределенных вычислений, основанная на понятии устойчивой к сбоям распределенной коллекции данных (RDD).

Прочие технологии

Инструмент для статической инструментации кода программ для платформы ARM

Инструмент предназначен для статической инструментации бинарного кода с целью модификации поведения программ и библиотек в формате ARM ELF.