MMGP logo
Присоединяйтесь к нашему инвестиционному форуму, на котором уже 640,440 пользователей. Чтобы получить доступ ко многим закрытым разделам и начать общение - зарегистрируйтесь прямо сейчас.
Все новости о платежных криптовалютах, таких как BitCoin, Ethereum, LiteCoin, Ripple и прочих подобных p2p валютах
Старый 21.10.2016, 21:58
#1
Топ Мастер
 
Имя: Андрей
Пол: Мужской
Возраст: 44
Адрес: Украина
Инвестирую в: HYIP
Регистрация: 26.02.2015
Сообщений: 13,942
Благодарностей: 6,813
«Умные контракты»: полнота по Тьюрингу и реальность


Взлом DAO и недавние DDOS-атаки на сеть Ethereum вызвали споры о разумности использования полных по Тьюрингу языков для «умных контрактов». Tezos, криптографическая учетная база данных и платформа «умных контрактов», предлагает полные по Тьюрингу «умные контракты» на формально определенном языке (со строгой типизацией и статической проверкой типов). Мы решили прояснить некоторые недоразумения касательно значимости «полноты по Тьюрингу» в контексте «умных контрактов».

Теория

Полнота по Тьюрингу — свойство, которое указывает, что определенные (обычно, большинство) языки программирования универсальные. Согласно тезису Черча — Тьюринга (физического закона с существенными эмпирическими доказательствами), каждое вычисление, которое можно выполнить физически, даже в теории, можно выразить и реализовать на полном по Тьюрингу языке.

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



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

Отсюда следует вывод: так как нельзя предугадать, что эти программы будут делать, следует держаться подальше от таких языков. Разве неясно, что произошло с DAO? Участники контракта не смогли предугадать его поведение, что привело к катастрофе.

Это заблуждение, на удивление, распространено. Очевидно, что как минимум один человек, хакер, смог предугадать поведение контракта и понять его; лучше, чем создатели.

Теорема Райса утверждает, что нет универсальной процедуры, которая могла бы установить истинность свойства поведения программы. Это могут быть такие свойства, как: «прекращает ли программа работу», «возникла ли в программе ошибка», «может ли быть получен определенный результат».

Теорема предполагает, что существуют программы, которые завершают работу после выполнения и ведут себя, как предполагалось, но доказательств нет. Мы не знаем, что это за программы, но они существуют согласно разумным математическим доказательствам (благодаря Тьюрингу, Черчу и Геделю). Важно отметить, что могут существовать универсальные процедуры, которые способны вычислить поведение большинства программ, но не всех.



Курт Гедель
Некоторые языки отказались от полноты по Тьюрингу, и их программы всегда можно остановить. Например, скриптовый язык Биткойна. Некоторые люди считают верным утверждение, противоположное теореме Райса. Так звучит это заблуждение:

«Так как проблема остановки в полных по Тьюрингу языках предполагает, что мы не можем предугадать поведение программ, то пока мы пишем программы на языке, который гарантирует остановку, мы сможем прогнозировать все интересующие нас свойства».

Это не так: не в теории, ни на практике. Есть языки, чьи программы гарантированно вызовут исключения/остановят выполнение, несмотря на входные данные, но они не позволяют определить, приведут ли какие-либо входные данные к ошибке. (Для теоретиков: возьмем язык, на котором написана одна программа f. Она проверяет, служат ли входные данные x доказательством противоречивости ZFC [системы Цермело — Френкеля с аксиомой выбора]. f всегда будет останавливаться, но вернет ли она когда-либо true или нет — неразрешимо в ZFC).

Практика

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

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

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

for(all inputs < max size) {
run program for max time;
check property;
}

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

Я не хочу этим продемонстрировать, что мы всегда можем доказать истинность всех свойств в ограниченных по времени «умных контрактах». Как раз наоборот. Я хочу сказать, что существование универсального алгоритма и применимого алгоритма — две разные вещи.

Существует ли такой эффективный алгоритм для скриптов Биткойна? Конечно, нет!

Посмотрите на следующий Биткойн скрипт:

scriptPubKey: OP_HASH256 0123456789abcdef0123456789abcdef0123456789abcdef01 23456789abcdef OP_EQUAL

Это хеш-головоломка, согласно описанию на странице Биткойна в Википедии. Обратите внимание, что я определенно получил соответствующий хеш. Сценарий несомненно останавливается при любых входных данных. Но нам интересно узнать, можно ли использовать результат. Все зависит от того, существует ли прообраз к хешу, который я получил, и это абсолютно не ясно. Нам пришлось бы использовать полный перебор на хеш-функции, и ушли бы миллиарды лет, чтобы выяснить это.

