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

Максимов, Дмитрий Борисович Кафедра информатики
Бесплатно
В избранное
Работа доступна по лицензии 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 экспертов уже готовы начать работу над твоим проектом!

    Дарья Б. МГУ 2017, Журналистики, выпускник
    4.9 (35 отзывов)
    Привет! Меня зовут Даша, я окончила журфак МГУ с красным дипломом, защитила магистерскую диссертацию на филфаке. Работала журналистом, PR-менеджером в международных ко... Читать все
    Привет! Меня зовут Даша, я окончила журфак МГУ с красным дипломом, защитила магистерскую диссертацию на филфаке. Работала журналистом, PR-менеджером в международных компаниях, сейчас работаю редактором. Готова помогать вам с учёбой!
    #Кандидатские #Магистерские
    50 Выполненных работ
    Татьяна П.
    4.2 (6 отзывов)
    Помогаю студентам с решением задач по ТОЭ и физике на протяжении 9 лет. Пишу диссертацию на соискание степени кандидата технических наук, имею опыт годовой стажировки ... Читать все
    Помогаю студентам с решением задач по ТОЭ и физике на протяжении 9 лет. Пишу диссертацию на соискание степени кандидата технических наук, имею опыт годовой стажировки в одном из крупнейших университетов Германии.
    #Кандидатские #Магистерские
    9 Выполненных работ
    Ксения М. Курганский Государственный Университет 2009, Юридический...
    4.8 (105 отзывов)
    Работаю только по книгам, учебникам, статьям и диссертациям. Никогда не использую технические способы поднятия оригинальности. Только авторские работы. Стараюсь учитыв... Читать все
    Работаю только по книгам, учебникам, статьям и диссертациям. Никогда не использую технические способы поднятия оригинальности. Только авторские работы. Стараюсь учитывать все требования и пожелания.
    #Кандидатские #Магистерские
    213 Выполненных работ
    Андрей С. Тверской государственный университет 2011, математический...
    4.7 (82 отзыва)
    Учился на мат.факе ТвГУ. Любовь к математике там привили на столько, что я, похоже, никогда не перестану этим заниматься! Сейчас работаю в IT и пытаюсь найти время на... Читать все
    Учился на мат.факе ТвГУ. Любовь к математике там привили на столько, что я, похоже, никогда не перестану этим заниматься! Сейчас работаю в IT и пытаюсь найти время на продолжение диссертационной работы... Всегда готов помочь! ;)
    #Кандидатские #Магистерские
    164 Выполненных работы
    Мария Б. преподаватель, кандидат наук
    5 (22 отзыва)
    Окончила специалитет по направлению "Прикладная информатика в экономике", магистратуру по направлению "Торговое дело". Защитила кандидатскую диссертацию по специальнос... Читать все
    Окончила специалитет по направлению "Прикладная информатика в экономике", магистратуру по направлению "Торговое дело". Защитила кандидатскую диссертацию по специальности "Экономика и управление народным хозяйством". Автор научных статей.
    #Кандидатские #Магистерские
    37 Выполненных работ
    Анна К. ТГПУ им.ЛН.Толстого 2010, ФИСиГН, выпускник
    4.6 (30 отзывов)
    Я научный сотрудник федерального музея. Подрабатываю написанием студенческих работ уже 7 лет. 3 года назад начала писать диссертации. Работала на фирмы, а так же помог... Читать все
    Я научный сотрудник федерального музея. Подрабатываю написанием студенческих работ уже 7 лет. 3 года назад начала писать диссертации. Работала на фирмы, а так же помогала студентам, вышедшим на меня по рекомендации.
    #Кандидатские #Магистерские
    37 Выполненных работ
    Екатерина С. кандидат наук, доцент
    4.6 (522 отзыва)
    Практически всегда онлайн, доработки делаю бесплатно. Дипломные работы и Магистерские диссертации сопровождаю до защиты.
    Практически всегда онлайн, доработки делаю бесплатно. Дипломные работы и Магистерские диссертации сопровождаю до защиты.
    #Кандидатские #Магистерские
    1077 Выполненных работ
    Петр П. кандидат наук
    4.2 (25 отзывов)
    Выполняю различные работы на заказ с 2014 года. В основном, курсовые проекты, дипломные и выпускные квалификационные работы бакалавриата, специалитета. Имею опыт напис... Читать все
    Выполняю различные работы на заказ с 2014 года. В основном, курсовые проекты, дипломные и выпускные квалификационные работы бакалавриата, специалитета. Имею опыт написания магистерских диссертаций. Направление - связь, телекоммуникации, информационная безопасность, информационные технологии, экономика. Пишу научные статьи уровня ВАК и РИНЦ. Работаю техническим директором интернет-провайдера, имею опыт работы ведущим сотрудником отдела информационной безопасности филиала одного из крупнейших банков. Образование - высшее профессиональное (в 2006 году окончил военную Академию связи в г. Санкт-Петербурге), послевузовское профессиональное (в 2018 году окончил аспирантуру Уральского федерального университета). Защитил диссертацию на соискание степени "кандидат технических наук" в 2020 году. В качестве хобби преподаю. Дисциплины - сети ЭВМ и телекоммуникации, информационная безопасность объектов критической информационной инфраструктуры.
    #Кандидатские #Магистерские
    33 Выполненных работы
    user1250010 Омский государственный университет, 2010, преподаватель,...
    4 (15 отзывов)
    Пишу качественные выпускные квалификационные работы и магистерские диссертации. Опыт написания работ - более восьми лет. Всегда на связи.
    Пишу качественные выпускные квалификационные работы и магистерские диссертации. Опыт написания работ - более восьми лет. Всегда на связи.
    #Кандидатские #Магистерские
    21 Выполненная работа

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

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