Летняя школа в г. Марктобердорф 2009 — различия между версиями
Ulysses (обсуждение | вклад) (Новая страница: «Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальны…») |
Ulysses (обсуждение | вклад) (edu.mmcs → mmcs.; rename category) |
||
(не показаны 42 промежуточные версии 3 участников) | |||
Строка 1: | Строка 1: | ||
− | Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальным методам «[http://asimod.in.tum.de/ Logics and Languages for Reliability and Security]», ежегодно проводимой в немецком городе Марктобердорф с 1970 года. | + | Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальным методам «[http://asimod.in.tum.de/ Logics and Languages for Reliability and Security]», ежегодно проводимой в немецком городе Марктобердорф с 1970 года. [[Image:Timetable-Marktoberdorf09.jpg|thumb|right|Расписание школы]] |
==Анализ и верификация программ с помощью абстрактной интерпретации== | ==Анализ и верификация программ с помощью абстрактной интерпретации== | ||
− | '''Патрик Кюзо ([http://www.di.ens.fr/~cousot/ Patrick Cousot) | + | '''Патрик Кюзо ([http://www.di.ens.fr/~cousot/ Patrick Cousot]), École Normale Supérieure, Париж, Франция''' |
− | В исследованиях по верификации программ самой популярной моделью для программы является ''система переходов'': тройка из множества состояний, его подмножества начальных состояний и бинарного отношения перехода на множестве состояний, которое является отношением порядка. Можно рассмотреть иерархию семантик программ, абстрагированных таким образом. Например, множество [http://en.wikipedia.org/wiki/Total_order#Chains цепей], порождённых отношением перехода называют ''семантикой частичных трасс'' (partial trace semantics). Эту семантику можно абстрагировать, оставив от каждой цепи её начало и конец — получается ''семантика рефлексивного транзитивного замыкания'' отношения перехода. Вводятся несколько подобных семантик, которые выстраиваются в иерархию в том смысле, что определяются операторы абстрагирования и конкретизации, позволяющие переходить между уровнями этой иерархии (различными семантиками). Каждая пара операторов абстрагирования—конкретизации, как правило, обладают связью Галуа ([http://en.wikipedia.org/wiki/Galois_connection Galois connection]). Каждая из рассматриваемых семантик может быть определена в | + | В исследованиях по верификации программ самой популярной моделью для программы является ''система переходов'': тройка из множества состояний, его подмножества начальных состояний и бинарного отношения перехода на множестве состояний, которое является отношением порядка. Можно рассмотреть иерархию семантик программ, абстрагированных таким образом. Например, множество [http://en.wikipedia.org/wiki/Total_order#Chains цепей], порождённых отношением перехода называют ''семантикой частичных трасс'' (partial trace semantics). Эту семантику можно абстрагировать, оставив от каждой цепи её начало и конец — получается ''семантика рефлексивного транзитивного замыкания'' отношения перехода. Вводятся несколько подобных семантик, которые выстраиваются в иерархию в том смысле, что определяются операторы абстрагирования и конкретизации, позволяющие переходить между уровнями этой иерархии (различными семантиками). Каждая пара операторов абстрагирования—конкретизации, как правило, обладают связью Галуа ([http://en.wikipedia.org/wiki/Galois_connection Galois connection]). Каждая из рассматриваемых семантик может быть определена в терминах неподвижной точки специального оператора, что позволяет проводить вычисления этих семантик — с помощью [http://en.wikipedia.org/wiki/Kleene_fixpoint_theorem теоремы Клини], используя итерации Клини. Сложность состоит в том, что в конкретных случаях итерации Клини могут расходиться (неподвижная точка, хотя в силу теоремы Клини существует, но не достигается). Для уточнения процесса поиска неподвижных точек вводятся понятия операторов расширения (widening) и сужения (narrowing), которые подбираются в каждом случае отдельно. |
− | Описанные концепции реализованные в программном анализаторе [http://www.astree.ens.fr/ ASTRÉE], который с марта этого года является коммерчески распространяемым. | + | Описанные концепции реализованные в программном анализаторе [http://www.astree.ens.fr/ ASTRÉE], который с марта этого года является коммерчески распространяемым. Кроме статического анализа, абстрактная интерпретация может применяться для построения доказуемо корректных преобразований программ [[http://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-02-ACM-p178--190-2002-A4.ps.gz Cousot and Cousot, 2002]]. |
===Ссылки=== | ===Ссылки=== | ||
− | *[http:// | + | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Cousot_Abs_09.pdf Аннотация лектора] |
− | *[http:// | + | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Basic%20Concepts%20of%20Abstract%20Interpretation.pdf Basic Concepts of Abstract Interpretation] |
− | *[http:// | + | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Abstract%20interpretation%20based%20static%20analysis%20parameterized%20by%20semantics%20.pdf Abstract interpretation based static analysis parameterized by semantics] |
− | *[http:// | + | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Abstract%20interpretation%20of%20resolution-based%20semantics.pdf Abstract interpretation of resolution-based semantics] |
− | *[http:// | + | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20A%20Case%20Study%20in%20Abstract%20Interpretation%20Based%20Program%20Transformation_%20Blocking%20Command%20Elimination.pdf A Case Study in Abstract Interpretation Based Program Transformation: Blocking Command Elimination] |
− | *[http:// | + | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Automatic%20Verification%20by%20Abstract%20Interpretation.pdf Automatic Verification by Abstract Interpretation] |
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Constructive%20design%20of%20a%20hierarchy%20of%20semantics%20of%20a%20transition%20system%20by%20abstract%20interpretation.pdf Constructive design of a hierarchy of semantics of a transition system by abstract interpretation] | ||
+ | |||
+ | ==Многозначные автоматы и их приложения== | ||
+ | '''Орна Купферман ([http://www.cs.huji.ac.il/~ornak/ Orna Kupferman]), Еврейский университет в Иерусалиме, Израиль''' | ||
+ | |||
+ | [http://ru.wikipedia.org/wiki/Конечный_автомат Конечный автомат] можно рассматривать как отображение из множества слов над алфавитом в множество {0, 1} (слово может быть принято или нет). Рассматриваются обобщения, заменяющие {0, 1} на произвольное [http://en.wikipedia.org/wiki/Semiring полукольцо] или [http://ru.wikipedia.org/wiki/Решётка_(теория_множеств) решётку]. К первому обобщению относится понятие взвешенного автомата. Он получается из обычного (недетерминированного) конечного автомата приписыванием переходам неотрицательных вещественных чисел (стоимости). В процессе работы автомата, стоимость переходов при чтении каждой буквы складывается. Если существует несколько вариантов работы автомата, при котором слово распознаётся, то из нескольких возможных стоимостей выбирается наименьшая; нераспознанным словам приписывается стоимость ∞(полукольцо, таким образом, образует множество неотрицательных вещественных чисел и ∞ с бинарными операциями минимума и сложения — т. н. [http://en.wikipedia.org/wiki/Tropical_semiring#Basic_definitions тропическое полукольцо]). Говорят, что один автомат α-аппроксимирует другой, если стоимости распознавания каждого слова отличаются не более чем в α раз. Рассматривается операция удаления переходов взвешенного автомата: говорят, что взвешенный автомат α-детерменизируем удалением переходов, если существует детерминированный автомат, который получен из исходного удалением переходов и α-аппроксимирует его. | ||
+ | |||
+ | Далее рассматриваются некоторые оптимизационные задачи: [http://en.wikipedia.org/wiki/Ski_rental_problem задача аренды лыж], [http://en.wikipedia.org/wiki/Page_replacement_algorithm задача замещения страниц в кэш-памяти] и другие. Вводится понятие [http://en.wikipedia.org/wiki/Online_algorithm онлайн-алгоритма] для решения оптимизационной задачи. Онлайн-алгоритм работает с последовательностью запросов, обработка каждого запроса имеет некоторую стоимость, особенность состоит в том, что онлайн-алгоритм не знает заранее всю последовательность запросов. Эффективность онлайн-алгоритм оценивается с помощью сравнения с оптимальным оффлайн-алгоритмом для данной оптимизационной задачи («оффлайн» означает, что вся последовательность запросов известна изначально). Это формализуется понятием α-соревновательный онлайн-алгоритм. Основная теорема этой части курса гласит, что для задачи существует α-соревновательный онлайн-алгоритм решения, если автомат, построенный по этой задаче, α-детерменизируем удалением переходов. | ||
+ | |||
+ | Вторая разновидность обобщённых автоматов предполагает, что множество состояний и отношение переходов конечного автомата являются L-множествами, где L — некоторая решётка. Обычное множество, назовём его M, можно представлять себе как отображения некоторого универсального множества в множество {0, 1} (принадлежит или не принадлежит рассматриваемому множеству M). L-множество использует тот же самый подход, но вместо {0, 1} используется решётка L. По определению в решётке есть бинарные операции ∧, ∨ — с их помощью можно определить стоимость распознавания слова. Решёточные автоматы могут использоваться для анализа решёточных линейных [http://ru.wikipedia.org/wiki/Темпоральная_логика темпоральных логик] LLTL, которые являются обобщением широко используемых в верификации ПО (а именно, в [http://ru.wikipedia.org/wiki/Проверка_моделей model checking]) линейных темпоральных логик, LTL. | ||
+ | |||
+ | В курсе приведены оценки сложности операций, связанных с понятиями аппроксимации, вложения, детерминируемости удалением переходов многозначных автоматов и др. | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Kupferman_Abs_09.pdf Аннотация лектора] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Kupferman/Kupferman%20et%20al.%20Reasoning%20about%20Online%20Algorithms%20with%20Weighted%20Automata.pdf Reasoning about Online Algorithms with Weighted Automata] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Kupferman/Kupferman,%20Lustig.%20Lattice%20Automata.pdf Lattice Automata] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Kupferman/Albers.%20Competitive%20Online%20Algorithms,%201996.ps Albers. Competitive Online Algorithms] | ||
+ | *[http://springerlink.com/content/x4432l/?p=dfe6eec16d6344e7a65f63d1786e1e4b&pi=0 Handbook of Weighted Automata // Monographs in Theoretical Computer Science, Springer-Verlag, 2009.] | ||
+ | |||
+ | ==Модальные логики неподвижных точек== | ||
+ | '''Герхард Ягер ([http://www.iam.unibe.ch/til/staff/jaeger Gerhard Jäger]), Университет Берна, Швейцария''' | ||
+ | |||
+ | В первой части курса последовательно рассматриваются синтаксис, семантика и различные аксиоматизации µ-исчисления. µ-исчисление расширяет обычное [http://en.wikipedia.org/wiki/Propositional_calculus исчисление высказываний]<ref>Не рекомендуется консультироваться со статьёй об исчислении высказываний в русской Википедии.</ref> операторами наименьшей и наибольшей неподвижных точек, которые широко используются при изучении [http://en.wikipedia.org/wiki/Transition_system систем переходов] (в курсе приводились примеры выражения свойств живучести и безопасности системы на языке неподвижных точек). При изучении ''помеченных'' систем переходов, когда есть не одно отношение перехода, а целое семейство этих отношений, подходящую формализацию доставляет добавление в логику [http://en.wikipedia.org/wiki/Modal_logic модальностей]. Семантика модального µ-исчисления вводится с помощью систем переходов (например, пропозициональным переменным ставятся в соответствие множества состояний системы, в которых они считаются истинными). Наиболее очевидная аксиоматизация µ-исчисления, хотя обладает обоими фундаментальными свойствами формальных исчислений в отношении семантики, полнотой и корректностью (soundness) (то есть, грубо говоря, все истинные в данной семантике утверждения могут быть доказаны и только они), является неудобной для автоматического поиска доказательств — в основном из-за присутствия правила [http://ru.wikipedia.org/wiki/Modus_ponens Modus Ponens] (MP). В связи с этим развивается семантика µ-исчисления: доказывается разрешимость задачи выполнимости формулы (однако лучший теоретико-сложностный результат для этой задачи NP ∩ coNP — интересно, имеется ли полиномиальный алгоритм) и теорема о малой модели, которая говорит, что если формула выполняется на какой-то системе переходов, то она выполняется на некоторой конечной (экспоненциально большой от размера формулы) системе переходов. Последнее позволяет выполнить следующий трюк. Строится полная и корректная аксиоматиация µ-исчисления, свободная от MP (говорят: «свободная от сечений»), но содержащая одно правило вывода с бесконечным (счётным) количеством посылок (которые являются итерациями оператора наибольшей неподвижной точки), а затем с помощью теоремы о малой модели доказывается, что любой вывод в этой аксиоматизации можно оборвать после конечного числа шагов — это позволяет сформулировать финитарный вариант аксиоматизации µ-исчисления, который также (доказывается) является полным и корректным. Открытыми остаются вопросы о том, можно ли получить финитарную аксиоматизацию на основе рассмотренных, не прибегая к семантическим доводам (чисто синтаксическими методами), и есть ли более естественный путь построения свободной от сечений аксиоматизации µ-исчисления. | ||
+ | |||
+ | Во второй части курса изучаются различные сужения µ-исчисления для формализации понятия знания и общего знания. Если ограничиться рассмотрением систем переходов, семейство отношений перехода которых представляет собой конечное множество, то пронумеровав его элементы, можно смотреть на него как на набор стратегий n агентов. Формулы с модальностями трактуются в стиле [http://en.wikipedia.org/wiki/Modal_logic#Epistemic_logic эпистемологической логики]: [a]ψ понимается как «a знает, что ψ» (a ∊ {1,..,n}). Для выражения общего знания достаточно ограничиться применением операторов неподвижной точки к формулам специального вида — мы получаем подсистему модального µ-исчисления, которая остаётся полной и корректной. Полностью избавиться от сечений не удаётся и здесь, однако имеется следующий результат: для истинного множества формул Г можно заранее указать множество формул DC(Г), которые будут использоваться в сечениях при выводе этих формул — мы получаем некий контроль над сечениями. DC(Г) является специфическим дизъюнктивно-конъюнктивным замыканием Г, которое, однако, всё ещё слишком велико, чтобы приносить пользу на практике. Есть ощущение, что его можно сузить — это является одним из открытых вопросов. | ||
+ | |||
+ | В заключении курса приведён пример исчисления, соединяющего в себе суженное модальное µ-исчисление для n агентов и «логику доказательств», разработанную [http://web.cs.gc.cuny.edu/~sartemov/ Сергеем Артёмовым]. Последняя рассматривает понятие «свидетельства доказательства», когда в процессе вывода формул к ним приписываются по определённым правилам специальные термы («свидетельства»). Обнаружено несколько интересных соотношений между понятиями свидетельства, знания и общего знания, однако это направление требует дальнейшей разработки. | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Jaeger_Abs_09.pdf Аннотация лектора] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Bradfield,%20Stirling.%20Modal%20Mu-Calculi.pdf Bradfield, Stirling. Modal Mu-Calculi] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/About%20cut%20elimination%20for%20logics%20of%20common%20knowledge.pdf About cut elimination for logics of common knowledge] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Cut-free%20common%20knowledge.pdf Cut-free common knowledge] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Brunnler,%20Studer.%20Syntactic%20Cut-elimination%20for%20Common%20Knowledge.pdf Brunnler, Studer. Syntactic Cut-elimination for Common Knowledge] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Yavorskaya.%20Interacting%20Explicit%20Evidence%20Systems.pdf Yavorskaya. Interacting Explicit Evidence Systems] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Artemov.%20Evidence-based%20common%20knowledge.pdf Artemov. Evidence-based common knowledge] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Artemov,%20Beklemishev.%20Provability%20logic.pdf Artemov, Beklemishev. Provability logic] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Walukiewicz.%20How%20to%20Fix%20It_%20Using%20Fixpoints%20in%20Different%20Contexts%20.pdf Walukiewicz. How to Fix It_ Using Fixpoints in Different Contexts] | ||
+ | |||
+ | ==Ньютоновский анализ программ== | ||
+ | '''Хавьер Эспарза ([http://www7.informatik.tu-muenchen.de/~esparza/ Javier Esparza]), Технический университет Мюнхена, Германия''' | ||
+ | |||
+ | Ряд методик анализа программ основывается на изучении управляющего графа программы. Один распространённый подход к анализу потока данных программы основывается на приписывании каждой инструкции программы значения из некоторой [http://en.wikipedia.org/wiki/Semilattice полурешётки] и введении в этой решётке операции «произведения», соответствующей конкатенации (последовательному выполнению) инструкций, которое (после некоторых дополнительных усилий) превращает исходную полурешётку в идемпотентное [http://en.wikipedia.org/wiki/Semiring полукольцо]. В терминах управляющего графа программы это означает приписывание дугам значений полукольца. Последовательный фрагмент программы можно записать как произведение таких значений, а фрагмент с ветвлениями — как сложение. В результате фрагмент программы может быть выражен алгебраически. | ||
+ | |||
+ | Занимаясь межпроцедурным анализом программ можно поступить так: пусть есть несколько процедур, вызывающих друг друга, тогда, выписывая выражение указанным выше образом для каждой, можно инструкцию вызова другой процедуры заменять именем этой процедуры, понимая его как имя переменной. В результате получается система алгебраических уравнений нескольких переменных. Важная информация о поведении программы может быть получена из решения этой системы. Характер информации зависит, конечно, от того, какой смысл вложен в операции полукольца. В частности, можно подсчитывать вероятности завершения программы или наименьшее количество выполнений фрагментов программы перед завершением. Более того, уравнения такого вида могут анализироваться в контексте задач, несвязанных с анализом программ: например, если рассматривать полукольцо языков, состоящих из слов над некоторым алфавитом, то система алгебраических уравнений задаёт контекстно-свободную грамматику, а её наименьшее решение является языком этой грамматики. | ||
+ | |||
+ | Первые методы решения систем алгебраических уравнений над данным полукольцом основывались на вариантах [http://en.wikipedia.org/wiki/Kleene_fixpoint_theorem теоремы Клини о неподвижной точке для решёток]: на полукольце вводится частичный порядок, связанный с полукольцевыми операциями, алгебраические функции автоматически являются непрерывными и монотонными, чего требует классическая теорема Клини. Метод Клини для нахождения наименьшей неподвижной точки отображения (который даёт теорема Клини) имеет ряд недостатков: он может не давать значения неподвижной точки (и так происходит в ряде важных случаев, например, при решении некоторых уравнений, содержащих операцию * — звезду Клини), он может сходиться к неподвижной точке очень медленно. Для решения этих проблем итерационный метод Ньютона был распространён на ω-непрерывные полукольца. Имеется две очевидных сложности на этом пути: отсутствия вычитания и деления. Деление используется в определении производной, однако производную полинома можно определить формально, используя фигурирующие в анализе формулы для производной произведения и суммы. Разность же (например, ''a-b'') может быть заменена элементом (например, ''c'') с соответствующим свойством(''c+b=a'') — доказывается, что такой элемент существует и, что, каким бы его ни выбрать, будет получено одно и то же приближение на очередной итерации метода Ньютона. | ||
+ | |||
+ | Кроме информации, полученной с решением системы, интерес могут представлять приближения, вычисляемые на каждой итерации. Например, для упомянутого выше полукольца языков ''i''-ое приближение описывает подмножество слов языка данной грамматики индекса ''i'' (слово имеет индекс ''i'', если существует вывод этого слова, такой что в каждой сентенциальной форме участвует не более, чем ''i'' нетерминалов); кроме того, приближения Клини и Ньютона можно охарактеризовать также с помощью свойств деревьев вывода для слов, содержащихся в них. | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Esparza_Abs_09.pdf Аннотация лектора] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Esparsa/Esparza.%20newtProgAn.pdf Newtonian Program Analysis] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Esparsa/Kuich.%20Semirings%20and%20FPS.pdf Kuich. Semirings and Formal Power Series] | ||
+ | |||
+ | ==Принципы и приложения уточнённых типов (refinement types)== | ||
+ | '''Эндрю Гордон ([http://research.microsoft.com/en-us/um/people/adg/ Andrew Gordon]), Microsoft Research, Кэмбридж, Англия''' | ||
+ | |||
+ | Курс лекций состоял из трёх частей, в каждой из которых рассматривались технологии (языки программирования, моделирования и формальные языки), решающие задачи, связанные с безопасностью (в разных смыслах этого слова). Общий подход к решению задачи доказательства некоторых свойств системы таков: разработать достаточно богатую для выражения интересующего свойства систему типов и попытаться оттипизировать исследуемую систему. На этом пути важным инструментом являются уточнённые типы. Идея уточнённых типов проста: уточнённый тип это базовый тип плюс предикат для значения этого типа. Например, уточнённый тип чётных чисел это целые числа плюс предикат проверки на чётность. Использование этой идеи в промышленном программировании многие годы сдерживалось разными факторами: проверка предикатов была не достаточно эффективна, не всегда возможна и не всегда надёжна. Последние достижения в разработке формальных методов, появление эффективных инструментов класса [http://en.wikipedia.org/wiki/SMT_solver SMT solvers] и появление задач, в которых некоторые недостатки реализации уточнённых типов не играют решающей роли, изменили положение дел. | ||
+ | |||
+ | Первая часть знакомила с [http://msdn.microsoft.com/en-us/oslo/default.aspx проектом «Oslo»] от Microsoft. Oslo это набор технологий для моделирования жизненного цикла и характеристик корпоративных приложений, разрабатываемых с использованием разнообразных технологий Microsoft (.NET, ASP.NET, Visua Studio, XAML). Такое моделирование предусматривает высокоуровневое описание форматов данных, схем данных, окружений и источников данных. Это новая ступень эволюции таких известных средств как, например, конфигурационные файлы, управляющие сценарии, XML-[http://en.wikipedia.org/wiki/Deployment_Descriptor дескрипторы развёртывания] корпоративных приложений. | ||
+ | |||
+ | Составной частью проекта Oslo является [http://msdn.microsoft.com/en-us/library/dd129617%28VS.85%29.aspx язык M]. Были продемонстрированы детали реализации уточнённых типов в этом языке и приведён пример описания некоторой политики безопасности для приложений (обычно описываемой в XML-файлах и диктующей, к примеру, использование криптоключей определённой длины, сертификатов и т. п.) с помощью системы типов M: в конечном счёте определяется тип «безопасная конфигурация», и конкретные конфигурации приложений могут быть пропущены через type checker и допущены или отвергнуты. Более подробное описание достоинств системы типов M содержится в ещё не опубликованной работе Bierman, Gordon, Langworthy. | ||
+ | |||
+ | Вторая часть курса посвящена описанию подхода к верификации криптопротоколов на основе верификации программного кода этих протоколов, выполненных на функциональном языке с поддержкой конкурентности (concurrency) в духе [http://en.wikipedia.org/wiki/Pi-calculus pi-исчисления] — [http://en.wikipedia.org/wiki/F_Sharp_%28programming_language%29 F#]. В третьей части курса рассматривается новая формальная система RFC (Refined Concurrent FPC (Fixpoint Calculus); FPC — возможная формальная основа ML и Haskell, разработанная Плоткиным, 1985 и Гюнтером, 1992), которая должна служить теоретическим базисом для полноценной реализации идей, встретившихся во второй части. Кроме FPC, pi-calculus и уточнённых типов используются такие теоретические разработки как печати Морриса (см. ссылки), спецификации безопасности assume/assert (Флойд, Хоар, Дейкстра) и другие. Описывается разрабатывающийся в настоящее время язык F7, расширение F#, который должен стать реализацией RFC. С помощью богатых выразительных средств F7 можно описывать требования безопасности в виде интерфейсов, а затем проверять соответствие этим интерфейсам реализаций криптопротоколов на F# (такая проверка типов является частью F7). | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Gordon_Abs_09.pdf Аннотация лектора] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Gordon/Principles%20and%20Applications%20of%20Refinement%20Types,%20slides.pdf Слайды] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Gordon/refinement-types-for-secure-implementations.pdf Refinement Types for Secure Implementations] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Gordon/morris73.pdf Morris, Protection in Programming Languages] | ||
+ | |||
+ | ==Model Checking вычислений высших порядков== | ||
+ | '''Люк Онг ([http://users.comlab.ox.ac.uk/luke.ong/ Luke Ong]), Оксфорд, Англия''' | ||
+ | |||
+ | Зарекомендовавшим себя формализмом для представления программ на функциональных языках программирования (использующих [http://ru.wikipedia.org/wiki/Функция_высшего_порядка вычисления высших порядков]) являются ''схемы рекурсии высших порядков'': это синтаксический инструмент наподобие порождающих [http://ru.wikipedia.org/wiki/Формальная_грамматика грамматик Хомского], описывающий (бесконечные) деревья (слова, описываемые грамматиками Хомского, являются, очевидно, частным случаем деревьев). Схемы рекурсии могут также рассматриваться как уравнения, записанные в термах, принадлежащих фрагменту [http://en.wikipedia.org/wiki/Simply-typed_lambda_calculus просто типизированного λ-исчисления]. Позволяя конечными средствами описывать бесконечный объект, схемы рекурсии являются актуальным понятием в приложениях к верификации ПО, а именно software model cheking (в отличие от уже достаточно разработанного hardware model cheking, работающего с системами с конечным числом состояний). В первой части курса устанавливается связь между схемами рекурсии и стековыми автоматами высших порядков (САВП). Последние были введены ещё А. Н. Масловым в 74 году и являются обобщением обычных [http://ru.wikipedia.org/wiki/Стековый_автомат стековых автоматов], у которых внутри стека хранятся другие стеки, внутри которых хранятся другие стеки и т. д., глубиной вложенности ''n'' для ''стекового автомата порядка n''. Приводятся примеры описания одних и тех же языков с помощью схем рекурсии и САВП. Основной результат, существовавший до недавнего времени это равномощность САВП и ''сохранных'' (safe) схем рекурсии. Совсем недавно была доказана эквивалентность общих схем рекурсии и ''сворачивающихся'' (collapsible) САВП. Последние представляют собой САВП с возможностью в любой момент развернуть стек до определённого (заранее отмеченного) места. Тем не менее, являются ли ССАВП собственным подклассом САВП, остаётся открытым вопросом. Множество открытых вопросов остаётся также в отношении «''иерархии Маслова''» языков САВП (например, 0-языки это регулярные языки, 1-языки это контекстно-свободные языки, 2-языки это [http://en.wikipedia.org/wiki/Indexed_language индексированные языки], предложенные Ахо в 68 году, строго более широкие, чем КС-языки — являются ли 3-языки в точности контекстно-зависимыми языками? можно ли предложить для языков САВП аналоги [http://ru.wikipedia.org/wiki/Лемма_о_накачке лемм о накачке]?). При описании семантики и верификации ПО, использующего вычисления высших порядков удобно иметь в запасе оба рассмотренных формализма. | ||
+ | |||
+ | Далее в курсе формулируется задача Model Checking для вычислений высших порядков. Модели задаются деревьями, порождаемыми схемами рекурсии или играми. Для спецификации используются формулы [http://en.wikipedia.org/wiki/Monadic_second-order_logic монадических логик второго порядка] (МВП-логик) (которые, как утверждается, наилучшим образом подходят для выражения интересных свойств встречающихся системы). Приводятся новые результаты о разрешимости МВП-теорий (и её сложности). Рассматривается метод решения задачи Model Checking, основанный на сведении её к задаче типизации исходной схемы рекурсии. | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Ong_Abs_09.pdf Аннотация лектора] | ||
+ | *Слайды к лекциям: [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/slides-part1.pdf часть 1], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/slides-part2.pdf часть 2] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Ong.%20On%20model-checking%20trees%20generating%20by%20higher-order%20recursion%20schemes,%202006.pdf Ong et al. On model-checking trees generating by higher-order recursion schemes, 2006] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Ong%20et%20al.%20Collapsible%20Pushdown%20Automata%20and%20Recursion%20Schemes,%202008.pdf Ong et al. Collapsible Pushdown Automata and Recursion Schemes, 2008] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Hague,%20Ong.%20Symbolic%20Backwards-Reachability%20Analysis%20for%20Higher-Order%20Pushdown%20Systems,%202008.pdf Hague, Ong. Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems, 2008] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Knapik%20et%20al.%20Deciding%20Monadic%20Theories%20of%20Hyperalgebraic%20Trees,%202001.pdf Knapik et al. Deciding Monadic Theories of Hyperalgebraic Trees, 2001] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Knapik%20et%20al.%20Higher-Order%20Pushdown%20Trees%20Are%20Easy,%202002.pdf Knapik et al. Higher-Order Pushdown Trees Are Easy, 2002] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Knapik%20et%20al.%20Unsafe%20Grammars%20and%20Panic%20Automata,%202005.pdf Knapik et al. Unsafe Grammars and Panic Automata, 2005] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Blum,%20Ong.%20The%20Safe%20Lambda%20Calculus,%202009,%20LMCS.pdf Blum, Ong. The Safe Lambda Calculus, 2009, LMCS] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/de%20Miranda.%20Structures%20Generated%20by%20Higher-Order%20Grammars%20and%20the%20Safety%20Constraint,%202006,%20PhD.pdf de Miranda. Structures Generated by Higher-Order Grammars and the Safety Constraint, 2006, PhD] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Rabin.%20Decidability%20of%20Second-Order%20Theories%20and%20Automata%20on%20Infinite%20Trees,%201969.pdf Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees, 1969] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Maslov.%20Multilevel%20stack%20automata,%201976.pdf Маслов. Многоуровневые магазинные автоматы, 1976] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Indermark.%20Schemes%20with%20recursion%20on%20higher%20types,%201976.pdf Indermark. Schemes with recursion on higher types, 1976] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Damm,%20Goerdt.%20An%20automata-theoretic%20characterization%20of%20the%20OI-hierarchy,%201986.pdf Damm, Goerdt. An automata-theoretic characterization of the OI-hierarchy, 1986] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Damm.%20Languages%20defined%20by%20higher%20type%20program%20schemes,%201977.pdf Damm. Languages defined by higher type program schemes, 1977] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Damm.%20The%20IO-%20and%20OI-hierarchy,%201982.pdf Damm. The IO- and OI-hierarchy, 1982] | ||
+ | |||
+ | ==Трёхзначная абстракция и её приложения в Model Checking== | ||
+ | '''Орна Грумберг ([http://www.cs.technion.ac.il/~orna/ Orna Grumberg]), TECHNION — Технический университет Израиля''' | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Grumberg_Abs_09.pdf Аннотация лектора] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Grumberg/Grumberg.%20Compositional%20Verification%20and%203-Valued%20Abstractions%20Join%20Forces.pdf Compositional Verification and 3-Valued Abstractions Join Forces] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Grumberg/Grumberg.%20A%20Game-Based%20Framework%20for%20CTL%20Counter-Examples%20and%203-Valued%20Abstraction-Refinement.ps.gz A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Grumberg/Grumberg-abstraction-and-refinement.pdf Abstraction and Refinement in Model Checking] | ||
+ | |||
+ | ==Механизированные семантики== | ||
+ | '''Ксавье Леруа ([http://pauillac.inria.fr/~xleroy/ Xavier Leroy]), INRIA, Франция''' | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Leroy_Abs_09.pdf Аннотация лектора] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/slides.pdf Слайды к лекции] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/handout.pdf Раздаточный материал к лекции] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/Grall,%20Leroy.%20Coinductive%20big-step%20operational%20semantics.pdf Grall, Leroy. Coinductive big-step operational semantics] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/Nipkow.%20Winskel%20is%20(almost)%20Right_%20Towards%20a%20Mechanized%20Semantics%20Textbook.ps Nipkow. Winskel is (almost) Right_ Towards a Mechanized Semantics Textbook] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/coq-hurry.pdf Bertot. Coq in a Hurry] | ||
+ | |||
+ | ==Эффективный анализ стохастических процессов и игр с бесконечным числом состояний== | ||
+ | '''Антонин Кучера ([http://www.fi.muni.cz/usr/kucera/ Antonin Kučera]), Masaryk University, Чехия''' | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Kucera_Abs_09.pdf Аннотация лектора] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Kucera%20et%20al.%20Qualitative%20Reachability%20in%20Stochastic%20BPA%20Games.pdf Kucera et al. Qualitative Reachability in Stochastic BPA Games] | ||
+ | |||
+ | ==Синтаксический контроль утечек и освобождения информации== | ||
+ | '''Андрей Сабельфельд ([http://www.math.chalmers.se/~andrei/ Andrey Sabelfeld]), Gothenburg University, Швеция''' | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Sabelfeld_Abs_09.pdf Аннотация лектора] | ||
+ | |||
+ | ==Использование политик конфиденциальности (security policies) для написания безопасного (secure) ПО== | ||
+ | '''Эндрю Майерс ([http://www.cs.cornell.edu/andru/ Andrew Myers]), Cornell University, США''' | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Myers_Abs_09.pdf Аннотация лектора] | ||
+ | |||
+ | ==Два приложения систем доказательства теорем== | ||
+ | '''Тобиас Нипков ([http://www4.informatik.tu-muenchen.de/~nipkow/ Tobias Nipkow]), Технический университет Мюнхена, Германия''' | ||
+ | |||
+ | ===Ссылки=== | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Nipkow_Abs_09.pdf Аннотация лектора] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Nipkow/Verifying%20a%20Hotel%20Key%20Card%20System.pdf Verifying a Hotel Key Card System] | ||
+ | *[http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Nipkow/Social%20choice%20theory%20in%20HOL.pdf Social choice theory in HOL] | ||
+ | |||
+ | ==Аудио некоторых лекций== | ||
+ | Этот материал в силу своей разрозненности и неполноты не очень помогает в понимании, он выложен для того, чтобы можно было лучше представить как проходили лекции и обсуждения по итогам дня... Например, можно оценить скорость речи Гордона или понять, что Купферман единственная использовала доску и мел. | ||
+ | |||
+ | [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0806000-Kupferman.MP3 Купферман], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0806001-Jager-1.MP3 Ягер], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0806002-Sabelfeld-discussion.MP3 Сабельфельд+обсуждение], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0808000-Esparsa-2.MP3 Эспарза], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0808001-Kucera-1.MP3 Кучера], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0808002-Kupferman.MP3 Купферман], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0808003-Ong-4-discussion.MP3 Онг+обсуждение], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0814000-Nipkow-1-discussion.MP3 Нипков+обсуждение], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0815000-Leroy.MP3 Леруа], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0815001-Gordon.MP3 Гордон], [http://mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0815002-Grumberg.MP3 Грумберг]. | ||
+ | |||
+ | ==Примечания== | ||
+ | <references /> | ||
+ | |||
+ | [[Категория:Школы, семинары]] |
Текущая версия на 11:27, 15 июля 2015
Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальным методам «Logics and Languages for Reliability and Security», ежегодно проводимой в немецком городе Марктобердорф с 1970 года.Error code: 127
Содержание
- 1 Анализ и верификация программ с помощью абстрактной интерпретации
- 2 Многозначные автоматы и их приложения
- 3 Модальные логики неподвижных точек
- 4 Ньютоновский анализ программ
- 5 Принципы и приложения уточнённых типов (refinement types)
- 6 Model Checking вычислений высших порядков
- 7 Трёхзначная абстракция и её приложения в Model Checking
- 8 Механизированные семантики
- 9 Эффективный анализ стохастических процессов и игр с бесконечным числом состояний
- 10 Синтаксический контроль утечек и освобождения информации
- 11 Использование политик конфиденциальности (security policies) для написания безопасного (secure) ПО
- 12 Два приложения систем доказательства теорем
- 13 Аудио некоторых лекций
- 14 Примечания
Анализ и верификация программ с помощью абстрактной интерпретации
Патрик Кюзо (Patrick Cousot), École Normale Supérieure, Париж, Франция
В исследованиях по верификации программ самой популярной моделью для программы является система переходов: тройка из множества состояний, его подмножества начальных состояний и бинарного отношения перехода на множестве состояний, которое является отношением порядка. Можно рассмотреть иерархию семантик программ, абстрагированных таким образом. Например, множество цепей, порождённых отношением перехода называют семантикой частичных трасс (partial trace semantics). Эту семантику можно абстрагировать, оставив от каждой цепи её начало и конец — получается семантика рефлексивного транзитивного замыкания отношения перехода. Вводятся несколько подобных семантик, которые выстраиваются в иерархию в том смысле, что определяются операторы абстрагирования и конкретизации, позволяющие переходить между уровнями этой иерархии (различными семантиками). Каждая пара операторов абстрагирования—конкретизации, как правило, обладают связью Галуа (Galois connection). Каждая из рассматриваемых семантик может быть определена в терминах неподвижной точки специального оператора, что позволяет проводить вычисления этих семантик — с помощью теоремы Клини, используя итерации Клини. Сложность состоит в том, что в конкретных случаях итерации Клини могут расходиться (неподвижная точка, хотя в силу теоремы Клини существует, но не достигается). Для уточнения процесса поиска неподвижных точек вводятся понятия операторов расширения (widening) и сужения (narrowing), которые подбираются в каждом случае отдельно.
Описанные концепции реализованные в программном анализаторе ASTRÉE, который с марта этого года является коммерчески распространяемым. Кроме статического анализа, абстрактная интерпретация может применяться для построения доказуемо корректных преобразований программ [Cousot and Cousot, 2002].
Ссылки
- Аннотация лектора
- Basic Concepts of Abstract Interpretation
- Abstract interpretation based static analysis parameterized by semantics
- Abstract interpretation of resolution-based semantics
- A Case Study in Abstract Interpretation Based Program Transformation: Blocking Command Elimination
- Automatic Verification by Abstract Interpretation
- Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
Многозначные автоматы и их приложения
Орна Купферман (Orna Kupferman), Еврейский университет в Иерусалиме, Израиль
Конечный автомат можно рассматривать как отображение из множества слов над алфавитом в множество {0, 1} (слово может быть принято или нет). Рассматриваются обобщения, заменяющие {0, 1} на произвольное полукольцо или решётку. К первому обобщению относится понятие взвешенного автомата. Он получается из обычного (недетерминированного) конечного автомата приписыванием переходам неотрицательных вещественных чисел (стоимости). В процессе работы автомата, стоимость переходов при чтении каждой буквы складывается. Если существует несколько вариантов работы автомата, при котором слово распознаётся, то из нескольких возможных стоимостей выбирается наименьшая; нераспознанным словам приписывается стоимость ∞(полукольцо, таким образом, образует множество неотрицательных вещественных чисел и ∞ с бинарными операциями минимума и сложения — т. н. тропическое полукольцо). Говорят, что один автомат α-аппроксимирует другой, если стоимости распознавания каждого слова отличаются не более чем в α раз. Рассматривается операция удаления переходов взвешенного автомата: говорят, что взвешенный автомат α-детерменизируем удалением переходов, если существует детерминированный автомат, который получен из исходного удалением переходов и α-аппроксимирует его.
Далее рассматриваются некоторые оптимизационные задачи: задача аренды лыж, задача замещения страниц в кэш-памяти и другие. Вводится понятие онлайн-алгоритма для решения оптимизационной задачи. Онлайн-алгоритм работает с последовательностью запросов, обработка каждого запроса имеет некоторую стоимость, особенность состоит в том, что онлайн-алгоритм не знает заранее всю последовательность запросов. Эффективность онлайн-алгоритм оценивается с помощью сравнения с оптимальным оффлайн-алгоритмом для данной оптимизационной задачи («оффлайн» означает, что вся последовательность запросов известна изначально). Это формализуется понятием α-соревновательный онлайн-алгоритм. Основная теорема этой части курса гласит, что для задачи существует α-соревновательный онлайн-алгоритм решения, если автомат, построенный по этой задаче, α-детерменизируем удалением переходов.
Вторая разновидность обобщённых автоматов предполагает, что множество состояний и отношение переходов конечного автомата являются L-множествами, где L — некоторая решётка. Обычное множество, назовём его M, можно представлять себе как отображения некоторого универсального множества в множество {0, 1} (принадлежит или не принадлежит рассматриваемому множеству M). L-множество использует тот же самый подход, но вместо {0, 1} используется решётка L. По определению в решётке есть бинарные операции ∧, ∨ — с их помощью можно определить стоимость распознавания слова. Решёточные автоматы могут использоваться для анализа решёточных линейных темпоральных логик LLTL, которые являются обобщением широко используемых в верификации ПО (а именно, в model checking) линейных темпоральных логик, LTL.
В курсе приведены оценки сложности операций, связанных с понятиями аппроксимации, вложения, детерминируемости удалением переходов многозначных автоматов и др.
Ссылки
- Аннотация лектора
- Reasoning about Online Algorithms with Weighted Automata
- Lattice Automata
- Albers. Competitive Online Algorithms
- Handbook of Weighted Automata // Monographs in Theoretical Computer Science, Springer-Verlag, 2009.
Модальные логики неподвижных точек
Герхард Ягер (Gerhard Jäger), Университет Берна, Швейцария
В первой части курса последовательно рассматриваются синтаксис, семантика и различные аксиоматизации µ-исчисления. µ-исчисление расширяет обычное исчисление высказываний[1] операторами наименьшей и наибольшей неподвижных точек, которые широко используются при изучении систем переходов (в курсе приводились примеры выражения свойств живучести и безопасности системы на языке неподвижных точек). При изучении помеченных систем переходов, когда есть не одно отношение перехода, а целое семейство этих отношений, подходящую формализацию доставляет добавление в логику модальностей. Семантика модального µ-исчисления вводится с помощью систем переходов (например, пропозициональным переменным ставятся в соответствие множества состояний системы, в которых они считаются истинными). Наиболее очевидная аксиоматизация µ-исчисления, хотя обладает обоими фундаментальными свойствами формальных исчислений в отношении семантики, полнотой и корректностью (soundness) (то есть, грубо говоря, все истинные в данной семантике утверждения могут быть доказаны и только они), является неудобной для автоматического поиска доказательств — в основном из-за присутствия правила Modus Ponens (MP). В связи с этим развивается семантика µ-исчисления: доказывается разрешимость задачи выполнимости формулы (однако лучший теоретико-сложностный результат для этой задачи NP ∩ coNP — интересно, имеется ли полиномиальный алгоритм) и теорема о малой модели, которая говорит, что если формула выполняется на какой-то системе переходов, то она выполняется на некоторой конечной (экспоненциально большой от размера формулы) системе переходов. Последнее позволяет выполнить следующий трюк. Строится полная и корректная аксиоматиация µ-исчисления, свободная от MP (говорят: «свободная от сечений»), но содержащая одно правило вывода с бесконечным (счётным) количеством посылок (которые являются итерациями оператора наибольшей неподвижной точки), а затем с помощью теоремы о малой модели доказывается, что любой вывод в этой аксиоматизации можно оборвать после конечного числа шагов — это позволяет сформулировать финитарный вариант аксиоматизации µ-исчисления, который также (доказывается) является полным и корректным. Открытыми остаются вопросы о том, можно ли получить финитарную аксиоматизацию на основе рассмотренных, не прибегая к семантическим доводам (чисто синтаксическими методами), и есть ли более естественный путь построения свободной от сечений аксиоматизации µ-исчисления.
Во второй части курса изучаются различные сужения µ-исчисления для формализации понятия знания и общего знания. Если ограничиться рассмотрением систем переходов, семейство отношений перехода которых представляет собой конечное множество, то пронумеровав его элементы, можно смотреть на него как на набор стратегий n агентов. Формулы с модальностями трактуются в стиле эпистемологической логики: [a]ψ понимается как «a знает, что ψ» (a ∊ {1,..,n}). Для выражения общего знания достаточно ограничиться применением операторов неподвижной точки к формулам специального вида — мы получаем подсистему модального µ-исчисления, которая остаётся полной и корректной. Полностью избавиться от сечений не удаётся и здесь, однако имеется следующий результат: для истинного множества формул Г можно заранее указать множество формул DC(Г), которые будут использоваться в сечениях при выводе этих формул — мы получаем некий контроль над сечениями. DC(Г) является специфическим дизъюнктивно-конъюнктивным замыканием Г, которое, однако, всё ещё слишком велико, чтобы приносить пользу на практике. Есть ощущение, что его можно сузить — это является одним из открытых вопросов.
В заключении курса приведён пример исчисления, соединяющего в себе суженное модальное µ-исчисление для n агентов и «логику доказательств», разработанную Сергеем Артёмовым. Последняя рассматривает понятие «свидетельства доказательства», когда в процессе вывода формул к ним приписываются по определённым правилам специальные термы («свидетельства»). Обнаружено несколько интересных соотношений между понятиями свидетельства, знания и общего знания, однако это направление требует дальнейшей разработки.
Ссылки
- Аннотация лектора
- Bradfield, Stirling. Modal Mu-Calculi
- About cut elimination for logics of common knowledge
- Cut-free common knowledge
- Brunnler, Studer. Syntactic Cut-elimination for Common Knowledge
- Yavorskaya. Interacting Explicit Evidence Systems
- Artemov. Evidence-based common knowledge
- Artemov, Beklemishev. Provability logic
- Walukiewicz. How to Fix It_ Using Fixpoints in Different Contexts
Ньютоновский анализ программ
Хавьер Эспарза (Javier Esparza), Технический университет Мюнхена, Германия
Ряд методик анализа программ основывается на изучении управляющего графа программы. Один распространённый подход к анализу потока данных программы основывается на приписывании каждой инструкции программы значения из некоторой полурешётки и введении в этой решётке операции «произведения», соответствующей конкатенации (последовательному выполнению) инструкций, которое (после некоторых дополнительных усилий) превращает исходную полурешётку в идемпотентное полукольцо. В терминах управляющего графа программы это означает приписывание дугам значений полукольца. Последовательный фрагмент программы можно записать как произведение таких значений, а фрагмент с ветвлениями — как сложение. В результате фрагмент программы может быть выражен алгебраически.
Занимаясь межпроцедурным анализом программ можно поступить так: пусть есть несколько процедур, вызывающих друг друга, тогда, выписывая выражение указанным выше образом для каждой, можно инструкцию вызова другой процедуры заменять именем этой процедуры, понимая его как имя переменной. В результате получается система алгебраических уравнений нескольких переменных. Важная информация о поведении программы может быть получена из решения этой системы. Характер информации зависит, конечно, от того, какой смысл вложен в операции полукольца. В частности, можно подсчитывать вероятности завершения программы или наименьшее количество выполнений фрагментов программы перед завершением. Более того, уравнения такого вида могут анализироваться в контексте задач, несвязанных с анализом программ: например, если рассматривать полукольцо языков, состоящих из слов над некоторым алфавитом, то система алгебраических уравнений задаёт контекстно-свободную грамматику, а её наименьшее решение является языком этой грамматики.
Первые методы решения систем алгебраических уравнений над данным полукольцом основывались на вариантах теоремы Клини о неподвижной точке для решёток: на полукольце вводится частичный порядок, связанный с полукольцевыми операциями, алгебраические функции автоматически являются непрерывными и монотонными, чего требует классическая теорема Клини. Метод Клини для нахождения наименьшей неподвижной точки отображения (который даёт теорема Клини) имеет ряд недостатков: он может не давать значения неподвижной точки (и так происходит в ряде важных случаев, например, при решении некоторых уравнений, содержащих операцию * — звезду Клини), он может сходиться к неподвижной точке очень медленно. Для решения этих проблем итерационный метод Ньютона был распространён на ω-непрерывные полукольца. Имеется две очевидных сложности на этом пути: отсутствия вычитания и деления. Деление используется в определении производной, однако производную полинома можно определить формально, используя фигурирующие в анализе формулы для производной произведения и суммы. Разность же (например, a-b) может быть заменена элементом (например, c) с соответствующим свойством(c+b=a) — доказывается, что такой элемент существует и, что, каким бы его ни выбрать, будет получено одно и то же приближение на очередной итерации метода Ньютона.
Кроме информации, полученной с решением системы, интерес могут представлять приближения, вычисляемые на каждой итерации. Например, для упомянутого выше полукольца языков i-ое приближение описывает подмножество слов языка данной грамматики индекса i (слово имеет индекс i, если существует вывод этого слова, такой что в каждой сентенциальной форме участвует не более, чем i нетерминалов); кроме того, приближения Клини и Ньютона можно охарактеризовать также с помощью свойств деревьев вывода для слов, содержащихся в них.
Ссылки
Принципы и приложения уточнённых типов (refinement types)
Эндрю Гордон (Andrew Gordon), Microsoft Research, Кэмбридж, Англия
Курс лекций состоял из трёх частей, в каждой из которых рассматривались технологии (языки программирования, моделирования и формальные языки), решающие задачи, связанные с безопасностью (в разных смыслах этого слова). Общий подход к решению задачи доказательства некоторых свойств системы таков: разработать достаточно богатую для выражения интересующего свойства систему типов и попытаться оттипизировать исследуемую систему. На этом пути важным инструментом являются уточнённые типы. Идея уточнённых типов проста: уточнённый тип это базовый тип плюс предикат для значения этого типа. Например, уточнённый тип чётных чисел это целые числа плюс предикат проверки на чётность. Использование этой идеи в промышленном программировании многие годы сдерживалось разными факторами: проверка предикатов была не достаточно эффективна, не всегда возможна и не всегда надёжна. Последние достижения в разработке формальных методов, появление эффективных инструментов класса SMT solvers и появление задач, в которых некоторые недостатки реализации уточнённых типов не играют решающей роли, изменили положение дел.
Первая часть знакомила с проектом «Oslo» от Microsoft. Oslo это набор технологий для моделирования жизненного цикла и характеристик корпоративных приложений, разрабатываемых с использованием разнообразных технологий Microsoft (.NET, ASP.NET, Visua Studio, XAML). Такое моделирование предусматривает высокоуровневое описание форматов данных, схем данных, окружений и источников данных. Это новая ступень эволюции таких известных средств как, например, конфигурационные файлы, управляющие сценарии, XML-дескрипторы развёртывания корпоративных приложений.
Составной частью проекта Oslo является язык M. Были продемонстрированы детали реализации уточнённых типов в этом языке и приведён пример описания некоторой политики безопасности для приложений (обычно описываемой в XML-файлах и диктующей, к примеру, использование криптоключей определённой длины, сертификатов и т. п.) с помощью системы типов M: в конечном счёте определяется тип «безопасная конфигурация», и конкретные конфигурации приложений могут быть пропущены через type checker и допущены или отвергнуты. Более подробное описание достоинств системы типов M содержится в ещё не опубликованной работе Bierman, Gordon, Langworthy.
Вторая часть курса посвящена описанию подхода к верификации криптопротоколов на основе верификации программного кода этих протоколов, выполненных на функциональном языке с поддержкой конкурентности (concurrency) в духе pi-исчисления — F#. В третьей части курса рассматривается новая формальная система RFC (Refined Concurrent FPC (Fixpoint Calculus); FPC — возможная формальная основа ML и Haskell, разработанная Плоткиным, 1985 и Гюнтером, 1992), которая должна служить теоретическим базисом для полноценной реализации идей, встретившихся во второй части. Кроме FPC, pi-calculus и уточнённых типов используются такие теоретические разработки как печати Морриса (см. ссылки), спецификации безопасности assume/assert (Флойд, Хоар, Дейкстра) и другие. Описывается разрабатывающийся в настоящее время язык F7, расширение F#, который должен стать реализацией RFC. С помощью богатых выразительных средств F7 можно описывать требования безопасности в виде интерфейсов, а затем проверять соответствие этим интерфейсам реализаций криптопротоколов на F# (такая проверка типов является частью F7).
Ссылки
- Аннотация лектора
- Слайды
- Refinement Types for Secure Implementations
- Morris, Protection in Programming Languages
Model Checking вычислений высших порядков
Люк Онг (Luke Ong), Оксфорд, Англия
Зарекомендовавшим себя формализмом для представления программ на функциональных языках программирования (использующих вычисления высших порядков) являются схемы рекурсии высших порядков: это синтаксический инструмент наподобие порождающих грамматик Хомского, описывающий (бесконечные) деревья (слова, описываемые грамматиками Хомского, являются, очевидно, частным случаем деревьев). Схемы рекурсии могут также рассматриваться как уравнения, записанные в термах, принадлежащих фрагменту просто типизированного λ-исчисления. Позволяя конечными средствами описывать бесконечный объект, схемы рекурсии являются актуальным понятием в приложениях к верификации ПО, а именно software model cheking (в отличие от уже достаточно разработанного hardware model cheking, работающего с системами с конечным числом состояний). В первой части курса устанавливается связь между схемами рекурсии и стековыми автоматами высших порядков (САВП). Последние были введены ещё А. Н. Масловым в 74 году и являются обобщением обычных стековых автоматов, у которых внутри стека хранятся другие стеки, внутри которых хранятся другие стеки и т. д., глубиной вложенности n для стекового автомата порядка n. Приводятся примеры описания одних и тех же языков с помощью схем рекурсии и САВП. Основной результат, существовавший до недавнего времени это равномощность САВП и сохранных (safe) схем рекурсии. Совсем недавно была доказана эквивалентность общих схем рекурсии и сворачивающихся (collapsible) САВП. Последние представляют собой САВП с возможностью в любой момент развернуть стек до определённого (заранее отмеченного) места. Тем не менее, являются ли ССАВП собственным подклассом САВП, остаётся открытым вопросом. Множество открытых вопросов остаётся также в отношении «иерархии Маслова» языков САВП (например, 0-языки это регулярные языки, 1-языки это контекстно-свободные языки, 2-языки это индексированные языки, предложенные Ахо в 68 году, строго более широкие, чем КС-языки — являются ли 3-языки в точности контекстно-зависимыми языками? можно ли предложить для языков САВП аналоги лемм о накачке?). При описании семантики и верификации ПО, использующего вычисления высших порядков удобно иметь в запасе оба рассмотренных формализма.
Далее в курсе формулируется задача Model Checking для вычислений высших порядков. Модели задаются деревьями, порождаемыми схемами рекурсии или играми. Для спецификации используются формулы монадических логик второго порядка (МВП-логик) (которые, как утверждается, наилучшим образом подходят для выражения интересных свойств встречающихся системы). Приводятся новые результаты о разрешимости МВП-теорий (и её сложности). Рассматривается метод решения задачи Model Checking, основанный на сведении её к задаче типизации исходной схемы рекурсии.
Ссылки
- Аннотация лектора
- Слайды к лекциям: часть 1, часть 2
- Ong et al. On model-checking trees generating by higher-order recursion schemes, 2006
- Ong et al. Collapsible Pushdown Automata and Recursion Schemes, 2008
- Hague, Ong. Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems, 2008
- Knapik et al. Deciding Monadic Theories of Hyperalgebraic Trees, 2001
- Knapik et al. Higher-Order Pushdown Trees Are Easy, 2002
- Knapik et al. Unsafe Grammars and Panic Automata, 2005
- Blum, Ong. The Safe Lambda Calculus, 2009, LMCS
- de Miranda. Structures Generated by Higher-Order Grammars and the Safety Constraint, 2006, PhD
- Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees, 1969
- Маслов. Многоуровневые магазинные автоматы, 1976
- Indermark. Schemes with recursion on higher types, 1976
- Damm, Goerdt. An automata-theoretic characterization of the OI-hierarchy, 1986
- Damm. Languages defined by higher type program schemes, 1977
- Damm. The IO- and OI-hierarchy, 1982
Трёхзначная абстракция и её приложения в Model Checking
Орна Грумберг (Orna Grumberg), TECHNION — Технический университет Израиля
Ссылки
- Аннотация лектора
- Compositional Verification and 3-Valued Abstractions Join Forces
- A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement
- Abstraction and Refinement in Model Checking
Механизированные семантики
Ксавье Леруа (Xavier Leroy), INRIA, Франция
Ссылки
- Аннотация лектора
- Слайды к лекции
- Раздаточный материал к лекции
- Grall, Leroy. Coinductive big-step operational semantics
- Nipkow. Winskel is (almost) Right_ Towards a Mechanized Semantics Textbook
- Bertot. Coq in a Hurry
Эффективный анализ стохастических процессов и игр с бесконечным числом состояний
Антонин Кучера (Antonin Kučera), Masaryk University, Чехия
Ссылки
Синтаксический контроль утечек и освобождения информации
Андрей Сабельфельд (Andrey Sabelfeld), Gothenburg University, Швеция
Ссылки
Использование политик конфиденциальности (security policies) для написания безопасного (secure) ПО
Эндрю Майерс (Andrew Myers), Cornell University, США
Ссылки
Два приложения систем доказательства теорем
Тобиас Нипков (Tobias Nipkow), Технический университет Мюнхена, Германия
Ссылки
Аудио некоторых лекций
Этот материал в силу своей разрозненности и неполноты не очень помогает в понимании, он выложен для того, чтобы можно было лучше представить как проходили лекции и обсуждения по итогам дня... Например, можно оценить скорость речи Гордона или понять, что Купферман единственная использовала доску и мел.
Купферман, Ягер, Сабельфельд+обсуждение, Эспарза, Кучера, Купферман, Онг+обсуждение, Нипков+обсуждение, Леруа, Гордон, Грумберг.
Примечания
- ↑ Не рекомендуется консультироваться со статьёй об исчислении высказываний в русской Википедии.