Символическое тестирование с Halmos: использование существующих тестов для формальной проверки

Формальная верификация — процесс использования математических методов для «проверки» программы или смарт-контракта на любом количестве входных данных — обычно рассматривается как более краткая и всеобъемлющая альтернатива традиционному тестированию для написания более качественного и безопасного кода. Но на самом деле формальная проверка — это открытый и интерактивный процесс. Подобно модульному тестированию, разработчики должны динамически определять формальные спецификации и накладывать их друг на друга, повторяя свой подход по мере развития своего кода и анализа. Кроме того, формальная верификация эффективна настолько, насколько эффективны ее спецификации, написание которых может занять много времени (и часто сопряжено с крутой кривой обучения). 

Для многих разработчиков, которые находят этот процесс сложным, модульные тесты часто являются более экономичным и быстрым способом проверки правильности программы. На практике формальная верификация — это не более полная альтернатива модульному тестированию, а дополнительная. Эти процессы имеют разные сильные стороны и ограничения, обеспечивая еще большую надежность при совместном использовании. Разработчикам всегда нужно будет писать модульные тесты — что, если бы мы могли использовать те же свойства для формальной проверки?

Халмос, наш инструмент формальной проверки с открытым исходным кодом, позволяет разработчикам снова использовать те же свойства, написанные для модульных тестов для формальных спецификаций посредством символьного тестирования. Вместо того, чтобы создавать надежный набор свойств с самого начала, разработчики могут избежать дублирования работы и улучшать свои тесты по нескольким спецификациям за раз, не начиная с нуля. Мы разработали этот инструмент для использования, наряду с другими, в процессе формальной проверки, как переход к формальной проверке; разработчики могут начать с нескольких анализов с минимальными усилиями, прежде чем добавить больше позже в процессе.

В этом посте мы рассмотрим проблемы формальной проверки и возможность преодолеть разрыв между модульным тестированием и формальной проверкой с помощью символического тестирования. Затем мы рассмотрим демонстрацию Halmos с использованием существующего кода смарт-контракта и кратко рассмотрим другие формальные инструменты проверки (многие с открытым исходным кодом), доступные разработчикам.

Формальная проверка против тестирования

Формальная проверка — обычно предпочитаемый разработчиками блокчейна за его строгость и полноту — это процесс доказательства правильности программы путем проверки того, что она удовлетворяет определенным свойствам правильности. Свойства, специфичные для программы, обычно предоставляются извне и выражаются с использованием формального языка или нотации, которые поддерживаются используемым инструментом проверки. Разработчики часто воспринимают формальную верификацию как простое решение для автоматического тестирования свойств во всех возможных сценариях, но на самом деле формальная верификация может быть трудоемким и очень интерактивным процессом.

Как и формальная проверка, модульное тестирование включает в себя оценку того, работает ли программа должным образом; тестирование, однако, только проверяет поведение программы на некоторые входные данные, в то время как формальная проверка может проверить их на наличие Найти возможные входы. И тестирование, и формальная верификация требуют описания ожидаемого поведения программы (с тестовыми примерами, используемыми при тестировании, и формальными спецификациями, используемыми при формальной верификации). Но при совместном использовании они могут обеспечить более тщательное изучение программы. Тестирование, например, эффективно для поиска простых багов и ошибок, но, как правило, выполняется быстрее и легче. Формальная верификация, хотя и более обременительна в использовании, достаточно мощна, чтобы доказать отсутствие ошибок или выявить тонкие ошибки, которые легко пропустить при тестировании или проверке кода.

Накладные расходы спецификации

Одна из основных проблем формальной верификации — накладные расходы на написание и поддержание формальных спецификаций. Этот процесс часто включает в себя трудоемкую задачу ручного написания спецификаций с использованием специального языка (который многим разработчикам придется сначала изучить). Этот процесс также является пошаговым, обычно начиная с написания простых свойств и их проверки, а затем постепенно добавляя более сложные свойства. Как и тестирование, это процесс с открытым концом, без четкой точки остановки, и можно добавить только столько свойств, сколько возможно в течение доступного периода времени. Кроме того, когда разработчики изменяют код во время его проверки, они также должны обновлять свои существующие спецификации, что приводит к дополнительным усилиям по обслуживанию. Эти факторы могут сделать формальную проверку сложной задачей для некоторых разработчиков, которые не решаются брать на себя дополнительные накладные расходы.

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

Преодоление разрыва между тестированием и формальной проверкой с помощью символического тестирования и Halmos

Символическое тестирование, практика запуска тестов с символьными входными данными, является эффективным формальным методом проверки, который снижает накладные расходы на спецификацию. Такой подход позволяет использовать одни и те же тестовые примеры как для тестирования, так и для формальной проверки. В отличие от традиционного тестирования, которое проверяет правильность работы программы для ограниченного набора входных данных, символьное тестирование проверяет программу на наличие всех возможных входных данных, поэтому программа, прошедшая символическое тестирование, может считаться формально проверенной.

