Формальная проверка — это процесс, используемый для проверки правильности смарт-контрактов, который может помочь в предотвращении потенциальных проблем безопасности или ошибок. В этом сообщении блога мы рассмотрим формальную проверку в Solidity, обсудим ее подходы, методы и примеры.
Что такое формальная проверка?
Формальная верификация — это процесс доказательства правильности системы или программы с использованием математических методов. Формальная верификация использует формальные методы, которые представляют собой математические методы для определения, проектирования и проверки систем. Методы формальной проверки могут доказать, что программа удовлетворяет заданной спецификации, или обнаружить ошибки или нарушения спецификации.
Подходы к формальной верификации в Solidity
Существует два основных подхода к формальной проверке в Solidity: проверка ограниченной модели и доказательство теорем.
1. Проверка ограниченной модели
Проверка ограниченной модели (BMC) — это метод, используемый для проверки правильности программы путем анализа ее поведения для конечного числа шагов. BMC проверяет, выполняется ли данное свойство для программы с фиксированным числом шагов выполнения. Свойство можно указать с помощью формулы темпоральной логики или утверждения в программе.
Одним из инструментов, используемых для BMC в Solidity, является средство проверки моделей на основе SMT Mythril. Mythril — это инструмент с открытым исходным кодом для анализа смарт-контрактов, в котором используется символическое выполнение, анализ испорченных данных и другие методы анализа смарт-контрактов. Mythril можно использовать для выполнения различных проверок безопасности, таких как обнаружение уязвимостей повторного входа, целочисленных переполнений и других потенциальных проблем безопасности.
Например, рассмотрим следующий код Solidity, реализующий простой контракт голосования:
contract Voting {
mapping(address => bool) public hasVoted;
uint public yesVotes;
uint public noVotes;
function vote(bool voteYes) public {
require(!hasVoted[msg.sender]);
if (voteYes) {
yesVotes++;
} else {
noVotes++;
}
hasVoted[msg.sender] = true;
}
}
Чтобы проверить правильность функции vote с помощью Mythril, мы можем использовать следующую команду:
$ myth analyze Voting.sol --execution-timeout 120
Эта команда проанализирует контракт Voting в течение 120 секунд и сообщит о любых потенциальных проблемах безопасности или уязвимостях. Mythril может обнаружить, что функция vote не имеет никаких проверок входных данных и может быть вызвана с недопустимыми входными данными, что может привести к переполнению или потере значимости переменных yesVotes и noVotes.
2. Доказательство теорем
Доказательство теорем — это метод, используемый для доказательства правильности программы путем построения математического доказательства того, что программа удовлетворяет заданной спецификации. Доказательство теорем включает ручное построение доказательства правильности с использованием языка формальных спецификаций, такого как Coq, Isabelle или HOL.
Одним из инструментов, используемых для доказательства теорем в Solidity, является платформа K. Платформа K — это формальная семантическая структура, которую можно использовать для определения и проверки языков программирования. Платформу K можно использовать для определения семантики Solidity и проверки ее программ с использованием методов доказательства теорем.
Например, рассмотрим следующий код Solidity, реализующий простой смарт-контракт для сложения двух целых чисел:
contract Adder {
function add(uint a, uint b) public pure returns (uint) {
uint c = a + b;
return c;
}
}
Чтобы проверить правильность функции add, используя K framework, мы можем определить формальную спецификацию функции, используя язык K. Спецификация K функции add может быть записана следующим образом:
rule <k> add(a:UInt, b:UInt) => c:UInt requires true ensures c == a + b </k>
Эта спецификация K определяет правило, которое принимает два целых числа без знака a и b в качестве входных данных и возвращает их сумму c в качестве вывода. Правило указывает, что выход c равен сумме входов a и b. Мы можем использовать структуру K, чтобы проверить правильность функции add, доказав, что спецификация K функции удовлетворяется.
Чтобы доказать правильность функции add с помощью платформы K, мы можем использовать следующую команду:
$ kprove add.k
Эта команда будет использовать структуру K, чтобы доказать, что спецификация K функции add удовлетворяется, и вернет доказательство, если спецификация действительна.
Примеры формальной проверки в Solidity
Давайте рассмотрим несколько примеров формальной верификации в Solidity с использованием методов BMC и доказательства теорем.
Пример 1: Обнаружение уязвимостей повторного входа с помощью Mythril
Повторный вход — это уязвимость безопасности, которая может возникнуть в смарт-контрактах, когда функция может быть вызвана несколько раз до того, как ее предыдущее выполнение будет завершено. Повторный вход может позволить злоумышленнику манипулировать состоянием контракта и украсть средства или активы из контракта.
Чтобы обнаружить уязвимости повторного входа в Solidity, мы можем использовать символьный механизм выполнения Mythril. Механизм символического исполнения Mythril может отслеживать пути выполнения смарт-контракта и обнаруживать потенциальные уязвимости повторного входа.
Рассмотрим следующий код Solidity, реализующий простой банковский контракт:
contract Bank {
mapping(address => uint) public balances;
function deposit() public payable {
balances[msg.sender] += msg.value;
}
function withdraw(uint amount) public {
require(amount <= balances[msg.sender]);
(bool success, ) = msg.sender.call{value: amount}("");
require(success);
balances[msg.sender] -= amount;
}
}
Этот контракт позволяет пользователям вносить и снимать средства со своего счета. Чтобы обнаружить потенциальные уязвимости повторного входа в этом контракте, мы можем использовать следующую команду:
$ myth analyze Bank.sol --execution-timeout 120 --truffle
Эта команда проанализирует контракт Bank с помощью механизма символического исполнения Mythril и сообщит о любых потенциальных уязвимостях повторного входа или проблемах безопасности.
Пример 2: Проверка смарт-контракта с использованием K Framework
Мы можем использовать фреймворк K для проверки корректности смарт-контрактов, написанных в Solidity. Платформу K можно использовать для определения семантики Solidity и проверки ее программ с использованием методов доказательства теорем.
Рассмотрим следующий код Solidity, реализующий простой контракт голосования:
contract Voting {
mapping(address => bool) public hasVoted;
uint public yesVotes;
uint public noVotes;
function vote(bool voteYes) public {
require(!hasVoted[msg.sender]);
if (voteYes) {
yesVotes++;
} else {
noVotes++;
}
hasVoted[msg.sender] = true;
}
}
Мы можем использовать структуру K для проверки правильности функции vote в этом контракте, определив спецификацию K функции и доказав, что спецификация удовлетворяется.
Спецификация K функции vote может быть записана следующим образом:
rule <k> vote(hv:Map, yv:UInt, nv:UInt, v:Address, b:Bool) => hv':Map, yv':UInt, nv':UInt requires !hv
Эта спецификация K определяет правило, которое принимает четыре входа: отображение hv, которое представляет набор адресов, которые уже проголосовали, два целых числа без знака yv и nv, которые представляют количество голосов «за» и «против» соответственно, и логическое значение значение b, которое представляет голос текущего избирателя. Правило возвращает три результата: новое сопоставление hv', включающее текущий адрес избирателя, и два обновленных целых числа без знака yv' и nv', представляющих обновленное количество голосов «за» и «против» соответственно. Правило указывает, что выходные данные hv' включают текущий адрес избирателя, а выходные данные yv' и nv' обновляются на основе текущего голоса избирателя.
Мы можем использовать структуру K, чтобы доказать, что спецификация K функции vote удовлетворяется реализацией этой функции в Solidity. Для этого мы можем использовать следующую команду:
$ kprove vote.k
Эта команда будет использовать структуру K, чтобы доказать, что спецификация K функции vote удовлетворяется реализацией функции Solidity, и вернет доказательство, если спецификация действительна.
Заключительные слова
Формальная проверка — важный метод обеспечения правильности и безопасности смарт-контрактов. Используя методы формальной проверки, такие как проверка ограниченной модели и доказательство теорем, мы можем обнаруживать и предотвращать уязвимости безопасности в смарт-контрактах и обеспечивать их правильное поведение. Solidity предлагает различные инструменты и фреймворки, которые упрощают применение методов формальной проверки к смарт-контрактам, включая Mythril и фреймворк K. Используя эти инструменты и фреймворки, вы можете создавать более безопасные и надежные смарт-контракты, менее подверженные атакам.
Если вы нашли эту статью информативной и полезной, подпишитесь на меня, чтобы получать больше материалов, связанных с блокчейном и криптовалютой. Вы также можете подписаться на мою рассылку, чтобы получать новости о моих последних статьях и проектах.
Новичок в трейдинге? Попробуйте криптотрейдинговые боты или копи-трейдинг на лучших криптобиржах
Присоединяйтесь к Coinmonks Telegram Channel и Youtube Channel и получайте ежедневные Крипто новости
