Создание системы формальной верификации смарт-контрактов. Часть 1: символьная виртуальная машина на php и python
Формальная верификация подобна атомной бомбе в мире информационной безопасности:
это средство, которое позволяет найти в программе все баги либо же доказать, что их нет.
Разумеется, со своими преимуществами, недостатками и ограничениями.
Раньше я описывал основы формальной верификации на примере задачи о Волке, Козе, и капусте. Ее решение и стало основой архитектуры ядра нашей символьной виртуальной машины.
Символьные вычисления представляют собой способ одновременного выполнения программы на широком диапазоне данных и являются главным инструментом для формальной верификации программ.
Например, мы можем задать входные условия где первый аргумент может принимать любые положительные значения, второй отрицательные, третий — ноль, а выходной аргумент, к примеру, 42.
Символьные вычисления за один запуск дадут нам ответ, возможно ли получение нами нужного результата и пример набора таких входных параметров. Либо же доказательство того, что таких параметров нет.
Более того, мы можем задать входные аргументы вообще как все возможные, и выберем только выходной, например пароль администратора.
В этом случае мы найдём все уязвимости программы или же получим доказательство того, что пароль админа в безопасности.
Можно заметить, что классическое выполнение программы с конкретными входными данными представляет собой лишь частный случай символьного.
Поэтому наша символьная VM может работать и в режиме эмуляции стандартной виртуальной машины.
Читать дальше →
это средство, которое позволяет найти в программе все баги либо же доказать, что их нет.
Разумеется, со своими преимуществами, недостатками и ограничениями.
Раньше я описывал основы формальной верификации на примере задачи о Волке, Козе, и капусте. Ее решение и стало основой архитектуры ядра нашей символьной виртуальной машины.
Символьные вычисления представляют собой способ одновременного выполнения программы на широком диапазоне данных и являются главным инструментом для формальной верификации программ.
Например, мы можем задать входные условия где первый аргумент может принимать любые положительные значения, второй отрицательные, третий — ноль, а выходной аргумент, к примеру, 42.
Символьные вычисления за один запуск дадут нам ответ, возможно ли получение нами нужного результата и пример набора таких входных параметров. Либо же доказательство того, что таких параметров нет.
Более того, мы можем задать входные аргументы вообще как все возможные, и выберем только выходной, например пароль администратора.
В этом случае мы найдём все уязвимости программы или же получим доказательство того, что пароль админа в безопасности.
Можно заметить, что классическое выполнение программы с конкретными входными данными представляет собой лишь частный случай символьного.
Поэтому наша символьная VM может работать и в режиме эмуляции стандартной виртуальной машины.
Читать дальше →
Источник: Хабрахабр
Похожие новости
- Распознаем STL-код легко: std::vector
- Есть ли жизнь после Cisco ISE? Распаковка и тест-драйв российского NAC от Eltex в сетевой лаборатории
- ИИ взломали. Кто бы мог подумать?
- DPI, ТСПУ и операторы: архитектура блокировки трафика в России
- Максим Котенков: Мы сделали своё API для семантического анализа — и это убрало 70% рутины при подготовке SEO-ТЗ
- Почему автотесты пропускают изменения в API и как это исправить с Pydantic
- Что сегодня действительно важно в AI: 10 направлений по версии MIT Technology Review
- АЙNET: АЙNET: 30% крупных брендов отказываются от лендингов в пользу чековых ботов, а интерес к промо в Max вырос на 40%
- Как мы написали свой forward-proxy на Go и отказались от VPN для доступа к админкам
- i-Media: 43% потребителей идут на маркетплейсы за эмоциональной подзарядкой, а нейросети вытесняют поисковики: i-Media выпускает обзор digital-рынка за Q1 2026