Halmos — это формальный инструмент проверки, предназначенный для символьного тестирования. Вместо того, чтобы требовать отдельных спецификаций или изучать новый язык, Халмос использует существующие тесты в качестве формальных спецификаций. Запуск тестов через Halmos автоматически подтвердит, что они пройдены для всех возможных входных данных, или предоставит контрпримеры. Это не только устраняет необходимость в написании дополнительных спецификаций, но также позволяет повторно использовать тесты, написанные для модульного тестирования или фаззинга, в целях формальной проверки.

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

Пример: Тестирование isPowerOfTwo() функция

В качестве примера рассмотрим следующее isPowerOfTwo() функция, которая определяет, является ли данное число степенью двойки. Эта функция использует алгоритм обработки битов для эффективности, но может быть сложно доказать его правильность, особенно в случае, когда входные данные не являются степенью двойки.

Представьте себе следующий тест для isPowerOfTwo() функция: она сравнивает фактический результат функции с ожидаемым результатом для данного ввода. Это параметризованный тест (также известный как тест на основе свойств), что означает, что вы можете легко запустить его с различными входными значениями, возможно, с помощью инструментов фаззинга, таких как Foundry.

Вы можете использовать этот тест для проверки isPowerOfTwo() функционировать с помощью модульного тестирования или нечеткого тестирования, запуская его с выбором входных данных. Подобные тесты не могут формально доказать правильность функции, поскольку вычислительно невозможно запустить тест для всех возможных входных данных.

Однако Halmos позволяет разработчикам повторно использовать эти ранее существовавшие тесты для формальной проверки с небольшими дополнительными усилиями. Инструмент проверяет, проходят ли тесты для всех возможных входных данных, выполняя символическое выполнение теста, а затем проверяя, что утверждение никогда не нарушается (или, если утверждение is нарушаться, приведя контрпример). Это означает, что если тест проходит Halmos, правильность функции формально подтверждена, то есть алгоритм правильно реализован и был точно переведен компилятором в байт-код.

Ограничение: ограниченное символьное выполнение

Как правило, невозможно выполнить полностью автоматическое, полное символьное тестирование, так как это потребовало бы решения проблема остановки, который, как известно, неразрешимый. Одна из причин этого заключается в том, что часто невозможно автоматически определить, сколько раз цикл должен повторяться символически. В результате полностью автоматическая формальная верификация, как правило, неразрешима.

Учитывая эти фундаментальные ограничения, Халмос отдает предпочтение автоматизации, а не полноте. С этой целью Halmos предназначен для выполнения ограниченных символьных рассуждений для неограниченных циклов (где количество итераций зависит от входных данных программы) или массивов переменной длины (включая строки). Это жертвует некоторой полнотой, но позволяет Халмосу не требовать от пользователя предоставления дополнительных аннотаций, таких как инварианты циклов.

Например, рассмотрим следующую итеративную версию isPowerOfTwo() функция, которая имеет неограниченный цикл while, где количество итераций цикла определяется минимальным количеством битов, необходимых для представления входного числа.

Халмос символически повторяет этот неограниченный цикл только до указанной границы. Например, если граница установлена ​​на 3, Халмос будет повторять цикл не более 3 раз и не будет учитывать входные значения, которые заставят цикл повторяться более 3 раз (т. е. любые значения, большие или равные 2^3). ). В этом конкретном случае установка границы на 256 или выше позволит Халмосу быть полным.

Демонстрация: формальная проверка ERC721A с помощью Halmos

Чтобы продемонстрировать возможности Halmos, мы использовали его для символического тестирования и формальной проверки. ЭРК721А, оптимизированная для газа реализация стандарта ERC721, которая позволяет производить пакетную чеканку почти по той же цене, что и единичную чеканку. ERC721A включает в себя несколько инновационных оптимизации для достижения этой эффективности; например, газ можно сэкономить, откладывая обновления данных о владении токеном до тех пор, пока токен не будет передан, а не во время чеканки. Это требует использования сложных структур данных и алгоритмов для эффективного извлечения информации о владении из ленивой структуры данных. И хотя эта оптимизация повышает эффективность использования газа, она также увеличивает сложность кода и затрудняет доказательство правильности реализации. Это делает ERC721A хорошим кандидатом для формальной проверки, поскольку он может повысить уверенность в реализации и принести пользу потенциальным пользователям.

Свойства символьного тестирования

