Алгоритмическое и программное обеспечение оценки качества приложений, работающих в среде распределенных реестров

Максимов, Дмитрий Борисович Кафедра информатики
Бесплатно
В избранное
Работа доступна по лицензии Creative Commons:«Attribution» 4.0

ВВЕДЕНИЕ ………………………………………………………………………………………………….. 4
1 Анализ средств формальной верификации систем, работающих в среде
распределенных реестров………………………………………………………………………………. 6
1.1 Распределенный реестр ………………………………………………………………………….. 6
1.2 Умные контракты…………………………………………………………………………………… 9
1.3 Формальная верификация …………………………………………………………………….. 11
1.4 Проводимые исследования …………………………………………………………………… 16
1.5 Существующие решения ………………………………………………………………………. 18
1.5.1 PRISM …………………………………………………………………………………………….. 18
1.5.2 Isabelle …………………………………………………………………………………………….. 18
1.5.3 K-Tool ……………………………………………………………………………………………… 19
1.5.4 BIP Framework …………………………………………………………………………………. 20
1.5.5 Выбор средства для проведения исследования …………………………………. 22
2 Конструирование модели исследуемой программной системы…………………… 24
2.1 Метод проверки моделей ……………………………………………………………………… 24
2.2 Описание модели …………………………………………………………………………………. 26
2.3 Исследуемые ограничения ……………………………………………………………………. 30
2.4 Методы оценки результатов работы ……………………………………………………… 33
3 Проведение исследования …………………………………………………………………………. 36
3.1 Используемые модули для исследования ………………………………………………. 36
3.2 Исследование процесса регистрации пользователя ……………………………….. 36
3.3 Проверка адекватности модели ……………………………………………………………. 42
ЗАКЛЮЧЕНИЕ …………………………………………………………………………………………… 47
СПИСОК СОКРАЩЕНИЙ ………………………………………………………………………….. 49
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ ……………………………………….. 50

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

При рассмотрении приложений, работающих в среде распределенных
реестров и случаев взлома подобных приложений было выявлено, что основная
причина наличия уязвимостей в программном обеспечении, является
недостаточное тестирование программного обеспечения. Для того чтобы
повысить качество разрабатываемого программного обеспечения,
были проведено исследование возможности применения методов формальной
верификации для приложений, работающих в среде распределенных реестров.
На основе анализа существующих программных решений для проведения
формальной верификации была выбрана система BIP Framework исходя из
следующих критериев:
– возможность моделирования стохастической системы;
– возможность проведения параметрического исследования;
– формирование графиков сравнительного анализа;
– подключение пользовательского исполняемого кода.
В качестве исследуемой модели был выбрана модель системы, которая
выдает пользователю псевдоним.
На основе требований из первого раздела и составленной модели и
ограничений из второго раздела, была решена задача по проведению формальной
верификации системы. Она состояла из следующих этапов:
– создание модели;
– формирование ограничений;
– симуляция работы системы и проверка работы системы в рамках
заданных ограничений.
В ходе исследования была выдвинута и экспериментально проверена
гипотеза о том, что возможно построение и формальное исследование модели
умного контракта для регистрации новых пользователей. Была построена
модель, для которой на языке линейной темпоральной логики сформулировано
ограничение на состояние модели, отражающее особенности процесса
регистрации в условиях нехватки ресурсов. Формальная верификация
построенной модели позволила оценить степень достоверности
сформулированного ограничения.
Результаты исследования прошли апробацию на международной научно-
практической конференции и опубликованы в сборнике трудов [25].
В дальнейшем, планируется расширить модель исследования и добавить в
исследуемую модель злоумышленника, чтобы проанализировать возможность
получения чужого пользовательского псевдонима в процессе регистрации.
Также предполагается использовать метод проверки гипотез для анализа данных
полученных при исследовании.
СПИСОК СОКРАЩЕНИЙ

DOS – denial of service;
DSL – domain specific language;
ЭЦП – электронная цифровая подпись;
NASA – National aeronautics and space administration;
PRISM – probabilistic model checker;
PCTL – probabilistic computation tree logic;
CSL – computation tree logic;
LTL – linear temporal logic;
BIP – behavior interaction priority;
PESTIM – probability estimation;
GUI – graphical user interface;
SSE – stochastic simulation engine;
MM – monitoring module;
SMCE – statistical model checking engine;
PEM – parametric exploration module.

