Slides of the talk. [pdf]
Abstract: What is the shortest proof of a given statement? Are there Boolean tautologies that require exponential-size proofs? These are typical questions in propositional proof complexity.
In my short tutorial I will speak on two aspects of this topic. The first one concerns specific proof systems and lower bounds on the proof length there. The second one concerns structural questions: is there the "best" proof system?
Abstract: Language Engineering is an interdisciplinary area addressing many problems related to computer languages. Parsing and translation are the most widely known ones, but there are many more: typing and other static analyses, creating IDEs, which includes syntax highlighting, building outlines, code navigation, completion and refactoring, and many more. Many of such problems are solved in a generative fashion: we write high-level specifications (like grammars with embedded semantic actions for parsing) and generate code from them.
Now if we come up with a language (which is an everyday practice if you consider DSLs) we have to specify many things for it. The problem is that specification languages are built upon a grammar of the language in question (e.g. for parsing we embed semantic actions into grammar rules, other languages work the same way) and if we specify many solutions separately, we have to duplicate the grammar. The alternative approach is to attach all the specifications to the same grammar which leads to huge tangled specifications.
We propose a solution for this problem based on usage of a pointcut-advice language inspired by AspectJ to attach specifications to a grammar without mixing them together. This language was successfully applied to specify attributed translation, IDE features and grammar transformations.
Slides of the talk. [pdf]
Abstract: The Cantor (product) topology, which is the default setting for cellular automata (CA) dynamics, has the disadvantage of making the shift a chaotic map. Consequently, no translation-invariant distance can induce the product topology.
To overcome this, Formenti et al. introduced in 1999 the Besicovitch and Weyl pseudo-distances on bi-infinite words. By identifying configurations at pseudo-distance zero, new topological spaces are obtained, whose properties are dramatically different from those of the Cantor space. Remarkably, 1D CA induce are well-defined over equivalence classes, and several properties of the induced functions on these new spaces are linked to those of the original CA.
In this talk, we illustrate the original formulation and the main results on 1D CA. We then switch to a generalization to higher dimension, and show how several of those results still hold. We will focus in particular on surjectivity, both of CA and of induced maps.
Slides of the talk. [pdf]
Abstract: Monads and the intimately related concept of adjunctions are perhaps the central topic in category theory. Mathematics and computer science are littered with examples of them. Motivated by some persuasive examples that are nearly monads but not quite, we generalise the theory of monads and adjunctions to allow monads which are not endofunctors. In this talk, I will describe the basic setup and some examples. (Joint work with Thorsten Altenkirch and Tarmo Uustalu.)
Slides of the talk. [pdf]
Abstract: In set system auctions, a single auctioneer needs to purchase services from multiple competing selfish providers (agents), and the set of providers has a combinatorial structure; a popular example is provided by shortest path auctions. Each agent i can perform a simple task at some cost ci known only to himself. Based on the agents' bids bi, the auctioneer must select a feasible set --- a set of agents whose combined skills are sufficient to perform the complex task --- and pay each selected agent individually some amount pi.
A truthful mechanism for winners selection and payments to them is a mechanism, which forces each agent i to say ci for his bid bi. The frugality ratio of a mechanism, introduced by Karlin, Kempe, Tamir et al. at FOCS 2005, measures the amount by which a mechanism "overpays".
Slides of the talk. [pdf]
Abstract: We study the problem of generating a database and parameters for a given parameterized SQL query satisfying a given test condition. We introduce a formal background theory that includes arithmetic, tuples, and sets, and translate the generation problem into a satisfiability or model generation problem modulo the background theory. We use the satisfiability modulo theories (SMT) solver Z3 in the concrete implementation. We describe an application of model generation in the context of the database unit testing framework of Visual Studio. (Joint work with Margus Veanes, Peli de Halleux, Nikolai Tillmann.)
Slides of the talk. [pdf]
Abstract: We will give a short introduction to circuit complexity lower bounds -- one of the oldest and most difficult branches of Theoretical Computer Science. We will first survey some known lower bounds for various circuit models. Then we will concentrate on the so-called gate elimination method. This is essentially the only known method for proving lower bounds for unrestricted circuits.
Slides of the talk. [pdf]
Abstract: Reiter and Rubin's Crowds (TISSEC 1998) is a system for communicating anonymously, using a peer-to-peer network (a crowd) to pass messages. A related scheme, ADU, presented by Munoz Gea et al. at ESORICS 2008, was claimed to improve on Crowds by achieving lower message path length variance for the same mean latency, without a compromise in security.
We present traffic analysis of the ADU anonymity scheme and show that optimal attacks are able to de-anonymize ADU messages more effectively than in the case of Crowds. We then generalize Crowds to support any path length distribution, while leaking the least possible information, and quantify the optimal attacks. This allows us to prove that the original Crowds anonymity system provides the best security for any given mean messaging latency and hence, the search of a "better" scheme is bound to fail. (Joint work with George Danezis, Claudia Diaz and Carmela Troncoso.)
Slides of the talk. [pdf]
Abstract: In this talk, we report the results of the formal analysis performed on the Estonian Mobile-ID protocol (deployed since 2008), allowing citizens and permanent residents of Estonia to authenticate themselves and issue digital signatures with the help of a signature-capable SIM-card inside their mobile phone. We analyze the resiliency of the protocol to network attacks under various threat models (compromised infrastructure, client application, etc., confusing user interface) and give suggestions for improvement. (Joint work with Meelis Roos.)
Slides of the talk. [pdf]
Abstract: First, we show how to express an arbitrary integer interval $I = [0, H]$ as a sumset $I = \sum_{i=1}^\ell G_i * [0, u - 1] + [0, H']$ of smaller integer intervals for some small values $\ell$, $u$, and $H' < u - 1$, where $b * A = \{b a : a \in A\}$ and $A + B = \{a + b : a \in A \land b \in B\}$. We show how to derive such expression of $I$ as a sumset for any value of $1 < u < H$, and in particular, how the coefficients $G_i$ can be found by using a non-trivial but efficient algorithm. This result may be interesting by itself in the context of additive combinatorics.
Second, a range proof is a $\Sigma$-protocol that allows a prover to convince a verifier that a digitally committed value lies in a specified integer interval $I$. Given the sumset-representation of $I$, we show how to decrease the communication complexity of the recent range proof of Camenisch, Chaabouni and Shelat from ASIACRYPT 2008 by the factor of $2$. (Joint work with Rafik Chaabouni, Abhi Shelat).
Slides of the talk. [pdf]
Abstract: In cryptography, one-way functions and trapdoor functions are the basic primitives for constructing private-key and public-key cryptosystems, respectively. Unfortunately, it is not yet proved that there exists a one-way (or trapdoor) function (not breakable by any polynomial-time adversary).
However, it is possible to prove the existence of "feebly" secure one-way and trapdoor functions where adversary is guaranteed to spend more time (in terms of circuit complexity) than the honest parties by a constant factor (Hiltgen, ASIACRYPT '92; Hirsch and Nikolenko, CSR 2009). In this talk I review old and present new improved constructions of feebly secure cryptographic primitives both in the worst-case and in the average-case setting.
Slides of the talk. [pdf]
Abstract: In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously designed a trace-based coinductive big-step semantics for While, accounting for both terminating and nonterminating program runs. In this talk I present a Hoare logic counterpart of our coinductive trace-based semantics, which is proved sound and complete. Our logic generalizes both the partial correctness Hoare logic and the total correctness Hoare logic: derivations in these logics can be meaningfully transformed into derivations in our logic. However expressivity of our logic goes beyond that of the partial and the total correctness Hoare logics. I demonstrate this point by a search algorithm example, inspired by Markov's principle. Our logic can constructively prove the algorithm is not nonterminating. (Joint work with Tarmo Uustalu.)
Slides of the talk. [pdf]
Abstract: Attack trees are a method of analyzing security threats by decomposing them into sub-threats. We consider a two-parameter financial threat model where an adversary can perform the sub-attacks one after the other, always knowing what happened on the previous sub-attacks. It turns out that under some restrictions on the order of attacks this model can in fact be computed in linear time and that even after many sensible generalizations the model still remains polynomial-time computable. This presents a substantial step forward in the state of the art as the best previously known model required exponential time. (Joint work with Aivo Jürgenson and Jan Willemson.)
Slides of the talk. [pdf]
Abstract: We consider the Boolean circuit satisfiability problem in full binary basis (CIRCUIT SAT).
Similarly to the SAT problem, no approaches are known for proving upper bounds in form of cn (c < 2 is a constant) for the general case of CIRCUIT SAT. But if the size of the circuit is relatively small compared to the number of variables, then one may be interested in upper bounds in form of cm, where m is the size of the circuit.
We introduce a recursive algorithm, that runs in time O(20.4058m).
The algorithm has very much in common with typical splitting algorithms for SAT and also uses the xor-chains technique earlier applied to prove lower bounds on the circuit complexity of certain Boolean functions.
Slides of the talk. [pdf]
Abstract: In multi-party computation (MPC) the task is to compute a function, or, more generally, evaluate a reactive functionality, among a number of parties, each giving input or receiving output. An MPC is secure if it computes the correct result (correctness), no party learns anything but the result (privacy), and it terminates (robustness), even if parties are corrupted and maliciously deviate from their prescribed program or protocol.
We present approaches to tolerating a majority of corrupted participants in secure MPC. As shown by Cleve (STOC '86) fully secure general MPC is not attainable if more than half of the participants are corrupted. However, this result does not preclude every function from being computable with full security, nor does it preclude functions from being computable with weaker security. Thus, we explore which classes of functions are actually computable with full information-theoretic (IT) security, while tolerating arbitrarily many corrupted parties. Furthermore, we examine weaker notions than full IT security. For instance, we discuss long-term security without robustness, where we admit computational assumptions for the duration of a computation, but require IT privacy once the computation is concluded.
Abstract: Several parties care about scientific publishing: researchers, publishers and funders. But their motives are wildly different. Over the last 15 years or so, scientific publishing and the world around it have rapidly undergone some very significant changes and these have amplified the intrinsic conflict to a state of unprecedented controversy. I will review some of the issues and would then like to hear a hot debate on matters like meaningfulness of citation indexes and bibliometrics, who protects who from what in rights protection, what has caused the mushrooming of fake publication venues, who should pay for the costs of publishing, and the ethics of the enterprise.
Slides of the talk. [pdf]
Abstract: Everybody loves Race Detection! I will discuss the techniques we have devised to detect races in operating system code, placing this work in the wider context of race detection techniques for dynamically allocated memory. Our methods are based on various pointer analyses which we have used successfully in isolation, but our ultimate goal is to exploit the synergy among these analyses and integrate them all into a coherent race detection tool, the Goblint 1.0! (Joint work with Kalmer Apinis, Helmut Seidl, and Varmo Vene.)
Slides of the talk. [pdf]
Abstract: This talk covers the first linear hull and a revisit of the algebraic cryptanalysis of reduced-round variants of the block cipher PRESENT, under known-plaintext and ciphertext-only settings. We introduce a pure algebraic cryptanalysis of 5-round PRESENT and in one of our attacks we recover half of the bits of the key in less than three minutes using an ordinary desktop PC. PRESENT is a design by Bogdanov et al. presented in CHES 2007 and aimed at RFID tags and sensor networks. Our linear attacks reach up to 26-round PRESENT and improve on previously reported attacks in terms time, data or memory complexities. Additionally, this talk includes linear hulls computed in practice for the original PRESENT cipher, which corroborated and even improved on the predicted bias (and the corresponding attack complexities) of conventional linear relations based on a single linear trail. (Joint work with Jorge Nakahara Jr., Pouyan Sepehrdad, Meiqin Wang.)