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

В статье описывается расширение статического анализа программ на основе резюме для поиска ошибок взаимных блокировок потоков. Анализ на основе резюме является популярным подходом для поиска ошибок в программах благодаря высокой производительности и масштабируемости. При этом реализация детекторов поиска взаимных блокировок в таком анализе является нетривиальной, так как в процессе внутрипроцедурного анализа функций отсутствует информация об удерживаемых блокировках выше по стеку вызовов. Для моделирования семантики многопоточных программ используется граф блокировок, который строится во время основного анализа. Граф блокировок является модификацией графа вызовов с добавлением информации об удерживаемых блокировках. После построения графа блокировок запускается детектор обнаружения взаимных блокировок. Как построение графа блокировок, так и алгоритм обнаружения взаимных блокировок, не требуют существенного процессорного времени. На выполненных замерах общее время анализа увеличилось на 4%. По результатам анализа 8 проектов с открытым исходном кодом на языках C/C++/Java общим размером более 14 млн. строк кода предложенный алгоритм показал высокий уровень истинных срабатываний. Описываемые алгоритмы были реализованы в инструменте Svace.

В составе современных вычислительных систем все чаще используются аппаратные спецпроцессоры, программируемые на предметно-ориентированных языках. Популярность набирает подход compiler-in-the-loop, предполагающий совместную разработку спецпроцессора и компилятора. При этом традиционный инструментарий (GCC и LLVM) оказывается недостаточным для быстрой разработки оптимизирующих компиляторов, порождающих целевой код нерегулярной архитектуры со статическим параллелизмом операций. В статье предлагается использовать методы решения NP-полных задач для реализации машинно-зависимых фаз компиляции. Фазы осуществляются на основе сведения к задаче SMT, что дает возможность избавиться при построении компилятора от эвристических и приближенных подходов, требующих трудоемкой программной реализации. В частности, с использованием SMT-решателя предлагается реализовать синтез правил машинно-зависимой оптимизации, выбор команд, планирование команд и распределение регистров. Обсуждаются вопросы апробации разработанных методов и алгоритмов на примере компилятора для спецпроцессора с набором команд, ускоряющим реализации алгоритмов низкоресурсных шифров из области Интернета вещей. Полученные результаты компиляции и программного моделирования для 8 криптоалгоритмов и 3 вариантов спецпроцессора (CISC, VLIW и вариант delayed load) демонстрируют практическую применимость предложенного подхода.

В статье представлено описание семейства эмуляторов архитектур мейнфреймов IBM, история их разработки, их функциональные особенности и возможности применения, а также опыт многолетнего развития (начиная с 1994 года) состава эмуляторов, и сфер их применения. Решена относительно простая по современным представлениям задача создания виртуальной машины в операционной системе VSE/ESA для переноса в эту целевую среду унаследованных платформозависимых приложений. Задача решена сначала для ЕС ЭВМ в РФ, а потом для машин IBM 9221 в ФРГ и других западных странах. Перенос осуществлялся в среду современной по тем временам OS/390, а также IBM AIX. Обеспечена возможность виртуального исполнения любых существующих операционных систем мейнфреймов IBM в средах основных серверных ОС: Linux, Windows, AIX, Z/OS, ZLinux. Разработано решение по объединению образовавшихся виртуальных вычислительных узлов любых типов в гетерогенные территориально распределенные вычислительные сети, обеспечивающие в частности множественное взаимное резервирование узлов в сети.

Многие современные СУБД предоставляют процедурное расширение декларативного языка программирования SQL, которое позволяет выполнять сложные вычисления с условной логикой на стороне сервера. Данные расширения стимулируют модулярность и переиспользование кода, упрощают процесс программирования логики некоторых приложений, а также позволяют избавиться от накладных расходов на передачу данных по сети и повысить производительность вычислений. В большинстве случаев для исполнения SQL-запросов и процедурных расширений используется подход интерпретации, который сопряжен с существенными накладными расходами по неявному вызову функций и выполнению лишних обобщенных проверок. Ситуация ухудшается тем, что для выполнения SQL-запросов и процедурных расширений, как правило, применяются два разных движка-исполнителя, в рамках которых необходимо осуществлять дополнительные операции по переключению контекста для сохранения промежуточных вычислений и контроля используемых ресурсов. В совокупности, совместная интерпретация SQL-запросов и процедурных расширений может в значительной степени снижать общую производительность СУБД. Одно из решений этой проблемы – динамическая компиляция. В рамках данной работы рассматривается метод динамической компиляции процедурного расширения PL/pgSQL в СУБД PostgreSQL с использованием компиляторной инфраструктуры LLVM. Работа выполняется в рамках динамического компилятора SQL-запросов, реализованного в виде расширения к СУБД PostgreSQL. Предлагаемый метод позволяет избавиться от накладных расходов, связанных с интерпретацией. Результаты тестирования на некоторых синтетических тестах показывают ускорение выполнения SQL-запросов в несколько раз.

