В последние годы ИСП РАН разрабатывает систему дедуктивной верификации машинного (бинарного) кода. Мотивация понятна: современные компиляторы, такие как GCC и Clang/LLVM, не застрахованы от ошибок; тем самым, проверка корректности сгенерированного кода (хотя бы для компонентов с повышенными требованиями к надежности и безопасности) не является лишней. Ключевая особенность предлагаемого подхода состоит в возможности переиспользования формальных спецификаций (пред- и постусловий, инвариантов циклов, лемм и т.п.) уровня исходного кода для верификации машинного кода. Инструмент основан на формальной спецификации системы команд и обеспечивает высокий уровень автоматизации: он дизассемблирует машинный код, извлекая его семантику, адаптирует высокоуровневые спецификации для машинного кода и генерирует условия верификации. Система использует ряд сторонних компонентов, включая анализатор исходного кода (Frama-C), анализатор машинного кода (MicroTESK) и SMT-решатель (СVC4). Модульная архитектура позволяет заменять один компонент другим при изменении формата входных данных или используемой техники верификации. В работе рассматривается архитектура инструмента, описывается наша реализация и демонстрируется пример верификации библиотечной функции memset.

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

Написание статических анализаторов затруднено из-за наличия множества эквивалентных преобразований между исходным кодом программы, промежуточным представлением и большими формулами в формате Satisfiability Modulo Theories (SMT). Традиционные методы, такие как использование отладчика, инструментарий и ведение журналов, заставляют разработчиков сосредотачиваться на определенных мелких проблемах. В то же время каждая архитектура анализатора навязывает уникальное представление о том, как следует представлять промежуточные результаты, необходимые для отладки. Таким образом, отладка остается проблемой для каждого исследователя статического анализа. В этой статье представлен наш опыт отладки незавершенного промышленного статического анализатора. Представлено несколько наиболее эффективных методов конструктивной (генерация кода), тестовой (генерация случайных тестовых случаев) групп, а также группы журнализации (объединение и визуальное представление журналов). Генерация кода помогает избежать проблем с копируемым кодом, мы улучшаем его с помощью проверки использования кода. Генерация случайных тестовых наборов на основе целей снижает риски разработки инструмента, сильно смещенного в сторону конкретных вариантов использования конструкции синтаксиса, путем создания проверяемых тестовых программ с утверждениями. Слияние журналов объединяет журналы модулей и устанавливает перекрестные ссылки между ними. Модуль визуального представления показывает объединенный журнал, представляет основные структуры данных и предоставляет отчеты о работоспособности и производительности в форме отпечатков журнала. Эти методы реализованы на основе Equid, платформы статического анализа для промышленных приложений, и используются для внутренних целей. Они представлены в статье, изучены и оценены. Основные вклады включают изучение причин сбоев в авторском проекте, набор методов, их реализации, результаты тестирования и два тематических исследования, демонстрирующие полезность методов.

Эта статья посвящена генерации кода для вещественной арифметики в архитектуре MIPS. Эта работа является частью проекта «RuC». В ней рассматривается только генерация кодов для операций с числами с плавающей запятой. В статье не рассматриваются лексический, синтаксический и видозависимый анализы.

В последние десять лет наблюдается быстрый прогресс в науке и технологиях благодаря разработке интеллектуальных мобильных устройств, рабочих станций, суперкомпьютеров, интеллектуальных гаджетов и сетевых серверов. Увеличение числа пользователей интернета и многократное увеличение скорости интернета привело к генерации огромного количества данных, которые сейчас обычно называют «большими данными». При таком сценарии хранение и обработка данных на локальных серверах или персональных компьютерах может вызвать ряд проблем, которые могут быть решены с помощью распределенных вычислений, распределенного хранения данных и распределенной передачи данных. В настоящее время существует несколько провайдеров облачных услуг для решения этих проблем, таких как Amazon Web Services, Microsoft Azure, Cloudera и т. Д. Подходы к распределенным вычислениям поддерживаются с помощью мощных центров обработки данных (ЦОД). Однако традиционные ЦОДы требуют дорогого оборудования, большого количества энергии для работы и эксплуатации системы, мощной системы охлаждения и занимают большую площадь. Кроме того, для поддержания такой системы необходимо ее постоянное использование, поскольку ее резервирование экономически невыгодно. Целью статьи является возможность использования кластера Raspberry Pi и Hadoop для распределенного хранения и обработки «больших данных». Такое отключение обеспечивает низкое энергопотребление, использование ограниченного физического пространства, быстрое решение проблем обработки данных. Hadoop предоставляет необходимые модули для распределенной обработки больших данных путем развертывания программных подходов MapReduce. Данные хранятся с использованием распределенной файловой системы Hadoop (HDFS), которая обеспечивает большую гибкость и большую масштабируемость, чем один компьютер. Предлагаемая аппаратно-программная система обработки данных на базе микрокомпьютера Raspberry Pi 3 может быть использована для исследовательских и научных целей в университетах и научных центрах. Рассмотренная распределенная система демонстрирует экономическую эффективность по сравнению с традиционными ЦОД. Представлены результаты пилотного проекта применения кластера Raspberry Pi. Отличительной особенностью данной работы является использование распределенных вычислительных систем на одноплатных микрокомпьютерах для академических целей для исследовательских и учебных задач учащихся с минимальными затратами и простотой создания и использования системы.

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

