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

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

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

При полносистемном анализе бинарного кода зачастую применяется динамический бинарный анализ, при котором предоставляемый аналитику объем данных представлен потоком выполняемых инструкций и содержимым оперативной памяти и регистров. Для обработки таких данных требуется глубокое понимание особенностей исследуемой системы, при этом трудозатраты на выполнение анализа и требования к технической осведомленности пользователя становятся очень велики. Для упрощения процесса анализа необходимо привести входные данные к более дружелюбному для пользователя виду, т.е. предоставить высокоуровневую информацию об исследуемом программном обеспечении. Такой высокоуровневой информацией является информация о потоке выполнения программы. Для восстановления потока выполнения программы важно иметь представление о вызываемых ею процедурах. Получить такое представление можно с помощью стека вызова функций для конкретного потока. Построение стека вызовов без информации о выполняемых потоках невозможно, т.к. каждому потоку однозначно соответствует один стек и vice versa. Помимо этого, само наличие информации о потоках повышает уровень знаний о системе, позволяет более тонко профилировать объект исследования и проводить узконаправленный анализ, применяя принципы выборочного инструментирования. Виртуальная машина не предоставляет напрямую такой информации, и строить предположения о работе исследуемой системы приходится, основываясь на доступных низкоуровневых данных (поток выполняемых виртуальным процессором инструкций и оперативная память виртуальной машины). Таким образом, существует необходимость в разработке метода для автоматической идентификации потоков в исследуемой системе, опирающегося на имеющемся объеме данных. В данной работе рассматриваются существующие подходы к реализации получения высокоуровневой информации при полносистемном анализе и предлагается метод для восстановления данных о потоках в условиях полносистемной эмуляции с низкой степенью ОС-зависимости. Также приводятся примеры практического использования данного метода при реализации инструментов анализа, а именно: восстановление стека вызовов, обнаружение подозрительных операций возврата и обнаружение обращений к освобожденной памяти в стеке. Приведенное в статье тестирование показывает, что накладываемое описанными алгоритмами замедление позволяет проводить работу с исследуемой системой, а сравнение с эталонными данными подтверждает корректность получаемых алгоритмами результатов.

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

В данной статье рассматривается задача автоматического исправления дефектов кода на языках C/C++, найденных статическим анализатором на больших программных проектах. Описан опыт реализации соответствующего инструмента для статического анализатора Svace и принципы исправления дефектов разных типов. Особое внимание уделено исправлению разыменования нулевого указателя как наиболее важного и сложного из поддержанных в инструменте типов дефектов; приведена статистика работы инструмента по исправлению дефектов этого типа. Исследуются общие ограничения и специфика поставленной задачи, объясняется невозможность использования для её решения существующих систем автоматического исправления дефектов. В заключение кратко излагаются соображения по дальнейшему развитию реализованного продукта.

Данная статья посвящена обзору наиболее популярных запахов кода, одного из компонентов технического долга, а также методов и инструментов их поиска. В статье проводится сравнительный анализ результатов работы таких инструментов как DesigniteJava, PMD, SonarQube. Инструменты были применены к набору проектов с открытым исходным кодом для вычисления точности обнаружения и согласованности выбранных инструментов. Показаны сильные и слабые стороны подхода, основанного на подсчете метрик кода и отсечения по пороговым значениям, который используется в инструментах. Ручная разметка результатов работы показала низкий процент истинных срабатываний (10% для божественного класса и 20% для сложного метода). Проведён обзор работ, предлагающих усовершенствование стандартного подхода и альтернативные, не использующие метрики. Для оценки потенциала альтернативных подходов разработан прототип обнаружения длинных методов с системой фильтрации ложноположительных срабатываний, использующие методы машинного обучения.

В данной работе сделан обзор открытых инструментов логического синтеза, трассировки и размещения элементов моделей цифровой аппаратуры, анализа временных характеристик и синтеза топологических схем. Среди инструментов были выбраны системы проектирования qFlow, OpenLANE, Coriolis и SymbiFlow, поддерживающие полные маршруты: от RTL-модели до двоичных образов для ПЛИС или исходных данных для полупроводниковых фабрик. Для экспериментальной оценки инструментов была взята модель микропроцессора с архитектурой RISC-V под названием PicoRV32. Результаты испытаний показали, что открытые инструменты пригодны для создания топологических схем реалистичных примеров. Однако коммерческие инструменты позволяют создавать более эффективные с точки зрения производительности топологические модели.

