• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Найдено 120 публикаций
Сортировка:
по названию
по году
Статья
Хорошилов А. В., Щепетков И. Труды Института системного программирования РАН. 2017. Т. 29. № 3. С. 43-56.

В статье рассматривается семейство требований доверия к безопасности ADV_SPM «Моделирование политики безопасности», которое определяется стандартом ГОСТ Р ИСО/МЭК 15408-3-2013 «Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности». Обсуждаются задачи, решаемые этим семейством, и вопросы, которые возникают при попытке интерпретировать его требования. На простом примере представляется подход к формализации политик безопасности при помощи языка формальных спецификаций Event-B и инструментов платформы Rodin.

Добавлено: 28 августа 2017
Статья
Semenkovich S. A., Kolekonova O. I., Degtiarev K. Y. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 5. P. 19-38.

Существует несколько известных методов, позволяющих оценить усилия, которые придется потратить на разработку программного обеспечения. В популярной на сегодняшний день методологии гибкой разработки Scrum для этих целей широко используется подход, основанный на story points. Однако, их использование для оценки объема работы может быть затруднительным для тех людей, которые только начинают знакомство с методологией Scrum или впервые попадают в новую Scrum-команду. Описанный в статье подход предлагает использовать оценку трудозатрат на разработку конкретной части программного продукта на основе привычных и понятных для всех фраз естественного языка. Предложенная система нечеткого вывода (модель Мамдани) позволяет преобразовывать мнения людей, выраженные в виде предложений на естественном языке, в число story points – проведенные исследования эмпирически показывают, что те, кто делает первые шаги в методологии Scrum, считают такой подход более удобным и простым, по сравнению с обычным методом оценивания в story points. Также, с целью выяснения, может ли разработанный подход использоваться при работе над реальными проектами, был проведен дополнительный эксперимент, в котором приняли участие четыре группы людей с различными уровнями квалификации в Scrumразработке. Представителям этих групп было дано задание оценить трудозатраты на разработку отдельных частей некоторого проекта с использованием предложенного подхода и обычных story points единицах. Оценки группы экспертов в области Scrum оказались примерно одинаковы для обоих подходов, в то время как оценки новичков′ в методологии сильно отличались при применении двух разных методов. По мнению авторов, предложенный подход может дать возможность более плавного вхождения в методологию Scrum, лучшего понимания природы story points и более быстрой выработке навыков работы с ними на практике.

Добавлено: 20 октября 2018
Статья
Avdoshin S. M., Beresneva E. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 233-250.
Добавлено: 10 июля 2018
Статья
Tatarnikov A., Kamkin A., Проценко А. С. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 3. P. 125-138.

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

Добавлено: 10 декабря 2017
Статья
Shugurov I., Mitsyuk A. A. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 103-122.

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

Добавлено: 12 сентября 2016
Статья
Gordenko M., Beresneva E. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 251-270.
Добавлено: 10 июля 2018
Статья
Pavlov V., Novikov B. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 1. P. 137-160.

After huge amount of big scientific data, which needed to be stored and processed, has emerged, the problem of large multidimensional arrays support gained close attention in the database world. Devising special database engines with support of array data model became an issue. Development of a well-organized database management system which stands on completely uncommon data model required performing the following tasks: formally defining a data model, building a formal algebra operating on objects from the data model, devising optimization rules on logical level and then on the physical one. Those tasks has already been completed by creators of different array databases. In this paper array formalization, core algebra and optimization techniques are revised using examples of AML, RasDaMan, SciDB – developed array database management systems with different algebras and optimization approaches.

Добавлено: 15 марта 2019
Статья
Burdonov I. B., Kossatcheva A. S., Kuliamin V. et al. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 1. P. 69-88.

The paper provides a review of distributed graph algorithms research conducted by authors. We consider an asynchronous distributed system model represented by a strongly connected directed rooted graph with bounded edge capacity (in a sense that only a bounded number of messages can be sent through an edge in a given time interval). A graph can be static or dynamic, i.e. changing. For a static graph we propose a spanning (in- and out-) tree construction algorithm of time complexity O(n/k+d)O(n/k+d), requiring O(ndlogΔ+)O(ndlog⁡Δ+)message size and the same size of memory of each computing agent located in graph vertex, where nn is the number of vertices of the graph, kk is the capacity of an edge, dd is the maximum length of simple path in the graph, Δ+Δ+ is the maximum outdegree of the vertices. The spanning trees constructed can be used in distributed computation of a function of the multiset of values assigned to graph vertices in a time not greater than 3d3d. In a dynamic graph we suppose that k=1k=1 and an edge can appear, disappear, or change its end. We propose a dynamic graph monitoring algorithm than delivers information on any change to the root of the graph in O(n)O(n) or O(d)O(d) after the changes are stopped. We also propose graph exploration and marking algorithm with time complexity O(n)O(n). The marking provided by it is used in distributed computation of a function of the multiset of values assigned to dynamic graph vertices, which can be performed in time O(n2)O(n2)with messages of size O(logn)O(log⁡n) or in time O(n)O(n) with messages of size O(nlogn)O(nlog⁡n).

