В чем разница между символическим исполнением и анализом заражения?

Интересный вопрос! Вот мои 2 цента: символическое выполнение использует своего рода анализ заражения для построения ограничений пути. В символьном исполнении также используется решатель SMT / SAT для генерации конкретных значений переменных и / или входных данных, чтобы удовлетворялось определенное ограничение пути.

Поскольку анализ помеченных данных не использует решатель SMT / SAT, я бы сказал, что это не разновидность символьного исполнения. Можно сказать, что анализ заражения - это часть символического исполнения.

Это всего лишь мнение. Пожалуйста, не стесняйтесь оспаривать это.

Я согласен с @Benny, это действительно интересный вопрос. Вы, вероятно, многому научитесь, формулируя такие вопросы, и даже больше, когда попытаетесь на них ответить.

Я хотел бы добавить к ответу Бенни:

Чтобы реализовать отслеживание заражения и символьное выполнение, необходимо определить семантику языка (например, сборку x86 в случае двоичных файлов). Например, нужно описать, что

add eax, ebx

'означает', то есть делает по отношению к государству. Определение семантики отслеживания заражения можно рассматривать как своего рода подмножество семантики символьного выполнения. Семантика отслеживания заражения закодирована в семантике символического выполнения. Общая часть

• Если ebx испорчен, то eax испорчен.
• Если ebx является символическим (i.o.w. содержит формулу SMT, содержащую одну или несколько символьных переменных), тогда eax является символическим

Тем не менее, семантика для символьного выполнения должна содержать дополнительную информацию (например, точную арифметическую операцию): - eax это «все, что было в eax до» + «все, что было в ebx до»

Прокомментируйте или поправьте меня!

На мой взгляд, чтобы ответить на ваш вопрос, мы должны ответить на следующий вопрос: i) имеет ли символьное выполнение потенциал для поиска всех путей выполнения, которые может испортить анализ, и многое другое; ii) имеет ли анализ заражения потенциал для обнаружения всех путей выполнения, которые может выполнять символическое выполнение, и многое другое; iii) обладают ли они одинаковым потенциалом поиска одинаковых путей выполнения; iv) могут ли они оба вычислить пути выполнения, которые другой не может.

На мой взгляд, пункт iv) правильный, что означает, что он не является подмножеством. Однако я согласен с тем, что действительно существует большое совпадение.

Мы можем исключить варианты i) и iii), потому что символьное выполнение находит только возможные пути выполнения, тогда как анализ помеченных данных может находить недопустимые, при этом не прибегает к решению ограничений.

Чтобы исключить вариант ii), я думаю (поправьте меня, если я ошибаюсь), что есть пути выполнения, которые могут быть обнаружены при символьном выполнении, а анализ на искажении не может. Например:

for(int i=0;i<3;i++) {
   if(someString.charAt(i)=='4')
       //do something
   else
       //do something else
}

В таком случае символьное выполнение раскрывает все восемь возможных путей выполнения, тогда как анализ помеченных данных (если я не ошибаюсь) - нет.

Я думаю, что ключевое различие заключается в том, является ли выполнение конкретным или символическим - заинтересованы ли вы в распространении заражения (для проверки утечки информации или перехвата потока управления) при единственном конкретном выполнении или если вы хотите изучить другие возможности такого распространения, используя возможности решающих программ. Достоинство динамического анализа заражения заключается в его низких накладных расходах и, следовательно, подходит для мониторинга во время выполнения. С другой стороны, (чистое / динамическое) символьное выполнение способно исследовать пути, отличные от конкретного, и, таким образом, подходит для автономного анализа интересующих вас свойств безопасности.