Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models

## Контекст Современные цифровые среды требуют надежных методов верификации программного кода, особенно в сфере блокчейнов и смарт-контрактов. Одним из наиболее актуальных языков для написания смарт-контрактов является Solidity. Однако статические анализаторы и искусственные нейронные сети (LLMs), которые используются для обнаружения ошибок в коде, часто генерируют ложные срабатывания (false alarms), что снижает надежность и эффективность данных инструментов. Это вызывает необходимость разработки более точных методов, которые могут формально или эмпирически доказать наличие ошибок в смарт-контрактах. ## Метод Главная идея метода заключается в сочетании двух подходов: символьного и конкретного выполнения. Символьное выполнение используется для формального моделирования поведения программы, в то время как конкретное выполнение позволяет проверить реальное поведение на реальных данных. Для реализации этого подхода использовались следующие инструменты: Slither (для статического анализа), Kontrol (для подтверждения фактического поведения программы) и Forge (для тестирования и выполнения смарт-контрактов). Эти инструменты были объединены в единую архитектуру, которая позволяет эффективно обнаруживать и проверять ошибки в Solidity-коде. ## Результаты Проведенные эксперименты показали, что подход эффективен в обнаружении семи критичных типов ошибок в Solidity-коде: Reentrancy, Complex Fallback, Faulty Access Control Policies, и других. Набор данных, использованный в экспериментах, включал реальные смарт-контракты с известными ошибками. Результаты показали, что система способна точно классифицировать эти ошибки, также уменьшив число ложных срабатываний. Это демонстрирует значительный потенциал метода в снижении бремени ручной верификации. ## Значимость Предлагаемый подход может быть применен в различных областях, где требуется высокая надежность и автоматизация проверки программного кода. Особенно он полезен в сфере блокчейнов, где смарт-контракты являются критичными для безопасности и эффективности. Преимущества метода включают уменьшение числа ложных срабатываний, повышение точности обнаружения ошибок, а также снижение времени и стоимости ручного аудита. Это может привести к повышению эффективности и надежности систем, основанных на Solidity. ## Выводы Предложенный подход является перспективным для решения проблемы ложных срабатываний в статическом анализе и LLMs. Он доказал способность эффективно обнаруживать критичные ошибки в Solidity-коде и уменьшить нагрузку на ручную верификацию. Будущие исследования будут сфокусированы на улучшении точности и снижении стоимости использования LLMs, а также на расширении под