О конкретной силе абстракций
АрхивCтруктурное программирование - это очень просто: вместо того, чтобы анализировать корректность программы "в терминах выполнения", в процессуальных терминах ("водя пальцем" по тексту программы или блок схеме и индуктивно убеждая себя в ее "правильности"), мы анализируем ее структуру ...
Cтруктурное программирование - это очень просто: вместо того, чтобы анализировать корректность программы "в терминах выполнения", в процессуальных терминах ("водя пальцем" по тексту программы или блок схеме и индуктивно убеждая себя в ее "правильности"), мы анализируем ее структуру (комбинируя контрольные утверждения, операторы и управляющие конструкции по весьма бедному набору правил, мы можем дедуцировать правильность полученной программы).
Вопреки распространенному мифу теоретическое подвижничество Дейкстры и методические усилия Гриса не пропали даром, и сегодня формальный структурный анализ алгоритмов находит достаточно широкое применение. Во-первых, при проектировании встроенных систем (и понятно почему: встроенная система, в отличие от коробки с очередным @#$, является частью продукта, за последствия применения которого производитель несет гражданскую ответственность, тут уже лицензией AS IS не отмажешься).
Во-вторых, в критических узлах безлюдных систем военного назначения, например в ядрах встроенных специализированных ОС (и тоже понятно почему: "зависшая" или "рухнувшая" ОС в летящей ракете неизбежно приведет к известному результату, по крайней мере, для разработчика).
Структурный анализ находит и инструментальную поддержку (из языков общего применения более или менее широко известен жестко объектный Eiffel, поддерживающий явное указание контрольных утверждений, в частности инвариантов цикла).
Структурный анализ - это то, что создано и разработано для информатики, но чего пока нет для криптологии. В отличие от "алгоритма" такой объект анализа и конструирования, как "протокол", мы пока можем обсуждать лишь в процессуальных терминах: Аня сказала А, Боря подумал Б, Вера послала Ане сообщение В втайне от Бори...
В некотором смысле информатика (computer science) - это редуцированная область криптологии - исчисление алгоритмов, выполняемых доверяющими друг другу участниками вычислений. Последнее становится, заметим, очень сильным предположением в мире, в котором широко используется софт стороннего производства и в котором сетевые (в клиент-серверной или агент-агентской архитектуре) вычисления становятся скорее правилом, чем исключением.
Для обобщения результатов, полученных в информатике, на область криптологии не хватает очень многого. Формализмов для обозначения того, что известно, а что нет тому или иному участнику вычислений. Формализмов для явного задания теоретико-сложностных параметров примитивов. Просто приемлемой системы нотации для записи самих протоколов.
Однако все это придется создавать. "На пальцах" можно выстроить один протокол, другой, третий, но поставить их "производство" на поток (реализуя документарный цифровой трейдинг [1] или внедряя в массовом порядке "смарт-контракты" [2], например) без серьезной теоретической базы не удастся.
Любая попытка движения в этом направлении интересна. Самой продвинутой из известных мне попыток создать нотацию для записи криптопротоколов является проект языка E.
На что это похоже?
Довольно самонадеянно было бы пытаться дать описание языка на двух страницах (да и не предназначен компьютерный еженедельник для таких экзерсисов), зато на двух страницах можно заинтересовать и заинтриговать.
На рис 1. представлена достаточно запутанная "родословная" E. Большинство широко используемых сегодня языков - процедурные [1], происходящие от идей Алана Тьюринга. Исключение составляет LISP [2], являющийся функциональным, то есть основанным на <greek>l</greek>-исчислении Алонзо Черча. "Функциональный" программист думает в терминах рекурсии и конкретизации значений там, где "процедурный" думает в терминах итерации и присвоения значений (и, кстати, "структурность" для них означает не вполне одно и то же), однако тезис эквивалентности Тьюринга-Черча, утверждающий, что вычислимый на машине Тьюринга алгоритм можно записать как <greek>l</greek>-определение и наоборот, никто не отменял.
E претендует, очевидно, на большую <greek>l</greek>-правоверность, чем LISP, если судить по восходящей к
Actors - это экспериментальное расширение
Акторная модель вычислений, как таковая, нашла развитие в языке Joule, разработанном в Agorics, Inc. В добавление к акторной модели Joule "прихватил" идею последовательной реализации мандатной архитектуры в ОС KeyKOS (более известной в России по ее x86-клону с замечательным названием EROS) [3]. В отличие от Actors Joule ориентирован на практическое применение при сохранении строгой верифицируемости модели безопасности [5].
Joule, в свою очередь, стал моделью для E [6]. Е комбинирует формализмы:
- объектно-ориентированного программирования (абстракция и композиция);
- моделей безопасности (прежде всего мандатной) современных операционных систем (управление полномочиями процессов);
- финансовой криптографии (описание кооперативных протоколов передачи прав между не доверяющими друг другу сторонами).
Диаграммы Грановеттера
Интересно, что базовую метафору разработчики берут совсем из другой области: в начале семидесятых американский социолог Марк Грановеттер (Mark Granovetter) предложил исследовать динамику топологии межличностных отношений с помощью простой модели, которую теперь называют диаграммой Грановеттера. На рис. 2 изображена диаграмма Грановеттера, фиксирующая простой факт: Аня знакомит Борю с Верой.
Марк Миллер с коллегами видят возможность шести интерпретаций этого формализма:
- как шага в объектных вычислениях;
- как передачи мандата (делегирования полномочий) в модели безопасности ОС;
- как криптографического протокола, реализующего распределение полномочий;
- как элемента инфраструктуры открытых ключей, сертификаты в которых служат сообщениями, авторизирующими участников;
- как правила в игре с массовым участием
- и, наконец, как элемента для построения финансового инструмента на предъявителя.
Последняя интерпретация неочевидна? Но авторы вводят еще один схематизм (рис. 3), особым образом изображая простой оператор присвоения. "Запаковав" переменную в отдельный объект и предоставив доступ к ней посредством порождаемых при его создании объектов-функций ("установщика" и "получателя" значения), они изображают совокупность этих объектов в виде составной сущности (composite) с гранями (facets) - объектами, на которые можно ссылаться из внешнего контекста.
Эта составная сущность, как и любой объект, представляет собой комбинацию состояния (значения внутренних переменных) и поведения (кода). Однако поведение ее зависит не только от содержания полученного составным объектом сообщения, но также и от того, к какой "грани" (к какому из составляющих ее индивидуальных объектов) обращено это сообщение. Мы получили новое измерение свободы, новую степень гибкости!
После этого оказывается, что полный протокол обращения простейшего инструмента на предъявителя можно очень легко и наглядно изобразить в следующем виде (рис. 4). А после этого обнаруживается и собственно факт, который и подвигнул меня на написание этой статьи. Оказывается, что запрограммировать порождение "пресса" на E можно в 26 строк! Для сравнения: реальный mint из любого пакета поддержки обращения "цифровой наличности" - это несколько тысяч строк на C++.
Реальный mint, конечно, посложнее учебного примера Миллера [6], однако несколько недель экспериментирования с E показывают, что и вполне практичные протоколы (обращение опционов, например) программируются в десятки, в крайнем случае в сотни строк.
Документацию, описания E, примеры программ на нем и, наконец, исходный и исполняемый код самой среды программирования (распространяется на условиях лицензии Mozilla) можно найти на www.erights.org.Литература
[1] Айан Григг. Цифровой трейдинг // "Компьютерра" #12 (240) от 30 марта 1998 (Приложение).
[2] Ник Cабо. Умные контракты (Четвертая революция стоимости) // "Компьютерра" #38 (266) от 29 сентября 1998 г.
[3] G. Agha, I. A. Mason, S. Smith, and C. L. Talcott. Towards a theory of Actor Computation. In Concur '92, volume 630 of Lecture Notes in Computer Science, pages 565-579. Springer-Verlag, 1992.
[4] G. Agha, I. A. Mason, S. Smith, and C. L. Talcott. A Foundation for Actor Computation. Journal of Functional Programming, 1993.
[5] The Joule Manual. Agorics Tech Report ADd003.4P (www.agorics.com/joule.html).
[6] Mark S. Miller, Chip Morningstar, Bill Frantz. Capability-based Financial Instruments // Financial Cryptography '00. Springer-Verlag, готовится к печати.
1 (обратно к тексту) - Линия от <greek>l</greek>-исчисления к Алголу-60 выглядит большой натяжкой: с некоторым основанием непроцедурной можно назвать лишь одну конструкцию последнего - условное присваивание, которое очень хорошо ложится в контекст процедурного программирования.
2 (обратно к тексту) - LISP - это, безусловно, <greek>l-</greek>-язык по основаниям, однако обращаться к корпусу кода на LISP в надежде получить яркие примеры функционального программирования - сомнительная затея: LISP допускает процедурный стиль, и программисты много лет беззастенчиво пользуются этой минутной слабостью его разработчиков. В педагогических целях для изучения функционального программирования можно порекомендовать, например, ML с его жестким контролем типов и их соответствия.
3 (обратно к тексту) - См. www.cis.upenn.edu/%7EKeyKOS.