Добавлено: 11 августа 2018
Статья
Samokhvalov D., Dworzanski L. W. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 65-84.

Вложенные сети Петри – это расширение формализма раскрашенных сетей Петри, которые используют сети Петри в качестве фишек. Данный формализм позволяет создавать подробные модели мультиагентных систем, осуществлять имитационное моделирование, верифицировать и анализировать их свойства на формальном и строгом уровне. Мультиагентные системы находят применение во многих областях – начиная системами, для которых безопасность играет критическую роль, заканчивая повседневными системами, работающими на персональных вычислительных устройствах. Число таких систем в современном мире растет вместе с увеличивающимся числом мобильных вычислительных устройств. На данный момент разработаны инструменты и методы моделирования и анализа вложенных сетей Петри, но синтез мультиагентных систем по моделям вложенных сетей Петри еще недостаточно исследован и находится в стадии активного изучения. Метод автоматической генерация исполняемого кода целевой системы по спроектированной и верифицированной модели вложенной сети Петри обеспечивает получение корректных системы из корректных спецификаций на языке вложенных сетей Петри. В данной работе, демонстрируется применение формализма вложенных сетей Петри для построения модели системы управления поисковыми и спасательными операциями и автоматической генерации реализации в виде исполняемого кода событийно-управляемых систем основанных на платформе Telegram. Мы добавляем возможность аннотировать модели вложенных сетей Петри с помощью Action Language, который позволяет связывать срабатывания переходов на модельном уровне с вызовами Telegram Bot API на уровне реализации. Предложенный подход продемонстрирован на примере аннотированной модели системы координирования спасательной операции.

Добавлено: 15 сентября 2016
Статья
Avdoshin S.M., Lazarenko A.V. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 1. P. 89-101.
Добавлено: 25 марта 2018
Статья
Fedotov A. N., Kaushan V. V., Gaysaryan S. S. et al. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 6. P. 151-162.

Approaches for code execution using program vulnerabilities are considered in this paper. Particularly, ways of code execution using buffer overflow on stack and on heap, using use-after-free vulnerabilities and format string vulnerabilities are examined in section 2. Methods for automatic generation input data, leading to code execution are described in section 3. This methods are based on dynamic symbolic execution. Dynamic symbolic execution allows to gain input data, which leads program along the path of triggering vulnerability. The security predicate is an extra set of symbolic formulas, describing program's state in which code execution is possible. To get input data, leading to code execution, path and security predicates need to be united, and then the whole system should be solved. Security predicates for pointer overwrite, function pointer overwrite and format string vulnerability, that leads to stack buffer overflow are presented in the paper. Represented security predicates were used in method for software defect severity estimation. The method was applied to several binaries from Darpa Cyber Grand Challenge. Testing security predicate for format string vulnerability, that leads to buffer overflow was conducted on vulnerable version of Ollydbg. As a result of testing it was possible to obtain input data that leads to code execution.

Добавлено: 10 августа 2018
Статья
N. Nikitina, A. Mitsyuk. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 3. P. 219-236.

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

Добавлено: 18 августа 2015
Статья
Ivanov S. Y., Kalenkova A. A. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 3. P. 255-266.

На сегодняшний день различным организациям приходится все чаще сталкиваться с моделированием своих бизнес-процессов для сокращения издержек и для обеспечения четкого понимания процессов, которые используются в организации. Но из-за изменения законодательства, внедрения инноваций и других факторов бизнес- процессы компании постоянно изменяются. В свою очередь системным и бизнес аналитикам, которые занимаются моделированием бизнес-процессов, нужен инструмент для сравнения моделей бизнес-процессов и определения их различий. Сложность решения данной проблемы объясняется недостатком инструментов, которые могут быть использованы для сравнения моделей бизнес-процессов. Также нет общепризнанного стандарта для моделирования. EPC, YAWL, BPEL, XPDL и BPMN только небольшая часть широко используемых нотаций, которые нашли признание среди разработчиков. Каждая нотация имеет свои преимущества и недостатки, но почти все из них описаны с помощью XML-схемы, которая определяет правила сериализации. В этой статье предложен общий подход к сравнению моделей бизнес-процессов, который опирается на XML представления моделей. Предложенный подход реализован в виде плагина для фреймворка ProM, который активно используется аналитиками и исследователями в рамках новой научной дисциплины process mining.

