Филип Кант е директор на отдел Формални методи в “IOHK“. Можете да намерите повече подробности за неговата кариера и опит тук .
- Неговата група се фокусира върху въвеждането на формалните методи в методологичния процес на разработване на софтуер.
- Идеята на тази група е да се увери, че резултатите от изследователите, които пишат научни трудове и доказват аспекти от протокола на абстрактно ниво, могат да бъдат преведени в нещо, което е изпълнимо и от машина, и може да накара софтуера да работи.
- “IOHK” е уникален в способността си да прилага формални методи в блокчейн технология.
- Формалните методи обикновено се прилагат в индустрии като космонавтиката или медицината: системи, където залог са високи производствени стойности или човешки животи.
- Блокчейн системите имат голяма стойност и това е причината за прилагането на това (разгледайте следващия видео материал):
Това видео Д-р Кант започва с въведение за „Кардано“ и протокола – “Proof-of-Stake”, след което води презентация за Формални методи. Трябва да се вземе под внимание, че това е само резюме и някои раздели биха били по-добре разбрани, ако презентацията се гледа успоредно с неговите слайдове по темата (кодове и графики).
Kакво представлява “ PoS ” ( Proof of Stake – Доказателство за залог)?
- Какво искате да постигнете с криптовалутата?
o Децентрализация: валута без централен орган, чието управление е в ръцете на потребителите.
o Валута, с която да се борави без нужда от разрешение: всеки трябва да има достъп до нея без да среща бариери.
o Система със стабилен счетоводен регистър.
o Постоянство: транзакциите, които се записват в регистъра, трябва да останат там и да не могат да бъдат изтрити от него.
o Жизненост: заявените транзакции трябва да попадат в регистъра на блокчейна след известно време.
o Сигурност, даваща обществено доверие на системата: всички горе споменати изисквания са трудно изпълними едновременно – затова възниква нуждата от нещо, което е много стабилно, на което всеки да има доверие, но за което не трябва централизиран орган, който да придава достоверност на системата и да взема решенията в нея.
На какво се базира доверието в Биткойн блокчейна?
- Потребителите на Биткой изпращат транзакции в мрежата.
- Транзакциите се завеждат с „частен ключ“, така че никой не може да харчи парите на трети лица.
- Потребителите искат да се уверят, че информацията за изпратените транзакции, които са в обработка, както и транзакциите, които вече са извършени са показни в него и не изчезват на по-късен етап.
- Изпратените транзакции се групират в така наречените „блокове“, които се разглеждат като страници в счетоводен регистър.
- След това те се разпределят, чрез привеждане на блоковете в определен ред: всеки блок се позовава на предишния блок, включвайки неговия „хеш“ ( “hash”/„хеш“- цялата транзакция бива събрана в един низ; използва се хеш-функция за това събиране, така транзакцията получава уникален код, който не може да се дублира и ТРАНЗАКЦИЯТА може да бъде разпозната по него).
- Подредбата на преводите е важна, защото ако някой се опита да похарчи двойно парите си и заяви втора транзакция докато първата се обработва от блокчейна /и няма достатъчна наличност за двете транзакции/, системата ще изиска от него да посочи една от двете транзакции за валидна.
- Постига се доверие, като се оставят всички участници в блоковата верига да се редуват, вместо да има една централна фигура.
- Редуване на участниците в блоковата верига позволява, дори и да има сред тях някои, които не играят по правилата на блокчейна, резултатът да остане един стабилен регистър, където всички транзакции са включени в блоковата верига.
- Предотвратява се изтриването на транзакции, чрез правилото за най-дългата верига, тъй като този, който се опита да изтрие транзакция, ще трябва да се върне назад по веригата, за да подмени останалите транзакции.
- Система, която не изисква разрешение и не прави проверка на самоличността, означава, че човек може да се регистрира няколко пъти и това е проблем за система, базирана на редуване на участниците в нея.
- Защита на системата от така наречената „Атака на Сибил“.
- Решението, което Биткой използва, за да пребори проблема с потенциалната атака от горепосочения метод, е като добави разход за регистрацията във веригата.
- Този разход за регистрация е под формата на произволен математически пъзел.
- Тогава това, което Биткой прави е да добави произволен низ от данни към блока, като същевременно „хешът“ на блока има редица водещи нули.
- Тъй като „хешът“ е необратим, това не позволява да бъдат изчислени просто какви са тези числа и трябва да се опитва отново и отново.
- След това трябва да се похарчи хешираща/изчислителна мощност, за да се изпробват някои получени данни, да се изчисли хеша на блока, и ако изчислението не съвпадне, трябва да бъде преизчислено наново.
- Този метод на изчисление на блоковата верига придава висока цена на всяка евентуална атака на мрежата, тъй като атакуващите ще трябва да притежават повече компютри /да имат по-голяма изчислителна мощ/ от всички останали участници в системата.
Какво представлява “PoW” ( Proof of Work – Доказателство за работа)?
- Има произволен избор на лидер, като за всеки ЦП /централен процесор/, добавен към системата, получавате по един глас.
- Шансът да бъдете избран е пропорционален на мощността на процесора, която сте вложили в системата.
- Победителите от гласуването получават правото да създадат/“напишат“ блок, като при извършването на тази работа получават награда от системата.
- Тъй като в системата важи правилото за „най-дългата верига печели“, е трудно да се върнат и преобразуват старите блокове (изключение от това правило съществува тогава, когато някой разполага с повече от 50% от процесорната мощност на системата).
- Проблемите на „Биткойн“ блокчейнът:
o Хеширащата мощност изисква огромен разход на енергия.
o Консумацията на енергия на „Биткойн“ мрежата е сравнима с тази на малка държава.
o Като всички тези процеси допринасят за една сравнително ниска скорост на транзакция (~10 Tx/second - транзакции/секунда).
o Трудно е да се мащабира системата в нещо, което да има по-висок процент на транзакциите.
o Форматът на блокчейна е превъплатен в състезание, в което победителя взима всичко.
o За да увеличат максимално шанса да получат някаква награда, хората работят заедно, за да формират т.нар. “pools“ /“басейни“, като се има предвид: сдружения/, като тези „басейни“ водят до централизация на системата.
Proof of Stake – Доказателство за залог
- Избира се различен лидер: като основна тежест дава големината на залога.
- За всеки времеви интервал, протоколът произволно връчва една „монета“ на някой от участниците, тогава собственикът на тази „монета“ получава правото да произведе следващия блок във веригата.
- За да има даден участник по-голям шанс да бъде избран, той трябва да закупува повече от валутата, като този процес ще става с времето все по-скъп на участника.
- Горепосоченият процес има обаче допълнително предимство, тъй като е пряко обвързан със самата система.
- Ако сте голям инвеститор и съответно притежавате много от дадената валута, ще имате по-голям шанс да я подривате и дори да триете транзакции, но не бихте искали да го направите, тъй като, ако някой от другите участници забележи това, валутата ще се обезцени – засягайки и вашите капиталовложения – което стимулира участниците в блокчейна да бъдат честни, като по този начин създават доверие и в самата система.
- Причината, поради която тази система не е толкова разпространена и използвана е, че се нуждае от случайност на изборния процес.
- Възниква нуждата от специфичен генератор на произволни числа → всички участници трябва да се съгласят относно кой да е източникът на случайност, но ако след този процес се създаде централен орган, който да отговаря за този произволен генератор, то тогава този орган ще има способността да контролира голяма част от системата.
- Друга причина, поради която тази система не се използва е, че много хора смятат, че не е толкова безопасна, тъй като според тях има възможност някой да предвиди стойностите на генератора на случайните числа.
- Загрижеността произлиза от начина на работа на тези системи, тъй като когато „монетите“ в системата се наредят, се създава произволно число и кореспондиращата на това число „ n“- та на брой монета се избира от системата.
- Ако някой може да предвиди резултатите от горепосочения метод, тогава ще може да изпрати пари през системата, опитвайки се да разпредели „монетите“ си, така че те да попаднат на място, където да бъдат избрани.
- Този проблем създава нуждата от: децентрализиран генератор на случайни числа, и то такъв, който не може да бъде предсказан предварително.
Ouroboros
- Един резултат от изследователите на “IOHK” е протоколът „Ouroboros“, който е първият доказано сигурен PoS-протокол /Proof of Stake – Доказателство за залог/.
- Това е разработка, която е била предадена за рецензия и е получила одобрение.
- Начин на работа: разделя се времето на слотове и към всеки слот се зачислява блок > за всеки слот ще бъде избран произволно един участник за лидер.
- Този модел създава необходимост от произволност на системата.
- Произволността на системата се поражда, като се групират слотовете в епохи, и преди започването на всяка една епоха всички участници трябва да се споразумеят за формата на „семето“, което да даде начало на следващия генератор на произволни числа.
- По същество самите участници се уединяват и хвърлят зар насаме, и така произвеждат произволност (като процеса не се разкрива на трети страни), като накрая изпращат доказателство, че вече знаят какво са хвърлили и вече не могат да го подправят.
- След като залогът за следващата епоха е вече ясно посочен, всички случайни числа се разкриват и комбинират по определен начин, и така получавате ново „семе“.
- Това „семе“ е нещо, върху което всеки има възможността да влияе, но никой не може да предвиди, тъй като се базира на много случайни числа, които се споделят между участниците.
- Този протокол е доказано защитен от всеки негов противник, притежаващ по-малко от 50% от залога (количество Ада в системата).
Ouroboros Praos
- Това е разширение на Ouroboros-протокола, което се занимава с въпроса: „Какво се случва, когато съобщенията се забавят?“.
- Тъй като PoS-протоколът /Proof of Stake – Доказателство за залог/ се занимава с време и времеви слотове и има блок за всеки слот… за да може веригата да работи, информацията на последния блок трябва да се разпространи в мрежата, преди да дойде ред на следващия лидер на слота, в противен случай резултатът ще е автоматично „вилично“ разклонение.
- В реалните мрежи е възможно да възникнат закъснения, при предаването на съобщенията (като прекъсвания – има се предвид прекъсвания на електрическата или комуникационната мрежа).
- “Praos” разширява моделът на защита срещу противници, за да включи и мрежови закъснения.
- Това е моделът, който в момента се прилага за изграждането на бъдещите версии на „Кардано“.
От хартия до изпълнение
- Превод на научни статии, написани на английски език, както и преобразяване на математически формули, в нещо, което да може да бъде изпълнено от изчислителна машина.
- Съществува празнина между двете, тъй като научните статии са написани, за да бъдат разбрани от хора и едновременно с това в тях са описани подробности, които принципно не са необходими на хората, които ги четат, затова няма и нужда да бъдат дискутирани от заинтересованите в тях, но тази информация е нужна, за да може протоколът да работи правилно след превеждането на информацията в цифровия език, който е понятен на изчислителната машина.
- Публикация = високо ниво на абстрактен език, написана на обикновен английски и с разписани математически формули, съдържа доказателствена част за сигурност.
- срещу Код = той се занимава с всяка подробност с точност, написан е на Хаскел /Haskell/; Ако имате код, можете ли да прехвърлите доказателствената част на публикацията в програмното изпълнение на проекта?.
Малки стъпки – без големи скокове
- Малките стъпки позволяват по-лесната проверка и затвърждаване, че всяка една от тях е била в правилната посока.
- Първата стъпка е да се преведе алгоритъмът на понятен официален език (без да бъдат добавяни никакви ненужни подробности – оставяйки алгоритъмът на същото абстракционно ниво, на което е записан и на хартия), но с цел да се достигне до информация, която да може да бъде разчитана и интерпретирана от изчислителна машина.
- След като сте получили тази точна, но абстрактна част, вече можете да работите по нейното усъвършенстване и да добавяте повече подробности към кода.
- Стъпките на работа трябва да са достатъчно малки, за да позволяват проверка и тестване, за да може да се затвърди, че точно тези са правилните стъпки на работа и едновременно с това никоя от тях не променя протокола по нежелан начин.
- По време на работния процес, при всяка една направена стъпка, се правят задължително симулации и тестове на кода.
Process Calculi - Процес на смятане
- Първата стъпка е преводът на официален език
- и какъв трябва да бъде този език?
- Блокчейн-веригите се състоят от много компютри, които комуникират помежду си и извършват разпределено изчисление на регистъра на данни.
- В компютърните науки, процесните изчисления /process calculi/ са разнообразно семейство свързани подходи за официално моделиране на едновременни системи.
- Избраното изчисление на процеса се нарича: “Psi Calculus” (параметрично семейство от изчисления на процесите).
Специфични езици на вградените домейни (Embedded Domain Specific Languages – EDSLs)
- Желателно е да се вгради този процесорен език в “Haskell“.
- Възможно е да се използва всеки език, но е по-лесно да се разсъждава и работи, ако езикът съвпада с домейна.
- примери за това: “PostScript” за описание на страници с текст или графики; “SQL” за бази данни.
- За вграден “DSL” → трябва да се създаде език в езика, което позволява да се използва синтаксиса и структурите на хост-езика /езикът приемник/ и след това да използвате самата програма, като термин за данни в рамките на този език .
- Вграденият “DSL” позволява множество интерпретации.
Вграждане на “Psi” в “Haskell”
- Внедрете “Psi Calculus” като “EDSL” в “Haskell”, след това напишете “Ouroboros Praos” на този език
- след това, написвайки различни преводачи за езика можете:
o да получите симулатори за програмата
o или да експортирате кода към синтаксисна система за проверка (като: “Isabelle” или “Coq”);
o да създадете преводач, който да изпълнява цялата плеяда от процеси и едновременно да има способността да прибавя допълнения, което в крайна сметка да го превърне в производствения код на системата.
Моделиране на ефективността (и на неуспеха)
- Това, от което се нуждае в PoS-протокола, е добро управление на производителността на системата.
- Преди старта са зададени еталони.
- Използвани са възли, работещи на различни континенти, които, при увеличаване на натиска, чрез изпращане на транзакции, позволяват откриването на параметри, които могат да бъдат анализирани и настроени с цел увеличаване на производителността на процеса.
- “IOHK” са искали да направят справка, не само чрез експерименти, но и тествайки теорията за това, колко добре трябва да работи този код.
- При извършването на експерименти, се получават сравнителни данни, но е необходимо да се разбере, каква е причината за получените резултати и кои параметри биха били оптимални.
- Следването на горепосочените стъпки позволява да се отговори на въпроси свързани с протокола, като:
o Колко време отнема записа на транзакциите?
o Колко време отнема присъединяването към мрежата?
o Могат ли блоковете да се разпространяват по цялата мрежа в един слот?
o Какви са ресурсните изисквания за създаването на възел?
Нарушение на качеството: ΔQ
- Време спрямо вероятността, че в определено време, ще е възникнало някакво събитие.
- В перфектни системи ще имате линия, която в даден момент се доближава до единица.
- Системите в реалния свят могат да се провалят и обикновено не са способни да достигнат единица, тъй като се „насищат“ на по-ниски нива и разликата, която се получава между тази линия на насищане и единица, отговаря на шанса за неуспех, ако се изчака произволен период от време = неправилна Кумулативна функция за разпределение.
- Това е нещо, което може да се моделира в “Haskell”.
- Това се постига, когато на ΔQ се зададе функция, която да приема състоянието на генератора на случайни числа.
- ΔQ-формулите могат да се използват за създаването на симулации, но също така и за алгебричното съждение с тях.
- Това се използва, при разглеждане на различни сценарии, като: паралелен сценарии или последователен композиционен сценарии.
Имплементации на блокчейн с висока степен на сигурност
- Криптовалутите притежават високи стойности.
- Поради това “IOHK” смятат, че е правилно да се правят системи с голяма степен на сигурност.
- Изследователите доказват неща за протокола, но също така трябва да се уверят, че доказателствата няма да се изгубят в превода.
- Възникват предложения за използването на блокчейн-технологията за критично важни инфраструктури, като тази отговорна за актовете на земеделска и неземеделска земи
- Следователно възниква нуждата от системи, подходящи за целта, които са проектирани за оптимална производителност, като същевременно с това са доказуемо сигурни.