Нехватка полноты по Тьюрингу в скриптах Биткойна не решает проблему. Это никак не помогает установить истинность фундаментального свойства этого очень простого скрипта.

Что действительно важно?

Как мы говорили ранее, теорема Райса указывает, что существуют программы, которые завершают работу после выполнения и ведут себя, как предполагалось, но доказательств нет.

Тем не менее почти все рассматриваемые корректные программы будут доказуемо корректными. Более того, доказательство их корректности будет довольно простым. Это особенно справедливо в контексте «умного контракта» в криптографических учетных журналах, который обычно реализует простую бизнес-логику (конечно, ситуация отличается, например, в сфере вычислительной алгебры).

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

Но когда разработчик пишет программу, он обычно держит в голове примерную схему доказательства корректности. Иногда это доказательство неполное или неправильное (люди могут ошибаться), но оно всегда направляет процесс разработки. Разработчик постоянно думает о поведении программы, чтобы в результате она точно выполняла то, для чего предназначена.

Это не тот случай, когда разработчик сидит за столом и пишет, из лучших побуждений, договор мены, который делает недействительной передачу всего предоставленного имущества, если и только если гипотеза Коллатца доказана или ZFC противоречива.

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

В этом отношении обычно легко понять поведение скриптов Биткойна. Они не приносят много сюрпризов. Это прообраз к 0x123…? Может, да. Может, нет. Но очень маловероятно, что кто-то сможет это выяснить, поэтому при любых обстоятельствах транзакцию не провести.

Компромисс


Эффективная граница и новая граница, созданная автоматизированной системой доказательства теорем и формального подтверждения

Языки программирования находятся ниже границы выразительности / простоты в понимании.

Выразительные языки упрощают описание определенного желаемого поведения. Теоретически все полные по Тьюрингу языки могут выражать одинаковый тип вычислений. Но на практике довольно сложно выразить определенные вычисления, если язык не отвечает требованиям. Забавный пример — язык Malbolge. Malbolge полный по Тьюрингу, но невероятно сложно писать на этом языке программы, которые выполняют то, для чего предназначены.

Как и выразительность, простота в понимании не бинарная переменная. Полнота по Тьюрингу имеет важное теоретическое и практическое значение для понимания языка, но как мы видели ранее, она не раскрывает всего.

Очень выразительные языки сложнее понять, а некоторые ограниченные языки (например, конечные автоматы) можно легко понять, но в них не хватает выразительности. К счастью, есть способ сдвинуть эту границу: формальная верификация.

Формальная верификация — развивающаяся дисциплина компьютерной науки, которая помогает создавать доказуемо корректные программы. Она как бы занимается созданием машины, которая проверяет корректность программ. Хотя часто само доказательство является программой. «Умные контракты» имеют мало строк кода, но высокую цену ошибки, что делает их отличным кандидатом для этой технологии.

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

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

Что делаем мы?

Так как Tezos был запущен летом 2014 года, ключевой принцип проекта звучал так: языки «умных контрактов» — отличная цель для формальной верификации. Нам нужен был язык, который ладит с системами доказательства теорем, но прост в понимании. Это привело к следующим решениям:

Мы начали с формальной спецификации языка, чтобы точно и четко определить, для чего программа предназначена.
Мы сделали язык строго типизированным, с алгебраическими типами данных и статическим контролем типов. Типы — отличный способ понять поведение программы. Они могут гарантировать, например, что мы не добавим по ошибке две совершенно разные вещи, но их можно сдвинуть, чтобы привести в исполнение определенные свойства контракта.
Мы сделали язык высокоуровневым. Контракты, которые заключают участники, составлены не на запутанном языке ассемблера, а на языке, который используют для написания контрактов. Это позволяет нам предоставить полезные высокоуровневые базисные элементы, например, функциональные карты и функциональные наборы. Наша цель — создать не некий механизм выполнения произвольного кода, а механизм, созданный для нужд разработчиков «умных контрактов».
Все эти свойства облегчают проверку данных в контрактах с помощью автоматизированных систем доказательства теорем, например, Coq proof assistant. Также они упрощают ручную проверку корректности программ.

Заключение

Полнота по Тьюрингу обрела форму! Существуют программы, чьи свойства легко понять и проверить. А есть программы, где сложно это сделать. Существуют языки программирования, которые облегчают такие проверки. А есть те, которые их только усложняют. Суть в компромиссах, а не в четко определенном решении проблемы остановки.

Источник
clipman77 вне форума
Войдите, чтобы оставить комментарий.
Опции темы

Быстрый переход