Аннотация:

Представлен опыт верификации реализаций сервера криптографического протокола TLS версии 1.3. TLS – широко распространенный криптографический протокол, предназначенный для создания защищенных каналов передачи данных и обеспечивающий необходимую для этого функциональность: конфиденциальность передаваемых данных, целостность данных, аутентификацию сторон. Новая версия протокола TLS 1.3 была представлена в августе 2018 года и имеет ряд существенных отличий по сравнению с предыдущей версией 1.2. Ряд разработчиков протокола TLS уже включил поддержку последней версии в свои реализации. Данные обстоятельства делают актуальным проведение исследований в области верификации и безопасности реализаций новой версии протокола TLS. В работе использован новый тестовый набор для верификации реализаций протокола TLS 1.3 на соответствие спецификациям интернета, разработанный на основе спецификации RFC 8446 с использованием технологии UniTESK и методов мутационного тестирования. Текущая работа является частью проекта верификации протокола TLS 1.3 и охватывает часть дополнительной функциональности и необязательных расширений протокола.

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

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

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

Аннотация:

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

В работе использован новый тестовый набор для верификации реализаций клиента протокола TLS 1.3 на соответствие спецификациям интернет, разработанный на основе спецификации RFC 8446 с использованием технологии UniTESK и методов мутационного тестирования. Для тестирования реализаций на соответствие формальным спецификациям применена технология UniTESK, предоставляющая средства автоматизации тестирования на основе использования конечных автоматов. Состояния тестируемой системы задают состояния автомата, а тестовые воздействия – переходы этого автомата. При выполнении перехода заданное воздействие передается на тестируемую реализацию, после чего регистрируются реакции реализации и автоматически выносится вердикт о соответствии наблюдаемого поведения спецификации. Мутационные методы тестирования используются для обнаружения нестандартного поведения тестируемой системы (завершение из-за фатальной ошибки, «подвисание», ошибки доступа к памяти) с помощью передачи некорректных данных, такие ситуации часто остаются за рамками требований спецификаций. В сообщения, сформированные на основе разработанной модели протокола, вносятся какие-либо изменения. Модель протокола дает возможность вносить изменения в поток данных на любом этапе сетевого обмена, что позволяет тестовому сценарию проходить через все значимые состояния протокола и в каждом таком состоянии проводить тестирование реализации в соответствие с заданной программой. Представленный подход доказал свою эффективность в нескольких наших проектах при тестировании сетевых протоколов, обеспечив обнаружение различных отклонений от спецификации и других ошибок. Текущая работа является частью проекта верификации протокола TLS 1.3 и охватывает реализации клиентской части протокола.

Аннотация:

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

В статье рассмотрены вероятностные структуры данных, которые могут быть использованы для решения задачи, а также предложена реализация – модуль проверки целостности данных с использованием фильтра Блума с подсчетом. Данный модуль интегрирован в Apache Airflow для автоматизации процесса.

Аннотация: Рассмотрена распределенная сеть, топология которой описана неориентированным графом. Сеть может сама изменять свою топологию, используя специальные «команды», подаваемые ее узлами. В работе предложена предельно локальная атомарная трансформация acb изменения конца c ребра ac, «движущегося» вдоль ребра cb от вершины c к вершине b. В результате этой операции ребро ac удаляется, а ребро ab добавляется. Такая трансформация выполняется по «команде» от общей вершины c двух смежных ребер ac и cb. Показано, что из любого дерева можно получить любое другое дерево с тем же множеством вершин, использовав только атомарные трансформации. Если степени вершин дерева ограничены числом d (d3), то трансформация не нарушает этого ограничения. В качестве примера цели такой трансформации рассмотрены задачи максимизации и минимизации индекса Винера дерева с ограниченной степенью вершин без изменения множества его вершин. Индекс Винера – это сумма попарных расстояний между вершинами графа. Максимальный индекс Винера имеет линейное дерево (дерево с двумя листовыми вершинами). Для корневого дерева с минимальным индексом Винера определены его вид и способ вычисления числа вершин в ветвях соседей корня. Предложены два распределенных алгоритма: трансформации дерева в линейное дерево и трансформации линейного дерева в дерево с минимальным индексом Винера. Доказано, что оба алгоритма имеют сложность не выше 2n–2, где n – число вершин дерева. Также рассмотрена трансформация произвольных неориентированных графов, в которых могут быть циклы, кратные ребра и петли, без ограничения на степени вершин. Показано, что любой связный граф с n вершинами может быть преобразован в любой другой связный граф с k вершинами и тем же числом ребер за время не более 2(n+k)–2.

