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

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

Реферат статьи "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)

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