Aggregates are used to compute single pieces of information from separate data items, such as records in a database or answers to a query to a logic program. The maximum and minimum are well-known examples of aggregates. The computation of aggregates in Prolog or variant-based tabling can loop even if the aggregate at hand can be finitely determined. When answer subsumption or mode-directed tabling is used, termination improves, but the behavior observed in existing proposals is not consistent. We present a framework to incrementally compute aggregates for elements in a lattice. We use the entailment and join relations of the lattice to define (and compute) aggregates and decide whether some atom is compatible with (entails) the aggregate. The semantics of the aggregates defined in this way is consistent with the LFP semantics of tabling with constraints. Our implementation is based on the TCLP framework available in Ciao Prolog, and improves its termination properties w.r.t. similar approaches. Defining aggregates that do not fit into the lattice structure is possible, but some properties guaranteed by the lattice may not hold. However, the flexibility provided by this possibility justifies its inclusion. We validate our design with several examples and we evaluate their performance.

Some of the recent blockchain proposals, such as Stellar and Ripple, use quorum-like structures typical for Byzantine consensus while allowing for open membership. This is achieved by constructing quorums in a decentralised way: each participant independently chooses whom to trust, and quorums arise from these individual decisions. Unfortunately, the theoretical foundations underlying such blockchains have not been thoroughly investigated. To close this gap, in this work we study decentralised quorum construction by means of federated Byzantine quorum systems, used by Stellar. We rigorously prove the correctness of basic broadcast abstractions over federated quorum systems and establish their relationship to the classical Byzantine quorum systems. In particular, we prove correctness in the realistic setting where Byzantine nodes may lie about their trust choices. We show that this setting leads to a novel variant of Byzantine quorum systems where different nodes may have different understanding of what constitutes a quorum.

Modern cryptography is a pessimistic discipline, in at least two ways: pessimistic in its fundamental belief ("There are problems you cannot solve"); pessimistic in its imperative ("Act as if the worst possible thing that can happen will happen"). These two attitudes may be somewhat uncomfortable, but they are clearly useful if they work in building strong security. And indeed they do work and indeed they are useful. Despite their usefulness, though, these two "mantras" have limitations. Take the first one, the "epistemological" pessimism. Given what we know today about complexity theory, there is no (mathematical) proof of its accuracy: all we can do is to assume that that is the case. This implies assuming not only that P != NP but quite some more. How would the world be different if this assumption turned out to be false? And for the second type of pessimism, the "ethical" one: how should we apply it according to the situation? For example, what is the "worst that can happen" in a quantum world (as opposed to one with classical computers)? Finally, can there ever be space for optimism? That is, are there situations where we can reasonably assume that the "worst" is not going to be that bad after all? In my talk I would try and give a broad overview of this topic, to partly (and subjectively) answer the questions above and argue that the two cryptographic "pessimisms" are actually intertwined.

In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources, i.e., state transition systems, to describe the invariants on the state and their allowed atomic changes. One of this logical frameworks is FCSL, developed by Aleksandar Nanevski et al. As usual, once we have a mathematical structure, it is only natural to study the functions that preserve them. This motivates the interest of defining and studying a morphism between resources. In this talk we will give an introduction to the main concepts of FCSL and the notion of resource morphism. We will also show how to apply morphisms to facilitate proof reuse between resources.

Mixing Networks are protocols that allow a set of senders to send messages anonymously. Such protocols are fundamental building blocks to achieve privacy in a variety of applications, such as anonymous e-mail, anonymous payments, and electronic voting. Back in 2002, Golle et al. proposed a new concept of mixing network, called optimistic mixing, that allows for fast mixing when all the parties execute the protocol honestly. If, on the other hand, one or more mix-servers cheat, then the attack is recognized and one can back up to a different, slow mix-net. Unfortunately, Abe and Imai (ACISP’03) and independently Wikström (SAC’03) showed several major flaws in the optimistic protocol of Golle et al. In this talk we give another look at optimistic mixing networks. I will introduce the concept of secure optimistic mixing and show a simple construction based on a new re-randomizable encryption scheme.

