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

ВВЕДЕНИЕ ………………………………………………………………………………………………….. 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