Инновации
Инновации
AstraVer Toolset: система верификации ключевых компонентов
AstraVer Toolset – система дедуктивной верификации ключевых компонентов. Позволяет разрабатывать и верифицировать модели политик безопасности, а также проводить доказательство корректности компонентов на языке С. Необходимый инструмент достижения целей семейств доверия ADV_SPM и ADV_FSP, определённых в ГОСТ Р ИСО/МЭК 15408-3-2013.
Klever: система автоматической статической верификации Си-программ
Klever – система верификации, которая автоматически строит модели на основе исходного кода на языке программирования Си. Klever позволяет специфицировать различные требования по безопасности и надёжности, а также проверять их выполнение автоматически с заданным уровнем точности. В основе системы верификации лежат методы для покомпонентной верификации, моделирования окружения и спецификации требований, что делает возможным применение формальных методов к исходному коду размером в сотни тысяч и миллионы строк.
Masiw: поддержка проектирования ответственных систем
MASIW – набор инструментов для разработки программно-аппаратных комплексов ответственных систем в сфере авиации, медицины и др. Создан для инженеров-конструкторов комплексов бортового оборудования для авиационных судов, разрабатываемого с применением интегрированной модульной авионики (ИМА). Оперативно адаптируется под другие предметные области.
MicroTESK: генератор тестовых программ
MicroTESK – реконфигурируемая и расширяемая среда генерации тестовых программ для функциональной верификации микропроцессоров. Позволяет автоматически конструировать генераторы тестовых программ для целевых архитектур микропроцессоров на основе их формальных спецификаций. MicroTESK применим для широкого спектра архитектур (RISC, CISC, VLIW, DSP). Поддерживает онлайн-генерацию тестовых программ.
Безопасный компилятор SAFEC предотвращает появление уязвимостей в программе при выполнении агрессивных оптимизаций кода (например, в результате использования конструкций, проявляющих неопределённое поведение). Минимально ограничивает выполняемые оптимизации, что позволяет избежать значительного падения производительности по сравнению с полным отключением оптимизаций.
Svace – необходимый инструмент жизненного цикла разработки безопасного ПО, основной статический анализатор компании Samsung. Обнаруживает более 50 классов критических ошибок в исходном коде. Поддерживает языки C, C++, C#, Java, Kotlin, Go; в бета-версии – язык Python. Включён в Единый реестр российского ПО (№4047). Поставляется с web-интерфейсом просмотра предупреждений Svacer (Svace History Server).
Svacer предназначен для хранения и обработки результатов статического анализатора Svace и других анализаторов, поддерживающих формат SARIF.
TestOS: окружение для тестирования ПО
TestOS — окружение для модульного тестирования программного обеспечения на целевой аппаратуре. Позволяет проводить отработку программного обеспечения для ответственного применения в целях выполнения сертификационных и иных мероприятий на архитектурах AArch64, ARM, PowerPC, MIPS, RISC-V и x86.
Блесна: инструмент динамического анализа помеченных данных
Блесна – специализированный инструмент, предназначенный для поиска утечек в памяти чувствительных данных, таких как пользовательские пароли и ключи шифрования. Применим для анализа всего программного стека от загрузчика до прикладного ПО.
Инструмент диверсификации: комплекс защиты от эксплуатации уязвимостей
Инструмент диверсификации ¬– комплекс технологий по противодействию массовой эксплуатации уязвимостей, возникающих в результате ошибок или закладок. Если злоумышленник смог атаковать одно из устройств с одинаковым ПО, остальные останутся под защитой благодаря изменениям, внесённым в код.
Платформа для анализа программ на основе эмулятора QEMU
Платформа ИСП РАН для анализа программ построена на базе открытого эмулятора QEMU, который используется при необходимости кроссплатформенной разработки. Поддерживает механизмы обратной отладки и интроспекции, а также режим полносистемной эмуляции для отладки низкоуровневого ПО.
ИСП Crusher: комплекс динамического и статического анализа программ
ИСП Crusher – программный комплекс, комбинирующий несколько методов динамического и статического анализа, в частности, фаззинг (ИСП Fuzzer) и символьное выполнение (в качестве одного из движков может выступать Sydr). В ближайшее время в комплекс планируется включить ещё одну технологию ИСП РАН: BinSide. ИСП Crusher позволяет построить процесс разработки в соответствии с ГОСТ Р 56939-2016 и «Методикой выявления уязвимостей и недекларированных возможностей в программном обеспечении» ФСТЭК России.
BinSide: статический анализатор бинарного кода
BinSide – платформа обнаружения дефектов в программе методами статического анализа исполняемого кода. Необходима, когда нет доступа к исходному коду (например, при анализе закрытых библиотек).
Casr: инструмент формирования отчётов об ошибках
Casr – это инструмент, позволяющий автоматически формировать отчёты об аварийных завершениях, возникающих во время эксплуатации и тестирования ПО на ОС Linux. В отчётах содержатся сведения о степени критичности аварийного завершения, а также дополнительная информация, которая помогает установить его причины.
Инструмент для определения поверхности атаки Natch
Natch - это инструмент для определения поверхности атаки, основанный на полносистемном эмуляторе Qemu. Инструмент использует технологии анализа помеченных данных, интроспекции виртуальных машин и детерминированного воспроизведения. Основная функция Natch — получение поверхности атаки, то есть поиск исполняемых файлов, динамических библиотек, функций, отвечающих за обработку входных данных (файлов, сетевых пакетов) во время выполнения задачи.
Комплекс гибридного фаззинга и динамического анализа Sydr + Sydr-fuzz
Sydr — инструмент автоматической генерации тестов для сложных программных систем с целью увеличения покрытия кода и обнаружения ошибок. Cтроит математическую модель программы, позволяя фаззеру открывать новые пути выполнения, которые сложно обнаружить классическими методами генетических мутаций. Разработанные методы развивают технологию символьного выполнения, представленную в созданных ранее в ИСП РАН инструментах Avalanche и Anxiety. Sydr-fuzz — инструмент динамического анализа программ для безопасного цикла разработки ПО, который сочетает в себе возможности инструмента динамического символьного выполнения Sydr и современных фаззеров (libFuzzer и AFL++).
Protosphere: система анализа сетевого трафика
Protosphere – система глубокого анализа сетевого трафика (DPI). Может встраиваться как компонент в системы мониторинга, классификации, защиты от вторжений и утечек информации. Регистрирует несоответствия между реализацией протокола и фактическим трафиком. Позволяет быстро добавлять поддержку новых (в том числе закрытых) протоколов благодаря универсальности внутреннего представления.
Requality: инструмент управления требованиями
Requality – расширяемый инструмент для управления требованиями. Позволяет как разрабатывать требования к проектируемым системам с нуля, так и формировать каталоги требований путём разметки существующих документов, сохраняя при этом связи между требованиями и текстовыми фрагментами исходных документов. Поддерживает организацию иерархической структуры требований, трассируемость между требованиями разных уровней, возможность совместной работы над требованиями с использованием системы управления версиями GIT.
Asperitas и другие облачные решения
Asperitas – платформа организации ресурсоёмких вычислений и хранения данных в научных, образовательных и коммерческих целях. Кроме одноимённой облачной среды в состав платформы входят также Michman − оркестратор платформенных распределенных сервисов и Clouni − мультиоблачный оркестратор инфраструктурных ресурсов, основанный на стандарте TOSCA. Кроме того, в число облачных решений ИСП РАН входит Fanlight − платформа для объединения исследований в web-лаборатории и Cotea − системное ПО, предназначенное для программного контроля исполнения сценариев Ansible.
Talisman – это комплекс взаимосвязанных программных инструментов для автоматизации типовых задач обработки данных, включая их сбор, интеграцию, анализ, хранение и визуализацию. Обеспечивает быструю разработку специализированных многопользовательских интеллектуальных аналитических систем, объединяющих информацию из внутренних баз данных и открытых источников сети Интернет (в том числе из социальных сетей).
Lingvodoc: виртуальная лаборатория для документации исчезающих языков
Lingvodoc – система для совместной многопользовательской документации исчезающих языков, создания многослойных словарей и научной работы с полученными звуковыми и текстовыми данными. Совместный проект с Институтом языкознания РАН и Томским государственным университетом. Разрабатывается с 2012 года.
Texterra: базовый семантический анализатор
Texterra — масштабируемая платформа для извлечения семантики из текста. Базовый комплекс технологий для создания многофункциональных прикладных приложений. Анализирует тексты с помощью выделения концептов. Включена в Единый реестр российского ПО (№4048).
Dedoc: система извлечения содержимого и структуры текстовых документов
Dedoc – универсальная открытая система для приведения документов к единому формату. Автоматически извлекает логическую структуру, таблицы и метаинформацию. Содержимое документов представляется в виде дерева, кодирующего заголовки и списки различного уровня вложенности. Dedoc может встраиваться как отдельный компонент в системы анализа структуры и содержимого документов.
DocMarking: противодействие анонимности при утечках документов
DocMarking – уникальная система внедрения цифровых водяных знаков (меток) в текстовые документы. Позволяет создавать едва отличимые от оригинала цифровые и физические копии документов, однозначно идентифицирующие пользователей и их устройства.
SciNoon: система исследовательского поиска
SciNoon - система совместного исследовательского поиска научных статей. Позволяет группе исследователей быстро погружаться в новую предметную область и находить ответы на свои вопросы, а затем отслеживать новые публикации по изучаемой тематике.
EcgHub: интеллектуальный анализ цифровой ЭКГ
EcgHub – система разметки 12-канальных ЭКГ и нейросетевые модели классификации патологий. Система позволяет предсказывать наличие или отсутствие ряда патологий, а также выполнять и верифицировать синдромальную разметку ЭКГ на основе специализированного опросника, обеспечивая подготовку качественного набора данных для дальнейшего развития нейросетевых моделей.
Constructivity 4D – технология для создания перспективных программных систем и сервисов, оперирующих динамическими сценами и большими массивами пространственно-временных данных. Способна проводить визуальный анализ миллионов объектов с различным геометрическим представлением и индивидуальным динамическим поведением. Внедрена в систему Synchro (Bentley Systems), предназначенную для 4D-моделирования крупных строительных объектов.
DigiTEF: программный комплекс для проведения компьютерного моделирования
DigiTEF – программный комплекс, предназначенный для разработки средств цифрового моделирования, для проведения компьютерного моделирования и инженерного анализа прикладных и научно-технических задач промышленности. Позволяет решать задачи газовой динамики, аэродинамики, гидродинамики, акустики, а также проводить сопряжённые расчеты. Включён в Единый реестр российского ПО (№5377).
Retrascope: инструмент статического анализа hdl-описаний
Retrascope – инструмент функциональной верификации модулей цифровой аппаратуры. Retrascope предоставляет автоматизированные средства анализа кода, извлечения формальных моделей и генерации функциональных тестов. В качестве входных данных инструмент принимает описания модулей цифровой аппаратуры на синтезируемых подмножествах языков Verilog и VHDL, а также спецификации поведения.
Среда анализа бинарного кода «ТРАЛ»
Уникальный промышленный инструмент для анализа свойств бинарного кода. Позволяет работать с кодом различных целевых процессорных архитектур. Не требует наличия отладочной информации и исходных текстов. Применим для анализа всего программного стека от загрузчика до прикладного ПО. Включена в Единый реестр российского ПО (№5323).
Доверенные фреймворки машинного обучения
Фреймворк машинного обучения – это среда с набором инструментов для обеспечения быстрой разработки соответствующих программных продуктов. Наиболее популярными открытыми фреймворками считаются TensorFlow и PyTorch. Работа по созданию их доверенных версий ведётся в Исследовательском центре доверенного искусственного интеллекта (ИЦДИИ) ИСП РАН. Цель проекта − найти и устранить ошибки, которые могут вызвать некорректную работу фреймворков, а значит, привести к некорректной работе приложений.
VALIDBIM: сервис верификации информационных моделей в архитектуре и строительстве
VALIDBIM – сервис верификации информационных моделей в архитектуре и строительстве, представленных в формате IFC SPF и обеспечивающих функциональную совместимость программных приложений на уровне BIM Level3. Данный уровень технологической зрелости в модели Бью-Ричардса предполагает интероперабельность ТИМ -приложений и возможность их интеграции в составе перспективных мультидисциплинарных программных комплексов для проектной деятельности в архитектуре, инженерии, строительстве и эксплуатации зданий и сооружений.
ML IDS: сетевая система обнаружения вторжений с применением машинного обучения
ML IDS − сетевая система обнаружения вторжений (СОВ), базирующаяся на результатах передовых научных исследований в области применения машинного обучения для обнаружения компьютерных атак. За счёт обобщающей способности используемых моделей машинного обучения система позволяет обнаруживать ранее неизвестные атаки (атаки нулевого дня, zero day).