В работе рассмотрены вопросы построения и практической реализации модели обнаружения компьютерных атак на основе методов машинного обучения. Среди доступных публичных наборов данных выбран один из наиболее актуальных – CICIDS2017. Для рассматриваемого набора данных подробно разработаны процедуры предварительной обработки данных и сэмплирования. При проведении экспериментов для сокращения времени вычислений в обучающей выборке оставлен единственный класс компьютерных атак – веб-атаки (brute force, XSS, SQL injection). Последовательно описана процедура формирования признакового пространства, позволившая существенно снизить его размерность – с 85 до 10 наиболее значимых признаков. Произведена оценка качества десяти наиболее распространенных моделей машинного обучения на полученной предобработанной подвыборке данных. Среди моделей (алгоритмов), которые продемонстрировали наилучшие результаты (k-nearest neighbors, decision tree, random forest, AdaBoost, logistic regression), с учетом минимального времени выполнения обоснован выбор модели «случайный лес». На этапе настройки и обучения выбранной модели осуществлен квазиоптимальный подбор гиперпараметров, что позволило добиться повышения качества модели в сравнении с ранее опубликованными результатами исследований. Произведена апробация синтезированной модели обнаружения атак на реальном сетевом трафике, показавшая ее состоятельность только при условии обучения на данных, собираемых в конкретной защищаемой сети, в виду зависимости ряда значимых признаков от физической структуры сети и настроек используемого оборудования. Сделан вывод о возможности применения методов машинного обучения для обнаружения компьютерных атак с учетом указанных ограничений.

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

Одной из основных задач при анализе данных РНК-секвенирования единичных клеток является идентификация типов и подтипов клеток, которая обычно основана на каком-либо методе кластеризации. Существует ряд общепринятых подходов к решению проблемы кластеризации, один из которых реализован в пакете Seurat. На качество кластеризации, помимо прочего, влияет использование алгоритмов предварительной обработки, таких как импутация, уменьшение размерности, отбор признаков и т. д. В статье для кластеризации данных scRNA-seq используется метод иерархической кластеризации HDBSCAN. Для более полного сравнения эксперименты и сравнения проводились на двух размеченных наборах данных: Zeisel (3005 клеток) и Romanov (2881 клетка). Для сравнения качества кластеризации использовались две внешние метрики: скорректированный индекс Рэнда и V-мера. Эксперименты продемонстрировали более высокое качество кластеризации методом HDBSCAN на наборе данных Zeisel и более низкое качество на наборе данных Romanov.

Разработана и описана методика проведения неинвазивного скрининга населения на нарушение углеводного обмена (НУО). Новизна методики заключается в том, что по неинвазивному типу скрининга еще не существует медицинских стандартов в области эндокринологии, поэтому методика составлялась на основе результатов клинического исследования по изучению электрокардиографических отклонений у больных с НУО, где использовался метод неинвазивного определения НУО по ЭКГ первого отведения. Во время разработки методики был проведен дополнительный анализ выборки ЭКГ, полученной в ходе исследования. В результате анализа сделаны выводы, что показатели эффективности метода (чувствительность и специфичность) слабо изменяются в зависимости от времени съема ЭКГ в течение суток. Это означает, что пациент может явиться на скрининг по методике неинвазивного определения НУО не только утром и не обязательно натощак, в отличие от инвазивных методик (тест глюкозы плазмы натощак и пероральный тест толерантности к глюкозе). Для принятия решения «есть подозрение на НУО»/«нет подозрения на НУО» пациенту достаточно снять до 2 ЭКГ.

Мониторинг информационной безопасности промышленных киберфизических систем (КФС) является постоянным процессом, необходимым для обеспечения их безопасности. Эффективность мониторинга зависит от качества и скорости сбора, обработки и анализа гетерогенных данных КФС. Сегодня существует много методов анализа для решения задач безопасности распределенных промышленных киберфизических систем. У этих методов разные требования к характеристикам входных данных, но есть общие особенности, обусловленные предметной областью. Работа посвящена предварительной обработке данных при мониторинге безопасности промышленных КФС в современных условиях. Задача рассматривается от требований к системе предварительной обработки данных и особенностей предметной области, до специфических методов агрегации, основанных на PCr – связях между структурами данных. Разработана архитектура обработки данных сочетающая методы агрегации и нормализации информации в системе мониторинга.

