Компиляторные технологии


Инновации

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

Статический анализатор 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 позволяет автоматизированным образом подготовить исходный код драйверов к верификации на основе спецификаций модели ядра и проверить его на соответствие спецификациям правил корректности с помощью инструментов статической верификации.

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

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

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

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

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

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

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

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

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

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