Поскольку существующие тесты для ERC721A были написаны на JavaScript с помощью Hardhat (который в настоящее время не поддерживается Halmos), мы написали новые тесты на Solidity для основных функций точки входа: mint(), burn()и transfer(). Эти тесты проверяли, что каждая функция правильно обновляет владение токеном и баланс и влияет только на соответствующих пользователей, не изменяя баланс или право собственности других пользователей. Последнее нетривиально доказать из-за использования алгоритма ленивой структуры данных в ERC721A. Например, следующий тест проверяет, что transfer() функция правильно обновляет право собственности на указанный токен:

Другой тест проверяет, что transfer() функция не изменяет баланс для других адресов, что сложно доказать, как упоминалось ранее:

Результаты проверки

Мы провели эксперимент по проверке с использованием Halmos на смарт-контракте ERC721A, написав в общей сложности 19 тесты. Тесты проводились через Halmos с разверткой цикла, равной 3, что заняло 16 минут. Разбивку времени проверки можно увидеть в таблице ниже. Эксперимент проводился на MacBook Pro с чипом M1 Pro и 16 ГБ памяти.

Пусконаладка	Время (с)
testBulanceUpdate	6.67
testBurnNextTokenIdUnchanged	1.40
testBurnOtherBalancePreservation	5.69
testBurnДругоеВладениеСохранение	189.70
testBurnOwnershipUpdate	3.81
testBurnRequirements	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintДругоеВладениеСохранение	5.74
testMintOwnershipUpdate	1.38
testMintRequirements	0.09
testПереводБалансБез изменений	9.03
testПереводБалансОбновить	53.53
testTransferNextTokenIdUnchanged	4.47
тестПередачаДругоеБалансСохранение	19.57
testПередачаДругоеВладениеСохранение	430.61
testПередача права собственностиОбновление	18.71
testTransferRequirements	149.18

В то время как большинство тестов были завершены за считанные секунды, некоторые из них заняли несколько минут. Эти трудоемкие тесты было сложно проверить из-за сложного характера рассматриваемых случаев, и они были тесно связаны с правильностью алгоритма ленивой структуры данных.

В целом результаты этого эксперимента показывают, что Халмос может эффективно проверять правильность кода смарт-контракта. Это обеспечивает повышенную уверенность в целостности кода, несмотря на сложность и потенциальные пограничные случаи смарт-контракта.

Экспериментируйте с внедряемыми ошибками

Чтобы продемонстрировать эффективность ограниченного рассуждения Халмоша, мы использовали его для обнаружения ошибок в предыдущей версии контракта ERC721A. В этой версии была проблема, которая неправильно обрабатывала арифметическое переполнение и потенциально допускала пакетную чеканку большого количества токенов, что могло нарушить целостность ленивой структуры данных и привести к тому, что некоторые пользователи потеряли право собственности на токен (проблема решен в текущей версии). Мы провели тот же набор из 19 тестов для ERC721A на версии с ошибками, и Халмос смог найти контрпример для свойств ERCXNUMXA. mint() функция. В частности, Халмос предоставил входные данные, которые привели к описанному выше сценарию эксплойта. Результаты этого эксперимента показывают, что, несмотря на свою неполноту, ограниченное рассуждение Халмоша может быть эффективным способом обнаружения и предотвращения ошибок в смарт-контрактах, которые можно использовать.

Связанных с работой

Формальные инструменты проверки байт-кода смарт-контракта Ethereum были разработаны различными командами. Эти инструменты, в том числе Halmos, можно использовать для обеспечения безопасности и корректности смарт-контрактов. Сравнение и понимание различных функций, возможностей и ограничений этих инструментов может помочь разработчикам выбрать наиболее подходящий для их уникальных потребностей.

Хотя Halmos является ценным дополнением к набору инструментов, доступных для проверки смарт-контрактов, он предназначен для дополнения (а не замены) существующих инструментов. Разработчики могут комбинировать Halmos с другими инструментами для достижения более высокого уровня надежности своих контрактов. Ниже мы сравниваем Halmos с несколькими выбранными формальными инструментами, поддерживающими байт-код EVM.

• K — это мощная формальная структура проверки, которая обеспечивает дедуктивную проверку и интерактивное доказательство теорем. Лежащая в его основе теория и реализация обеспечивают высокий уровень выразительности, что делает его пригодным для проверки сложных программ и алгоритмов. Однако следует отметить, что K не разработан с упором на автоматическую проверку и не имеет определенных функций автоматизации, которые могут потребовать дополнительных ручных усилий в процессе проверки. Чтобы использовать структуру K, формальные спецификации написаны на языке K, который необходимо изучить перед использованием. Его сила особенно полезна при проверке сложных систем, анализ которых с помощью автоматизированного рассуждения может быть сложным.
• Certora — это формальный инструмент проверки смарт-контрактов, ориентированный на автоматическую проверку и поддерживающий проверку ограниченной модели, аналогичный Halmos. Чтобы использовать Certora, разработчики должны выучить свой новый язык, ЛПМ, чтобы написать спецификации. Этот язык позволяет сжато описать многие критические свойства с помощью инвариантов контракта, функция, которую Halmos в настоящее время не поддерживает. Несмотря на то, что Certora является проприетарным инструментом с закрытым исходным кодом, он предоставляет надежные инструменты формальной проверки с постоянной разработкой и хорошей поддержкой пользователей.
  
  Halmos, с другой стороны, представляет собой инструмент с открытым исходным кодом, который меньше по масштабу и в настоящее время лишен некоторых функций, предоставляемых Certora, но предназначен для общественного блага и предназначен как нишевое решение для быстрой проверки смарт-контрактов без необходимость обширной настройки и обслуживания.
