Ettekande slaidid. [ppt]
Abstract: We address the problem of constructing mechanisms for popular voting that are computationally hard to manipulate. A recent paper by Conitzer and Sandholm shows that one can make many well-known mechanisms resistant to manipulation by prepending them with a pre-round of a certain form. Variants of these technique result in mechanisms that are NP-hard, #P-hard, or PSPACE-hard. We extend this result in several directions.
First, we show that using this approach, one can make manipulation as hard as inverting one-way functions. This hardness criterion is standard in cryptography, and is an important step in achieving average-case hardness.
Second, we introduce a general technique for obtaining a new mechanism by combining two or more base mechanisms, and study the resulting class of hybrid voting mechanisms. We show that the mechanisms of Conitzer and Sandholm can be viewed as a special case of our construction. Moreover, many other mechanisms in this class are also hard to manipulate, and some of them have a combination of desirable properties not shared by previously known manipulation-resistant mechanisms.
Finally, we discuss the limitations of pre-round based mechanisms and show that they cannot be used to achieve some natural average-case hardness goals. (Joint work with Helger Lipmaa.)
Ettekande slaidid. [pdf]
Abstract: Recently, there has been significant research activity in the algorithmic analysis of complex networks, such as social networks, or information networks. A problem of great practical importance is that of network immunization against virus spread. Given a network, a virus-propagation model, and an immunization cost function, we are interested in containing the spread of the virus while minimizing the immunization cost. We will discuss two virus propagation models and immunization various algorithms for each model. We also discuss experimental results on both synthetic and real graphs. Our experiments show the following interesting facts (a) the simple heuristic of immunizing the nodes with the highest degree is not optimal, and (b) our algorithms perform significantly better in small-world networks.
Abstract:We will focus on the crucial practical question of writing software for integrating different databases: on the web and off the web. We'll attempt to show why this task is still very hard and has not been getting easier. There exist several semantics-based ideas and approaches for simplifying the task, but none of these has been successful so far. We'll give a brief overview of the the main ideas and their shortcomings. Finally we'll present several new ideas and techniques, all with their own shortcomings, but worth trying out nevertheless.
Ettekande slaidid. [ppt]
Abstract: Event logging is a widely accepted practice in modern IT systems, and event logs are an excellent source of information for monitoring the IT system in real time and for conducting retrospective event analysis. Event correlation is one of the most prominent on-line (real time) event processing techniques today, and in this talk we will discuss the concept of event correlation, existing approaches and solutions, and the Simple Event Correlator (SEC) tool developed by the auhor for event log monitoring. We will also discuss data mining techniques for off-line analysis of event logs, with the focus being on data clustering and frequent itemset mining algorithms.
Ettekande slaidid. [pdf]
Abstract: Histomorphisms are a categorical construction that capture the course-of-value iteration pattern. We investigate how histomorphisms can be used for implementing several dynamic programming algorithms and expose some properties of the translation of non-dynamic implementations to dynamic ones.
Abstract: Structural Synthesis of Programs (SSP) is a method of program synthesis where new software is composed from existing modules. Modules are extended with specifications describing their interface variables and their propositional interdependencies. This means an interface describes which variables can be computed out of which variables under which conditions. The actual values are not considered during the synthesis. This approach of program synthesis is often used during the runtime and has to be fast.
During the presentation we are going to study some of the algorithms of SSP and try to evaluate their efficiency, soundness and completeness.
Ettekande slaidid. [pdf]
Abstract: A5/1 is the most common encryption algorithm used in GSM networks with over 1 billion potential users. The subject of this talk is the cryptanalysis of A5/1 with special focus on attacks that could benefit from hardware assistance. First, we introduce the cipher, explain the attack algorithms and estimate their computational complexity. Later, we turn our attention to implementations. Special-purpose hardware has proved useful for example in cracking the DES block cipher. We explore whether a similar approach could speed up the cryptanalysis of the A5/1 stream cipher, and compare existing software and hardware implementations.
Ettekande slaidid. [ps.gz]
Abstract: We present a type system for checking secrecy of messages handled by protocols that use the Backes-Pfitzmann-Waidner library for cryptographic operations. A secure realization of this library exists, therefore we obtain for the first time a cryptographically sound analysis for a full language for expressing protocols, particularly handling symmetric encryption and unbounded number of sessions. The language is similar to the spi-calculus, but has a completely deterministic semantics. The type system is similar to the Abadi-Blanchet type system for asymmetric communication. (To be presented at ACM CCS 2005.)
Ettekande slaidid. [pdf]
Abstract: Private itemset support counting (PISC) is a basic building block of various privacy-preserving data mining algorithms. In PISC, Client wants to know the support of her itemset in Server's database with the usual privacy guarantees.
We propose several solutions to this problem. If the number of attributes is small, then a communication-efficient PISC protocol can be constructed from a communication-efficient oblivious transfer protocol. The converse is also true: any communication-efficient PISC protocol gives a rise to a communicationefficient oblivious transfer protocol. For the general case, we propose a computationally efficient PISC protocol with linear communication in the size of the database. We show how to further reduce the communication by using various tradeoffs and random sampling techniques. (Joint work with Helger Lipmaa and Taneli Mielikäinen, to be presented at ICICS 2005.)
Ettekande slaidid. [pdf]
Abstract: In a paper recently published in ICALP 2005, Lipmaa, Wang and Bao identified a new essential security property, non-delegatability, of designated verifier signature (DVS) schemes. Briefly, in a non-delegatable DVS scheme, neither a signer nor a designated verifier can delegate the signing rights to any third party without revealing their secret keys. We show that the Susilo-Zhang-Mu identity-based strong DVS scheme, Ng-Susilo-Mu universal designated multi verifier signature scheme, the Laguillaumie-Vergnaud multi-DVS scheme and the Zhang-Furukawa-Imai universal DVS scheme are delegatable. Together with the results of Lipmaa, Wang and Bao, our results show that most of the previously proposed DVS schemes are delegatable. However, the Laguillaumie-Vergnaud and Zhang-Furukawa-Imai schemes may still be secure in practice, since there the only party who can delegate signing is the designated verifier, who may not have motivation to do so. We finish the paper with some discussion on whether the the non-delegatability notion of Lipmaa, Wang and Bao is appropriate. (Joint work with Yong Li, Dingyi Pei, to be presented a ICICS 2005.)
Ettekande slaidid. [pdf]
Abstract: It is widely believed that low-level languages with jumps must be difficult to reason about by being inherently non-modular. We have recently argued that this in untrue proposing a novel method for developing compositional natural semantics and Hoare logics for low-level languages and demonstrating its viability on the example of a simple low-level language with expressions. The central idea is to use the implicit structure of finite disjoint unions present in low-level code as an (ambiguous) phrase structure.
Here we apply our method to a stack-based language and develop it further. We define a compositional natural semantics and Hoare logic for this language and go then on to show that, in addition to Hoare logics, one can also derive compositional type systems as weaker specification languages with the same method. We describe type systems for stack-error freedom and secure information flow. (Joint work with Tarmo Uustalu, to be presented at CATS 2006.)
Ettekande slaidid. [ppt]
Abstract: In this talk, we discuss different approaches to program construction. In particular, we briefly introduce a method based on proof search, known as structural synthesis of programs (SSP), and on the other hand, a technique based on the optimization of a specific fitness function related to the task to be solved. The SSP method is a deductive approach for program synthesis carried out via special logical inference rules from a general relational specification of a problem. This specification is often called the computational model of the problem. Here we are going to design an inductive approach for automatic program construction based on the same specification language (computational model) that is augmented by experimental data that describe desirable input-output behavior of the program to be composed. (Joint work with Jaan Penjam.)
Ettekande slaidid. [pdf]
Abstract: We study the category of arrays, i.e., maps from "locations" to "values", subject to the axiomatics of global state.
Plotkin and Power have shown that computational effects, such as side effects, may be modeled using algebraic operations and equations. For side effects the operations are "update" and "lookup" subject to computationally natural equations, defining the theory of global state.
Plotkin and Power consider finite sets of locations. They model the effect of allocating new cells via the theory of local state, whith the idea that a computation creates new locations and performs the jump into the state (array) of higher, but still finite, dimension. This corresponds to the concept of potential infinity. We will focus on the concept of actual infinity, where states are represented by infinite arrays subject to the axiomatics of global state. We will consider the canonical, based on Frechet filter, model for this theory.
Ettekande slaidid. [ppt]
Abstract: We enhance the technique of static analysis for confidentiality in cryptographic protocols with support for digital signature operations. The technique presented is an extension of the cryptographic protocol analysis presented by Laud, being similar to Abadi and Rogaway based on replacing the cryptographic operations in the protocols with constructs that are "obviously secure". The replacements are made in such a way that no insecure protocol becomes secure. The transformed protocols are then statically analysed; they should be easier to analyse than the original protocol. Handling the digital signatures is a step in exploring the general approach and making it able to handle realistic scenarios gracefully. (Joint work with Peeter Laud, was presented at NordSec 2005.)
Ettekande slaidid. [pdf]
Abstract: The advent of proof-carrying code has generated significant interest in reasoning about low-level languages. It is widely believed that low-level languages with jumps must be difficult to reason about by being inherently non-modular. We argue that this is untrue. We take it seriously that, differently from statements of a high-level language, pieces of low-level code are multiple-entry and multiple-exit. And we define a piece of code to consist of either a single labelled instruction or a finite union of pieces of code. Thus we obtain a compositional natural semantics and a matching Hoare logic for a basic low-level language with jumps. By their simplicity and intuitiveness, these are comparable to the standard natural semantics and Hoare logic of While. The Hoare logic is sound and complete wrt. the semantics and allows for compilation of proofs of the Hoare logic of While. (Joint work with Ando Saabas, was presented at SOS 2005.)
Ettekande slaidid. [pdf]
Abstract: The Goblin is a static analyzer for multithreaded C. It specializes in detecting race conditions and is based on ideas from the Trier Data Race analyzer. The presentation will be demonstration of the tool and will give an overview of this approach to the analysis of multithreaded programs.
Ettekande slaidid. [pdf]
Kokkuvõte: Monte-Carlo meetodeid on mängupuude analüüsil kasutatud edukalt olukordades, kus mängijatel puudub täielik informatsioon või kus mäng sõltub juhuslikust elemendist (bridz^, pokker, backgammon, scrabble). Viimastel aastatel on Monte-Carlo meetodeid hakatud aga rakendama ka täieliku informatsiooniga ilma juhuseta kahe mängija mängudes, näiteks go's. Käesolevas ettekandes käsitleme võimalust defineerida clobberi staatilist seisuhinnangut Monte-Carlo meetodil ning uurime, millised on lähenemise kitsaskohad ja kuidas neist üle saada.
Slaidid. [pdf]
Peeter Laud