1Программа«ЦифроваяэкономикаРоссийскойФедерации»:
распоряжение правительства Российской Федерации от 28 июля 2017 г. №1632-
р // Председатель правительства Российской Федерации. c. 1-5.
2 Шадрин, Ф. Г. Технология blockchain. Смарт-контракты / Ф. Г. Шадрин
//ЭлектронныйсборникстатейпоматериаламXLIVстуденческой
международной научно-практической конференции / Университетская книга. –
Курск. – 2018. – C. 110–117.
3 Stuart Haber. How to TimeStamp a Digital Document / Stuart Haber, W Scott
Stornetta // Journal of Cryptology. – 1991. – Vol.3, No. 2, P. 99–111.
4 Lotte Fekkes. Comparing Bitcoin and Ethereum : Bachelor thesis Computer
Science : 0613 / Lotte Fekkes. – Nijmegen, 2018. – P. 43.
5 Matteo Gianpietro Zago. 50+ Examples of How Blockchains are Taking Over
the World [Электронный ресурс] // Medium. – San Francisco, 2018. – Режим
доступа: https://medium.com/@matteozago/50-examples-of-how-blockchai
ns-are-taking-over-the-world-4276bf488a4b.
6 Ходаков, А. Д. Особенности разработки смарт-контракта на базе
блокчейн платформы ethereum / А. Д. Ходаков, С. А. Зайкова // Сборник научных
трудов XIII Международной научно-практической конференции / Ассоциация
научных сотрудников «Сибирская академическая книга». – Новосибирск. – 2018.
– C. 205–207.
7 Karthikeyan Bhargavan. Formal Verification of Smart Contracts / Karthikeyan
Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi //
Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis
for Security. – 2016. – P. 91–96.
8 Romain Edelmann. Behaviour-Interaction-Priority in Functional Programming
Languages: Formalisation and Implementation of Concurrency Frameworks in Haskell
and Scala / Romain Edelmann, Simon Bliudze, Joseph Sifakis // Infoscience. EPFL
scientific publications. – 2015. – P. 201.
9 Jeff Hu. Learn Blockchain’s Top 25 Hacks in History [Электронный ресурс]
// Medium. – San Francisco, 2019. – Режим доступа: https://hackernoon.com/tech-
explained-top-24-blockchain-hacks-in-history-first-half-40c390dc4a96.
10 Сергеев, Д. В. Верификация и способы описания формальных моделей
/ Д. В. Сергеев // Альманах современной науки и образования / Издательство
«Грамота». – Тамбов. – 2011. – № 4. – C. 84–85.
11 Fuzhi Wang. Symbolic implementation of model-checking probabilistic
timed automata : Thesis for the degree of doctor of philosophy : 0223 / Fuzhi Wang. –
Birmingham, 2006. – P. 166.
12 Robert C. Armstrong. Survey of Existing Tools for Formal Verification /
Robert C. Armstrong, Ratish J. Punnoose, Matthew H. Wong, Jackson R. Mayo //
Center for Computing Research. – 2014. – P. 40.
13 Christel Baier. Principles of Model Checking / Christel Baier, Joost-Pieter
Katoen. – .: The MIT Press, 2018. – P. 984.
14 Stacy D. Nelson. Formal Verification for a Next-Generation Space Shuttle /
Stacy D. Nelson, Charles Pecheur. // Formal Approaches to Agent-Based Systems,
2002. – P. 53-57.
15 Jasim O. Formal verification of quadcopter flight envelop using theorem
prover / Jasim O. ,Veres S.M. // Proceedings of 2018 IEEE Conference on Control
Technology and Applications (CCTA), 2018. – P. 1502-1507
16 Marta Kwiatkowska. PRISM 4.0: Verification of Probabilistic Real-time
Systems / Marta Kwiatkowska, Gethin Norman, David Parker // In Proc. 23rd
International Conference on Computer Aided Verification (CAV’11). – 2011. – Vol.
6806, P. 585–591.
17 Баринова, А. А. Методы и средства обеспечения конфиденциальности
смарт-контрактов / А. А. Баринова, С. В. Запечников // Безопасность
информационных технологий / – КлАССное снаряжение. – Москва. – Т. 24, №
2. – C. 16–23.
18 Isabelle [Электронный ресурс] : Официальный сайт программного
обеспечениядляверификацииIsabelle-Режимдоступа:
https://www.prismmodelchecker.org/
19 K-tool [Электронный ресурс] : Официальный сайт программного
обеспечениядляверификацииK-tool-Режимдоступа:
http://www.kframework.org/index.php/Main_Page/
20BIPFramework[Электронныйресурс]:Официальныйсайт
программного обеспечения для верификации BIP Framework – Режим доступа :
http://www-verimag.imag.fr/New-BIP-tools.html?lang=en
21 Tesnim Abdellatif. Formal verification of smart contracts based on users and
blockchain behaviors models / Tesnim Abdellatif, Kei-Léo Brousmiche // IFIP NTMS
International Workshop on Blockchains and Smart Contracts (BSC). – 2018. – P. 5.
22 Braham Lotfi Mediouni. SBIP 2.0: Statistical Model Checking Stochastic
Real-time Systems / Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga,
Mahieddine Dellabani // Verimag Research Report № TR-2018-5. – 2018. P. 22.
23 Jérôme Darbon. Approximate Probabilistic Model Checking for Programs /
Jérôme Darbon, Richard Lassaigne, Sylvain Peyronnet // LRDE/EPITA. – 2007. P. 6.
24 Wassily Hoeffding. Probability inequalities for sums of bounded random
variables / Wassily Hoeffding // Department of Computer Science and Electrical
Engineering. – 2008. – P. 13 – 29.
25 Максимов, Д. Б. Использование методов формальной верификации для
оценки качества умных контрактов / Д. Б. Максимов, И. А. Якимов, А. C.
Кузнецов//ИНТЕЛЛЕКТУАЛЬНЫЙПОТЕНЦИАЛОБЩЕСТВАКАК
ДРАЙВЕР ИННОВАЦИОННОГО РАЗВИТИЯ НАУКИ. – Тюмень. – 2019 – Часть
1 C. 57 – 62.
26 Kristin Y. Rozier. Linear Temporal Logic Symbolic Model Checking //
Computer Science Review, 2011. P. 163-203