Almost every programming language possess some kind of type system. These systems ensures some safety over the code execution, be it statically at compile-time or dynamically at run-time. Effectively, these types encode a specification of an object, allowing them to be composed in a relatively safe manner. Most type systems only allow for weak specifications, for instance there is no way to say that a list is sorted in its type. This is something you can do with dependent types, which was first introduced by Per Martin-Löf in 1972. This, together with the relationship between programs and proofs knows as the Curry-Howard correspondence, allows us to treat programs written in these type systems as proofs. In this talk I will explain the correspondence between propositional logic and simply typed lambda calculus, and show how this extends to dependent types. I will also explain what a dependent type is and show examples of these types in Agda and Coq, which are both proof assistants and programming languages.

Today's workloads in the datacenter suffer from stagnating CPU performance and increasing data volumes. One promising solution to breaking traditional trade-offs and scaling further comes in the form of specialization, that is, moving parts of an application to a more efficient hardware implementation. Field programmable gate arrays (FPGAs) are one example of re-programmable hardware that can be used as a specialized accelerator for a wide range of applications. Since they are being widely deployed in datacenters (e.g., at Microsoft) and in the cloud (e.g., Amazon EC2 and Huawei Cloud), building heterogeneous systems and incorporating acceleration functionality in software systems is expected to become common. However, since these devices operate differently from traditional CPUs, a shift is required in the ways we express algorithms and write code for them. In this talk I will provide an overview of FPGA internals, programming flow and capabilities, through the example of a Regular Expression matching accelerator. This example will also give an intuition on how FPGA-based execution breaks trade-offs inherent to software running on CPUs.

The Transport Layer Security (TLS) protocol is the de-facto standard for encrypted communication on the Internet. However, it has been plagued by a number of different attacks and security issues over the last years. Addressing these attacks requires changes to the protocol, to server- or client-software, or to all of them. In this paper we conduct the first large-scale longitudinal study examining the evolution of the TLS ecosystem over the last six years. We place a special focus on the ecosystem's evolution in response to high-profile attacks. For our analysis, we use a passive measurement dataset with more than 319.3B connections since February 2012, and an active dataset that contains TLS and SSL scans of the entire IPv4 address space since August 2015. To identify the evolution of specific clients we also create the-to our knowledge-largest TLS client fingerprint database to date, consisting of 1,684 fingerprints. We observe that the ecosystem has shifted significantly since 2012, with major changes in which cipher suites and TLS extensions are offered by clients and accepted by servers having taken place. Where possible, we correlate these with the timing of specific attacks on TLS. At the same time, our results show that while clients, especially browsers, are quick to adopt new algorithms, they are also slow to drop support for older ones. We also encounter significant amounts of client software that probably unwittingly offer unsafe ciphers. We discuss these findings in the context of long tail effects in the TLS ecosystem.

Symmetric key cryptography is an essential part of communication systems, where a secret key is used to protect data confidentiality. Surprisingly, the only way of trusting these ciphers is to perform continuous analysis that update the security margin. With the advent of quantum computers in an arguably near future, the security of nowadays ciphers has been put into question. While most currently used asymmetric primitives would be completely broken, doubling the key size of symmetric constructions provides the same level of security with respect to exhaustive key search. However, we still have a long way to go in the field of quantum cryptography and further cryptanalysis must be carried out to reassure the validity of these emerging ciphers. We have studied the Salsa20 family of ciphers, which has received very little cryptanalysis ever since the most relevant result one decade ago despite the inclusion of this cipher suit in TLS 1.3. During this talk, I will explain a new attack to 8 rounds of Salsa using conditional differential cryptanalysis, which comprises the main result of my Master internship. This work has taken place at Inria Paris in the context of the ERC project QUASYModo under the supervision of the researcher María Naya Plasencia.