Функциональным онлайн-тестированием называется верификация опытных образцов микропроцессоров или их ПЛИС-прототипов, т.е. пост-производственная верификация (post-silicon verification). Такой вид тестирования отличается как от производственного тестирования, нацеленного на проверку работоспособности произведенных микросхем (отсутствие дефектов производства, допустимость значений физических характеристик), так и от функциональной верификации моделей микропроцессоров, проводимой в симуляторе (где можно наблюдать за внутренними сигналами микропроцессора и контролировать процесс исполнения). Пост-производственная верификация позволяет на высокой скорости испытывать огромные массивы тестов и обнаруживать ошибки, пропущенные при функциональной верификации на до-производственном этапе. Тесты для микропроцессоров обычно имеют вид программ; соответственно, основными задачами онлайн-тестирования микропроцессоров являются высокопроизводительная генерация тестовых программ в заданной системе команд и создание тестового окружения, отвечающего за запуск программ, оценку корректности их исполнения микропроцессором, диагностику ошибок и взаимодействие с внешним миром. В данной статье рассматриваются проблемы, возникающие при разработке систем онлайн-тестирования (онлайн-генераторов тестовых программ), делается обзор существующих решений в этой области и на их основе предлагается перспективный подход к организации онлайн-тестирования.

Управление мастер-данными (Master Data Management, MDM) является важной дисциплиной управления данными в современных компаниях. В настоящее время индустриальные решения в этой сфере активно развиваются, о чем свидетельствует, в частности, ежегодные обзоры консалтинговой компании Gartner. Однако проблема эффективной настройки стандартных MDM-продуктов под индивидуальные нужды организаций стоит очень остро. Естественным решением этой проблемы является компонентная архитектура стандартного продукта, а также его открытость.  Однако, фактически, единственным индустриальным открытым компонентным MDM-продуктом является на сегодняшний день платформа Unidata, разработанная в российской компании ООО «Юнидата». В данной работе представлена архитектура этой платформы, а также проведён обзор имеющихся на рынке открытых компонентных разработок в области MDM.

В статье представлена система расследования утечек конфиденциальных текстовых документов, где в качестве каналов утечек рассматриваются изображения, полученные путем сканирования/фотографирования напечатанных документов, а также фотографии документов на экране монитора. Таким образом, система нацелена на защиту каналов, не защищаемых традиционными DLP-решениями. В качестве механизма защиты документов выбрано внедрение цифрового водяного знака (ЦВЗ), предполагающее изменение визуального представления документа. В случае анонимной утечки конфиденциального документа ЦВЗ позволит установить сотрудника, допустившего утечку – намеренно или в результате нарушения протокола безопасности. В статье описана архитектура системы, состоящая из клиентской и серверной частей. На рабочие станции сотрудников устанавливаются компоненты, обеспечивающие внедрение ЦВЗ в документы, отправляемые на печать или выводимые на экран монитора. Факты маркирования документов регистрируются и отправляются на удаленный сервер, использующий данную информацию при расследовании утечек аналитиком службы безопасности. Разработаны алгоритмы маркирования для встраивания ЦВЗ в текстовые документы, выводимые на печать и экран монитора. При маркировании документа на экране монитора ЦВЗ встраивается в межстрочные интервалы: цифровая метка кодируется последовательностью затемненных и осветленных областей. Для встраивания ЦВЗ в печатаемые документы разработано три алгоритма маркирования: на основе горизонтального и вертикального смещения слов, а также посредством изменения яркости отдельных фрагментов слов. Разработана методика тестирования алгоритмов маркирования в условиях, приближенным к условиям эксплуатации, оценена область применимости алгоритмов. Проведен анализ вероятных атак на систему, и сформулирована модель нарушителя.

Искусственные нейронные сети широко распространены в современном мире. Для их исполнения используются различные устройства: от микропроцессоров до ПЛИС и заказных СБИС. Важной проблемой при этом является ускорение исполнения нейронных сетей. В этой области на данный момент существует множество открытых инструментов. В данной статье содержится обзор нескольких открытых инструментов для исполнения, ускорения нейронных сетей и синтеза аппаратуры по ним. Некоторые из рассмотренных инструментов были выбраны для апробации на ПЛИС. Для этого было разработано пять тестовых моделей нейронных сетей. Процессор Intel, графический процессор NVIDIA и ПЛИС Cyclone V использовались для проведения экспериментов. Результаты показали, что инструменты TVM/VTA и LeFlow оказались способны довести тестовые модели до исполнения на ПЛИС. Однако результаты исполнения показали, что в большинстве случаев ПЛИС проигрывает в быстродействии другим платформам.

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

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

