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

Формальна верифікація — процес використання математичних методів для «перевірки» програми або смарт-контракту за будь-якою кількістю вхідних даних — зазвичай розглядається як більш стисла, більш повна альтернатива традиційному тестуванню для написання якіснішого та безпечнішого коду. Але насправді формальна перевірка є відкритим та інтерактивним процесом. Подібно до модульного тестування, розробники повинні динамічно визначати та накладати на них формальні специфікації, повторюючи свій підхід у міру розвитку коду та аналізу. Крім того, формальна перевірка настільки ефективна, наскільки ефективна її специфікація, написання якої може зайняти багато часу (і часто потребує крутого навчання). 

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

Халмош, наш формальний інструмент перевірки з відкритим кодом, дозволяє розробникам знову використовувати ті самі властивості, написані для модульних тестів для формальних специфікацій через символьне тестування. Замість того, щоб створювати надійний набір властивостей із самого початку, розробники можуть уникнути повторюваної роботи та покращити свої тести по кількох специфікаціях одночасно, не починаючи з нуля. Ми розробили цей інструмент для використання, поряд з іншими, у формальному процесі верифікації, як вихід на рампу до формальної верифікації; розробники можуть почати з кількох аналізів із мінімальними зусиллями, перш ніж додати більше пізніше в процесі.

У цій публікації ми розглядаємо проблеми формальної перевірки та потенціал подолання розриву між модульним тестуванням і формальною перевіркою за допомогою символічного тестування. Потім ми ознайомимося з демо-версією Halmos з використанням існуючого коду смарт-контракту та коротко поглянемо на інші формальні інструменти перевірки (багато з них із відкритим кодом), доступні розробникам.

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

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

Подібно до формальної перевірки, модульне тестування передбачає оцінку того, чи програма працює належним чином; Проте тестування перевіряє лише поведінку програми деякі входи, тоді як формальна перевірка може перевірити це всі можливі входи. І тестування, і формальна перевірка вимагають опису очікуваної поведінки програми (з тестовими прикладами, які використовуються під час тестування, та формальними специфікаціями, які використовуються під час формальної перевірки). Але при спільному використанні вони можуть забезпечити більш ретельний аналіз програми. Тестування, наприклад, є ефективним для пошуку простих помилок і помилок, але, як правило, його швидше та легше виконати. Формальна перевірка, хоч і більш громіздка у використанні, є достатньо потужною, щоб довести відсутність помилок або виявити тонкі помилки, які легко пропустити під час тестування чи перегляду коду.

Накладні витрати на специфікацію

Однією з основних проблем формальної перевірки є накладні витрати на написання та підтримку формальних специфікацій. Цей процес часто включає трудомістке завдання ручного написання специфікацій за допомогою спеціальної мови (яку багатьом розробникам доведеться спочатку вивчити). Процес також є поетапним, зазвичай починаючи з написання простих властивостей і спочатку їх перевірки, а потім поступово додаючи більш складні властивості зверху. Як і тестування, це відкритий процес без чіткої точки зупинки, і можна лише додати якомога більше властивостей протягом доступного періоду часу. Крім того, коли розробники змінюють код під час його перевірки, вони також повинні оновити свої існуючі специфікації, що призводить до додаткових зусиль з обслуговування. Ці фактори можуть зробити формальну перевірку складним завданням для деяких розробників, які не бажають взяти на себе додаткові витрати.

І хоча тестування та формальна перевірка можуть покращити якість коду при спільному використанні, обидва вимагають (іноді схожих) описів очікуваної поведінки програми різними мовами та форматами. Написання та підтримка цих описів трудомістка, а підтримка двох різних форм одного опису може здаватися дубльованим зусиллям. Це викликає таке запитання: чи можна описати очікувану поведінку таким чином, щоб розробники могли використовувати її як для тестування, так і для перевірки?

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

Символьне тестування, практика виконання тестів із символьними вхідними даними, є ефективним формальним методом перевірки, який зменшує накладні витрати на специфікацію. Цей підхід дозволяє використовувати ті самі тестові випадки як для тестування, так і для формальної перевірки. На відміну від традиційного тестування, яке перевіряє, що програма працює правильно для обмеженого набору вхідних даних, символічне тестування перевіряє програму на всі можливі вхідні дані, отже, програму, яка проходить символічне тестування, можна вважати формально перевіреною.

Halmos — формальний інструмент верифікації, призначений для символічного тестування. Замість того, щоб вимагати окремих специфікацій або вивчати нову мову, Halmos використовує існуючі тести як формальні специфікації. Запуск тестів через Halmos автоматично перевірить, що всі можливі вхідні дані пройшли, або надасть контрприклади. Це не тільки усуває потребу в написанні додаткових специфікацій, але також дозволяє повторно використовувати тести, написані для модульного тестування або фаззингу, для формальної перевірки.

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

Приклад: Тестування isPowerOfTwo() функція

Як приклад розглянемо наступне isPowerOfTwo() функція, яка визначає, чи є задане число степенем двійки. Ця функція використовує a алгоритм обробки бітів для ефективності, але може бути важко довести його правильність, особливо у випадку, коли вхідні дані не є ступенем двійки.

Уявіть наступний тест для isPowerOfTwo() функція: вона порівнює фактичний вихід функції з очікуваним результатом для даного входу. Це параметризований тест (також відомий як тест на основі властивостей), що означає, що ви можете легко запустити його з різними вхідними значеннями, можливо, за допомогою інструментів фаззингу, таких як Foundry.

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