Добавлено: 17 сентября 2015
Статья
Avdoshin S. M., Beresneva E. Proceedings of the Institute for System Programming of the RAS. 2019. Vol. 31. No. 3. P. 145-156.
Добавлено: 12 сентября 2019
Статья
Зеленов С. В., Карнов А. Труды Института системного программирования РАН. 2017. Т. 29. № 4. С. 191-202.

В данной работе рассматривается марковский анализ моделей комплексных программно-аппаратных систем. Инструмент марковского анализа может быть использован, в частности, для верификации моделей систем интегральной модульной авионики. Во введении перечисляются основные достоинства и недостатки марковского анализа. К примеру, марковский анализ, в отличие от других подходов — анализа дерева неисправности и анализ алогической схемы, позволяет анализировать модели систем, способных к восстановлению. Основным недостатком данного подхода является экспоненциальный рост размера моделей в зависимости от числа компонентов в анализируемой системе. Это существенно ограничивает возможность применения марковского анализа на практике. Другой важной проблемой является создание нового алгоритма трансляции исходной модели системы в модель, пригодную  для марковского анализа (марковскую цепь), так как существующие решения накладывают существенные ограничения на архитектуру анализируемой системы. Далее идет краткое описание контекста, в котором инструмент должен работать — язык моделирования AADL с библиотекой Error Model Annex, набор инструментов MASIW, а также описывается сам метод марковского анализа. В основной части предлагается алгоритм трансляции модели системы в марковскую цепь, частично решающий проблему экспоненциального роста марковской цепи. Затем следует описание дальнейших шагов, а также предлагаются эвристики, позволяющие значительно сократить время работы итоговой программы. В работе также рассматриваются существующие инструменты марковского анализа и их недостатки. В качестве результата данной работы предлагается новый инструмент марковского анализа, который может быть эффективно использован на практике.

Добавлено: 8 ноября 2017
Статья
Avdoshin S.M., Lazarenko A.V. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 21-34.
Добавлено: 31 августа 2016
Статья
Mallachiev K., Pakulin N. V., Khoroshilov A. V. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 2. P. 181-192.
Добавлено: 11 августа 2018
Статья
Asryan S. A., Gaysaryan S. S., Kurmangaleev S. F. et al. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 7-20.

The article describes new method of use after free bug detection using program dynamic analysis. In memory-unsafe programming languages such as C/C++ this class of bugs mainly accurse when program tries to access specific area of dynamically allocated memory that has been already freed. This method is based on combination of two basic components. The first component tracks all memory operations through dynamic binary instrumentation and searches for inappropriate memory access. It preserves two sets of memory address for all allocation and free instructions. Using both sets this component checks whether current memory is accessible through its address or it has been already freed. It is based on dynamic symbolic execution and code coverage algorithm. It is used to maximize the number of execution paths of the program. Using initial input, it starts symbolic execution of the target program and gathers input constraints from conditional statements. The new inputs are generated by systematically solving saved constraints using constraint solver and then sorted by number of basic blocks they cover. Proposed method detects use after free bugs by applying first component each time when second one was able to open new path of the program. It was tested on our synthetic tests that were created based on well-known use after free bug patterns. The method was also tested on couple of real projects by injecting bugs on different levels of execution.

Добавлено: 10 августа 2018
Статья
Nurmukhametov A. R., Zhabotinskiy E. A., Kurmangaleev S. F. et al. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 6. P. 163-182.

Program vulnerabilities are a serious security threat. It is important to develop defenses preventing their exploitation, especially with a rapid increase of ROP attacks. State of the art defenses have some drawbacks that can be used by attackers. In this paper we propose fine-grained address space layout randomization on program load that is able to protect from such kind of attacks. During the static linking stage executable and library files are supplemented with information about function boundaries and relocations. A system dynamic linker/loader uses this information to perform functions permutation. The proposed method was implemented for 64-bit programs on CentOS 7 operating system. The implemented method has shown good resistance to ROP attacks based on two metrics: the number of survived gadgets and the exploitability estimation of ROP chain examples. The implementation presented in this article is applicable across the entire operating system and has shown 1.5 % time overhead. The working capacity of proposed approach was demonstrated on real programs. The further research can cover forking randomization and finer granularity than on the function level. It also makes sense to implement the randomization of short functions placement, taking into account the relationships between them. The close arrangement of functions that often call each other can improve the performance of individual programs.

Добавлено: 10 августа 2018
Статья
Turdakov D., Aleksiyants A., Borisenko O. et al. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 5. P. 35-48.
Добавлено: 13 сентября 2016
Статья
I. Shugurov, A. Mitsyuk. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 3. P. 237-254.

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

Добавлено: 18 августа 2015