Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Эффективный алгоритм разрешения коллизий в правилах политики безопасности
Get PDFA firewall is the main classic tool for monitoring and managing the network traffic on a local network. Its task is to compare the network traffic passing through it with the established security rules. These rules, which are often also called security policy, can be defined both before and during the operation of the firewall. Managing the security policy of large corporate networks is a complex task. In order to properly implement it, firewall filtering rules must be written and organized neatly and without errors. In addition, the process of changing or inserting new rules should be performed only after a careful analysis of the relationship between the rules being modified or inserted, as well as the rules that already exist in the security policy. In this article, the authors consider the classification of relations between security policy rules and also give the definition of all sorts of conflicts between them. In addition, the authors present a new efficient algorithm for detecting and resolving collisions in firewall rules by the example of the Floodlight SDN controller.Межсетевой экран является основным классическим инструментом для контроля и управления сетевым трафиком в локальной сети. Его задача — сравнивать проходящий через него сетевой трафик с установленными правилами безопасности. Эти правила, которые часто также называют политикой безопасности, могут быть определены как до, так и во время работы межсетевого экрана. Управление политикой безопасности крупных корпоративных сетей является сложной задачей. Для того чтобы правильно ее реализовать, правила фильтрации межсетевого экрана должны быть написаны и организованы аккуратно и без ошибок. Кроме того, процесс изменения или вставки новых правил должен выполняться только после тщательного анализа отношений между изменяемыми или вставляемыми правилами, а также правилами, которые уже существуют в политике безопасности. В данной статье авторы рассматривают классификацию отношений, в которых могут находиться правила политики безопасности между собой, и дают определение возможных коллизий между ними. Авторы представляют также новый эффективный алгоритм обнаружения и устранения коллизий в правилах межсетевого экрана на примере контроллера ПКС Floodlight
Автоматизированный поиск средств ритмизации художественного текста для сравнительного анализа оригинала и перевода на материале английского и русского языков
Get PDFAnalysis of the functional equivalence of an original text and its translation based on the achievement of rhythm equivalence is an extremely important task of modern linguistics. Moreover, the rhythm component is an integral part of functional equivalence that cannot be achieved without communication of rhythm figures of the text. To analyze rhythm figures in an original literary text and its translation, the authors developed the ProseRhythmDetector software tool that allows to find and visualize lexical and syntactic figures in English- and Russian-language prose texts: anaphora, epiphora, symploce, anadiplosis, epanalepsis, reduplication, epistrophe, polysyndeton, and aposiopesis. The goal of this work is to present the results of ProseRhythmDetector testing on two works by English authors and their translations into Russian: Ch. Bronte “Villette” and I. Murdoch “The Black Prince”. Basing on the results of the tool, the authors compared rhythm figures in an original text and its translation both in aspects of the rhythm and their contexts. This experiment made it possible to identify how the features of the author’s style are communicated by the translator, to detect and explain cases of mismatch of rhythm figures in the original and translated texts. The application of the ProseRhythm-Detector software tool made it possible to significantly reduce the amount of linguistsexperts work by automated detection of lexical and syntactic figures with quite high precision (from 62 % to 93 %) for various rhythm figures.Анализ функциональной эквивалентности перевода, основанный на достижении ритмической эквивалентности, представляет собой чрезвычайно важную задачу современной лингвистики. При этом ритмическая составляющая является неотъемлемой частью функциональной эквивалентности, которая не может быть достигнута без передачи ритмических характеристик текста. Для анализа ритмических средств в оригинальном тексте и переводе художественного произведения авторами был разработан программный инструмент ProseRhythmDetector, позволяющий находить и визуализировать лексические и синтаксические средства в англоязычных и русскоязычных прозаических текстах: анафору, эпифору, симплоку, анадиплозис, эпаналепсис, редупликацию, эпистрофу, многосоюзие и апозиопезу. Целью данной работы является представление результатов апробации ProseRhythmDetector на двух произведениях английских авторов и их переводах на русский язык: Ш. Бронте «Городок» (Ch. Bronte “Villette”) и А. Мердок «Черный принц» (I. Murdoch “The Black Prince”). На основе результатов работы инструмента авторы сопоставили ритмические характеристики в оригинале текста и его переводе и сравнили как аспекты ритма, так и их контексты. Данный эксперимент позволил выявить особенности передачи стиля автора художественного произведения переводчиком, обнаружить и объяснить случаи несовпадения ритмических средств оригинала и перевода. Применение программного инструмента ProseRhythmDetector позволило существенно сократить объем работы экспертов-лингвистов за счет автоматизированного выявления лексических и синтаксических средств с достаточно высокой точностью (от 62 % до 93 %) для различных ритмических средств
К вопросу использования «полезных» задач для обеспечения работой блокчейн систем
Get PDFThis paper is a logical continuation of the paper about possible approaches to solving the “Useful Proof-of-work for blockchains” problem. We suggest some alternative ways for searching useful tasks for Proof-of-work systems. These ways are based on the process of the multiple and independent repetition of a simple experiment. The experiment is to chose an element independently and uniformly from a quite large set and then to check if the chosen element has a specific rare property. In the classic blockchain of Bitcoin this experiment is a so-called hash-puzzle. In these terms the process of solving a hash-puzzle may be replaced by searching rare astronomical objects or Go positions with specific conditions. Moreover, we describe a possible attack on the blockchain systems in which the task instance generation algorithm is replaced by the algorithm of selecting the task instance from the existing database with public access for publication of task instances and discuss the way of protection.Статья является продолжением работы о возможных подходах к решению задачи «UsefulProof-of-workforblockchains». Мы предлагаем некоторые альтернативные направления поиска полезных задач для обеспечения работой, основанные на том, что процесс решения хеш-головоломки близок к многократному независимому повторению следующего эксперимента: пусть задано достаточно большое по мощности множество (например, состоящее из 2" элементов, для достаточно большого п), только незначительная часть элементов которого обладает определенным свойством. Эксперимент состоит в равномерном выборе элемента из этого множества с последующей проверкой наличия у него указанного свойства. Таким образом, процесс решения хеш-головоломки может быть заменен, например, поиском редких астрономических объектов или поиском позиций игры Го, удовлетворяющих определенным условиям. Кроме того, мы описываем возможную атаку на блокчейн-систему, в которой алгоритм генерации индивидуальных представителей задач для обеспечения работой заменен алгоритмом выбора индивидуальных представителей из имеющейся базы данных, со стороны недобросовестных поставщиков индивидуальных представителей задач, в случае их публичного сбора, и обсуждаем некоторые способы защиты от этой атаки
Алгоритм минимизации количества правил маршрутизации в ПКС
Get PDFSoftware-Defined Networking (SDN) is a network architecture that introduces a physical separation of data-plane from control-plane. It implements a new way of analyzing network statistics through counters installed on forwarding rules. These counters measure the number of packets processed by these rules and represent per-flow network statistics. In order to get information about the number of packets from different flows SDN applications can install additional forwarding rules, sole purpose of which is to count packets with specific headers. But in order to produce a full network statistics analysis these applications may install a large amount of forwarding rules thus limiting the space in the forwarding table for other applications. So we need algorithms to minimize the number of such rules. In this paper, we consider the problem of minimizing the number of forwarding rules installed on SDN switches by applications that analyze network statistics. We introduce a heuristic algorithm that creates a reduced representation for sets of rules installed in the network. The experimental results show that this algorithm reduces the number of rules by at least 2.2 times on uniformly distributed random input.Архитектура ПКС (программно-конфигурируемые сети) предоставляет новые возможности по управлению сетью при помощи физического разделения уровня передачи данных (Data-Plane) от уровня управления данными (Control-Plane). Такое разделение достигается при помощи передачи функций управления сетью на отдельный сетевой элемент — контроллер. Архитектура ПКС позволяет устанавливать на контроллер сетевые приложения, которые могут использовать протокол OpenFlow для реализации множества различных сетевых функций, например для маршрутизации или анализа сетевой статистики. Анализ сетевой статистики производится при помощи счетчиков, установленных на правилах маршрутизации. Чтобы собирать информацию о числе пакетов в различных потоках, ПКС приложения могут устанавливать дополнительные правила маршрутизации, единственной целью которых является подсчет пакетов с определенными заголовками. Для полноценного анализа сетевой статистики приложения должны устанавливать в сеть большое количество дополнительных правил, что может привести к снижению производительности сети. В силу ограниченного размера таблиц маршрутизации, большое число дополнительных правил может мешать другим приложениям устанавливать свои правила. Таким образом, необходимо разработать алгоритм, который будет минимизировать число дополнительных правил. В данной работе рассмотрена задача минимизации числа дополнительных правил, устанавливаемых на ПКС коммутаторы приложениями для анализа сетевой статистики. Был разработан эвристический алгоритм минимизации количества правил маршрутизации, основанный на алгоритме Блейка нахождения сокращенной дизъюнктивной нормальной формы (ДНФ). Экспериментальные исследования показали, что алгоритм уменьшает число правил более чем в 2.2 раза на равномерно распределенных входных данных
Формальная верификация диаграмм троичных цифровых сигналов
Get PDFWe investigate a formal verification problem (mathematically rigorous correctness checking) for digital waveforms used in practical development of digital microelectronic devices (digital circuits) at early design stages. According to modern methodologies, a digital circuit design starts at high abstraction levels provided by hardware description languages (HDLs). One of essential steps of an HDLbased circuit design is an HDL code debug, similar to the same step of program development in means and importance. A popular way of an HDL code debug is based on extraction and analysis of a waveform, which is a collection of plots for digital signals: functional descriptions of value changes related to selected circuit places in real time. We propose mathematical means for automation of correctness checking for such waveforms based on notions and methods of formal verification against temporal logic formulae, and focus on such typical featues of HDL-related digital signals and corresponding (informal) properties, such as real time, three-valuededness, and presence of signal edges. The three-valuededness means that at any given time, besides basic logical values 0 and 1, a signal may have a special undefined value: one of the values 0 and 1, but which one of them is either not known, or not important. An edge point of a signal is a time point at which the signal changes its value. The main results are mathematical notions, propositions, and algorithms which allow to formalize and solve a formal verification problem for considered waveforms, including: definitions for signals and waveforms which the mentioned typical digital signal features; a temporal logic suitable for formalization of waveform correctness properties, and a related verification problem statement; a solution technique for the verification problem, which is based on reduction to signal transfromation and analysis; a corresponding verification algorithm together with its correctness proof and “reasonable” complexity bounds.В работе исследуется задача формальной верификации (математически строгой проверки правильности) диаграмм цифровых сигналов, используемых на практике на ранних стадиях разработки микроэлектронных цифровых устройств (цифровых схем). Отправной точкой разработки схемы, согласно современным методам проектирования, является её описание на каком-либо высокоабстрактном языке описания аппаратуры (hardware description language, HDL). Обязательным этапом разработки HDL-кода схемы является отладка этого кода, схожая по устройству и важности с отладкой программ. Один из популярных способов отладки HDL-кода основан на получении и проверке правильности диаграммы сигналов, то есть совокупности графиков сигналов: функций, описывающих изменение значений в выделенных местах схемы в реальном времени. В работе предлагаются математические средства автоматизации проверки правильности таких диаграмм, основанные на понятиях и методах верификации систем относительно формул темпоральных логик и учитывающие такие характерные особенности сигналов в HDL и соответствующих свойств правильности диаграмм в неформальном смысле, как реальное время, троичность и наличие точек фронтов. Троичность сигнала означает, что наряду с основными логическими значениями 0 и 1 сигнал может принимать и неопределённое значение: одно из значений 0 и 1, но неизвестно или неважно, какое именно. Точкой фронта называется момент изменения значения сигнала. В работе предлагаются понятия, утверждения и алгоритмы, предназначенные для формализации и решения задачи верификации диаграмм сигналов: определения сигналов и диаграмм, учитывающие упомянутые характерные особенности сигналов; темпоральная логика, предназначенная для описания свойств диаграмм сигналов, и соответствующая постановка задачи верификации диаграмм; метод решения предлагаемой задачи верификации, основанный на сведении к задачам преобразования и анализа сигналов; соответствующий алгоритм верификации диаграмм с обоснованием корректности и “приемлемой” оценкой сложности
Направляемый свойством поиск реляционных инвариантов
Get PDFProperty Directed Reachability (PDR) is an efficient and scalable approach to solving systems of symbolic constraints also known as Constrained Horn Clauses (CHC). In the case of non-linear CHCs, which may arise, e.g., from relational verification tasks, PDR aims to infer an inductive invariant for each uninterpreted predicate. However, in many practical cases this reasoning is not successful, as invariants should be derived for groups of predicates instead of individual predicates. The article describes a novel algorithm that identifies these groups automatically and complements the existing PDR technique. The key feature of the algorithm is that it does not require a possibly expensive synchronization transformation over the system of CHCs. We have implemented the algorithm on top of a up-to-date CHC solver Spacer. Our experimental evaluation shows that for some CHC systems, on which existing solvers diverge, our tool is able to discover relational invariants.Достижимость, направляемая свойством, (Property Directed Reachability, PDR) — эффективный и масштабируемый подход к решению систем символьных ограничений, известных как дизъюнкты Хорна с ограничениями (Constrained Horn Clauses, CHC). В случае нелинейных систем дизъюнктов, которые могут возникнуть, к примеру, из задач реляционной верификации, PDR выводит индуктивные инварианты для каждого неинтерпретированного предикатного символа. Тем не менее на практике автоматический вывод таких решений не удаётся, т.к. инварианты должны выводиться для групп предикатных символов вместо индивидуальных предикатных символов. В статье описан новый алгоритм, автоматически определяющий такие группы и обобщающий существующий подход PDR. Ключевая особенность алгоритма состоит в том, что он не требует потенциально дорогой синхронизирующей трансформации системы дизъюнктов Хорна. Алгоритм был реализован над современным решателем дизъюнктов Хорна Spacer. Эксперименты показывают, что полученная реализация успешно выводит реляционные инварианты для некоторых систем дизъюнктов, на которых существующие решатели не завершаются
Пороговый анализ деградации запросов внутри вычислительной сети
No full textIn this paper, the existing approaches to the assessment of computer networks performance are considered. The standard structure of a network of the application layer of the OSI model using the example of SBIS3 application (product of Tensor Company) is treated.Further, two approaches allowing to analyze degradations in a network are considered - on the basis of aggregated data and the operational analysis.The degradation study of more than 60 000 request types between two versions of application which works on the basis of the computer network is the cornerstone of the first decision. Each type of requests is described by four based metrics, each metrics representing a time series. The input data are aggregated every 10 minutes before an analysis algorithm. Further, the threshold criteria based on mathematical expectation and dispersion within two adjacent versions of the software are used. Such an approach allows to significantly reduce time for the analysis of potential problems in case of updates within the computer network.The second decision is based on not aggregated input data. It consists of detail information about all requests, there are data section of the computer network. A threshold criterion is based on durations in the selected queue. This analysis type allows to diagnose the errors with problem clients.В данной работе рассматриваются существующие подходы к оценке производительности вычислительных сетей. Представлена типовая структура сети прикладного уровня модели OSI на примере приложения СБИС3 (продукт Компании Тензор). Далее рассмотрены два подхода, позволяющие анализировать деградации внутри сети на основе агрегированных данных и оперативного анализа.В основе первого решения лежит исследование деградации более 60 000 типов запросов между двумя соседними версиями приложения, которое работает на базе вычислительной сети. Каждый тип запросов описывается четырьмя основными метриками, каждая метрика представляет собой временной ряд. На вход алгоритму анализа поступают агрегированные данные выборками по 10 минут. Далее используются пороговые критерии, основанные на математическом ожидании и дисперсии в рамках двух соседних версий программного обеспечения. Такой подход позволяет существенно сократить время для анализа потенциальных проблем при обновлениях в вычислительной сети.Информация о каждом запросе на том или ином участке вычислительной сети служит входными данными для второго решения. В качестве порогового критерия выбирается продолжительность ожидания в очереди. Этот тип анализа позволяет диагностировать дефекты, которые становятся причиной 5-образных очередей продолжительностью от нескольких секунд до 10 минут. Подобные дефекты практически не диагностируются в рамках первого подхода
Операционная семантика аннотированных Reflex программ
Get PDFReflex is a process-oriented language that provides a design of easy-to-maintain control software for programmable logic controllers. The language has been successfully used in a several reliability critical control systems, e. g. control software for a silicon single crystal growth furnace and electronic equipment control system. Currently, the main goal of the Reflex language project is to develop formal verification methods for Reflex programs in order to guarantee increased reliability of the software created on its basis. The paper presents the formal operational semantics of Reflex programs extended by annotations describing the formal specification of software requirements as a necessary basis for the application of such methods. A brief overview of the Reflex language is given and a simple example of its use – a control program for a hand dryer – is provided. The concepts of environment and variables shared with the environment are defined that allows to disengage from specific input/output ports. Types of annotations that specify restrictions on the values of the variables at program launch, restrictions on the environment (in particular, on the control object), invariants of the control cycle, pre- and postconditions of external functions used in Reflex programs are defined. Annotated Reflex also uses standard annotations assume, assert and havoc. The operational semantics of the annotated Reflex programs uses the global clock as well as the local clocks of separate processes, the time of which is measured in the number of iterations of the control cycle, to simulate time constraints on the execution of processes at certain states. It stores a complete history of changes of the values of shared variables for a more precise description of the time properties of the program and its environment. Semantics takes into account the infinity of the program execution cycle, the logic of process transition management from state to state and the interaction of processes with each other and with the environment. Extending the formal operational semantics of the Reflex language to annotations simplifies the proof of the correctness of the transformation approach to deductive verification of Reflex programs developed by the authors, transforming an annotated Reflex program to an annotated program in a very limited subset of the C language, by reducing a complex proof of preserving the truth of program requirements during the transformation to a simpler proof of equivalence of the original and the resulting annotated programs with respect to their operational semantics.Reflex — процесс-ориентированный язык, который обеспечивает разработку простого в обслуживании управляющего программного обеспечения для программируемых логических контроллеров. Язык был успешно использован в нескольких системах управления с повышенными требованиями к надежности, например, в системе управления печью для выращивания монокристаллов кремния и в комплексе контроля радиоэлектронной аппаратуры. В настоящее время основной целью языкового проекта Reflex является разработка методов формальной верификации для Reflex программ для того, чтобы гарантировать повышенную надежность создаваемого на его основе программного обеспечения. В статье представлена формальная операционная семантика Reflex программ, расширенных аннотациями, описывающими формальную спецификацию программных требований, как необходимый базис для применения таких методов. Дан краткий обзор языка Reflex и приведен простой пример его использования — управляющая программа для сушилки рук. Определены понятия окружения и переменных, разделяемых с окружением, позволяющие абстрагироваться от конкретных портов ввода/вывода. Определены типы аннотаций, задающие ограничения на значения переменных при запуске программы, ограничения на окружение (в частности, на объект управления), инварианты цикла управления, пред- и постусловия внешних функций, используемых в Reflex программах. Аннотированный Reflex также использует стандартные аннотации assume, assert и havoc. Операционная семантика аннотированных Reflex программ использует глобальные часы и локальные часы отдельных процессов, время которых измеряется в количестве итераций цикла управления, для моделирования временных ограничений на исполнение процессов в определенных состояниях. Она хранит полную историю изменений значений разделяемых переменных для более полного описания временных свойств программы и ее окружения. Семантика учитывает бесконечность цикла выполнения программы, логику управления переходами процессов из состояния в состояние и взаимодействие процессов между собой и с окружением. Расширение формальной операционной семантики языка Reflex на аннотации упрощает доказательство корректности разрабатываемого авторами трансформационного подхода к дедуктивной верификации Reflex программ, трансформирующего аннотированную Reflex программу к аннотированной программе на сильно ограниченном подмножестве языка C, за счет сведения сложного доказательства сохранения истинности требований к программе при трансформации к более простому доказательству эквивалентности исходной и результирующей аннотированных программ относительно их операционных семантик
Об обнаружении атак типа повторного использования исполнимого кода
Get PDFWhen exploiting software vulnerabilities such as buffer overflows, code reuse techniques are often used today. Such attacks allow you to bypass the protection against the execution of code in the stack, which is implemented at the software and hardware level in modern information systems. At the heart of these attacks lies the detection, in the vulnerable program of suitable areas, of executable code — gadgets — and chaining these gadgets into chains. The article proposes a way to protect applications from attacks that use code reuse. For this purpose, features that distinguish the chains of gadgets from typical chains of legal basic blocks of the program are highlighted. The appearance of an atypical chain of the base block during program execution may indicate the execution of a malicious code. An algorithm for identifying atypical chains has been developed. A feature of the algorithm is that it is focused on identifying all currently known techniques of re-execution of the code. The developed algorithm is based on a modified QEMU virtualization system. One of the hallmarks of the chain of gadgets is the execution at the end of the chain of instructions of the processor used to call the function of the operating system. For the Linux operating system based on the x86/64 architecture, experiments have been conducted showing the importance of this feature in detecting the execution of the malicious code.При эксплуатации уязвимостей программного обеспечения типа переполнения буфера в настоящее время часто используется техника повторного использования кода. Такие атаки позволяют обходить защиту от исполнения кода в стеке, реализуемую на программно-аппаратном уровне в современных информационных системах. В основе атак лежит нахождение в уязвимой программе подходящих участков исполнимого кода - гаджетов - и сцепление этих гаджетов в цепочки. В статье предлагается способ защиты приложений от атак, использующих повторное использование кода. Способ основан на выделении свойств, которые позволяют отличить цепочки гаджетов от типичных цепочек легальных базовых блоков программы. Появление во время выполнения программы нетипичной цепочки базовых блоков может свидетельствовать о выполнении вредоносного кода. Одним из свойств цепочки гаджетов является исполнение в конце цепочки специальной инструкции процессора, используемой для вызова функции операционной системы. Для операционной системы Linux на базе архитектуры x86/64 проведены эксперименты, показывающие важность этого свойства при выявлении исполнения вредоносного кода. Разработан алгоритм выявления нетипичных цепочек, который позволяет выявлять все известные на настоящий момент техники повторного использования кода
Линейная интерполяция на евклидовом шаре в Rⁿ
Get PDFFor x^{(0)}\in{\mathbb R}^n, R>0, by we denote a Euclidean ball in given by the inequality , . Put . We mean by the space of continuous functions with the norm and by the set of polynomials in variables of degree , i.e. linear functions on . Let be the vertices of -dimensional nondegenerate simplex . The interpolation projector corresponding to is defined by the equalities Denote by the norm of as an operator from into . Let us define as minimal value of under the condition . In the paper, we obtain the formula to compute making use of , , and coefficients of basic Lagrange polynomials of . In more details we study the case when is a regular simplex inscribed into . In this situation, we prove that where and integer has the form For this projector, . The equality takes place if and only if is an integer number. We give the precise values of for . To supplement theoretical results we present computational data. We also discuss some other questions concerning interpolation on a Euclidean ball.Пусть x^{(0)}\in{\mathbb R}^n, R>0. Через обозначим евклидов шар в , задаваемый неравенством , . Положим . Под будем понимать пространство непрерывных функций с нормой под - совокупность многочленов от переменных степени , то есть линейных функций на . Пусть - вершины - мерного невырожденного симплекса . Интерполяционный проектор , соответствующий , определяется равенствами Через обозначим норму как оператора из в . Определим как минимальную величину при условии . В статье получена формула для вычисления через , и коэффициенты базисных многочленов Лагранжа, соответствующих Более подробно исследован случай, когда - правильный симплекс, вписанный в . Доказано, что в этой ситуации справедливо равенство где , целое имеет вид Для такого проектора , причём равенство имеет место тогда и только тогда, когда число является целым. Приводятся точные значения для . Даются результаты компьютерных вычислений, дополняющие теоретический анализ. Обсуждаются некоторые другие вопросы, связанные с интерполяцией на евклидовом шаре, в том числе открытые