Формальные языки
Теорема о рекурсии
1984 год. Кен Томпсон, соавтор Unix, получает премию Тьюринга и читает лекцию 'Reflections on Trusting Trust'. Он показывает: можно модифицировать компилятор C так, чтобы тот вставлял backdoor в любую программу - включая новые версии себя. Модифицированный компилятор самовоспроизводит backdoor бесконечно. Исходный код чистый. Это теорема о рекурсии в реальной атаке на безопасность.
- **GCC bootstrap:** GNU Compiler Collection написан на C. Компиляция GCC из исходников проходит три стадии (stage1, stage2, stage3). Результат stage2 и stage3 должны совпадать побайтово - самовоспроизведение как проверка корректности
- **Reproducible Builds (debian.org):** проект по верификации bootstrap-компиляторов. Если компилятор содержит скрытый код (Thompson attack), разные машины дадут разные бинарники. Воспроизводимые сборки обнаруживают такие атаки
- **Полиморфный вирус Conficker (2008):** заразил ~9 млн компьютеров. Использовал полиморфный движок: при каждом заражении код шифровался новым ключом. Сигнатурные антивирусы не могли его обнаружить - quine с шифрованием
- **Злобные компиляторы (XcodeGhost, 2015):** поддельный Xcode вставлял малварь в iOS приложения. Разработчики не подозревали - они компилировали чистый код. Атака на цепочку поставок через компилятор, аналог Thompson attack
Самореференция в вычислениях
**Quine** - программа, которая выводит собственный исходный код. Это не трюк и не баг - это прямое следствие теоремы Клини о рекурсии. Любая достаточно мощная вычислительная система допускает самореференцию. Понимание этого факта критично для безопасности: полиморфные вирусы и самомодифицирующийся код работают именно так.
Quine не просто программа-игрушка. **Компиляторы** (bootstrap) используют самовоспроизведение: компилятор языка X написан на X. **Полиморфные вирусы** модифицируют свой код при каждом запуске, сохраняя функциональность. **Docker-контейнеры** с Dockerfile, который содержит команды для своего воспроизведения. Всё это - приложения теоремы о рекурсии.
Quine - программа, печатающая свой код. Это возможно потому что...
Теорема о неподвижной точке (Recursion Theorem)
**Теорема Клини о рекурсии (1938):** для любой вычислимой функции t: Σ* → Σ* существует МТ M такая, что M и t(<M>) вычисляют одну и ту же функцию. Иными словами: у любого вычислимого преобразования программ есть неподвижная точка - программа, которую это преобразование не меняет функционально.
**Теорема о рекурсии:** пусть t: Σ* → Σ* - вычислимая функция. Тогда существует МТ M такая, что φ_M = φ_{t(<M>)}, где φ_M - функция, вычисляемая M. То есть M и МТ с описанием t(<M>) вычисляют одно и то же. Интуитивно: M 'знает' своё описание и может его использовать.
Теорема о рекурсии утверждает: для любой вычислимой t существует МТ M где φ_M = φ_{t(<M>)}. Что это означает практически?
Приложения теоремы о рекурсии
Теорема о рекурсии - один из самых мощных инструментов теории вычислимости. Она используется для построения программ, которые 'знают' своё описание, что позволяет создавать самовоспроизводящиеся конструкции и доказывать важные теоремы.
**Thompson's Trusting Trust Attack (1984):** Кен Томпсон показал: компилятор C можно модифицировать так, чтобы он вставлял backdoor в программы, которые его компилируют - включая новые версии компилятора. Модифицированный компилятор 'воспроизводит' backdoor при каждой компиляции самого себя. Это реальная атака на цепочку поставок через теорему о рекурсии.
Thompson's Trusting Trust Attack использует модифицированный компилятор для вставки backdoor в свои копии. Как это связано с теоремой о рекурсии?
Теорема о рекурсии и доказательство Райса
Теорема о рекурсии даёт альтернативное доказательство теоремы Райса. Предположим, что некоторое непрямолинейное свойство P разрешимо. Построим функцию t, которая при наличии свойства P возвращает программу без P, и наоборот. По теореме о рекурсии существует неподвижная точка - программа M = t(M). Противоречие.
Это доказательство короче, чем через сведение от A_TM, но требует понимания теоремы о рекурсии. В обоих доказательствах суть одна: **самореференция создаёт противоречие** при предположении разрешимости. Диагонализация Тьюринга, теорема о рекурсии Клини, теорема о неполноте Гёделя - все используют этот же принцип.
Теорема о рекурсии говорит о рекурсивных функциях в программировании
Теорема Клини о рекурсии - это теорема о существовании неподвижной точки для любого вычислимого преобразования программ. 'Рекурсия' здесь - математическая самореференция, не конструкция языка программирования
В теореме нет рекурсивных вызовов в смысле программирования. Речь о программе M, которая функционально эквивалентна t(M) - программа 'знает' своё описание. Это математическая рекурсия в смысле самореференции.
В доказательстве теоремы Райса через рекурсию строится функция t, которая 'инвертирует' свойство P. Почему существование неподвижной точки t приводит к противоречию?
Итоги
- **Теорема о рекурсии (Клини):** для любой вычислимой t существует M такая что φ_M = φ_{t(<M>)}. Программа может 'знать' своё описание
- **Quine:** программа, печатающая свой исходный код. Конструктивное доказательство теоремы о рекурсии. Существует на любом Тьюринг-полном языке
- **Приложения:** bootstrap компиляторы, полиморфные вирусы, Thompson Trusting Trust attack, reproducible builds
- **Доказательство теоремы Райса:** альтернатива через рекурсию. Неподвижная точка инвертирующего t создаёт противоречие
Связанные темы
Теорема о рекурсии - инструмент для доказательства других теорем:
- Теорема Райса — Теорема о рекурсии даёт альтернативное доказательство теоремы Райса через неподвижную точку
- Проблема остановки — Диагонализация Тьюринга и теорема о рекурсии используют один принцип - самореференцию для создания противоречия
- Тезис Чёрча-Тьюринга — Теорема о рекурсии применима ко всем моделям вычислений - следствие универсальности МТ
Вопросы для размышления
- Напишите quine на любом языке программирования. Какой принцип позволяет это сделать и почему это работает?
- Thompson Trusting Trust attack: как reproducible builds защищают от этой атаки? Какие ограничения у этой защиты?
- Теорема о рекурсии гарантирует существование самовоспроизводящихся программ. Означает ли это, что жизнь (биологическая самовоспроизводящаяся система) является вычислимой?