Однак Halmos дозволяє розробникам повторно використовувати ці вже існуючі тести для формальної перевірки, доклавши лише трохи додаткових зусиль. Інструмент перевіряє, що тести проходять для всіх можливих вхідних даних, виконуючи символічне виконання тесту, а потім перевіряючи, що твердження ніколи не порушується (або, якщо твердження is порушено, надаючи контрприклад). Це означає, що якщо тест проходить Halmos, правильність функції формально перевіряється, тобто алгоритм правильно реалізовано та точно переведено компілятором у байт-код.

Обмеження: обмежене символічне виконання

Як правило, неможливо виконати повністю автоматичне, повне символьне тестування, оскільки це потребує вирішення проблема зупинки, який, як відомо, є невирішений. Однією з причин цього є те, що часто неможливо автоматично визначити, скільки разів цикл має символічно повторюватися. Як наслідок, повна автоматична формальна перевірка, як правило, неможлива.

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

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

Халмос символічно повторює цей необмежений цикл лише до заданої межі. Наприклад, якщо межа встановлена ​​на 3, Halmos повторюватиме цикл щонайбільше 3 рази та не враховуватиме вхідні значення, які призведуть до повторення циклу більше 3 разів (тобто будь-які значення, більші або рівні 2^3 ). У цьому конкретному випадку встановлення межі на 256 або вище дозволить Халмосу бути завершеним.

Демо: формальна перевірка ERC721A з Halmos

Щоб продемонструвати можливості Halmos, ми використали його для символічного тестування та формальної перевірки ERC721A, дуже оптимізоване за газом впровадження стандарту 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 ГБ пам'яті.

Тест	час (с)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdUnchanded	1.40
testBurnOtherBalancePreservation	5.69
testBurnOtherOwnershipPreservation	189.70
testBurnOwnershipUpdate	3.81
testBurnRequirements	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintOtherOwnershipPreservation	5.74
testMintOwnershipUpdate	1.38
testMintRequirements	0.09
testTransferBalanceUnchanded	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdUnchanded	4.47
testTransferOtherBalancePreservation	19.57
testTransferOtherOwnershipPreservation	430.61
testTransferOwnershipUpdate	18.71
testTransferRequirements	149.18

Хоча більшість тестів було виконано за лічені секунди, деякі з них зайняли кілька хвилин. Ці трудомісткі тести було складно перевірити через складний характер випадків, які розглядалися, і вони були тісно пов’язані з правильністю алгоритму ледачої структури даних.

Загалом результати цього експерименту показують, що Halmos здатний ефективно перевірити правильність коду смарт-контракту. Це забезпечує підвищену впевненість у цілісності коду, незважаючи на складність і потенційні крайні випадки смарт-контракту.

Експериментуйте з введеними помилками

Щоб продемонструвати ефективність обмеженого міркування Халмоса, ми використали його для виявлення помилок у попередній версії контракту ERC721A. У цій версії була проблема, яка неправильно обробляла арифметичне переповнення та потенційно дозволяла пакетне карбування великої кількості токенів, що могло порушити цілісність ледачої структури даних і призвести до того, що деякі користувачі втратили право власності на токени (проблема вирішене у поточній версії). Ми провели той самий набір із 19 тестів для ERC721A на версії з помилками, і Халмос зміг знайти контрприклад для властивостей mint() функція. Зокрема, Halmos надав вхідні значення, які призвели до описаного вище сценарію експлойту. Результати цього експерименту вказують на те, що, незважаючи на свою неповноту, обмежене міркування Халмоса може бути ефективним способом виявлення та запобігання помилкам у смарт-контрактах, які можна використовувати.

Супутні роботи

Формальні інструменти перевірки байт-коду смарт-контракту Ethereum були розроблені різними командами. Ці інструменти, включаючи Halmos, можна використовувати для забезпечення безпеки та коректності смарт-контрактів. Порівняння та розуміння різних функцій, можливостей і обмежень цих інструментів може допомогти розробникам вибрати найбільш відповідний для їхніх унікальних потреб.

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

• K це потужна система формальної верифікації, яка забезпечує дедуктивну перевірку та інтерактивне доведення теорем. Його базова теорія та реалізація забезпечують високий рівень виразності, що робить його придатним для перевірки складних програм і алгоритмів. Однак слід зазначити, що K не розроблено з великим наголосом на автоматизовану перевірку та не має певних функцій автоматизації, які можуть вимагати більше ручних зусиль під час процесу перевірки. Щоб використовувати структуру K, формальні специфікації написані мовою K, яку потрібно вивчити перед використанням. Його потужність особливо корисна під час перевірки складних систем, які може бути важко аналізувати за допомогою автоматизованих міркувань.
• Certora це формальний інструмент перевірки для смарт-контрактів, який зосереджений на автоматизованій перевірці та підтримує перевірку обмеженої моделі, подібно до Halmos. Щоб використовувати Certora, розробники повинні вивчити їхню нову мову, CVL, щоб написати специфікації. Ця мова дозволяє стислий опис багатьох критичних властивостей через контрактні інваріанти, функцію, яку Halmos наразі не підтримує. Незважаючи на те, що Certora є запатентованим інструментом із закритим вихідним кодом, він надає надійні формальні інструменти перевірки, які постійно розвиваються та мають гарну підтримку користувачів.
  
  Halmos, з іншого боку, є меншим за масштабом інструментом із відкритим вихідним кодом і наразі не має деяких функцій, наданих Certora, але він призначений для суспільного блага та призначений як нішеве рішення для швидкої перевірки смарт-контрактів без необхідність масштабного налаштування та обслуговування.
• HEVM це ще один формальний інструмент перевірки, схожий на 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.