Задача извлечения именованных сущностей, соответствующих лекарствам, заболеваниям и лекарственным реакциям, из текстов различных предметных областей и языков является основополагающим компонентом многих приложений, основанных на извлечении информации из текстов. В данной работе производится оценка эффективности многоязыковых моделей, основанных на архитектуре BERT, для решения задач распознавания именованных сущностей медицинской направленности и многоклассовой классификации предложений. В ходе экспериментов было исследовано влияние переноса знаний между двумя англоязычными корпусами и одним русскоязычным корпусом размеченных отзывов о лекарственных препаратах. Рассмотренные корпуса содержат разметку на уровне предложений, обозначающую присутствие или отсутствие в них медицинских сущностей некоторого типа. Предложения, принадлежащие некоторому классу, содержат дополнительную разметку на уровне сущностей, позволяющую установить принадлежность отдельных выражений к сущностям некоторого типа, таким, как название, показание к применению или эффект лекарства. Результаты экспериментов показали, что для русского языка наибольшая эффективность переноса знаний при предобучении моделей BERT на коллекции, состоящей из 5 миллионов неразмеченных русскоязычных и англоязычных пользовательских отзывах, наблюдается при распознавании побочных эффектов лекарств. Для задачи распознавания именованных сущностей наилучшее значение макро F-меры, равное 74,85%, показала модель RuDR-BERT, предобученная на русскоязычных текстах медицинской предметной области. Для задачи классификации наилучшее значение макро F-меры, равное 70%, показала модель EnRuDR-BERT, предобученная на русскоязычных и англоязычных текстах медицинской направленности. Превосходство данной модели над моделью BERT, предобученной на текстах общей предметной области, составляет 8,64% макро F-меры.

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

Работа посвящена созданию программного комплекса flagmanFoam, разрабатываемого на базе пакета OpenFOAM v2012. Решатель предназначен для моделирования процессов обледенения в условиях натекания мелких капель, при характерном размере до 40 мкм, что соответствует Приложению C Авиационных правил АП-25. Приведены физико-математические модели, реализованные в решателе: для описания динамики газокапельного потока используется Эйлер-Эйлер подход , термодинамическая модель Майерса используется для описания процесса нарастания жидкой пленки и льда, для движения межфазной поверхности используется Coupled Level Set – VoF метод, для учета взаимодействия между жидкостью и обтекаемым телом используется метод погруженных границ, турбулентная вязкость вычисляется с помощью k-w SST модели турбулентности. Представлены результаты моделирования на тестовых задачах и сравнение с экспериментальными данными.

Генерация магнитных полей галактик – важная задача как с точки зрения космической магнитной гидродинамики, так и с позиции вычислительной математики (как правило, моделирование полей требует значительных компьютерных ресурсов, часто необходимо использование параллельных вычислений). Процесс эволюции поля описывается с помощью уравнений динамо среднего поля, которые в общем случае являются нелинейными. Они допускают формирование контрастных структур, предсказываемых теорией сингулярных возмущений, описывающей уравнения с малым параметром при старшей производной. С астрономической точки зрения подобные решения обычно связывают со спиральной структурой галактик и с формированием инверсий магнитного поля: в разных частях галактики формируются области с противоположным направлением магнитного поля, разделенные узкими переходными слоями. С вычислительной точки зрения решение полной двумерной задачи является достаточно ресурсоемкой задачей, поэтому оказывается разумным использование параллельных вычислений. Одним из вариантов реализации данного решения выступает платформа OpenCL, позволяющая в несколько раз увеличить производительность процесса. OpenCL является перспективным кроссплатформенным стандартом для разработки приложений, в частности использующих GPU, производительность которых по мере эволюции драйверов стремительно увеличивается. В настоящей работе представлены основные теоретические оценки поведения магнитного поля, которые в дальнейшем подтверждаются и уточняются в ходе компьютерного моделирования на видеокартах. Показано, что механизм возникновения переходных слоев в радиальном и азимутальном направлениях описывается принципиально различными механизмами. В то время как радиальные инверсии магнитного поля оказываются достаточно устойчивыми, все азимутальные структуры быстро размываются за счет характера течений межзвездного газа. Это означает также практическую нереализуемость возникновения неосесимметричных распределений магнитного поля.

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