Создание системы формальной верификации смарт-контрактов. Часть 1: символьная виртуальная машина на php и python

Формальная верификация подобна атомной бомбе в мире информационной безопасности:
это средство, которое позволяет найти в программе все баги либо же доказать, что их нет.
Разумеется, со своими преимуществами, недостатками и ограничениями.

Раньше я описывал основы формальной верификации на примере задачи о Волке, Козе, и капусте. Ее решение и стало основой архитектуры ядра нашей символьной виртуальной машины.

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

Символьные вычисления за один запуск дадут нам ответ, возможно ли получение нами нужного результата и пример набора таких входных параметров. Либо же доказательство того, что таких параметров нет.

Более того, мы можем задать входные аргументы вообще как все возможные, и выберем только выходной, например пароль администратора.
В этом случае мы найдём все уязвимости программы или же получим доказательство того, что пароль админа в безопасности.

Можно заметить, что классическое выполнение программы с конкретными входными данными представляет собой лишь частный случай символьного.
Поэтому наша символьная VM может работать и в режиме эмуляции стандартной виртуальной машины.
Читать дальше →

Источник: Хабрахабр