Аннотация:

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

Аннотация:

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

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

Представлен подход к организации цифровой инфраструктуры электронного научного журнала на основе открытой программной системы Open Journal Systems (OJS). Предложены сервисы, расширяющие функциональные возможности этой системы и учитывающие специфику предметной области научных журналов. На основе технологии расширения функционала OJS созданы программные модули, обеспечивающие автоматизацию ряда редакционных процессов электронного научного журнала.

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

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

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

Охарактеризована проблема построения системы анализа и оценки информационного и социального воздействия публикуемого научного контента на его пользователей. Проведено сопоставление традиционных (библиометрических и наукометрических) и альтернативных показателей такой оценки. Описан мировой опыт использования информетрических сервисов на сайтах научных журналов. Обсуждены варианты реализации этих подходов в рамках цифровой инфраструктуры электронного научного журнала.

Аннотация:

Рассмотрено применение векторных моделей для предварительного анализа ответов студентов, сформулированных в свободной форме. Векторные представления слов и документов получены при помощи моделей word2vec, doc2vec, BERT. Сходство ответа, данного обучающимся, и корректного ответа определялось с использованием косинусной меры. Выявлено, что векторные модели позволяют определить явно неверные ответы с достаточной точностью. Для ответов, которые близки по формулировке, предлагается провести дополнительный этап проверки. При помощи word2vec выполнена двоичная классификация ответов на определенные вопросы, приведены оценки точности, полноты, F1-меры.

Аннотация:

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

Предложенная теория была проверена на вихревых ковариационных экологических данных по количеству/балансу CH₄, CO₂ и паров воды H₂O в атмосфере, где расположены соответствующие детекторы для измерения содержания искомых газов.

Для этих проверенных данных вихревой ковариации, связанных с наличием в атмосфере двух газов CH₄, CO₂ и паров H₂O, не существует простой гипотезы, содержащей минимальное число подгоночных параметров, и, следовательно, подгоночная функция, следующая из этой теории, может служить единственным и надежным средством количественного описания такого рода данных, принадлежащих сложной системе. Следует также отметить, что окончательная подгоночная функция, очищенная от неконтролируемых факторов, становится периодической и соответствует идеальному эксперименту.

Обсуждены приложения этой теории, ее место среди других альтернативных подходов (особенно затрагивающих профессиональные интересы экологов) и её дальнейшее развитие.

Аннотация:

Статья посвящена прогнозированию тенденций изменения цен финансовых инструментов рынка форекс. Рассмотрены способы формирования прогнозов на основании моделей бизнес-циклов и фрактальной самоорганизации ценообразования. На основании исторических прецедентов кризисов после 1812 и 1917 гг. определяются сроки кризиса 2015–2027 гг., завершение которого совпадает с одновременным окончанием 200-летней и 40-летних тенденций. Прогнозируется достижение точки технологической сингулярности в 2039 году. Разработаны способы интеграции инструментария фундаментального и технического анализа для прогноза глобальных событий, отсутствующих в экономическом календаре. Предложено увеличить эффективность прогнозирования изменения цен финансовых инструментов при помощи аналитической системы мультитрейдинга, спроектированной для работы с шестью стратегиями: долгосрочной (8 месяцев), среднесрочной (2 месяца), краткосрочными (1,5 недели и 1,5 дня) и внутридневными (8 часов, 2 часа). Выбор стратегии зависит от времени, которое трейдер готов использовать для аналитической деятельности и контролирования открытых сделок, допустимых рисков и ожидаемой доходности. Для всех стратегий установлен набор предпочтительных валютных пар брокеров Forex Club и FxPro, даны рекомендации для трейдеров. Определена необходимая и достаточная совокупность индикаторов технического анализа, участвующих в образовании тройного сигнала позиционирования стартовой точки Канала Регрессии, позволяющего автоматически спрогнозировать тактические уровни разворота тренда изменений цены на интервале формирования групп из восьми осцилляций. Разработан регламент создания, публикации и верификации тактических прогнозов длительности и амплитуды осцилляций цены для всех стратегий и множества финансовых инструментов. Прогнозы публикуются в каналах и группах «Мультитрейдинг» сетевых сервисов Телеграм, Дзен и ВКонтакте. Прогностический инструментарий предполагается использовать при формировании тактик системы мультитрейдинга.