" Elrond объявил в твиттере и статье на Medium о партнерстве с Runtime Verification, в рамках которого инструментарий разработки Elrond дополнится набором формальных инструментов на основе K Framework.
«Благодаря дорогостоящим и сложным инструментам тестирования, доступным в Devkit Elrond, общая безопасность нашей экосистемы DeFi повышается до соответствия требованиям институционального уровня», - говорится в заявлении.
Elrond (eGLD) позиционируется разработчиками, как масштабируемая, быстрая и безопасная блокчейн-платформа для распределенных приложений, корпоративных сценариев использования и новой интернет-экономики.
Runtime Verification применяет формальные методы для повышения безопасности, надежности и правильности вычислительных систем для аэрокосмической, автомобильной и других отраслей, включая блокчейн.
Подробности сотрудничества раскрывает Бенджамин Минку в статье официального блога под названием «От ракет к блокчейнам: формальная проверка, впервые введенная в НАСА, применена в Elrond с помощью Runtime Verification».
Блокчейны - это проверяемые вычислительные платформы, которые оптимально подходят для будущего финансов, бизнеса и управления. Однако эта возможность на несколько триллионов долларов полностью проявится только тогда, когда перемещение сложных процессов в цепочке будет предсказуемо безопасным.
Ситуации, начиная с форка Ethereum DAO и до сегодняшних частых эксплойтов DeFi, показывают, что баги, ошибки проектирования и недостаточное тестирование представляют очень высокий риск для процессов, основанных на смарт-контрактах. Смягчение, по словам Минку, возможно с помощью проактивных и реактивных методов.
В качестве примера он приводит тестирование, которое, по его словам «невозможно» сделать исчерпывающим в сложных сценариях.
«Тестирование - это здорово, но это довольно реактивный метод. Исчерпывающее тестирование в сложных сценариях непрактично или невозможно. Вопрос в том, можем ли мы создать процесс разработки, который гарантирует правильность и безопасность с помощью дизайна?», - задается вопросом глава Elrond.
Улучшить ситуацию, по словам Минку, помогут формальные методы. Формальные методы позволяют определять спецификации любого процесса с математической точностью и строгостью. После определения процесс проходит проверку того, что формальные выражения отражают то, что на самом деле желательно, и проверку того, что желаемое является безопасным, надежным и соответствует желаемому результату.
«Таким образом, формальная проверка может устранить тонкие ошибки и логические ошибки даже на этапе проектирования, убедительно демонстрируя соответствие между требованиями и спецификациями, создавая предпосылки для безопасного процесса разработки», - говорится в статье.
Runtime Verification и Elrond
«Мы рады сообщить, что мы работаем с Runtime Verification, чтобы дополнить инструментарий разработки Elrond набором формальных инструментов на основе K Framework. Формально проверенные смарт-контракты, развернутые друг над другом, составят эффективный стек убедительных примитивов DeFi. Предоставляя своим разработчикам такие инструменты «из коробки», Elrond установит более высокие стандарты безопасности и, мы надеемся, ускорит весь процесс внедрения блокчейна в масштабе», - сказал Бениамин Минку, генеральный директор Elrond.
Основe концепции K Framework, по словам Минку, заложил «друг и советник» проекта Григоре Росу, доктор компьютерных наук, когда он работал исследователем НАСА в критических для безопасности условиях, характерных для ракет и космических кораблей. Затем Григоре основал Runtime Verification и вместе со своей командой работает над тем, чтобы разработчики блокчейнов могли использовать эти инструменты ракетостроения.
Цель сотрудничества Elrond и Runtime Verification - создать набор инструментов, который позволит разработчикам лучше писать свой код, сразу же видеть и увеличивать покрытие кода тестирования и, в конечном итоге, добавлять символическое выполнение и даже формально проверять свои смарт-контракты Elrond. Формальные методы относительно сложны и трудны для среднестатистического разработчика, но разработчики надеются, что их совместная работа будет сосредоточена на добавлении значительной степени детализации этих инструментов и снижении барьера для немедленного использования, насколько это возможно.
«Хардкорный дух Elrond освежает. Они продолжают находить оригинальные решения сложных проблем, двигаясь вперед с большой скоростью. Добавление формальных инструментов в их блокчейн в масштабе Интернета кажется важным шагом вперед для широкого принятия технологии. Приятно видеть, как наша команда сотрудничает и добивается этого», - сказал Григоре Росу, основатель и генеральный директор Runtime Verification.
Этапы сотрудничества
«После нескольких месяцев совместной работы мы уже смогли создать K-Framework реплику нашей виртуальной машины Arwen, получившей название KArwen. Arwen - это виртуальная машина WASM, поэтому Runtime Verification смогла расширить свою семантику KWasm для WASM, чтобы она соответствовала нашей виртуальной машине», - сообщает Минку.
По его словам, KArwen теперь представляет собой полностью формализованную автоматически сгенерированную виртуальную машину, которая может выполнять смарт-контракты Elrond. Это закладывает основу для расширенного формального инструментария, который будет использоваться для смарт-контрактов Elrond. Важным результатом, по его мнению, также является то, что тестирование Mandos с использованием K Framework уже позволяет разработчикам выполнять тестирование покрытия кода на более низком уровне, чем это было возможно ранее.
«Инструменты Runtime Verification помогли нам сократить объем смарт-контрактов, написанных на Rust, до 40% за счет выявления и удаления неиспользуемых функций, которые компилятор Rust добавляет автоматически.
«Следующие шаги нашего сотрудничества будут сосредоточены на дополнительных инструментах покрытия для разработчиков и интеграции новых инструментов с erdpy и нашей Elrond IDE, чтобы сделать их более доступными», - пишет Минку.
Семантика Elrond, разработанная Runtime Verification, уже доступна в репозитории на Elrond на Github.
«Сотрудничество очень важно для наших команд. Разработчики Elrond скоро смогут использовать формальные инструменты для написания более безопасных смарт-контрактов, а Runtime Verification, возможно, откроет новую эру для широкого использования более детализированных формальных инструментов, доступных для всех разработчиков», - пишет CEO Elrond.
Минку считает, что с этими инструментами экосистема Elrond будет выделяться «как главный кандидат для подавляющего большинства стартапов и компаний, желающих развернуть безопасные высокоэффективные варианты использования с производительностью в масштабе Интернета».
