Летняя школа в г. Марктобердорф 2009 — различия между версиями

Текущая версия на 11:27, 15 июля 2015

Анализ и верификация программ с помощью абстрактной интерпретации

Патрик Кюзо (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 нетерминалов); кроме того, приближения Клини и Ньютона можно охарактеризовать также с помощью свойств деревьев вывода для слов, содержащихся в них.

Ссылки

• Аннотация лектора
• Newtonian Program Analysis
• Kuich. Semirings and Formal Power Series

Принципы и приложения уточнённых типов (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, Чехия

Ссылки

• Аннотация лектора
• Kucera et al. Qualitative Reachability in Stochastic BPA Games

Синтаксический контроль утечек и освобождения информации

Андрей Сабельфельд (Andrey Sabelfeld), Gothenburg University, Швеция

Ссылки

• Аннотация лектора

Использование политик конфиденциальности (security policies) для написания безопасного (secure) ПО

Эндрю Майерс (Andrew Myers), Cornell University, США

Ссылки

• Аннотация лектора

Два приложения систем доказательства теорем

Тобиас Нипков (Tobias Nipkow), Технический университет Мюнхена, Германия

Ссылки

• Аннотация лектора
• Verifying a Hotel Key Card System
• Social choice theory in HOL

Аудио некоторых лекций

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

Купферман, Ягер, Сабельфельд+обсуждение, Эспарза, Кучера, Купферман, Онг+обсуждение, Нипков+обсуждение, Леруа, Гордон, Грумберг.

Примечания

1. ↑ Не рекомендуется консультироваться со статьёй об исчислении высказываний в русской Википедии.