В статье рассматривается коммутатор, функционирующий под управлением протокола OpenFlow 1.3. Коммутатор работает на базе программируемого сетевого процессорного устройства (СПУ). Для классификации приходящих пакетов коммутатор выполняет поиск записи (правила) в таблице потоков по значениям полей заголовка для определения действий, которые необходимо выполнить над полученным пакетом.          Поиск в программе на языке ассемблера рассматриваемого СПУ может быть реализован в виде набора деревьев поиска. При этом существует ограничение на ширину сравниваемых значений, что не позволяет напрямую использовать деревья поиска для классификации по таблице потоков. В статье предлагается представление таблицы потоков, разработанное для трансляции таблицы потоков в программу на языке ассемблера СПУ, реализующую поиск по набору правил таблицы. Еще одной целью являлось создание компактной программы, которая может быть загружена в память СПУ. Архитектура рассматриваемого СПУ также обладает особенностью, заключающейся в необходимости обновления программы после каждого изменения таблицы потоков. Поэтому целесообразно поддерживать текущее представление таблицы потоков для быстрого обновления программы СПУ. В статье представлены алгориты для инкрементного обновления разработанного представления таблицы потоков (добавления и удаления правила). Разработанный подход был исследован на экспериментальных наборах правил, которые были транслированы в программы на языке ассемблера СПУ с использованием прямого способа, основанного на существующих подходах, и разработанного алгоритма. Экспериментальное исследование проводилось на основе модели СПУ и показало, что разработанный подход способен эффективно уменьшать размер программы.

В настоящее время многие люди используют образовательные онлайн-платформы. Большинство из них работают на бесплатной программной платформе с открытым исходным кодом «Open edX». Используя логи, которые предоставляет нам платформа, мы можем получить психометрические данные студентов, которые можно использовать для улучшения представления материала или других вещей, которые могут повысить качество онлайн-курсов. Мы предоставляем готовый инструмент, который поможет выяснить, как и с какой целью вы можете анализировать лог-файлы на основе «Open edX».

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

В данной работе представлен подход для обнаружения аккаунтов злоумышленников в крупнейшей российской социальной сети ВКонтакте на основе методов машинного обучения. Был проведен исследовательский анализ данных для определения аномалий и закономерностей в наборе данных, состоящем из 42394 вредоносных и 241035 подлинных учетных записей пользователей ВКонтакте. Кроме того, для получения набора данных был разработан инструмент для автоматического сбора информации о вредоносных аккаунтах в социальной сети ВКонтакте, описание архитектуры данного инструмента приведено в работе. На основе признаков, сгенерированных из пользовательских данных, была обучена модель классификации при помощи библиотеки CatBoost. Результаты показали, что эта модель может идентифицировать злоумышленников с общим качеством AUC 0.91, подтвержденной четырехкратным методом перекрестной проверки.

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

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

Интеграция вычислительных систем и методов в юридическую деятельность позволяет извлечь такие выгоды, как ресурсосбережение, повышение объективности, полноты и точности интеллектуальных результатов. Понимание основных научных достижений и тенденций на стыке компьютерных и правовых наук акцентирует внимание на перспективных научно-технологических направлениях информатизации права. Настоящий обзор систематизирует важнейшие достижения на стыке правовых и компьютерных наук, охватывая зарубежные и отечественные научные публикации за 1949–2020 годы. Исследования компьютерных методов и систем, инициированные американской юриметрикой, были направлены на хранение, индексацию, абстрагирование и поиск юридических текстов и привели к созданию правовых информационно-поисковых систем, тогда как отечественная правовая кибернетика стала пионером в сфере автоматизации криминалистической экспертизы. На базе методов искусственного интеллекта развилось компьютерное моделирование юридических рассуждений, сместившееся в дальнейшем в область юридического диалога и конфликта правовых аргументов, а в последние годы трансформирующего полученный опыт на основе современных компьютерных моделей, шаблонов и архитектур. Популяризация систем для поддержки принятия решений обеспечила мультизадачность систем, включающую информационный поиск, юридическую аргументацию, аналитику, прогноз и контроль. Новейшие сегменты исследований ориентированы на применение методов машинного обучения и интеллектуальный анализ больших данных. Практически все успешные методологические решения сохраняют свое значение, продолжая применяться непосредственно или послужив основой для дальнейшего развития вычислительных методов и информационных систем в правовой деятельности.