Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Новый подход к обнаружению и устранению аномалий в политике безопасности внешнего модуля межсетевого экрана контроллера ПКС Floodlight
No full textIn this paper, the authors analyze the developed PreFirewall network application for the Floodlight software defined network (SDN) controller. This application filters rules, which are added into the firewall module of the Floodlight SDN controller in order to prevent the occurrence of anomalies among them. The rule filtering method is based on determining whether the addition of a new rule will not cause any anomalies with already added ones. If an anomaly was detected while adding the new rule, PreFirewall application should be able to resolve it and must report the detection of the anomaly. The developed network application PreFirewall passed a number of tests. As a result of the stress testing, it was found that the time of adding a new rule, when using PreFirewall, substantially increases with increase in the number of previously processed rules. Analysis of the network application PreFirewall showed that while adding a rule (the most frequent operation), in the worst case it is necessary to compare it with all existing rules, which are stored as a two-dimensional array. Thus, the operation of adding a new rule is the most time-consuming and has the greatest impact on the performance of the network application, which leads to an increase in response time. A possible way to of solving this problem is to select a data structure used to store the rules, in which the operation of adding a new rule would be simple. After analyzing the structure of the policy rules for the Floodlight SDN controller, the authors noted that a tree is the most adequate data structure for its storage. It provides optimization of memory used for storing the rules and, more important, it allows to achieve the constant complexity of the operation of adding a new rule and, consequently, solving the performance problem of the network application PreFirewall. The article is published in the authors’ wording.Авторы рассматривают разработанное сетевое приложение PreFirewall для контроллера программно-конфигурируемой сети (ПКС) Floodlight. Данное сетевое приложение осуществляет фильтрацию устанавливаемых правил в модуль ядра firewall контроллера Floodlight с целью недопущения возникновения аномалий между устанавливаемыми правилами. Разработанное сетевое приложение PreFirewall прошло ряд тестов. В результате проведенного нагрузочного тестирования было установлено, что время добавления новых правил, при использовании PreFirewall, серьезно возрастает с ростом количества ранее обработанных правил. Анализ сетевого приложения PreFirewall показал, что при добавлении правила (самая частая операция), в худшем случае необходимо произвести его сравнение со всеми существующими правилами, которые хранятся в виде двумерного массива. Таким образом, операция добавления нового правила является наиболее трудоемкой и сильнее всего влияет на производительность сетевого приложения, что приводит к возрастанию времени его отклика. Одним из возможных путей решения данной проблемы является выбор такой структуры данных, используемой для хранения правил, в которой операция добавления нового правила была бы простой. В качестве такой структуры предлагается использование дерева, каждая вершина которого содержит всевозможные значения полей в устанавливаемых правилах. Данный подход обеспечивает константную сложность операции добавления нового правила и, следовательно, решает проблему производительности сетевого приложения PreFirewall. Статья публикуется в авторской редакции
Периодические изменения автоволнового фронта в двумерной системе параболических уравнений
Get PDFThe work is aimed to study front solutions of a nonlinear system of parabolic equations in a two-dimensional region. The system can be considered as a mathematical model describing an abrupt change in physical characteristics of spatially heterogeneous media. We consider a system with small parameters raised to the different powers at a differential operator, that represents the difference of typical processes speeds for the system components. The study of the system is conducted by using the contrast structures theory methods, which allowed us to obtain conditions for the existence of front solutions contained in the neighborhood of a closed curve, to determine the front velocity depending on time and coordinate along the front curve, and to obtain the zero-order and the first-order terms of the asymptotic approximation to the solution. The scope of the system includes the description of autowave solutions in the field of ecology, biophysics, combustion physics and chemical kinetics. The approximate solution allows us to choose the model parameters so that the result corresponds to the processes observed, to explain and describe the characteristics of the solutions with sharp gradients, to create models with stable solutions and thereby to simplify the numerical analysis. Note that the numerical experiment for the two-dimensional spatial models requires a considerable amount of processing power and the use of parallel computing techniques and does not allow to effectively analyze and modify the model. In this paper, we obtain the asymptotic approximation that is to be justified, which can be done by the method of differential inequalities. Работа направлена на исследование решений типа фронта для нелинейной системы параболических уравнений в двумерной области. Систему можно рассматривать как математическую модель, описывающую резкое изменение физических характеристик в пространственно неоднородных средах. Система уравнений содержит малые параметры в разных степенях при дифференциальном операторе, что означает различие характерных скоростей протекания процессов для каждой из компонент. Исследование проведено с помощью методов теории контрастных структур, что позволило получить условия существования решения типа фронта, локализованного в окрестности замкнутой кривой, определить зависимость скорости фронта от времени, получить асимптотическое приближение решения нулевого и первого порядков по малому параметру. Приближенное решение позволяет подобрать параметры модели таким образом, чтобы результат соответствовал наблюдаемым процессам, объяснять и описывать особенности решений с резкими градиентами, создавать модели, обладающие устойчивыми решениями, тем самым облегчая задачу получения численных результатов. Известно, что численный эксперимент для пространственно двумерных моделей требует значительных вычислительных мощностей, применения методов параллельного программирования и не позволяет эффективно анализировать и модифицировать модели. В данной работе получено асимптотическое приближение решения, требующее обоснования, которое может быть проведено по методу дифференциальных неравенств. Метод дифференциальных неравенств в данном случае предполагает построение верхнего и нижнего решений задачи на основе асимптотики. Область применения математической модели – описание автоволновых решений в задачах экологии, биофизики, физики горения, химической кинетики
Платформенно-независимая спецификация и верификация стандартной математической функции квадратного корня
Get PDFThe project “Platform-independent approach to formal specification and verification of standard mathematical functions” is aimed onto the development of incremental combined approach to specification and verification of standard Mathematical functions like sqrt, cos, sin, etc. Platform-independence means that we attempt to design a relatively simple axiomatization of the computer arithmetics in terms of real arithmetics (i.e. the field of real numbers) but do not specify neither base of the computer arithmetics, nor a format of numbers representation. Incrementality means that we start with the most straightforward specification of the simplest case to verify the algorithm in real numbers and finish with a realistic specification and a verification of the algorithm in computer arithmetics. We call our approach combined because we start with manual (pen-and-paper) verification of the algorithm in real numbers, then use this verification as proof-outlines for a manual verification of the algorithm in computer arithmetics, and finish with a computer-aided validation of the manual proofs with a proof-assistant system (to avoid appeals to “obviousness” that are common in human-carried proofs). In the paper, we apply our platform-independent incremental combined approach to specification and verification of the standard Mathematical square root function. Currently a computer-aided validation was carried for correctness (consistency) of our fix-point arithmetics and for the existence of a look-up table with the initial approximations of the square roots for fix-point numbers.Цель проекта “Платформенно-независимый подход к формальной спецификации и верификации стандартных математических функций” --- инкрементальный комбинированный подход к спецификации и верификации стандартных математических функций, таких как sqrt, cos, sin и так далее. Платформенно-независимый подход предполагает простую аксиоматизацию машинной арифметики в терминах вещественной арифметики (то есть арифметики поля вещественных чисел), не фиксируя ни основание системы счисления, ни формат машинного слова. Инкрементальность означает, что спецификация и верификация начинается с рассмотрения наиболее “простого” случая – элементарной спецификации и верификации простого алгоритма, работающего с вещественными числами, а заканчивается модификацией элементарной спецификации и алгоритма для машинной арифметики и верификацией алгоритма, работающего в машинной арифметике. А комбинированность подхода означает, что мы начинаем с рассмотрения “базового случая” --- “ручной” верификации (с ручкой и бумагой) для алгоритма, работающего в вещественной арифметике, затем выполняем ручную верификацию алгоритма, работающего в машинной арифметике, используя верификацию для базового случая в качестве “конспекта” (proof-outlines), а заканчиваем --- верификацией с использованием автоматизированной системы построения/поиска доказательства для того, чтобы исключить апелляцию к “очевидности” в ручной верификации. В статье платформенно-независимый инкрементальный комбинированный подход применяется для спецификации и верификации стандартной математической функции квадратного корня. В настоящий момент автоматизированная верификация разработанных алгоритмов выполнена только частично: с использованием системы ACL2 доказана реализуемость (существование) чисел с фиксированной запятой и таблицы начальных приближений квадратного корня
О рекурсивно-параллельном алгоритме решения задачи о рюкзаке
Get PDFIn this paper, we offer an efficient parallel algorithm for solving the NP-complete Knapsack Problem in its basic, so-called 0-1 variant. To find its exact solution, algorithms belonging to the category ”branch and bound methods” have long been used. To speed up the solving with varying degrees of efficiency, various options for parallelizing computations are also used. We propose here an algorithm for solving the problem, based on the paradigm of recursive-parallel computations. We consider it suited well for problems of this kind, when it is difficult to immediately break up the computations into a sufficient number of subtasks that are comparable in complexity, since they appear dynamically at run time. We used the RPM ParLib library, developed by the author, as the main tool to program the algorithm. This library allows us to develop effective applications for parallel computing on a local network in the .NET Framework. Such applications have the ability to generate parallel branches of computation directly during program execution and dynamically redistribute work between computing modules. Any language with support for the .NET Framework can be used as a programming language in conjunction with this library. For our experiments, we developed some C# applications using this library. The main purpose of these experiments was to study the acceleration achieved by recursive-parallel computing. A detailed description of the algorithm and its testing, as well as the results obtained, are also given in the paper.Предлагается эффективный параллельный алгоритм решения NP-полной задачи о рюкзаке в ее исходном, так называемом 0-1 варианте. Для нахождения ее точного решения издавна применяются алгоритмы, относящиеся к категории "методов ветвей и границ". Для ускорения получения результата с разной степенью эффективности применяются также различные варианты организации параллельных вычислений. Мы предлагаем здесь алгоритм решения задачи, основанный на парадигме рекурсивно-параллельных вычислений. Он представляется нам хорошо пригодным для задач такого рода, когда трудно сразу разбить вычисления на достаточное количество сравнимых по трудоемкости подзадач, поскольку она проявляется динамически во время вычислений. В качестве основного инструмента для программной реализации алгоритма использовалась разработанная автором библиотека RPM_ParLib, позволяющая создавать эффективные приложения для вычислений на локальной сети в среде .NET Framework. Такие приложения обладают способностью порождать параллельные ветви вычислений непосредственно во время выполнения программы и динамически перераспределять работу между вычислительными модулями. При этом в качестве языка программирования может использоваться любой язык с поддержкой .NET Framework. Для проведения экспериментов было написано несколько программ на языке C# с использованием упомянутой библиотеки. Основной целью этих экспериментов было исследование ускорения, достигаемого за счет рекурсивно-параллельной организации вычислений. Подробное описание алгоритма и эксперимента, а также полученные результаты приводятся в работе.
Особенности локальной динамики модели оптико-электронного осциллятора с запаздыванием
Get PDFWe consider electro-optic oscillator model which is described by a system of the delay differential equations (DDE). The essential feature of this model is a small parameter in front of a derivative that allows us to draw a conclusion about the action of processes with different order velocities. We analyse the local dynamics of a singularly perturbed system in the vicinity of the zero steady state. The characteristic equation of the linearized problem has an asymptotically large number of roots with close to zero real parts while the parameters are close to critical values. To study the existent bifurcations in the system, we use the method of the behaviour constructing special normalized equations for slow amplitudes which describe of close to zero original problem solutions. The important feature of these equations is the fact that they do not depend on the small parameter. The root structure of characteristic equation and the supercriticality order define the kind of the normal form which can be represented as a partial differential equation (PDE). The role of the ”space” variable is performed by ”fast” time which satisfies periodicity conditions. We note fast response of dynamic features of normalized equations to small parameter fluctuation that is the sign of a possible unlimited process of direct and inverse bifurcations. Also, some obtained equations possess the multistability feature. В работе рассматривается модель оптико-электронного осциллятора, описываемая системой дифференциальных уравнений с запаздыванием. Существенной особенностью данной модели является наличие малого параметра перед одной из производных, что позволяет сделать вывод о действии процессов со скоростями разных порядков. Анализируется локальная динамика сингулярно возмущенной системы в окрестности нулевого состояния равновесия. Характеристическое уравнение линеаризованной задачи при значениях параметров, близких к критическим, имеет асимптотически большое число корней с близкой к нулю вещественной частью. Для изучения происходящих в системе бифуркаций используется метод построения специальных нормализованных уравнений для медленных амплитуд, которые описывают поведение близких к нулю решений исходной задачи. Важной особенностью этих уравнений является то, что от малого параметра они не зависят. Структура корней характеристического уравнения и порядок надкритичности определяют вид нормальной формы, которая может быть представлена уравнением в частных производных. В роли «пространственной» переменной выступает «быстрое» время, для которого выполняются условия периодичности. Отмечается высокая чувствительность динамических свойств нормализованных уравнений к изменению малого параметра, что является признаком возможного неограниченного процесса прямых и обратных бифуркаций. Также некоторые построенные уравнения обладают свойством мультистабильности
Даже простые процессы π-исчисления трудны для анализа
Get PDFMathematical models of distributed computations, based on the calculus of mobile processes (π-calculus) are widely used for checking the information security properties of cryptographic protocols. Since π-calculus is Turing-complete, this problem is undecidable in general case. Therefore, the study is carried out only for some special classes of π-calculus processes with restricted computational capabilities, for example, for non-recursive processes, in which all runs have a bounded length, for processes with a bounded number of parallel components, etc. However, even in these cases, the proposed checking procedures are time consuming. We assume that this is due to the very nature of the π -calculus processes. The goal of this paper is to show that even for the weakest model of passive adversary and for relatively simple protocols that use only the basic π-calculus operations, the task of checking the information security properties of these protocols is co-NP-complete.Математические модели распределенных вычислений, построенные на основе исчисления мобильных процессов (-исчисления), широко используются для проверки свойств информационной безопасности криптографических протоколов. Поскольку -исчисление является полной по Тьюрингу моделью вычислений, эта задача в общем случае алгоритмически неразрешима. Поэтому ее исследование проводится лишь для некоторых специальных классов процессов -исчисления с ограниченными вычислительными возможностями, например, для нерекурсивных процессов, в которых все вычисления имеют ограниченную длину, для процессов с ограниченным числом параллельных компонентов и др. Однако и в этих случаях предложенные разрешающие алгоритмы оказываются весьма трудоемкими. Мы полагаем, что это обусловлено самой природой процессов -исчисления. Цель данной работы — показать, что даже для наиболее слабой модели пассивного противника и для сравнительно простых протоколов, в которых используются лишь базовые операции -исчисления, задача проверки свойств информационной безопасности этих протоколов является co-NP-полной
Верхнее и нижнее решения для системы уравнений типа ФицХью–Нагумо
Get PDFWe consider a moving front solution of a singularly perturbed FitzHugh–Nagumo type system of equations. The solution contains an internal transition layer, that is, a subdomain where a sharp change in the values of the functions describing the solution occurs. In initial-boundary value problems with moving front solutions, there naturally exists a small parameter that is equal to the ratio of the inner transition layer width to the width of the considered region. Taking into account this small parameter leads to the fact that the equations become singularly perturbed, thus the problems are classified as ”hard”, the numerical solution of which meets certain difficulties and does not always give a reliable result. In connection with this, the role of an analytical investigation of the existence of a solution with an internal transition layer increases. For these purposes the use of differential inequalities method is especially effective. The method consists in constructing continuous functions, which are called upper and lower solutions. An important role is played by the so-called ”quasimonotonicity condition” for functions which describe reactive terms. In this paper, we present an algorithm for constructing the upper and the lower solutions of a parabolic system with a single-scale internal transition layer. It should be mentioned that the quasimonotonicity condition in the present paper differs from the analogous condition in previous publications. The above algorithm can be further generalized to more complex systems with two-scale transition layers or to systems with discontinuous reactive terms. The study is of great practical importance for creating mathematically grounded models in biophysics. Рассматривается решение вида движущегося фронта сингулярно возмущенной системы уравнений типа ФицХью–Нагумо. Решение содержит внутренний переходный слой, то есть подобласть где происходит резкое изменение значений функций, описывающих решение. В начально-краевых задачах с решениями вида фронтов содержится естественный малый параметр, равный отношению ширины внутреннего переходного слоя к ширине рассматриваемой области. Учет малого параметра приводит к тому, что уравнения становятся сингулярно возмущенными, тем самым задачи относятся к разряду «жестких», численное решение которых встречает определенные трудности и не всегда дает достоверный результат. В связи с этим возрастает роль аналитического исследования таких задач и доказательства существования решения с внутренним переходным слоем. В этих целях особо эффективным является использование метода дифференциальных неравенств, который состоит в построении непрерывных функций, называемых верхним и нижним решениями. При этом важную роль играет так называемое «условие квазимонотонности» функций, описывающих реактивные слагаемые. В настоящей работе приведен алгоритм построения верхнего и нижнего решений системы параболических уравнений с одномасштабным внутренним переходным слоем, при этом условие квазимонотонности отличается от аналогичного условия в ранее опубликованных работах. Приведенный алгоритм может быть в дальнейшем обобщен на более сложные системы с двухмасштабными переходными слоями или на системы с разрывными реактивным слагаемыми. Подобные исследования имеют важное практическое значение для создания математически обоснованных моделей биофизики
Oб оптимальной интерполяции линейными функциями на n-мерном кубе
Get PDFLet , and let be the unit cube . By we denote the space of continuous functions with the norm by --- the set of polynomials of variables of degree (or linear functions). Let be the vertices of -dimnsional nondegenerate simplex . An interpolation projector corresponding to the simplex is defined by equalities The norm of as an operator from to may be calculated by the formula Here are the basic Lagrange polynomials with respect to is the set of vertices of . Let us denote by the minimal possible value of Earlier, the first author proved various relations and estimates for values and , in particular, having geometric character. The equivalence takes place. For example, the appropriate, according to dimension , inequalities may be written in the form \linebreak <\theta_n <3\sqrt{n}. If the nodes of the projector coincide with vertices of an arbitrary simplex with maximum possible volume, we have When an Hadamard matrix of order exists, holds In the paper, we give more precise upper bounds of numbers for . These estimates were obtained with the application of maximum volume simplices in the cube. For constructing such simplices, we utilize maximum determinants containing the elements Also, we systematize and comment the best nowaday upper and low estimates of numbers for a concrete Пусть , . Через обозначим пространство непрерывных функций с нормой через - совокупность многочленов от переменных степени (или линейных функций). Пусть --- вершины -мерного невырожденного симплекса . Интерполяционный проектор , соответствующий симплексу , определяется равенствами Норма как оператора из в может быть вычислена по формуле Здесь - базисные многочлены Лагранжа, соответствующие - совокупность вершин . Через обозначим минимальную величину Ранее первым автором были доказаны различные соотношения и оценки для величин и , в том числе имеющие геометрический характер.Справедлива эквивалентность Подходящими по размерности неравенствами являются, например, \frac{1}{4}\sqrt{n}<\theta_n<3\sqrt{n}. Для проектора , узлы которого совпадают с вершинами произвольного симплекса максимального объёма в~кубе, выполняется Если существует матрица Адамара порядка , то В настоящей статье приводятся уточнённые верхние границы чисел для , полученные с применением симплексов максимального объёма в~кубе. Для построения этих симплексов применяются максимальные определители, элементы которых равны Мы также систематизируем и комментируем лучшие на настоящий момент верхние и нижние оценки чисел для конкретных \(n.\
Решения уравнений нестационарного фронта реакции с вырожденными точками равновесия
Get PDFWe consider a nonstationary process of spreading some substance in a one-dimensional spatially inhomogeneous system of cells. It is assumed that a change in the concentration of in a cell with the number with time is determined by the difference in concentration in this cell and in its two neighbors on the left and on the right, as well as the source density, which depends on and depends on . Such a model leads to the initial-boundary value problem for the differentialdifference equation (differentiation with respect to t variable, the difference expression with respect to ). With a sufficiently small difference in concentration in each pair of neighboring cells we can replace the difference expression by the second partial derivative with respect to the spatial coordinate, and describe the propagation by the reaction-diffusion equation. This equation belongs to the class of quasilinear parabolic equations. It is assumed that the density of the sources vanishes (with changing the sign) at three values of the concentration, two of which, lower and upper, are stable. There is also an intermediate unstable state with zero source density, in which the sign reversal also takes place. The peculiarity of our model is that we assume, that two extreme roots of the source density function are degenerate (with an integer or fractional exponent). We intend to show analytically and by the computer simulation, that this model leads to the fact, that the rate of asymptotic aspiration of concentration to equilibrium values for a moving front becomes power-law instead of exponential, which takes place for standard models. In the paper, we have constructed a formal asymptotics solution of the initialboundary value problem for the reaction-diffusion equation in a homogeneous medium with a power-law dependence of the source density on the temperature, an upper and lower solutions are constructed, a rigorous justification of the formal asymptotics is given. Precise solutions of the diffusion reaction equation are constructed for a wide class of source density functions.Мы рассматриваем нестационарный процесс распространения некоторой субстанции в одномерной среде с диффузией и источниками, плотность которых зависит от концентрации (так для определенности будем называть исследуемую величину). Предполагается, что изменение концентрации в данной точке со временем определяется разностью потоков слева и справа, а также плотностью источников, которая зависит от и от . Такая модель приводит к начально-краевой задаче для квазилинейного уравнения параболического типа, которое называют уравнением реакции–диффузии. В частности, наша модель пригодна для описания нестационарного процесса передачи информации в одномерной системе объектов, которые могут быть описаны величиной, характеризующей степень информированности о некотором событии. Предполагается, что плотность источников обращается в нуль (меняя знак) при трех значениях концентрации, два из которых (крайние) являются устойчивыми, имеется еще промежуточное неустойчивое состояние с нулевой плотностью источников, в котором тоже имеет место перемена знака. Особенность нашей модели состоит в том, что мы предполагаем, что два крайних корня функции плотности источников являются вырожденными (с целым или дробным показателем, большим единицы). Такая модель соответствует ситуации, при которой плотность источников в окрестности стационарного значения концентрации является бесконечно малой величиной более высокого порядка, чем для стандартной модели, в которой эта величина имеет первый порядок малости. Мы намерены показать аналитически и методом компьютерного моделирования, что данная модель приводит к тому, что скорость асимптотического стремления концентрации к равновесным значениям для движущегося фронта становится степенной вместо экспоненциальной, имеющей место для стандартных моделей. Построена формальная асимптотика решения начально-краевой задачи в однородной среде со степенной зависимостью плотности источников от концентрации, построены верхнее и нижнее решения, дано строгое обоснование формальной асимптотики. Построены точные решения уравнения реакции–диффузии для широкого класса функций плотности источников
Элиминация инвариантов финитных итераций над массивами при верификации Си программ
No full textThis work represents the further development of the method for definite iteration verification [7]. It extends the mixed axiomatic semantics method [1] suggested for C-light program verification. This extension includes a verification method for definite iteration over unchangeable arrays with a loop exit in C-light programs. The method includes an inference rule for the iteration without invariants, which uses a special function that expresses loop body. This rule was implemented in verification conditions generator, which is the part of our C-light verification system. To prove generated verification conditions an induction is applied which is a challenge for SMT-solvers. At proof stage the SMT-solver CVC4 is used in our verification system. To overcome mentioned difficulty a rewriting strategy for verification conditions is suggested. A method based on theory extension by new theorems to prove verification conditions is suggested. An example, which illustrates the application of these methods, is considered. The article is published in the authors’ wording. Данная работа представляет дальнейшее развитие метода верификации финитной итерации [7]. Он расширяет метод смешанной аксиоматической семантики [1], предложенный для верификации C-light программ. Это расширение включает метод верификации для финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Данное правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности применяется метод математической индукции, вызывающий сложности у SMT-решателей. В нашей системе верификации на стадии доказательства используется SMT-решатель CVC4. Для преодоления упомянутой трудности применяется стратегия переписывания условий корректности. Для доказательства условий корректности предложен метод, основанный на расширении теории новыми теоремами. Рассмотрен пример, иллюстрирующий применение данных методов. Статья публикуется в авторской редакции.