27 січня 2022

Мова Michelson повна за Тюрінгом: що це означає і чому це важливо

Тюрінг-повна мова програмування — це мова, якою можна реалізувати будь-яку обчислювану функцію, тобто написати взагалі будь-яку програму. Більшість мов програмування повні за Тюрінгом, і це погано.

Пояснюємо простими словами, чим небезпечні тюрінг-повні мови, чому неповних за Тюрінгом мов майже немає, і як мова Tezos — Michelson — захищена від небезпек.

Детально про повноту за Тюрінгом

Алан Тюрінг — англійський математик, основоположник інформатики та творець першого комп’ютера в сучасному розумінні. В 1936 він описав поняття алгоритму як машину, яка може обчислити будь-яку функцію через найпростіші команди на кшталт додавання чисел. Ця абстракція отримала назву «машина Тюрінга».

У машині Тюрінга є нескінченно довга стрічка. Вона розбита на комірки, у яких містяться числа чи команди: перейти на комірку ліворуч чи праворуч, прочитати її значення чи записати до неї нове число. Крім того, машина вміє працювати із правилами переходу. Наприклад, якщо в комірці знаходиться число 0000, машина перейде на три комірки вліво і запише туди поточне число. Такого набору достатньо, щоби написати будь-яку програму.

Живий приклад цього принципу — мова програмування BrainFuck. У ній всього вісім команд: читання, запис, зсув комірки вліво та вправо, зменшення та збільшення поточного значення на одиницю, відкриття та закриття while-циклу.

Так виглядає «Hello World!» на BrainFuck:

Комп’ютери працюють з літерами в вигляді кодування ASCII: літера H позначається числом 72, e — 101, l — 108 тощо. Ця програма спочатку записує в комірку 0 число 10, а потім запускає цикл із десяти ітерацій: в комірку 1 записати 7, в комірку 2 — 10, і так десять разів. Потім вона підсумовує в кожну комірку недостатні числа, і виводить результат — слово “Hello”.

Будь-який сучасний комп’ютер працює з таким же набором команд, як і BrainFuck. Коли користувач у текстовому документі натискає клавішу “e”, комп’ютер так само рухає каретку, підсумовує біти та використовує цикли. Але завдяки швидкодії в трильйони операцій за секунду користувачі цього не помічають.

Аналогічно з комп’ютером, команда для виведення рядка на екран у будь-якій високорівневій мові зчитує одиниці та нулі з пристрою зберігання даних, складає їх у ANSII-код і лише тоді виводить Hello World!. По суті, команди мов програмування запускають величезні цикли із примітивів, які Тюрінг описав ще 1936 року.

Чому тюрінг-повні мови – небезпечні

Головна небезпека криється у циклах. Розробник не може довести, що його програма обов’язково припинить роботу в кінцевій точці, а не перезапустить один із циклів. Також розробник не може детермінувати результати роботи програми з будь-якими даними на вході. Завжди може знайтись комбінація вхідних аргументів, яка зламає примітив, і програма виконає не те що задумано.

Наприклад, у приставці GameBoy є 8-бітний процесор, який у якості вхідних аргументів приймає числа від 0 до 255. Кнопки також позначаються числами, наприклад, кнопка «вверх» передає в процесор число 16. Гра Pokemon Yellow зберігає інвентар та покемонів гравця у вигляді таких самих чисел в окремому файлі.

Якщо набрати в інвентар певну кількість предметів, то процесор GameBoy побачить замість опису вашого Пікачу виконуваний файл, тобто програму. Розробник Робер МакІнтур використав цю особливість приставки, щоб простим натисканням кнопок скласти в ній програму для програвання MIDI-музики та перегляду PNG-зображень.

Інший розробник під ніком Masterjun схожим чином зламав гру Super Mario World на 16-бітній приставці SNES. Він підключив до приставки відразу 8 контролерів, і з їх допомогою ввів у Mario виконуваний код простих ігор типу змійки.

Подібним чином гравці ламали стратегію Starcraft: переповнювали буфер пам’яті, а потім за допомогою внутрішньоігрових дії вводили бінарний код. Оскільки Starcrfat працює на повноцінних комп’ютерах, то в ньому вдалося запустити гру Super Mario Bros. і навіть редактор рівнів для неї.

Ігри іграми, але за таким же принципом хакери зламують смарт-контракти на блокчейнах. Вони ламають алгоритми контрактів за допомогою правильно підібраних аргументів, а потім змушують контракт надіслати кошти на вказану адресу. Таким чином колись обікрали The DAO на блокчейні Ethereum, та продовжують красти кошти зараз.

Але найнебезпечніше у тюрінг-повних мовах те, що вони скрізь. Якщо в мові є банальне додавання — вона є повною за Тюрінгом, а програми на ній — вразливими до атак.

Існують і неповні за Тюрінгом мови, наприклад HQ9+. У ній всього чотири команди: виведення Hello World, власного вихідного коду, вірша «99 пляшок пива на стіні» та нескінченного лічильника. Але такою мовою не можна написати нічого іншого.

Чому Michelson надійна попри повноту за Тюрінгом

Головна фіча Michelson — сувора типізація. Завдяки цьому хакер не зможе переконати смарт-контракт прийняти рядок за чисті байти чи число з комою за натуральне число. Саме через відсутність суворої типізації розробники з прикладів вище зламували ігри за допомогою інтерфейсу і впроваджували в них сторонній код.

Також смарт-контракти на Michelson можна формально верифікувати та переконатися, що за будь-яких вхідних аргументів контракт робить саме те, що задумав розробник.

Остання лінія захисту контрактів на Michelson — обмеження часу виконання. Машина Тюрінга здатна обчислити будь-яку функцію, тому що вона має нескінченний носій інформації та час роботи. У блокчейні обсяг пам’яті та час виконання контракту обмежені, тому хакер не зможе впровадити потрібний йому код, навіть якщо знайде лазівку.

Підписуйтесь на соціальні мережі Tezos Ukraine, щоб нічого не пропустити: