Теоретические проблемы программирования — различия между версиями

Рассмотривается задача обнаружения скомпрометированных коммутаторов в SDN сетях на основе анализа сетевой статистики.

Software-Defined Networking (SDN), по мнению ведущих производителей сетевого оборудования, является одним из самых перспективных направлений сетевой индустрии на данный момент. Архитектура SDN предполагает выделение специализированного устройства – контроллера – для передачи ему функций управления сетью, состоящей из коммутаторов. Коммутаторы представляют собой устройства, производящие обработку сетевого трафика по правилам маршрутизации, установленным на них контроллером.

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

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

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

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

Доклад по статье Petr Jancar, Faron Moller "Techniques for Decidability and Undecidability of Bisimilarity"

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

Слайды к докладу А.Р. Гнатенко

Доклад по статье R. Alur, D.L. Dill "A theory of timed automata" (Часть 3)

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

Доклад по статье R. Alur, D.L. Dill "A theory of timed automata" (Часть 2)

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

Доклад по статье R. Alur, D.L. Dill "A theory of timed automata" (Часть1)

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

We discuss the use of various temporal knowledge representation formalisms for ontology-mediated query answering over temporal data. In particular, we consider ontology and query languages based on the linear temporal logic LTL, the multi-dimensional Halpern-Shoham interval temporal logic HS, as well as the metric temporal logic MTL. Our main focus is on the data complexity of answering temporal ontology-mediated queries and their rewritability into standard first-order and datalog queries.

Professor of computer science Department of Computer Science and Information Systems Birkbeck, University of London

Доклад по статье Ashok K.Chandra "On the Decision Problems of Program Schemas with Commutative and Invertible Functions"

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

Доклад по статье H. Barringer, A. Goldberg, K. Havelund, K. Sen "Rule-Based Runtime Verification"

В статье описываются принципы работы программного средства, решающего следующую задачу. Имеется программа, работающая в режиме "чёрного ящика". В программе включен отладочный вывод: время от времени она предоставляет сообщения, содержащие информацию о значениях некоторых переменных. Требуется проверить, удовлетворяет ли текущая посланная последовательность сообщений заданным требованиям, в режиме он-лайн: выдавать результаты о выполнении требований по мере получения сообщений. Для решения этой задачи авторами предлагается особый логический формализм (Eagle): система правил, с одной стороны являющихся элементами синтаксиса формул, а с другой - описывающих способ перевычисления информации об истинности формул в режиме он-лайн. В предлагаемом формализме могут быть легко переформулированы требования, изначально записанные в ряде других известных логик, включая произвольные требования, выраженные формулами логики линейного прошлого времени (past-time LTL). Этот формализм и будет обсуждаться на семинаре.

Доклад по статье K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, Gerda Janssens "Verification of Source Code Transformations by Program Equivalence Checking"

Как правило, когда алгоритмы для обработки цифровых сигналов адаптируются для работы в энергоэффективных и эффективно функционирующих встроенных системах, применяется комбинация ручных и автоматических преобразований. Это порождает сложную задачу верификации. Задача верификации упрощается при конвертирования кода в DSA-форму (dynamic single assignment form). Данная статья описывает метод доказательства эквивалентности двух программ в DSA-форме, в которых индексация элементов массивов и условия завершения циклов являются (кусочно заданными) аффинными выражениями. Для таких программ может быть использовано геометрическое моделирование и сразу для наборов элементов может быть показано, что результат вычислений обеих программ представляет собой одну и ту же функцию от входных данных.

Доклад по статье Aleksandr Tvardovskii, Nina Yevtushenko "On minimization of Timed Finite State Machines"

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

Доклад по статье N.P. Lopes, J. Monteiro "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic"

Доказательство эквивалентности программ имеет несколько важных приложений, в таких отраслях, как алгоритмы распознавания, регрессионное тестирование, тестирование сделанных компилятором оптимизаций и проверка утечек потоков информации. Несмотря на то что данная тема обладает важными приложениями, наука в проверки программ на эквивалентность не достигла серьёзных успехов за последние десятилетие в виду сложности этой задачи. В рассматриваемой статье предложен первая полуразрешающая процедура для автоматической проверки частичной эквивалентности двух программ, использующих неинтерпретируемые функции и работающих над целочисленной арифметикой (UF + IA). Предлагаемый алгоритм применим, в частности, к программам с вложенными циклами. Вначале проводится преобразование неинтерпретируемых функций (UF) в целочисленные полиномы, которые позволяют точно суммировать циклы с вхождениями UF, использующих рекурсию. Затем алгоритм проверки на эквивалентность переходит к свободным от циклов программам, оперирующих только целыми числами.

Доклад по статье M.Christodorescu et al. "Semantics-aware malware detection"

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

Доклад по статье S. Baarir, A. Duret-Lutz “Mechanizing the Minimization of Deterministic Generalized Büchi Automata”

Рассматриваются методы получения и минимизации детерминированных автоматов Бюхи для разных классов свойств. Метод минимизации сводится к задаче выполнимости булевых формул. Представляются тесты, которые реализуют все эти методы.

Г. Темербекова

Продолжение доклада по статье A. Finkel, J. Leroux "Recent and Simple Algorithms For Petri Nets"

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

Доклад по статье A. Finkel, J. Leroux "Recent and Simple Algorithms For Petri Nets"

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

Доклад по статье J. Berstel, L. Boasson "Balanced Grammars and their Languages"

Balanced grammars are a generalization of parenthesis grammars in two directions. First, several kind of parentheses are allowed. Next, the set of right-hand sides of productions may be an infinite regular language. XML-grammars are a special kind of balanced grammars. It is shown that there exists a unique minimal balanced grammar equivalent to a given one.

Е. Докшина

Доклад по статье G.Klein, K.Elphinstone, G.Heiser et al. "seL4: Formal Verification of an OS Kernel"

Статья про опыт разработки микроядра операционной системы от формальной спецификации будущей программы до реализации на C с доказательством корректности спецификации.

Продолжение доклада по статье "The Byzantine Generals Problem", L. Lamport, R. Shostak, M. Pease. ACM Transactions on Programming Languages and Systems. 1982, 4 (3), p. 382–401.

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

В докладе будет рассмотрена задача проверки допустимости конфигураций модульных вычислительных систем реального времени (МВС РВ), возникающая при проектировании таких систем. Для решения данной задачи необходимо выполнять построение временных диаграмм функционирования МВС РВ, для чего требуется моделировать функционирование компонентов системы. В качества математического аппарата для описания моделей систем предлагается использовать сети временных автоматов с остановкой таймеров. В докладе будет представлена обобщенная формальная модель МВС РВ, метод построения на её основе моделей конкретных систем, а также подход к доказательству корректности и точности построенных моделей (детерминированность получаемых временных диаграмм, проверка выполнения требований точности и корректности из стандартов на МВС).

Реферат статьи "The Byzantine Generals Problem", L. Lamport, R. Shostak, M. Pease. ACM Transactions on Programming Languages and Systems. 1982, 4 (3), p. 382–401.

Reliable computer systems must handle malfunctioning components that give conflicting information to different parts of the system. This situation can be expressed abstractly in terms of a group of generals of the Byzantine army camped with their troops around an enemy city. Communicating only by messenger, the generals must agree upon a common battle plan. However, one or more of them may be traitors who will try to confuse the others. The problem is to find an algorithm to ensure that the loyal generals will reach agreement. It is shown that, using only oral messages, this problem is solvable if and only if more than two-thirds of the generals are loyal; so a single traitor can confound two loyal generals. With unforgeable written messages, the problem is solvable for any number of generals and possible traitors. Applications of the solutions to reliable computer systems are then discussed.

Одним из декларируемых преимуществ функциональных языков программирования является простота преобразований, а также формулирования и доказательства свойств программ, что достигается главным образом за счет отсутствия побочных эффектов. Например, если мы знаем, что ∀x (f(x)=g(x)), то мы всегда можем заменить f(x) на g(x) (или их частные случаи) и наоборот в любом месте программы. Равенства такого вида имеют разные применения, такие, как верификация, преобразование программ и использование в качестве лемм для доказательства других подобных свойств. Во всех случаях желательно удостовериться в том, что равенство действительно выполняется. Доказательство таких эквивалентностей часто требуется проводить по индукции и коиндукции (для бесконечных структур данных).

Насыщения равенствами (equality saturation) -- метод преобразования программ, заключающийся в применении преобразований к структуре данных, представляющей множество равенств над выражениями, и за счет этого способной хранить не одну программу, а целое множество семантически эквивалентных программ. Сам термин "насыщение равенствами" был введен в работе "Equality Saturation: A New Approach to Optimization" Тейта и др., где этот метод использовался для преобразования императивных программ. В насыщении равенствами каждое преобразование применяется недеструктивно и выводит новые равенства из уже существующих, расширяя таким образом множество представляемых программ. При этом потребление памяти значительно уменьшается за счет совмещения общих подвыражений. Насыщение равенствами можно применять для оптимизации -- при этом в конце из множества программ требуется выделить наилучшую. Насыщение равенствами можно также применять и для доказательства эквивалентности функций -- для этого определения функций преобразуются совместно до тех пор, пока не будет выведено равенство этих функций.

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

Рассматриваются задачи верификация одного класса систем взаимодействующих процессов с конечным числом состояний, которые обмениваются данными с помощью неограниченных ненадежных FIFO каналов с возможностью потери сообщений. Показано, что для этого класса распределенных систем разрешимы некоторые задачи верификации, а именно проблемы достижимости, проблема безопасности относительно регулярных множеств трасс и проблемы живости относительно множеств состояний управления. При этом следует заметить (и это очень удивительно!), что 1) все перечисленные задачи алгоритмически неразрешимы в том случае, если для каналы абсолютно надежны и 2) сложность указанных задач неэлементарна.

Рассказ о жизни и научных достижениях Риммы Ивановны Подловченко [1931-2016].

Римма Ивановна в 1953 г. окончила с отличием механико-математический факультет Московского Университета. В 1957-92 гг. она преподавала в Ереванском государственном университете, заведовала кафедрой вычислительной математики и кибернетики, кафедрой алгоритмических языков.

В Московском университете работала с 1993 г. в должности ведущего научного сотрудника НИВЦ и в должности профессора на кафедре математической кибернетики факультета ВМиК.

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

В Московском университете она читала основные курсы лекций «Эквивалентные преобразования в моделях вычислений», «Избранные вопросы математической теории вычислений», а также специальные курсы лекций «Теория моделей программ», «Схемы программ и автоматы», «Математические основы функционального программирования». Она также руководила работой постоянного спецсеминара «Теоретические проблемы программирования».

Формальные грамматики появились в конце 50-х гг. XX века, когда развитие вычислительной техники потребовало строго определить синтаксис языков программирования, а также подало надежду на машинную обработку естественных языков. К октябрю 1962 г. были в первом приближении разработаны основные понятия новой теории и получены некоторые результаты: системы перезаписи строк и иерархия Хомского, форма Бэкуса-Наура, синтаксический разбор с помощью рекурсивного спуска, лемма накачки и несколько неразрешимых задач. Эти ранние исследования определили первоначальное представление о формальных грамматиках, которое продолжает воспроизводиться и в современных учебниках по информатике.

Исследования в области грамматик продолжались, однако, и после Карибского кризиса, и за прошедшие полвека представление о том, что такое формальная грамматика, несколько изменилось. Ошибочные понятия (такие как контекстно-зависимые грамматики Хомского и многочисленные производные модели) постепенно сошли на нет, и с их уходом устарели и породившие их принципы классификации. Новые виды грамматик принесли с собой представление о формальных грамматиках как о специализированной логике для описания синтаксиса; важную роль в этом сыграла работа Раундса (1988), описавшего различные виды грамматик как фрагменты логики первого порядка над позициями в строке. Цель данного доклада --- рассказать, как изменилось понятие о формальных грамматиках за полвека, какие виды грамматик известны сегодня, как они соотносятся друг с другом, и что с ними можно попытаться делать дальше.

It is widely believed that Fully Homomorphic Encryption (FHE) only is sufficient to provide the security of cloud computations. However, Marten van Dijk and Ari Juels in a recent paper showed that in some cases cryptography alone can’t enforce the privacy demanded by common cloud computing services, even with such powerful tools as FHE. Can we bypass this impossibility result? What extra requirements should be imposed a model of cloud computations to guarantee the privacy? These and other questions concerning the security issues of cloud computing will be discussed.

Изучается преемственность методов распознавания эквивалентности для конечных автоматов и схем программ в алгебраических моделях программ.

We present some results by Goldreich and Krawczyk from the work with the same title (Proc. of ICALP'90 and SIAM J. on Computing, 1996, v.25, no. 1). By these results, zero-knowledge is not preserved under composition of protocols.

We study programs with the fixed set of variables and relationships between the complexity class containing all languages recognizable by such programs, and the complexity classes DLOGSPACE and NLOGSPACE.

Transducers over semigroups extend the concept of string transducers and may be used as a formal model of sequential reactive programs. We introduce a uniform techniques for building efficient procedures for checking functionality, $k$-valuedness, equivalence and inclusion for finite state transducers over semigroups. The obtained procedures are capable to decide equivalence for deterministic transducers in polynomial time, and check $k$-valuedness and decide equivalence in single exponential time for bounded valued transducers over semigroups that can be embedded into decidable groups.

Designing of network update algorithms is urgent for development of SDN control software. A particular case of Network Update Problem is that of adding a set of forwarding rules into flow-tables of SDN switches (say, to install new paths in the network) or restoring seamlessly a given network configuration after some packet forwarding rules have been disabled (say, at the expiry of their time-outs). Some algorithms provide solutions to these problems but only with the help of tagging techniques. But is it possible to perform a consistent network update without tagging? We study this problem in the framework of a formal model of SDN, develop correct and safe network updating algorithms, and show that in some cases it is impossible to update consistently network configurations without resorting either to tagging or to priorities of packet forwarding rules.

Counter abstraction is a powerful tool for parameterized model checking, if the number of local states of the concurrent processes is relatively small. In recent work, we introduced parametric interval counter abstraction that allowed us to verify the safety and liveness of threshold-based fault-tolerant distributed algorithms (FTDA). Due to state space explosion, applying this technique to distributed algorithms with hundreds of local states is challenging for state-of-the-art model checkers.

In this talk, we demonstrate that reachability properties of FTDAs can be verified by bounded model checking. To ensure completeness, we need an upper bound on the diameter, i.e., on the longest distance between states. We show that the diameters of accelerated counter systems of FTDAs, and of their counter abstractions, have a quadratic upper bound in the number of local transitions. Our experiments show that the resulting bounds are sufficiently small to use bounded model checking for parameterized verification of reachability properties of several FTDAs, some of which have not been automatically verified before. This part is based on the paper presented at CONCUR'14.

Further, we demonstrate how the proof ideas from CONCUR'14 can be re-used to implement a bounded model checker for accelerated counter systems without applying counter abstraction. The model checker constructs a finite (and typically small) set of representative accelerated schedules that together visit all reachable configurations. Finally, each representative schedule is checked for feasibility within an SMT solver. Our preliminary experiments show that this new technique over-performs counter abstraction on our case studies by three orders of magnitude.

В докладе будут представлены новые методы построения полиномиальных по времени алгоритмов проверки эквивалентности последовательных и рекурсивных программ в моделях программ с полугрупповой семантикой.

We suggest a candidate one-way function using combinatorial constructs such as expander graphs. These graphs are used to determine a sequence of small overlapping subsets of input bits, to which a hard-wired random predicate is applied. Thus, the function is extremely easy to evaluate: all that is needed is to take multiple projections of the input bits, and to use these as entries to a look-up table. It is feasible for the adversary to scan the look-up table, but we believe it would be infeasible to find an input that fits a given sequence of values obtained for these overlapping projections.

The conjectured difficulty of inverting the suggested function does not seem to follow from any well-known assumption. Instead, we propose the study of the complexity of inverting this function as an interesting open problem, with the hope that further research will provide evidence to our belief that the inversion task is intractable.

В рамках работы, результаты которой представлены в докладе, предлагается подход к верификации сложных, наукоемких программных комплексов. Его суть в том, чтобы описывать их покомпонентно с помощью языков, адекватно отражающих специфику предметной области (предметно-ориентированных языков), которые при этом имеют заданную формальную семантику. Для построения таких языков и их формальной семантики разработано промежуточное представление на основе λ-исчисления с зависимыми типами. Результаты тестовых испытаний демонстрируют программную реализуемость предлагаемого подхода и возможности его применения для описания фрагментов реально существующего и используемого на практике программного комплекса.

What is a homomorphic encryption? What is it good for? Is it sufficient to make cloud computing secure? These questions are the most accute topics in modern cryptography, and they will be discussed in this talk.

Ontology-based data access (OBDA) is regarded as a key ingredient for the new generation of information systems. In the OBDA paradigm, an ontology defines a high-level global schema of (already existing) data sources and provides a vocabulary for user queries. An OBDA system rewrites such queries and ontologies into the vocabulary of the data sources and then delegates the actual query evaluation to a suitable query answering system such as a relational database management system or a datalog engine.

This lecture will mainly focus on OBDA with the ontology language OWL 2 QL, one of three profiles of the W3C standard Web Ontology Language OWL 2, and relational databases, although other possible languages will also be discussed. It will cover the following topics:

- types of conjunctive query rewriting; their existence and succinctness;

- different architectures of OBDA systems;

- practical OBDA with open source system Ontop (http://ontop.inf.unibz.it)

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