Курчатовский комплекс НБИКС-природоподобных технологий ориентирован на междисциплинарные исследования и разработки в области нано-, био-, информационных, когнитивных, социогуманитарных наук и технологий. Экспериментальной основой НБИКС комплекса являются Ресурсные центры, действующие в режиме коллективного пользования различными научными лабораториями и содержащие современное оборудование для проведения широкого спектра научных экспериментов. Обработка и хранение полученных экспериментальных данных производится на суперкомпьютере Вычислительного центра, пользование которым также является коллективным. Таким образом, возникают задачи обмена данными между различными зданиями, организации их обработки, анализа и упорядоченного хранения, а также совмещения гетерогенных экспериментальных данных для получения научных результатов более высокого уровня. Для решения данных вопросов на базе распределённой модульной платформы «Цифровая Лаборатория» была организована информационно-аналитическая среда как система, объединяющая в единое виртуальное пространство научное оборудование Ресурсных центров, суперкомпьютер Вычислительного центра, виртуальные машины и персональные компьютеры научных лабораторий, организуя при этом обмен данными между различными зданиями, их обработку, анализ и хранение. Работа с системой осуществляется посредством пользовательского веб-интерфейса. По запросу исследователей каждая процедура работы с экспериментальными данными заданного типа реализуется в виде автономного модуля платформы «Цифровая Лаборатория». Так, например, введен в эксплуатацию и успешно функционирует Модуль «Нейровизуализация» для обработки и анализа фМРТ/МРТ экспериментальных данных головного мозга человека, получаемых на томографе Ресурсного центра. Использование этого модуля делает задачу анализа фМРТ/МРТ данных максимально простой для пользователя, а также позволяет многократно ускорить процесс обработки данных за счёт расспараллеливания вычислений на узлах суперкомпьютера. Помимо создания модулей для работы с экспериментальными данными, система предусматривает возможность создания модулей для работы с данными иного типа. В качестве примера можно привести Модуль «Проектная деятельность» для анализа эффективности научной деятельности исследовательских лабораторий. Использование данной системы позволяет оптимизировать работу с экспериментальными данными в ходе проведения научных исследований за счёт возможности программной реализации необходимых процедур их передачи, хранения, обработки и анализа.

Дается анализ проблематики надежности и безопасности в мировой практике и в нашей стране. Рассмотрены аспекты моделирования программно-технических систем (ПТС) из сервисных ресурсов и готовых КПИ с обеспечением надежности и безопасности. Приводятся сформировавшиеся базовые и теоретические основы проблемы моделирования, опыта использования современных сервисных средств SOA, SCA, SOAP в ПТС и Web-системах с обеспечением их надежности и безопасности в Интернет. Отмечается, что ПТС и Web-системы создаются методом сборки в современных средах: IBM WSDK + WebSphere, Apache Axis + Tomcat; Microsoft .Net + IIS и др. Должны проводиться верификация и тестирование систем для поиска ошибок, возникающих при исключительных ситуациях (кибератаках, запрещенных доступах к БД и др.). Описаны методы анализа таких ситуаций и применения методов надежности и безопасности для обеспечения устойчивой и безотказной работы сервисных компонентов ПТС в информационной среде Интернет.

Совмещение трехмерной модели с изображением можно рассматривать как установку визуальных соответствий, извлекаемых из данных, описывающих эти изображения. Эта непростая задача еще более усложняется, если при построении изображений используются разные методы визуализации. В статье представлен подход, позволяющий сопоставлять характеристики, обнаруживаемые в двух различных видах изображений – фотографиях и 3D-моделях – с использованием общего 2D-представления. Наш подход основан на модификации алгоритма Marching Cubes, позволяющей избежать неоднозначных решений, не добавляя вычислений при обработке каждого куба. Мы разделяем идею о решающей важности разделения случаев эквивалентности на два класса. С учетом всех возможных состояний внутри и снаружи в четырех углах одной грани куба имеются только четыре нетривиальных варианта после исключения эквивалентных вариантов путем вращения. Полученные результаты демонстрируют применимость предлагаемой методики.

Представлены результаты численного моделирования прикладной акустической задачи – моделирования газовых процессов, протекающих в измерительной камере инфразвукового пистонфона 3202 при различных частотах колебаний поршня (0,1 – 1000 Гц) и характеризующихся крайне малыми значениями числа Маха (9,1·10^-7÷9,1·10^-3). Моделирование проведено с использованием квазигазодинамических (КГД) и квазигидродинамических (КГиД) уравнений вязкого сжимаемого теплопроводного газа, определены границы устойчивости алгоритмов КГД и КГиД в данной задаче.