Смарт-контракт как угроза безопасности блокчейн-стартапа

    Смарт-контракты Ethereum, если верить официальному сайту, выполняются «в точности так, как запрограммированы, без какой-либо возможности простоя, цензуры, мошенничества или вмешательства третьей стороны». Сегодня я попробую разобраться, так ли всё радужно на самом деле, рассмотрев некоторые проблемы, с которыми пользователи смарт-контрактов сталкиваются на практике.


    В конце статьи я резюмирую свои размышления краткой инструкцией по написанию безопасных смарт-контрактов.


    image


    Ремарки


    1. Речь в статье пойдёт только о смарт-контрактах Ethereum. Сообщество молчаливо отождествило «smart contracts» с «Ethereum smart contracts». Меж тем первое — скорее концепция, а второе — реализация, и вопрос о том, насколько эта реализация отвечает концепции, можно обсуждать (как и в принципе саму концепцию смарт-контрактов и другие возможные имплементации). Это тема сложная, недооценённая и интересная, но это не тема данной статьи, поэтому интересующихся отошлю к работам Nick Szabo. Соответственно, везде далее, где я говорю «смарт-контракты», я на самом деле имею в виду «смарт-контракты Ethereum».
    2. Речь в статье пойдёт только о языке смарт-контрактов Solidity как о самом популярном и для пользователя Ethereum по сути единственном на данный момент.

    Проблемы безопасности смарт-контрактов


    Речь пойдёт о проблемах, с которыми в итоге сталкиваются разработчики смарт-контрактов, а не о безопасности самой платформы (хотя немного и о ней). Условно разделим эти проблемы на следующие типы:


    1. проблемы в коде смарт-контракта;
    2. проблемы в процессе разработки;
    3. проблемы в языке;
    4. проблемы в концепции.

    1. Проблемы в коде смарт-контракта


    Под проблемами в коде смарт-контракта здесь я подразумеваю такие проблемы, которые решаются редактированием .sol-файла. Это, в частности:


    • Известные уязвимые конструкции (например, re-entrancy).
      Пример из жизни: re-entrancy, или, шире, нарушение паттерна Checks-Effects-Interactions — даже широко известные (и ранее проэксплуатированные) уязвимости продолжают встречаться в новых контрактах.
    • Авторские уязвимые конструкции (в частности, ошибки в логике кода).
      Пример из жизни: MultiSig-кошелёк, который на самом деле не MultiSig. Для того чтобы подписать транзакцию и перевести средства, необходимо количество подписей владельцев кошелька, равное required. При этом для того чтобы поменять required (например, на единицу, чтобы дальше самому подписывать транзакции), достаточно подписи только одного из владельцев:

    image
    image


    • Неудачная архитектура.
      Пример из жизни: попытка имплементировать в рамках одного контракта и токен, и кошелёк, и хранилище ключей. Контракт получается чрезмерно усложнённым, код сложно поддерживать, аудировать, модифицировать. В итоге страдает и безопасность.
    • Низкое качество кода.
      Пример из жизни: контракты с разными отступами, произвольными переходами на новую строку и пробелами. Код трудно читать, а значит, снова страдает безопасность. При том, что для Solidity уже есть линтеры (Solium, Solhit).

    image
    image


    Проблемы в коде непосредственно приводят к атакам и потере средств. Хорошая новость в том, что проблемы в коде можно выявить в процессе аудита и устранить. При этом важно понимать, откуда они берутся, чтобы избежать их в дальнейшем. Поэтому переходим к следующему пункту.


    2. Проблемы в процессе разработки


    Проблемы в коде обусловлены в первую очередь неправильно выстроенным процессом разработки. Казалось бы, разработка ПО — дело давно изученное, с устоявшимися best practices. Тем не менее, молодость области смарт-контрактов, непропорционально большие деньги и хайп приводят к тому, что люди по тем или иным причинам пренебрегают стандартными процедурами, что часто приводит к серьёзным проблемам. Из самого типичного стоит упомянуть:


    • ТЗ: большинство смарт-контрактов Ethereum пишется без технического задания. К чему это может привести, объяснять излишне.
    • Сроки: в среднем на разработку выделяется очень мало времени, порядка месяца. Экстремальный пример из моей практики: заказчик попросил разработчика написать смарт-контракт за 3 дня до ICO.
    • Уровень разработчика: в область приходит много людей, в том числе вообще без бэкграунда в программировании.
    • Понимание экосистемы: а даже если с бэкграундом, то зачастую разработчики недостаточно глубоко погружены в тему и не понимают специфику смарт-контрактов.
    • Цена разработки: и тем не менее, тех, кто пишет смарт-контракты, мало; ещё меньше тех, кто пишет их хорошо. Отсюда неоправданно высокая цена разработки.

    3. Проблемы в языке


    Добавляет дёгтя сам язык Solidity. Изначально он был создан скорее для того, чтобы его могли быстро освоить большое количество людей, чем для того, чтобы на нём было удобно писать безопасные смарт-контракты. Вот лишь некоторые его особенности, которые мешают безопасности:


    • Множественное наследование, using for, call/delegate call — всё это запускает код не из текущего исходника, а значит, снижает читаемость и, как следствие, безопасность кода.
    • Checks-Effects-Interactions pattern — если конструкции, нарушающие CEI, небезопасны, то почему не запретить их (и многие другие) просто на уровне языка?
    • Вызывая другой контракт, можно внезапно попасть в его fallback-функцию с неожиданными последствиями.

    Понятно, что проект Ethereum развивается, и невозможно всё учесть заранее. Но в итоге разработчики вынуждены помнить о многих особенностях и пользоваться костылями, чтобы сделать свой смарт-контракт безопасным.


    4. Проблемы в концепции


    Однако самая серьёзная проблема ещё глубже — в том, что многие недостаточно хорошо понимают, для чего смарт-контракты нужны, что они могут, чего не могут и как работают. В худшем случае это приводит к тому, что смарт-контракт:


    1. Не смарт:


      • Плохо написан — делает то, что написано, но не то, что задумано.
      • Сильно завязан на backend и/или frontend — а этот код уже не смарт-контракт, он выполняется обычным образом, и его выполнение полностью контролирует администратор сервера.

    2. Не контракт:


      • Не фиксирует обязательства сторон — например, ICO продаёт свои токены за ETH, но токены по сути являются фантиками, т.к. не налагают на того, кто их выпустил, никаких ограничений или обязательств.
      • Допускает односторонние изменения — и получается, что одна из сторон может менять контракт уже после его подписания.

        Пример из жизни: владелец контракта может произвольно менять капитализацию, курс и продолжительность продажи токена:

        image

    3. Не нужен:


      • Смарт-контракт добавили не потому, что он был технически необходим, а в попытках придумать, что бы сделать на смарт-контрактах, и оседлать волну хайпа;
      • Пытались придумать, как к существующему продукту прикрутить смарт-контракты.

        image


    Смарт-контракт как угроза безопасности блокчейн-стартапа


    Что же в итоге? Хотели модно, безопасно, блокчейн, а получаем дорогой неподдерживаемый код, который угрожает безопасности и вообще не нужен. Хотели, чтобы наши смарт-контракты выполнялись «в точности так, как запрограммированы, без какой-либо возможности простоя, цензуры, мошенничества или вмешательства третьей стороны», и в итоге они действительно выполняются так, как написаны — только написаны они с уязвимостью. И нам остаётся лишь помахать ручкой своим средствам. Ну или сделать хардфорк (тем самым вообще-то дискредитировав саму исходную идею), если из-за уязвимости потеряли деньги в том числе создатели Ethereum.


    image


    Как писать безопасные смарт-контракты


    На самом деле, конечно же, всё не так плохо. Я просто сгущаю краски в попытках обратить внимание на некоторые важные, на мой взгляд, моменты. В целом же область развивается, люди учатся, в том числе и безопасности.


    Если же читатель решит-таки написать смарт-контракт, я бы посоветовал:


    • понять, зачем нужен (и нужен ли) смарт-контракт;
    • получить от заказчика или самостоятельно написать ТЗ;
    • рассчитать время;
    • использовать инструменты разработки и тестирования (Truffle, Remix, SmartCheck, линтер Solhint или Solium);
    • написать тесты;
    • провести несколько независимых аудитов и bug bounty;
    • следить за безопасностью остальных составляющих проекта (сайт, Twitter и т.п.).

    Следуя этим простым рекомендациям, можно избежать большинства описанных выше проблем (от хардфорка, впрочем, это всё равно не спасёт).


    Статья была создана совместно с Евгением Марченко (eMarchenko).

    Ростелеком-Solar

    206,82

    Безопасность по имени Солнце

    Поделиться публикацией
    Комментарии 47
      +1
      Картинка вначале статьи полностью отражает моё мнение о разговорах вокруг блокчейна.
        0
        Это правда, разговоров очень много, и, к сожалению, очень существенная часть — не по делу. Тем не менее трудно отрицать, что что-то из этого точно получится, а что именно — покажет время. Мы со своей стороны стараемся не фантазировать, а решать практическую задачу безопасности.
          +1

          Мне лично нравится, что больше спецов и денег пришло в область разработки алгоритмов для распределенных систем. Это точно полезно и рождаются уже новые алгоритмы и программы обучения. Это точно полезно для всего IT и останется даже если ethereum и bitcoin исчезнут.

        +2
        Мне вот интересно, как смарт контракт вообще можно связать с реальным миром, если это только не простенькая голосовалка?
        В умных книгах приводят кучу примеров, что смарт контракты могут заменить чуть ли не что угодно. Но для меня большой вопрос, можно ли принципиально реализовать следующие схемы:

        1. Я заключил пари с другом на выигрыш Динамо, как смарт контракт «поймет», что произошел выигрыш? Если смарт-контракт должен выкачать данные из REST API (и возможно ли это вообще в Эфире?), то что будет, если сервер ляжет, или вернет разные результаты? Ведь все участники эфира должны выполнить команды смарт контракта, чтобы его провалидировать.

        2. Или же я создал смарт контракт на установку ворот в гараж. Как смарт контракт в принципе может «понять», что работа выполнена? В отличие от предыдущего примера, здесь вообще нет какой-то незаинтересованой стороны, которой есть хоть какое-то дело до этих ворот. При этом различные статьи и книги постоянно ссылаются на то, что это и есть область применимости смарт контрактов (разве что только рак не лечат).
          +4
          Вопрос на самом деле очень важный.

          Если отвечать на него строго, то любая связь с внешним миром — это уже не смарт-контракт. Корректность обработки данных внутри смарт-контракта гарантирована математически (с оговорками); корректность внешних данных гарантирована математически быть не может. В строгом смысле в рамках смарт-контракта могут быть имлементированы только передачи эфиров/токенов по определённым заранее заданным правилам, в частности, игры (хотя, например, получение случайного числа внутри смарт-контракта — тоже нетривиальная задача).

          Если же отвечать на вопрос с практических позиций, то сейчас связь с внешним миром реализована при помощи оракулов, подробней можно почитать, например, тут. В двух словах — с помощью third party контрактов, создатели которых зарабатывают тем, что помещают в блокчейн Эфириума достоверные данные о внешнем мире. Более детальный ответ заслуживает отдельной статьи.

          Что касается двух предложенных кейсов:
          1. Смарт-контракт сам не может выкачать данные по двум причинам: во-первых, он запускается не сам, а только по запросу пользователя (или другого контракта), во-вторых, он не может обращаться к внешнему миру. Так что, напротив, пользователь (или сервер) обращается к смарт-контракту, помещая в него данные. При этом технически гарантировать, что данные пришли именно из определённого источника (например, доверенного спортивного сайта) нельзя; но другие пользователи смогут проверить результат и сообщить, если оракул соврал. Соответственно, проблемы с выполнением смарт-контракта не возникает, т.к. это не он запрашивает данные с сервера, а сервер вызывает его; если сервер не отработает — не будет вызван контракт.
          2. Статьи, которые ссылаются на то, что кейс с гаражом — это и есть область применимости смарт-контрактов, на мой взгляд ошибочны. Эта проблема действительно не решена и строго решена не может быть. Но можно говорить о том, что смарт-контракты не устраняют необходимость в доверии, а снижают её. Т.е. если раньше мне нужно было доверять, что а) в систему корректно будут введены данные об установке ворот, б) заказчик после этого преведёт деньги, то теперь б) автоматизировано, и доверять остаётся только в а).

          Уточню, что мой ответ носит очень поверхностный характер. Хороший глубокий ответ — отдельная статья. Спасибо за вопрос и идею для статьи!)
            +1
            А что будет, если выяснится, что оракул наврал?
              +3
              С точки зрения смарт-контракта уже ничего не исправить: данные попали в него, отыграть назад не получится (если только такой механизм явно не реализован в коде самого контракта). С точки зрения оракула — как минимум, этому оракулу перестанут доверять (по идее). Кроме того, оракул может, например, обещать неустойку в случае предоставления недостоверных данных (на практике не знаю таких). Но технически уже ничего не сделаешь. Оракул по сути и является single point of failure, тем самым местом, где мы вынуждены доверять (оракулу). Бороться с этим можно по-разному: например, использовать несколько оракулов и в качестве финального ответа брать результат их «голосования».
                0
                Ну кому-то же надо доверять :) А оракул это как раз не заинтересованная третья сторона. С таким же успехом можно не доверять ОС в которой работаете с конфиденциальными данными, родным, близким, друзьям и т.п. Кому-то/чему-то нужно доверять.
                В принципе открытость смарт-контрактов и возможность провести аудит безопасности кода контракта и даёт гарантию того что лишнего там не выполнится.
                  0
                  Я не о том, что оракулу доверить нельзя. Но может наврать не специально, всякое в жизни бывает.
                  Я пытаюсь выяснить, как мне гарантированно вернуть деньги, когда через какое-то время выяснится, что контракт реально не был выполнен, а деньги ушли?
                  Понятно, что это будет в теории, т.к. и сейчас можно так же сбежать, увести деньги со счетов и придумать ещё кучу действий, но во всяком случае есть механизмы, принцип работы которых, хотя бы в теории гарантирует возврат средств. В плане криптовалют я сейчас не вижу ни одного механизма, который бы смог обработать реальные случаи.
                    0
                    Я пытаюсь выяснить, как мне гарантированно вернуть деньги, когда через какое-то время выяснится, что контракт реально не был выполнен, а деньги ушли?

                    Опять же. Это всё логика смарт-контракта. Суть в том что перед тем как им воспользоваться вы можете его «прочитать» и удостовериться что деньги которые вы отправите смогут вернуться. Если в коде это будет прописано — деньги вернутся согласно выставленным условиям.
                    Механизмы есть, но они закладываются разработчиком смарт-контракта.
                    Это всё очень тесно связано с тем как в реальном мире заключаются контракты. Мелкий шрифт, расплывчатые понятия, сомнительные обязательства сторон… всё это можно заложить и в смарт-контракт :) Единственное что обеспечивают смарт-контракты — их нельзя поменять, всё видно как на ладони, всё будет выполнено так как запрограммировано, отдельные какие-то транзакции скрыть или удалить не удастся.
                    Т.к. смарт-контракт всё равно создаёт человек, то и ошибки, обман и прочие людские грехи могут быть в него заложены, увы.
                      0
                      Давайте не будем путать смарт-контракты и оракул. Вопрос касается именно оракула. Ваш ответ справедлив только для смарт-контракта.
                    0
                    Ну кому-то же надо доверять :)
                    — это не совсем так. Зачем доверять какой-то единой централизованной сущности? Что касается ОС, то некоторые люди и тут последовательно идут до конца, и сами собирают дистрибутив ОС из подписанных исходников. Даже BIOS есть с открытым исходным кодом. И да, свои пароли я даже близким не доверяю — не потому, что они обманут, а потому, что хуже знают ИБ, чем я.
                    И нет, аудит смарт-контракта не даёт гарантию того, что оракул не обманет, потому что то, что делает оракул, как раз лежит вне смарт-контракта.
                  +1
                  Спасибо, это многое объясняет!
                    0
                    Если вам действительно интересен механизм доказательств событий внешнего мира, то почитайте о проекте Augur. У них очень интересная концепция решения данного вопроса.
                    +7
                    Голосую за полноценную статью! Многим будет полезно разобраться, как контракты работают вне сферического вакуума с конями.
                    +1
                    но другие пользователи смогут проверить результат и сообщить, если оракул соврал.

                    Ок, сообщили, но смарт-контракт уже выполнен, деньги ушли не туда. Что потом? Оракул возмещает потери своими деньгами, или просто все разводят руками и говорят "ну опаньки, бывает"?

                    0
                    Смартконтракты в блокчейне не могут получать доступ к внешним ресурсам, потому что их выполнение должно быть постояемо и не может зависеть от доступности ресурса в конкретный момент для конкретного узла.
                    Но если рассматривать смартконтракты вне блокчейна (в многопользовательской игре, корпоративной системе и тп), то такой доступ возможен. Например, факт установки ворот проверяется по показаниям доверенного GPS-треккера и фотографии с привязкой к месту и времени.
                      0
                      При этом в человеческом мире если Nepherhotep не получил ворота и есть контракт (не смарт) — он может пойти в суд и возместить не только свои потери (вернуть деньги по контракту), но и (в теории) получить дополнительное возмещение, никто не скажет «ой, извини, мы ему погрозим пальчиком, но денег не вернуть». Конечно, может не быть контракта или исполнитель может сбежать, но смарт-контракты от этого тоже не страхуют, вообще. Можете мне возразить «но там же сумма не выплачивается до подтверждения» и будете не правы — «на материалы» предоплату они всё равно получат (как и без смарт), а оплата работ — после подтверждения (когда без смарт).
                        0
                        Суд тоже не гарантия — ответчик может сбежать или обанкротиться.
                        Кстати, и смартконтракт можно написать так, что бы он признавал решения суда.
                          0
                          Сбежать или обанкротиться человек может и с криптовалютой.
                          Только в реальном мире в банк уходит исполнительный лист о взыскании определённой суммы денег и банк обязан вернуть деньги пострадавшей стороне со счёта ответчика(да, можно успеть увести деньги, но это из другой оперы).
                          Как это можно реализовать в криптовалютах, учитывая, что их создатели принципиально позиционируют валюту как «вне юрисдикции»?
                          Что будет, если суд Зимбабве примет одно решение, а Уругвая другое? В реальном мире в договорах обязательно пишется пункт, что разбор конфликтов производится согласно законодательству страны Х
                            0
                            В смартконтракте тоже можно прописать, что признается решение суда, подписанное таким то ключем.
                            Отличия, по большому счету, а том, что с криптой значительно проще сбежать. Ну и отсутствие неявно прописаных общих законов.
                              0
                              Всё-таки я не могу понять как наложить крипту и смартконтракты на реальную жизнь.
                              Вполне возможная сейчас ситуация:
                              1. Допустим, что заказчик не получил ворота, и таких заказчиков много;
                              2. Сразу после получения денег, исполнитель переводит их на счёт своего брата/свата/друга, чтобы его счета были пустые;
                              3. Заказчики подают в суд на исполнителя и суд признаёт схему мошеннической, постановляет вернуть деньги, а также, что переводы родственникам были частью схемы, а потому также должны быть отменены (или деньги вернуть сразу с их счетов);
                              4. В банк идут исполнительные листы на нужные переводы денег, которые банк исполняет.

                              Теперь собственно вопрос, как смартконтракт, оракулы или ещё что-то смогут обеспечить, что деньги будут возвращены не непосредственно от исполнителя, а от третьих лиц? Ведь в реальной жизни куча ситуаций, когда схемы мошенничества/вывода активов и т.п. могут состоять из множества этапов.
                                +1
                                Смартконтракт может резервировать средства на своем аккаунте и, например, позволять тратить какую-то сумму для оплаты части закупаемых для работ материалов, а перевод на другой счет разрешать только после подтверждения выполнения заказа.
                                  +1
                                  Не буду комментировать весь тред, скажу лишь, что как раз вот такие вещи смарт-контракты позволяют делать удобно и дёшево:
                                  1) замораживать средства;
                                  2) размораживать только с подтверждения обеих сторон или арбитра;
                                  3) позволять переводы только на определённые аккаунты (например, поставщика материалов);
                                  4) предоставлять залог на случай мошенничества любого рода
                                  и т.д.
                                  Другими словами, грамотное использование смарт-контрактов позволяет не исключить мошенничество, но усложнить его (что тоже неплохо).
                                  Кроме того, технически довольно просто в бумажном договоре отождествить стороны с адресами в блокчейне. А вот вопрос признания такого договора государственным судом — это уже вопрос не к смарт-контрактам, а к судебной системе.
                                0
                                А зачем тогда смарт-контракт, если договор всё равно нужен (иначе с чем в суд? он не сделал, но и не обещал — смарт-контракты для суда не сильнее надписи на заборе). Хоть discovan в своём сообщении разъяснил область применения, а то у евангелистов ими разве что рак не лечат.
                                  0
                                  Как замена услуг банков и, частично, нотариусов.
                    0
                    Совершенно верно, смарт-контракт выполнен, деньги ушли, тут уже ничего не поделаешь. Как оракулы поступают в такой ситуации на практике — интересный вопрос, сходу не отвечу (возможно, освещу в уже запрошенной выше следующей статье). Среди возможных способов решения: 1) неустойка, которую по сути и описали вы, 2) в принципе не полагаться на один оракул, а брать результат «голосования» нескольких. Но пока в случае ошибки оракула всё скорее всего на уровне «ну опаньки, бывает».
                      +2

                      По-моему, это чуть ли не более фундаментальная проблема, чем плохо написанные контракты. С одной стороны, система полагается на данные, которые не являются 100% достоверными (по сути, любое взаимодействие с внешним миром), с другой — принципиально не имеет никаких механизмов отката.

                        0
                        Проблема действительно фундаментальная. Будет она решена или нет, станет ли её нерешаемость принципиальной проблемой для смарт-контрактов — для меня вопросы открытые. Но как минимум можно говорить о том, что смарт-контракты позволяют если не избавиться от доверия, то уменьшить его (см. выше в комментариях кейс с гаражом). А также о том, что смарт-контракты, как и любой другой инструмент, следует использовать, помня о границах их применимости.

                        Ну и в любом случае остаётся ряд применений (непонятно, насколько полезных, но тем не менее), никак не завязанных на оракул: например, multisignature кошельки, токенсейлы, временная заморозка средств и т.д.
                          +1
                          Проблема есть, но я пока не слушал, что бы из-за нее кто-то потерял деньги.
                          На практике она решается голосованием нескольких независимых оракулов. Можно предусмотреть отзыв лицензии у оракула, если он будет пойман на нечесной игре.
                          То есть проблема больше социальная, а не техническая.
                            +2
                            Вопрос остаётся открытым: «Как при этом вернуть потери из-за нечестной игры оракула?»
                              +1
                              Например, признавать оракула, который резервирует некую сумму на возмещение ущерба, если его поймали на обмане. Правда тут переход проблемы на следующий уровень — как этот обман доказывается? В простейшем случае голосованием коллегии оракулов.
                                0
                                С точки зрения смарт-контракт — никак, т.к. мы уже за его пределами, на поле централизации. Но при этом на наши отношения с централизованным оракулом можно переносить все уже существующие практики: письменный договор, репутация, суд. Какую конкретно конфигурацию выбрать — зависит от конкретной задачи. Например, можно советовать просто обращаться к общепризнанному оракулу; такому, что для него прибыль от обмана будет меньше репутационных (и иных) издержек.
                                  +1
                                  Все прошаренные нотариусы скоро будут называть себя Эфир-оракулами))
                                  обидно, я думал от них можно наконец избавится
                                    0
                                    Хохотнул) А если серьёзно, то, может, что-то похожее и будет. По крайней мере уже есть юридические конторы, которые пытаются смарт-контракты учитывать в бумажном договоре.
                            +2
                            Интересно было б почитать полноценную статью про разработку смарт-контрактов и их отладку, инструментарий и т.д
                              +1
                              Может, напишем такую, спасибо за интерес!
                                0
                                поддерживаю
                                +1

                                Ну и не надо забывать о тонкостях самого солидити, когда код "интуитивно понятен", но делает он совсем не то, чего от него ждут:


                                https://github.com/alatushkin/not-so-smart-contracts


                                Что в купе с низкой квалификацией новообращённых творит просто чудеса

                                  0
                                  Да, и такая проблема есть. За ссылку спасибо!
                                  +1
                                  А про формальную верификацию кто-нибудь думает?
                                  На мой взгляд язык смартконтрактов должен быть максимально строгий, с развитой системой типов, неограниченными целыми и натуральными числами (возможно, с оплатой за максимальную величину). В идеале, он вообще не должен позволять ошибиться и программировать на нем должны не программисты (умеющие тестировать, придерживаться процессов разработки, копипастить и тп), а люди, владеющие предметной областью — юристы и экономисты. При этом простота разработки не требуется, важна возможеость формально доказать свойства кода.
                                    +1
                                    Полностью поддерживаю ваши слова о том, каким должен быть язык смарт-контрактов.
                                    Что касается формальной верификации: думают, наболее актуальная информация должна быть тут (сам ещё не слушал).
                                      0
                                      Спасибо, послушаю. Про K-framework я слышал хорошие отзывы, но сам пока не разобрался.

                                  Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                                  Самое читаемое