Создание системы формальной верификации смарт-контрактов. Часть 1: символьная виртуальная машина на php и python
Формальная верификация подобна атомной бомбе в мире информационной безопасности:
это средство, которое позволяет найти в программе все баги либо же доказать, что их нет.
Разумеется, со своими преимуществами, недостатками и ограничениями.
Раньше я описывал основы формальной верификации на примере задачи о Волке, Козе, и капусте. Ее решение и стало основой архитектуры ядра нашей символьной виртуальной машины.
Символьные вычисления представляют собой способ одновременного выполнения программы на широком диапазоне данных и являются главным инструментом для формальной верификации программ.
Например, мы можем задать входные условия где первый аргумент может принимать любые положительные значения, второй отрицательные, третий — ноль, а выходной аргумент, к примеру, 42.
Символьные вычисления за один запуск дадут нам ответ, возможно ли получение нами нужного результата и пример набора таких входных параметров. Либо же доказательство того, что таких параметров нет.
Более того, мы можем задать входные аргументы вообще как все возможные, и выберем только выходной, например пароль администратора.
В этом случае мы найдём все уязвимости программы или же получим доказательство того, что пароль админа в безопасности.
Можно заметить, что классическое выполнение программы с конкретными входными данными представляет собой лишь частный случай символьного.
Поэтому наша символьная VM может работать и в режиме эмуляции стандартной виртуальной машины.
Читать дальше →
это средство, которое позволяет найти в программе все баги либо же доказать, что их нет.
Разумеется, со своими преимуществами, недостатками и ограничениями.
Раньше я описывал основы формальной верификации на примере задачи о Волке, Козе, и капусте. Ее решение и стало основой архитектуры ядра нашей символьной виртуальной машины.
Символьные вычисления представляют собой способ одновременного выполнения программы на широком диапазоне данных и являются главным инструментом для формальной верификации программ.
Например, мы можем задать входные условия где первый аргумент может принимать любые положительные значения, второй отрицательные, третий — ноль, а выходной аргумент, к примеру, 42.
Символьные вычисления за один запуск дадут нам ответ, возможно ли получение нами нужного результата и пример набора таких входных параметров. Либо же доказательство того, что таких параметров нет.
Более того, мы можем задать входные аргументы вообще как все возможные, и выберем только выходной, например пароль администратора.
В этом случае мы найдём все уязвимости программы или же получим доказательство того, что пароль админа в безопасности.
Можно заметить, что классическое выполнение программы с конкретными входными данными представляет собой лишь частный случай символьного.
Поэтому наша символьная VM может работать и в режиме эмуляции стандартной виртуальной машины.
Читать дальше →
Источник: Хабрахабр
Похожие новости
- Безопасность веб-приложений для самых маленьких фронтов
- SMS Firewall: жирная точка в войне со спамом или унылый обходной манёвр?
- Анализ распределение простых чисел. Часть 1
- Анализ распределения простых чисел. Часть 1
- Объявлены победители международной премии Workspace Digital Awards-2024
- <Cookie> ctrl+c ctrl+v: автоматизируем прохождение авторизации в DAST
- Конкурс Рейтинг Рунета-2024 открыл приём сайтов и приложений
- Социально-этичный маркетинг: в чём суть и как внедрить концепцию?
- Ландшафт угроз информационной безопасности последних лет. Часть 2
- Реализация SHA256 и SHA512 на языке RUST