Заказать новую

Лучшие эксперты сервиса ждут твоего задания

от 5 000 ₽

Не подошла эта работа?
Закажи новую работу, сделанную по твоим требованиям

    Нажимая на кнопку, я соглашаюсь на обработку персональных данных и с правилами пользования Платформой

    Последние выполненные заказы

    Хочешь уникальную работу?

    Больше 3 000 экспертов уже готовы начать работу над твоим проектом!

    Александр О. Спб государственный университет 1972, мат - мех, преподав...
    4.9 (66 отзывов)
    Читаю лекции и веду занятия со студентами по матанализу, линейной алгебре и теории вероятностей. Защитил кандидатскую диссертацию по качественной теории дифференциальн... Читать все
    Читаю лекции и веду занятия со студентами по матанализу, линейной алгебре и теории вероятностей. Защитил кандидатскую диссертацию по качественной теории дифференциальных уравнений. Умею быстро и четко выполнять сложные вычислительные работ
    #Кандидатские #Магистерские
    117 Выполненных работ
    Дарья Б. МГУ 2017, Журналистики, выпускник
    4.9 (35 отзывов)
    Привет! Меня зовут Даша, я окончила журфак МГУ с красным дипломом, защитила магистерскую диссертацию на филфаке. Работала журналистом, PR-менеджером в международных ко... Читать все
    Привет! Меня зовут Даша, я окончила журфак МГУ с красным дипломом, защитила магистерскую диссертацию на филфаке. Работала журналистом, PR-менеджером в международных компаниях, сейчас работаю редактором. Готова помогать вам с учёбой!
    #Кандидатские #Магистерские
    50 Выполненных работ
    Елена Л. РЭУ им. Г. В. Плеханова 2009, Управления и коммерции, пре...
    4.8 (211 отзывов)
    Работа пишется на основе учебников и научных статей, диссертаций, данных официальной статистики. Все источники актуальные за последние 3-5 лет.Активно и уместно исполь... Читать все
    Работа пишется на основе учебников и научных статей, диссертаций, данных официальной статистики. Все источники актуальные за последние 3-5 лет.Активно и уместно использую в работе графический материал (графики рисунки, диаграммы) и таблицы.
    #Кандидатские #Магистерские
    362 Выполненных работы
    Виктор В. Смоленская государственная медицинская академия 1997, Леч...
    4.7 (46 отзывов)
    Имеют опыт грамотного написания диссертационных работ по медицине, а также отдельных ее частей (литературный обзор, цели и задачи исследования, материалы и методы, выв... Читать все
    Имеют опыт грамотного написания диссертационных работ по медицине, а также отдельных ее частей (литературный обзор, цели и задачи исследования, материалы и методы, выводы).Пишу статьи в РИНЦ, ВАК.Оформление патентов от идеи до регистрации.
    #Кандидатские #Магистерские
    100 Выполненных работ
    Алёна В. ВГПУ 2013, исторический, преподаватель
    4.2 (5 отзывов)
    Пишу дипломы, курсовые, диссертации по праву, а также истории и педагогике. Закончила исторический факультет ВГПУ. Имею высшее историческое и дополнительное юридическо... Читать все
    Пишу дипломы, курсовые, диссертации по праву, а также истории и педагогике. Закончила исторический факультет ВГПУ. Имею высшее историческое и дополнительное юридическое образование. В данный момент работаю преподавателем.
    #Кандидатские #Магистерские
    25 Выполненных работ
    Кирилл Ч. ИНЖЭКОН 2010, экономика и управление на предприятии транс...
    4.9 (343 отзыва)
    Работы пишу, начиная с 2000 года. Огромный опыт и знания в области экономики. Закончил школу с золотой медалью. Два высших образования (техническое и экономическое). С... Читать все
    Работы пишу, начиная с 2000 года. Огромный опыт и знания в области экономики. Закончил школу с золотой медалью. Два высших образования (техническое и экономическое). Сейчас пишу диссертацию на соискание степени кандидата экономических наук.
    #Кандидатские #Магистерские
    692 Выполненных работы
    Елена С. Таганрогский институт управления и экономики Таганрогский...
    4.4 (93 отзыва)
    Высшее юридическое образование, красный диплом. Более 5 лет стажа работы в суде общей юрисдикции, большой стаж в написании студенческих работ. Специализируюсь на напис... Читать все
    Высшее юридическое образование, красный диплом. Более 5 лет стажа работы в суде общей юрисдикции, большой стаж в написании студенческих работ. Специализируюсь на написании курсовых и дипломных работ, а также диссертационных исследований.
    #Кандидатские #Магистерские
    158 Выполненных работ
    Юлия К. ЮУрГУ (НИУ), г. Челябинск 2017, Институт естественных и т...
    5 (49 отзывов)
    Образование: ЮУрГУ (НИУ), Лингвистический центр, 2016 г. - диплом переводчика с английского языка (дополнительное образование); ЮУрГУ (НИУ), г. Челябинск, 2017 г. - ин... Читать все
    Образование: ЮУрГУ (НИУ), Лингвистический центр, 2016 г. - диплом переводчика с английского языка (дополнительное образование); ЮУрГУ (НИУ), г. Челябинск, 2017 г. - институт естественных и точных наук, защита диплома бакалавра по направлению элементоорганической химии; СПХФУ (СПХФА), 2020 г. - кафедра химической технологии, регулирование обращения лекарственных средств на фармацевтическом рынке, защита магистерской диссертации. При выполнении заказов на связи, отвечаю на все вопросы. Индивидуальный подход к каждому. Напишите - и мы договоримся!
    #Кандидатские #Магистерские
    55 Выполненных работ
    Евгения Р.
    5 (188 отзывов)
    Мой опыт в написании работ - 9 лет. Я специализируюсь на написании курсовых работ, ВКР и магистерских диссертаций, также пишу научные статьи, провожу исследования и со... Читать все
    Мой опыт в написании работ - 9 лет. Я специализируюсь на написании курсовых работ, ВКР и магистерских диссертаций, также пишу научные статьи, провожу исследования и создаю красивые презентации. Сопровождаю работы до сдачи, на связи 24/7 ?
    #Кандидатские #Магистерские
    359 Выполненных работ

    Другие учебные работы по предмету

    Интеллектуальный анализ текстовых данных с rnприменением методов машинного обучения
    📅 2019год
    🏢 Национальный исследовательский Томский политехнический университет (ТПУ)