Теорема Райса: Почему антивирусы ошибаются, а компиляторы пропускают баги

Теорема Райса, доказанная Генри Гордоном Райсом в 1953 году, является мощным обобщением знаменитой проблемы остановки Машины Тьюринга. Она переводит фокус с процесса вычисления на семантику (смысл) работы алгоритма.

Математическая формулировка теоремы звучит так: Любое нетривиальное семантическое свойство программ, распознаваемых Машиной Тьюринга, является алгоритмически неразрешимым. Чтобы понять эту фразу, нужно разобрать два ключевых термина:

1. Семантическое свойство: это свойство того, что программа делает, а не того, как она написана. Количество строк кода, наличие цикла `while` или использование переменной `x` — это синтаксические свойства (их проверить элементарно). Но свойство "функция возвращает 0 при вводе 5" или "программа удалит файл с диска" — это свойства семантики.
2. Нетривиальное свойство: это свойство, которым обладают некоторые программы, но не все. "Программа содержит баги" — нетривиальное свойство. "Программа состоит из байтов" — тривиальное свойство.

Следствие Теоремы Райса невероятно жестоко для IT-индустрии: не существует и никогда не будет существовать универсального алгоритма, который бы по исходному коду чужой программы точно определял, обладает ли она заданным нетривиальным семантическим свойством.

Это означает, что математически невозможно создать идеальный антивирус. Любой антивирус обречен либо пропускать некоторые новые вирусы (ложноотрицательные срабатывания), либо блокировать абсолютно безопасные программы (ложноположительные срабатывания). Невозможно создать идеальный оптимизатор кода, который бы точно определял, выполняется ли кусок кода когда-нибудь или это "мертвый код" (Dead code).

Как же тогда работают SonarQube, PVS-Studio и антивирусы Касперского? Они работают на аппроксимациях и эвристиках. Вместо того чтобы пытаться решить неразрешимую математическую задачу в общем виде, они анализируют ограниченные шаблоны, используют абстрактную интерпретацию и символьное выполнение (Symbolic Execution). Они могут найти 95% типичных ошибок, но Теорема Райса гарантирует, что 100% гарантии корректности программного обеспечения дать невозможно.