Д-р Петър Цанков е старши научен изследовател във Факултета по компютърни науки в Швейцарския технологичен университет (ЕТН Zurich), където работи по създаването на нови методи за автоматизирана защита на съвременни софтуерни системи, включително умни договори за блокчейн, системи базирани на изкуствен интелект, компютърни мрежи и други. Той е съосновател на ChainSecurity – швейцарски стартъп, който се превръща в световен лидер по сигурността на умните договори и бе придобит от PricewaterhouseCoopers през януари 2020.
Как се развива сигурността на умните договори?
Интересът ми към сигурността на умните договори се зароди след първия пробив в най-известния умен договори в Ethereum, DAO, който доведе до загубата на $150,000,000. Този инцидент беше силно публицизиран в медиите и по този начин стигна и до мен. В този момент не бях запознат с концепцията на умните договори, въпреки че бях чувал за блокчейн и криптовалути. Научих, че умните договори са програми, които не само контролират огромни суми криптовалути, но също така и не могат да бъдат променени след активация, дори и това да е необходимо, за да се коригират грешки в техния код. В този момент ми стана ясно, че сигурността на умните договори е от изключителна важност и че програмистите ще трябва не само да тестват техния код, но също така и да гарантират че той е безгрешен, използвайки прецизни математически методи.
Започнахме да разработваме система, която автоматично намира уязвимости в умните договори, за да предотвратим атаки подобни на тази изпълнена срещу DAO договора. Важно беше да създадем система, която математически гарантира, че даден умен договор е защитен от този тип атаки. Разработихме този проект в Швейцарския технологичен университет заедно с други колеги и докторанти в лабораторията, преди да се стигне до основаването на стартъпа ChainSecurity.
Както често стартират великите проекти… От университета. Как бе приет проектът от Ethereum екосистемата?
Направихме демо версията на системата публично достъпна през лятото на 2017. Редица програмисти на умни договори за Ethereum се свързваха с екипа с въпроси, свързани със сигурността на техния код. Тук е важно да се спомене допълнителен контекст, свързан с времето, в което ние направихме системата достъпна. В периода 2017 и 2018, станахме свидетели на мащабни пробиви в умните договори за милиони долари. На всеки няколко седмици имаше нова сериозна атака. До известна степен, атаката на DAO договора мотивира не само изследователи в сферата на сигурността, но също така и хакерите които се се възползваха от уязвимости в умните договори. Именно затова програмистите на умни договори държаха техният код да бъде цялостно проверен от системи като тази, която създадохме.
В този момент ми стана ясно, че има силен комерсиален интерес за гарантиране на сигурността на умните договори. Заедно с колеги решихме да създадем стартъпа ChainSecurity, който да се фокусира върху този проблем. Нашата първа стъпка беше да подобрим прототипа, който бяхме разработили в университета като добавим поддръжка за повече типове уязвимости и го направим по-лесен за използване чрез интеграция с GitHub. През 2018 пуснахме първата официална версия на системата, която нарекохме Securify. Securify бързо стана световноизвестна система. Поканиха ни да демонстрираме системата на множество конференции по света, които допълнително допринесе към видимостта на екипа на младия стартъп. За около година, ChainSecurity се превърна в една от най-реномираните фирми в сферата на сигурността на умните договори.
А фирмата е регистрирана в Швейцария, нали така?
В Цюрих, Швейцария.
Какъв е принципът на регистриране на фирма там? И колко е голям екипът?
Необходим ти е адвокат и първоначален капитал, който е задължително да се осигури. Стартъпът бе регистриран като ETH spin-off тъй като е базиран на технологии развити в университета.
Какви други продукти разработвахте в ChainSecurity?
В средата на 2018 започнахме да развиваме втория ни основен продукт, наречен VerX. Целта на VerX е математически да докаже, че кодът на даден умен договор безгрешно имплементира функционалната спецификация на договора. Този метод за проверка на кода е известен като формална верификация (formal verification) в информатиката. Тази система е значително по-сложна, понеже всеки договор имплементира различна функционалност. Това означава, че VerX трябва да поддържа всякакъв вид спецификации.
За да използва VerX, програмистът предоставя кодът и функционалната спецификация на умния договор. Базирано на тази информация, VerX се опитва да изведе математическо доказателство, че кодът правилно имплементира зададената функционална спецификация.
Може ли да дадете пример?
Представете си че кодът имплементира посредник за събиране на инвестиции. Примерна спецификация би била: “След като инвеститорите вложат над един милион долара в умния договор, то той не позволява на инвеститорите да си изискват обратно техните инвестиции”. Този тип спецификация може да се опише математически, използвайки езици да логика. VerX ще се опита да докаже че кодът правилно имплементира тази спецификация, независимо какви транзакции ще бъдат изпратени от потребителите към договора за обработка след активация.
Според много експерти, формалната верификация е Светият граал в програмирането, който позволява да се докаже липсата на софтуерни бъгове. Този метод вече се използва за проверка на програмите които се изпълняват от самолети, автомобили, и други сфери където софтуерните грешки са допустими. Не е изненада, че този метод навлиза в сферата на умните договори. Именно умните договори са много подходящи за формална верификация, тъй като техният код обикновено е изчистен и описва само логиката на обработка на транзакциите.
Други екипи работят ли по този проблем?
Да. Трудността за създаването на система като VerX е фактът, че е теоретично невъзможно да се създаде универсална система, която автоматично верифицира коректността на произволни умни договори спрямо произволни спецификации. Именно затова, повечето специалисти в сферата доказват коректността на умните договори ръчно, като сами описват необходимото доказателство. Този процес е сложен и не само изисква специфични умения, но също така отнема месеци. Ние държахме да създадем интелигентна система, която е максимално автоматизирана и лесна за използване. VerX изисква от програмиста само да се опише спецификацията, и системата е достатъчно интелигентна, за да изведе математическото доказателство автоматично. VerX успешно и автоматично доказва коректността на умните договорите в над 95% от случаите. Напомням, че успеваемост в 100% от случаите е невъзможно, поради споменатата теоретична бариера.
VerX системата ще поддържа ли новата версия на Ethereum 2.0?
VerX поддържа EVM байт код, който е кодът на виртуалната машина на Ethereum. Новата версия на Ethereum се очаква да премине към друг формат, наречен Ethereum WebAssembly, или eWASM. Новият формат не би усложнил метода на верификация използван на VerX, така че бихме могли лесно да добавим поддръжка за новия формат.
Бих искал да попитам как успяхте да привлечете 150 000 000 долара инвестиция?
В началото на 2019 демонстрирах Securify и VerX системите в швейцарския офис на PwC. Екипът на PwC прояви силен интерес към тези продукти. След обсъждане по какъв начин да предоставим достъп до нашите системи, започнахме да дискутираме идеята PwC напълно да закупи ChainSecurity. PwC имат голямо портфолио от известни клиенти и беше ясно, че това е логична стъпка – те имат пазара и клиентите, а ние техническата експертиза и високотехнологични системи. В момента на сделката ChainSecurity се състоеше от 12 инженера.
С какво всъщност вашият продукт и вашата дейност допринасят за българската IT индустрия?
ChainSecurity е добър пример за стартъп, базиран на високотехнологичен продукт, който е конкурентен на световния пазар и е труден за репликация. Голяма част от основните конкуренти на ChainSecurity са в САЩ и Азия, не можеха да си представят как VerX постига толкова силно ниво на автоматизация. VerX намали времето на формална верификация от месеци до няколко часа, което е наистина значимо. Смятам, че е важно в България да се развиват повече високотехнологични стартъпи, базирани на високотехнологични продукти, които са конкурентни на световния пазар. По мое наблюдение, в България все още преобладават основно стартъпи, които работят в сферата на услугите, което означава, че иновациите и новите бизнес модели се развиват от други фирми извън България. Стъпката от услуги към високотехнологични продукти не е лесна. Тя изисква изграждане на система за висококвалифицираното образование в страната и развиването на иновации от световно ниво, които се публикуват в топ академични конференции.
Ако ще говорим за трендове, какви ще са те в бъдещето на блокчейн технологиите?
Според мен ще отнеме още няколко години, докато се стигне до мащабни приложения. Очаквам първите приложения да са в сферата на финансови транзакции и финансови инструменти. В Швейцария, например, активно се разработва система, която да замени сегашните системи за транзакции между банки. Това е съвсем логична стъпка. Голяма част от системите за транзакции между банки са морално остарели и са базирани на технологии от преди десетилетия. Това, което е трудно да се предвиди, е какви ще са неочакваните приложения на умните договори. Не визирам за вече съществуващи продукти, които да се заменят с умни договори с цел да се подобри тяхното ниво на сигурност, а за приложения, които не биха съществували без умни договори. По тази тема е трудно да се спекулира, времето ще покаже.
Имам един последен въпрос, два са, но ще ги комбинирам в един. Какво бихте посъветвали хората, които са неопитни и искат да се занимават с подобни технологии като вашия стартъп и какво бихте посъветвали хората, които вече са готови направят своя стартъп? От къде да започнат?
Това е много добър въпрос. За създаването на един високотехнологичен стартъп са необходими задълбочени умения в дадена сфера. Именно затова, голяма част от успешните високотехнологични стартъпи се създават след завършването на докторантура в дадена сфера. Друга важна предпоставка е да имаш достъп до екип от силно мотивирани и високообразовани специалисти, които обикновено се намират покрай силните университети. Като първа стъпка е важно да се намери тази среда.
Интервюто проведе Атанас Нейчев