• ХЭВМ — еще один формальный инструмент проверки, похожий на Halmos. Ранее он был частью DappTools, предшественника Foundry. И HEVM, и Halmos не требуют отдельной спецификации и могут символически выполнять существующие тесты для выявления нарушений утверждений. Это позволяет пользователям использовать оба инструмента взаимозаменяемо или запускать их параллельно для одних и тех же тестов, предоставляя им несколько вариантов символьного тестирования.
  
  Стоит отметить, что, несмотря на сходство, HEVM и Halmos разрабатывались независимо друг от друга и отличаются деталями реализации; особенно с точки зрения оптимизации и стратегий символического мышления. Кроме того, HEVM написан на Haskell, а Halmos — на Python, что обеспечивает доступ к богатой экосистеме Python. Возможность использовать оба инструмента дает пользователям больше гибкости и возможностей для обеспечения безопасности и корректности смарт-контрактов.

Халмос является открытым исходным кодом и в настоящее время находится в стадии бета-тестирования. Мы активно работаем над новыми функции и функциональность, включая чит-коды Foundry и несколько других ключевых функций удобства использования. Мы будем очень признательны за ваши мысли о том, какие функции наиболее важны, и будем рады любым отзывам, предложениям и вкладам, чтобы сделать Halmos лучшим инструментом для всех.

**

Мнения, выраженные здесь, принадлежат отдельным цитируемым сотрудникам AH Capital Management, LLC («a16z») и не являются мнением a16z или ее аффилированных лиц. Определенная информация, содержащаяся здесь, была получена из сторонних источников, в том числе от портфельных компаний фондов, управляемых a16z. Хотя информация взята из источников, считающихся надежными, a16z не проводила независимую проверку такой информации и не делает никаких заявлений о текущей или неизменной точности информации или ее уместности в данной ситуации. Кроме того, этот контент может включать стороннюю рекламу; a16z не просматривал такие рекламные объявления и не поддерживает какой-либо рекламный контент, содержащийся в них.

Этот контент предоставляется только в информационных целях и не может рассматриваться как юридическая, деловая, инвестиционная или налоговая консультация. Вы должны проконсультироваться со своими советниками по этим вопросам. Ссылки на любые ценные бумаги или цифровые активы предназначены только для иллюстративных целей и не представляют собой инвестиционную рекомендацию или предложение предоставить консультационные услуги по инвестициям. Кроме того, этот контент не предназначен и не предназначен для использования какими-либо инвесторами или потенциальными инвесторами, и ни при каких обстоятельствах на него нельзя полагаться при принятии решения об инвестировании в какой-либо фонд, управляемый a16z. (Предложение инвестировать в фонд a16z будет сделано только в меморандуме о частном размещении, договоре о подписке и другой соответствующей документации любого такого фонда, и их следует читать полностью.) Любые инвестиции или портфельные компании, упомянутые, упомянутые или описанные не являются репрезентативными для всех инвестиций в транспортные средства, управляемые a16z, и нет никаких гарантий, что инвестиции будут прибыльными или что другие инвестиции, сделанные в будущем, будут иметь аналогичные характеристики или результаты. Список инвестиций, сделанных фондами, управляемыми Andreessen Horowitz (за исключением инвестиций, в отношении которых эмитент не предоставил разрешение на публичное раскрытие информации a16z, а также необъявленных инвестиций в публично торгуемые цифровые активы), доступен по адресу https://a16z.com/investments. /.

Диаграммы и графики, представленные в нем, предназначены исключительно для информационных целей, и на них не следует полагаться при принятии каких-либо инвестиционных решений. Прошлые показатели не свидетельствуют о будущих результатах. Содержание говорит только по состоянию на указанную дату. Любые прогнозы, оценки, прогнозы, цели, перспективы и/или мнения, выраженные в этих материалах, могут быть изменены без предварительного уведомления и могут отличаться или противоречить мнениям, выраженным другими. Пожалуйста, посетите https://a16z.com/disclosures для получения дополнительной важной информации.