Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Разработка и исследование алгоритмов формирования правил для узлов сетевой безопасности в мультиоблачной платформе
Get PDFAs part of the study, existing solutions aimed at ensuring the security of the network perimeter of the multi-cloud platform were considered. It is established that the most acute problem is the effective formation of rules on firewalls. Existing approaches do not allow optimizing the list of rules on nodes that control access to the network. The aim of the study is to increase the effectiveness of firewall tools by conflict-free optimization of security rules and the use of a neural network approach in software-defined networks. The proposed solution is based on the sharing of intelligent mathematical approaches and modern technologies of virtualization of network functions. In the course of experimental studies, a comparative analysis of the traditional means of rule formation, the neural network approach, and the genetic algorithm was carried out. It is recommended to use the multilayer perceptron neural network classifier for automatic construction of network security rules since it gives the best results in terms of performance. It is also recommended to reduce the size of the firewall security rule list using the Kohonen network, as this tool shows the best performance. A conflict-free optimization algorithm was introduced into the designed architecture, which produces finite optimization by ranking and deriving the most common exceptions from large restrictive rules, which allows increasing protection against attacks that are aimed at identifying security rules at the bottom of the firewall list. On the basis of the proposed solution, the adaptive firewall module was implemented as part of the research.В рамках исследования рассмотрены существующие решения, направленные на обеспечение безопасности сетевого периметра мультиоблачной платформы. Установлено, что наиболее острой является проблема эффективного формирования правил на межсетевых экранах. Существующие подходы не позволяют оптимизировать список правил на узлах, контролирующих доступ к сети. Целью исследования является повышение эффективности средств межсетевого экрана путем бесконфликтной оптимизации правил безопасности и применения нейросетевого подхода в программно-определяемых сетях. Предлагаемое решение основано на совместном использовании интеллектуальных математических подходов и современных технологий виртуализации сетевых функций. В ходе экспериментальных исследований проведен сравнительный анализ традиционных средств формирования правил, нейросетевого подхода, а также генетического алгоритма. Для автоматического построения правил сетевой безопасности рекомендуется применять нейросетевой классификатор архитектуры «многослойный персептрон», поскольку он даёт лучшие результаты с точки зрения производительности, и уменьшать размерность списка правил безопасности межсетевого экрана при помощи сети Кохонена, поскольку это средство показывает лучшую производительность. В спроектированную архитектуру был внедрен алгоритм бесконфликтной оптимизации, который производит конечную оптимизацию путем ранжирования и выведения наиболее часто встречаемых исключений из больших запретительных правил, что позволяет увеличить защиту от атак, которые направлены на выявление правил безопасности, находящихся внизу списка межсетевого экрана. На базе предложенного решения в рамках исследования реализован модуль адаптивного межсетевого экрана
Анализ условий возникновения пространственно-неоднородных структур световых волн в оптических системах передачи информации
Get PDFA model of distributed information carriers in the form of stable spatially inhomogeneous structures in optical and fiber-optic communication systems is considered. We study the conditions for the occurrence of such stable spatially inhomogeneous structures of the light wave of the generator of optical radiation. The formation of inhomogeneous structures that occur in a plane orthogonal to the direction of wave propagation is provided by a thin layer of nonlinear medium and a two-dimensional lagging feedback loop with the rotation operator of the spatial coordinates of the light wave in the emission plane of the optical generator. In the space of the main parameters of the generator (a control parameter, the angle of rotation of the spatial coordinates, the magnitude of the delay), the areas of generation of stable spatially inhomogeneous structures are constructed, the mechanisms of their occurrence are analyzed.Рассматривается модель распределенных носителей информации в виде устойчивых пространственно-неоднородных структур в системах оптической и волоконно-оптической связи. Изучаются условия возникновения таких устойчивых пространственно-неоднородных структур световой волны генератора оптического излучения. Образование неоднородных структур, которые возникают в плоскости, ортогональной направлению распространения волны, обеспечивается тонким слоем нелинейной среды и контуром двумерной запаздывающей обратной связи с оператором поворота пространственных координат световой волны в плоскости излучения оптического генератора. В пространстве основных параметров генератора (управляющий параметр, угол поворота пространственных координат, величина запаздывания) построены области генерации устойчивых пространственно-неоднородных структур, был проведен анализ механизмов их возникновения
Сравнение диффеоморфных изображений на основе формирования персистентных гомологий
Get PDFAn object shape analysis is a problem that is related to such areas as geometry, topology, image processing and machine learning. For analyzing the form, the deformation between the source and terminal form of the object is estimated. The most used form analysis model is the Large Deformation Diffeomorphic Metric Mapping (LDDMM) model. The LDDMM model can be supplemented with functional non-geometric information about objects (volume, color, formation time). The paper considers algorithms for constructing sets of barcodes for comparing diffeomorphic images, which are real values taken by persistent homology. A distinctive feature of the use of persistent homology with respect to methods of algebraic topology is to obtain more information about the shape of the object. An important direction of the application of persistent homology is the study invariants of big data. A method based on persistent cohomology is proposed that combines persistent homology technologies with embedded non-geometric information presented as functions of simplicial complexes. The proposed structure of extended barcodes using cohomology increases the effectiveness of persistent homology methods. A modification of the Wasserstein method for finding the distance between images by introducing non-geometric information was proposed. The possibility of the formation of barcodes of images invariant to transformations of rotation, shift and similarity is considered. Анализ формы объекта – проблема, которая связана такими областями, как геометрия, топология, обработка изображений, машинное обучение или вычислительная анатомия. При анализе формы оценивается деформация между исходной и терминальной формой объекта. Наиболее используемой моделью анализа формы является модель диффеоморфного метрического отображения больших деформаций (Large Deformation Diffeomorphic Metric Mapping – LDDMM). Модель LDDMM может быть дополнена функциональной негеометрической информацией объектов (объем, цвет, момент времени формирования). В работе рассмотрены алгоритмы построения множеств баркодов для сравнения диффеоморфных изображений, которые являются вещественными значениями, принимаемыми персистентными гомологиями. Отличительной особенностью использования персистентных гомологий по отношению к методам алгебраической топологии является получение большего количества информации о форме объекта. Важным направлением применения персистентных гомологий является изучение инвариантов больших объемов данных. Предлагается метод, основанный на персистентных когомологиях, который объединяет технологии персистентных гомологий с внедренной негеометрической информацией, представленной в виде функций от симплициальных комплексов. Предлагаемая структура расширенных баркодов с использованием когомологий повышает эффективность методов персистентных гомологий. Предложена модификация метода Вассерштейна для нахождения расстояния между изображениями введением негеометрической информации. Рассмотрена возможность формирования баркодов изображений инвариантных к преобразованиям вращения, сдвига и подобия
Новый подход к моделированию генных сетей
Get PDFThe article is devoted to the mathematical modeling of artificial genetic networks. A phenomenological model of the simplest genetic network called repressilator is considered. This network contains three elements unidirectionally coupled into a ring. More specifically, the first of them inhibits the synthesis of the second, the second inhibits the synthesis of the third, and the third, which closes the cycle, inhibits the synthesis of the first one. The interaction of the protein concentrations and of mRNA (message RNA) concentration is surprisingly similar to the interaction of six ecological populations — three predators and three preys. This allows us to propose a new phenomenological model, which is represented by a system of unidirectionally coupled ordinary differential equations. We study the existence and stability problem of a relaxation periodic solution that is invariant with respect to cyclic permutations of coordinates. To find the asymptotics of this solution, a special relay system is constructed. It is proved in the paper that the periodic solution of the relay system gives the asymptotic approximation of the orbitally asymptotically stable relaxation cycle of the problem under consideration.Статья посвящена математическому моделированию искусственных генных сетей. Рассматривается феноменологическая модель простейшей трехзвенной осцилляторной генной сети — так называемого репрессилятора. Эта сеть содержит три элемента, однонаправленно связанных в кольцо. Первый из них ингибирует синтез второго, второй ингибирует синтез третьего, а третий, который замыкает цикл, ингибирует синтез первого. Взаимодействие концентраций белка и концентрации мРНК удивительно похоже на функционирование биоценоза, состоящего из шести экологических популяций — трех хищников и трех жертв. Это позволяет предложить новую феноменологическую модель, которая представлена системой однонаправленно связанных обыкновенных дифференциальных уравнений. В работе изучена задача существования и устойчивости у этой системы релаксационного периодического решения, инвариантного по отношению к циклическим перестановкам координат. Для нахождения асимптотики этого решения строится специальная релейная система. В статье доказывается, что периодическое решение релейной системы дает асимптотическое приближение орбитально асимптотически устойчивого релаксационного цикла рассматриваемой задачи
Анализ эффективности демультиплексирования транспортных потоков
Get PDFIt is known that the demultiplexing of the individual traffic flow into several independent transport subflows can increase the speed of it. This statement is true for a single flow but its truth for the massive case, when demultiplexing technics are applied to all traffic flows in the network of a single Internet Service Provider (ISP), is not obvious. The question arises, what impact the massive demultiplexing of traffic flows will have on the whole ISP network bandwidth. In this paper, this question is considered for the static case, when each flow is demultiplexed statically, i.e. every flow before its launching is demultiplexed into the same number of subflows. We developed a mathematical model that was used to construct a simulation model in order to obtain more accurate estimates of the network performance with and without flow demultiplexing. Using simulation model, network properties are defined, under which the demultiplexing of traffic flows is justified. We proved the correctness of the obtained results by emulating a network load based on a protocol stack virtualization for the same input. We considered various routing policies that can be used for massive demultiplexing. Special attention is paid to algorithms that allow you to build routes with minimal intersections, since using the nonintersecting routes with non-optimal cost can increase the network performance. The routes constructed with these algorithms were used both for the network performance analysis with demultiplexed flows and in the case of balancing non-demultiplexed flows.Известно, что разделение отдельного транспортного потока на несколько независимых транспортных подпотоков может повысить скорость этого потока. Справедливость этого утверждения, верная для одного потока, не очевидна для массового случая, когда демультиплексированию (разделению на подпотоки) подвергают все транспортные потоки в сети одного ISP оператора. Возникает вопрос, какое влияние окажет массовое демультиплексирование транспортных потоков на пропускную способность сети ISP оператора. В статье этот вопрос рассмотрен для статического случая, когда каждый поток разделяется статически, т.е. перед его запуском, на одинаковое число подпотоков. Была предложена математическая модель, на основе которой построена имитационная модель с целью получения более точных оценок производительности сети с демультиплексированием потоков и без него. С помощью имитационной модели определены свойства сети, при которых применение демультиплексирования транспортных потоков оправдано. Корректность полученных результатов обосновывается при помощи эмуляции сети и нагрузки в ней на основе виртуализации стека протоколов при тех же входных данных. В статье рассмотрены разные политики маршрутизации, которые могут быть использованы при массовом демультиплексировании. Особое внимание уделяется алгоритмам, позволяющим строить маршруты с минимальными пересечениями, так как использование неоптимальных по длине, но непересекающихся маршрутов может повысить производительность сети. Маршруты, построенные при помощи этих алгоритмов, использовались как для анализа производительности сети на предложенной имитационной модели с демультиплексированными потоками, так и в случае балансировки недемультиплексированных потоков
eT-сводимость множеств
No full textThis paper is dedicated to the study of eT -reducibility — the most common in the intuitive sense of algorithmic reducibility, which is both enumeration reducibility and decidable one. The corresponding structure of degrees — upper semilattice of eT -degrees is considered. It is shown that it is possible to correctly define the jump operation on it by using the T-jump or e-jump of sets. The local properties of eT -degrees are considered: totality and computably enumerable. It is proved that all degrees between the smallest element and the first jump in DeT are computably enumerable, moreover, these degrees contain computably enumerable sets and only them. The existence of non-total eT -degrees is established. On the basis of it, some results have been obtained on the relations between, in particular, from the fact that every eT -degree is either completely contained in some T -or e-degrees, or completely coincides with it, it follows that non-total e-degrees contained in the T-degrees, located above the second T -jump, coincide with the corresponding non-total eT -degrees.Статья посвящена eT-сводимости - самой общей в интуитивном смысле алгоритмической сводимости, являющейся одновременно сводимостью по перечислимости и сводимостью по разрешимости. Рассматривается соответственная степенная структура - верхняя полурешётка eT-степеней. Показано, что на ней можно корректным образом определить операцию скачка, используя Т -скачок или е-скачок множеств. Рассмотрены локальные свойства eT-степеней: тотальность и перечислимость. Доказано, что все степени между наименьшим элементом и первым скачком в DeT являются вычислимо перечислимыми, более того, эти степени содержат вычислимо перечислимые множества и только их. Установлено существование нетотальных еТ -степеней. На основе этого получены некоторые результаты о соотношениях между степенями, в частности, из того, что всякая eT-степень или содержится полностью в некоторой Т - или е-степени, или полностью совпадает с ней, следует, что нетотальные е-степени, содержащиеся в Т-степенях, расположенных выше второго Т -скачка, совпадают с соответствующими нетотальными еТ -степенями
Комплексный подход системы C-lightVer к автоматизированной локализации ошибок в C-программах
Get PDFThe C-lightVer system for the deductive verification of C programs is being developed at the IIS SB RAS. Based on the two-level architecture of the system, the C-light input language is translated into the intermediate C-kernel language. The meta generator of the correctness conditions receives the C-kernel program and Hoare logic for the C-kernel as input. To solve the well-known problem of determining loop invariants, the definite iteration approach was chosen. The body of the definite iteration loop is executed once for each element of the finite dimensional data structure, and the inference rule for them uses the substitution operation rep, which represents the action of the cycle in symbolic form. Also, in our meta generator, the method of semantic markup of correctness conditions has been implemented and expanded. It allows to generate explanations for unproven conditions and simplifies the errors localization. Finally, if the theorem prover fails to determine the truth of the condition, we can focus on proving its falsity. Thus a method of proving the falsity of the correctness conditions in the ACL2 system was developed. The need for more detailed explanations of the correctness conditions containing the replacement operation rep has led to a change of the algorithms for generating the replacement operation, and the generation of explanations for unproven correctness conditions. Modifications of these algorithms are presented in the article. They allow marking rep definition with semantic labels, extracting semantic labels from rep definition and generating description of break execution condition.В ИСИ СО РАН разрабатывается система C-lightVer для дедуктивной верификации С-программ. Исходя из двухуровневой архитектуры системы, входной язык C-light транслируется в промежуточный язык C-kernel. Метагенератор условий корректности принимает на вход C-kernel программу и логику Хоара для C-kernel. Для решения известной проблемы задания инвариантов циклов выбран подход финитных итераций. Тело цикла финитной итерации исполняется один раз для каждого элемента структуры данных конечной размерности, а правило вывода для них использует операцию замены rep, выражающую действие цикла в символической форме. Также в нашем метагенераторе внедрен и расширен метод семантической разметки условий корректности. Он позволяет порождать пояснения для недоказанных условий и упрощает локализацию ошибок. Наконец, если система ACL2 не справляется с установлением истинности условия, можно сосредоточиться на доказательстве его ложности. Ранее нами был разработан способ доказательства ложности условий корректности для системы ACL2. Необходимость в более подробных объяснениях условий корректности, содержащих операцию замены rep, привела к изменению алгоритмов генерации операции замены, извлечения семантических меток и генерации объяснений недоказанных условий корректности. В статье представлены модификации данных алгоритмов. Эти изменения позволяют пометить исходный код функции rep семантическими метками, извлекать семантические метки из определения rep, а также генерировать описание условия исполнения инструкции break
Доказательство свойств дискретных функций с помощью дедуктивного доказательства: приложение к квадратному корню
No full textFor many years, automotive embedded systems have been validated only by testing. In the near future, Advanced Driver Assistance Systems (ADAS) will take a greater part in the car’s software design and development. Furthermore, their increasing critical level may lead authorities to require a certification for those systems. We think that bringing formal proof in their development can help establishing safety properties and get an efficient certification process. Other industries (e.g. aerospace, railway, nuclear) that produce critical systems requiring certification also took the path of formal verification techniques. One of these techniques is deductive proof. It can give a higher level of confidence in proving critical safety properties and even avoid unit testing.In this paper, we chose a production use case: a function calculating a square root by linear interpolation. We use deductive proof to prove its correctness and show the limitations we encountered with the off-the-shelf tools. We propose approaches to overcome some limitations of these tools and succeed with the proof. These approaches can be applied to similar problems, which are frequent in the automotive embedded software.В течение многих лет автомобильные встраиваемые системы проверялись только тестированием. В ближайшем будущем усовершенствованные системы помощи водителю (ADAS) будут играть большую роль в дизайне и разработке программного обеспечения автомобиля. Кроме того, увеличение их критического уровня может привести к тому, что власти потребуют сертификации этих систем. Мы думаем, что привнесение формальных доказательств в их развитие может помочь обеспечить выполнение свойств безопасности и получить эффективный процесс сертификации. Другие отрасли (например, аэрокосмическая, железнодорожная, ядерная), которые создают критические системы, требующие сертификации, также могут быть заинтересованы в развитии формальных методов проверки. Одним из этих методов является дедуктивное доказательство. Это может дать более высокий уровень уверенности в доказательстве критических свойств безопасности и даже избежать модульное тестирование. В этой статье мы выбрали вариант прикладного использования: функцию, вычисляющую квадратный корень с помощью линейной интерполяции. Мы используем дедуктивное доказательство, чтобы доказать его правильность и показать ограничения, с которыми мы сталкиваемся при работе с готовыми инструментами. Мы предлагаем подходы для преодоления некоторых ограничений, связанных с этими инструментами, чтобы преуспеть с доказательством. Эти подходы могут быть применены к аналогичным проблемам, которые часто встречаются в автомобильном встроенном программном обеспечении
Анализ безопасности контроллеров продольного движения во время набора высоты
No full textDuring the climb flight of big passenger airplanes, the airplane’s vertical movement, i.e. its pitch angle, results from the elevator deflection angle chosen by the pilot. If the pitch angle becomes too large, the airplane is in danger of an airflow disruption at the wings, which can cause the airplane to crash. In some airplanes, the pilot is assisted by a software whose task is to prevent airflow disruptions. When the pitch angle becomes greater than a certain threshold, the software overrides the pilot’s decisions with respect to the elevator deflection angle and enforces presumably safe values. While the assistance software can help to prevent human failures, the software itself is also prone to errors and is - generally - a risk to be assessed carefully. For example, if software designers have forgotten that sensors might yield wrong data, the software might cause the pitch angle to become negative. Consequently, the airplane loses height and can - eventually - crash.In this paper, we provide an executable model written in Matlab/Simulink® for the control system of a passenger airplane. Our model takes also into account the software assisting the pilot to prevent airflow disruptions. When simulating the climb flight using our model, it is easy to see that the airplane might lose height in case the data provided by the pitch angle sensor are wrong. For the opposite case of correct sensor data, the simulation suggests that the control system works correctly and is able to prevent airflow disruptions effectively.The simulation, however, is not a guarantee for the control system to be safe. For this reason, we translate the Matlab/Simulink® -model into a hybrid program (HP), i.e. into the input syntax of the theorem prover KeYmaera. This paves the way to formally verify safety properties of control systems modelled in Matlab/Simulink®. As an additional contribution of this paper, we discuss the current limitations of our transformation. For example, it turns out that simple proportional (P) controllers can be easily represented by HP programs, but more advanced PD (proportional-derivative) or PID (proportional-integral-derivative) controllers can be represented as HP programs only in exceptional cases.Во время набора высоты на больших пассажирских самолетах вертикальное движение самолета, то есть его угол наклона, зависит от угла отклонения руля высоты, выбранного пилотом. Если угол наклона становится слишком большим, самолет рискует нарушить воздушный поток на крыльях, что может привести к его падению. В некоторых самолетах пилоту помогает программное обеспечение, задачей которого является предотвращение нарушения воздушного потока. Когда угол наклона становится больше определенного порога, программное обеспечение отменяет решения пилота относительно угла отклонения руля высоты и обеспечивает предположительно безопасные значения. Хотя вспомогательное программное обеспечение может помочь предотвратить человеческие сбои, само программное обеспечение также подвержено ошибкам и, как правило, представляет собой риск для тщательной оценки. Например, если разработчики программного обеспечения забыли, что датчики могут давать неправильные данные, программное обеспечение может привести к тому, что угол наклона станет отрицательным. Следовательно, самолет теряет высоту и может – в конечном итоге – разбиться.В этой статье мы представляем исполняемую модель, написанную на Matlab/Simulink® для системы управления пассажирским самолетом. Наша модель также учитывает программное обеспечение, помогающее пилоту предотвращать нарушение воздушного потока. При моделировании набора высоты с использованием нашей модели легко увидеть, что самолет может потерять высоту, если данные, предоставленные датчиком угла наклона, неверны. Для противоположного случая правильных данных датчика, моделирование предполагает, что система управления работает правильно и способна эффективно предотвращать нарушение воздушного потока.Однако симуляция не является гарантией безопасности системы управления. По этой причине мы переводим Matlab/Simulink®-модель в гибридную программу (НР), т. е. во входной синтаксис средства доказательства теорем KeYmaera. Это открывает путь для формальной проверки свойств безопасности систем управления, смоделированных в Matlab/Simulink®. В качестве дополнительного вклада в эту статью мы обсудим текущие ограничения нашей трансформации. Например, оказывается, что простые пропорциональные (Р) контроллеры могут быть легко представлены программами НР, но более продвинутые контроллеры РD (пропорционально-производные) или РID (пропорционально-интегрально-производные) могут быть представлены как программы НР только в исключительных случаях
Оркестрация жизненного цикла многопользовательской виртуальной сетевой функции
Get PDFNetwork function virtualization (NFV) is a promising technique of high quality, flexible and scalable service for telecommunication companies clients and for enterprise data center clients. One of the important capabilities of this technique is providing a virtual service as a combination of multiple virtual functions. There are two types of virtual functions: those intended for a single customer (su-VF) and those that can serve multiple users (mu-VF). In case when output of mu-VF is chained with inputs of several different su-VFs, there is a need for a mechanism of identification and separation of users network flows passing through mu-VF to allocate them correctly between inputs of su-VFs in the NFV infrastructure. In the cloud environment, it is not always possible to use VLAN tags, IP and MAC addresses for that. In this paper, we consider the problem of identification of network traffic coming from a certain user inside an NFV platform and present a solution implemented in C2 MANO-platform.Виртуализация сетевых функций (NFV) – перспективная технология предоставления качественного, гибкого и масштабируемого сервиса для клиентов телекоммуникационных компаний и операторов центров обработки данных. Одной из важных возможностей этой технологии является предоставление “сложного” (состоящего из нескольких виртуальных функций) сервиса. Есть два типа виртуальных функций: те, которые ориентированы на работу с конкретным пользователем (далее su-VF); и те, которые используют разные пользователи (далее mu-VF). Если выход mu-VF соединен с входами нескольких su-VF, то возникает необходимость в механизме идентификации и разделения трафика разных пользователей в NFV-инфраструктуре. В облачной среде идентификация пользователей традиционными способами через VLAN теги, IP и MAC-адреса не всегда возможна. В статье рассматривается описанная выше проблема идентификации трафика конкретного пользователя NFV-инфраструктуры, и представлено ее решение, реализованное на MANO-платформе С2