Ettekanded / Talks

Abel Armas-Cervantes: Behavioral comparison of process models based on canonically reduced event structures

Slides from the talk [pptx]

Abstract: In this paper we address the problem of diagnosing behavioral differences between pairs of business process models. The proposed solution is based on a translation from process models to Asymmetric Event Structures (AES). An AES represents the behavior of a process by means of events and binary behavioral relations. So, in order to find a behavioral representation (AES) of a process model that represents the behavior in a more succinct manner, we propose a technique to reduce the AES while preserving canonicity. Moreover, the AES of a process model with cycles is infinite and, therefore, we propose a notion of unfolding that captures all possible causes of each process's task. From there we derive an AES where repeated events are distinguished from non-repeated ones and that allows us to diagnose differences in terms of repetition and causal relations in one model but not in the other.

Joint work with Paolo Baldan, Marlon Dumas, Luciano Garca-Bauelos, presented at BPM 2014.

Kalmer Apinis: Efficiently intertwining widening and narrowing

Slides from the talk [pdf]

Abstract: Localized widening and narrowing, as proposed Amato and Scozzari, is an interesting improvement of the classical widening and narrowing approach. In many cases, it is able to improve precision of the analysis automatically---without changing the analysis domain. However, it is unable to cope with local solving and non-monotonic transfer functions.

In some aspects, the work of Amato and Scozzari is similar to the work of Apinis, Seidl and Vojdani, who considered non-monotonicity and local solving. Together, we now show how the effects of localized widening and narrowing can be achieved in a generic framework with local solving.

Silvio Capobianco: Martin-Lf randomness and measure preservation in cellular automata

Slides from the talk [pdf]

Abstract: In his 1966 paper, P. Martin-Lf addressed the question: what does it mean for a single sequence (rather than a distribution of) to be random? His answer formalizes the intuitive idea that a random object should not display any "recognizable" regularities. Later, P. Hertling and K. Weihrauch expanded this notion to define randomness for objects of more general classes, such as d-dimensional configurations, of which bi-infinite sequences are a special case.

Cellular automata (briefly, CA) are models of synchronous parallel computation, where the next state of each node of a regular grid (e.g., the Cayley graph of a group) is a function of the current state of a finite neighborhood of the node itself, different nodes having neighborhoods of identical shape. Several noteworthy facts about CA are known, among those: the 2001 result by C. Calude et al. that the global function of a d-dimensional CA is surjective if and only if it preserves Martin-Lf randomness of configurations; and the 2010 result by L. Bartholdi that preservation of the product measure (generated by setting 1/K^N as the measure of the set of the configurations on K states taking given values on N given points) of surjective CA characterizes amenable groups, a class introduced by J. von Neumann to explain the Banach-Tarski paradox.

This talk, which is a continuation of the one I gave at the Estonian-Latvian Theory Days in Medzabaki, is divided into two parts. In the first one, we illustrate the Hertling-Weihrauch procedure in the specific case of configurations over finitely generated groups with decidable word problem. In the second part, we discuss our 2013 result with P. Guillon (CNRS and IML Marseille) and J. Kari (University of Turku) that, for this class of groups, Calude's property is equivalent to amenability: in particular, we show that on every non-amenable, finitely generated group with decidable word problem there exists a CA such that every Martin-Lf random configuration has a nonrandom image and only nonrandom preimages.

Denis Firsov: Functional incremental computing

Abstract: We describe a basic framework for incremental computing in Haskell and develop a notion of change and change application for sequences. Finally, we implement an efficient algorithm for incremental stable sorting of sequences.

Joint work with Wolfgang Jeltsch.

Liina Kamm: Privacy-preserving statistical analysis using secure multi-party computation

Slides from the talk [pdf]

Abstract: Secure multi-party computation platforms are becoming more and more practical. This has paved the way for privacy-preserving statistical analysis using secure multi-party computation. Simple statistical analysis functions have been emerging here and there in literature, but no comprehensive system has been compiled. We consider the most used statistical analysis functions in the privacy-preserving setting including simple statistics, t-test, chi-square test, Wilcoxon tests and linear regression. We introduce a privacy-preserving statistical analysis tool called Rmind that works on the Sharemind platform and is similar to the statistics environment R that is widely used among data analysts. This tool allows analysts to perform statistical queries on Sharemind databases without requiring them to have a thorough background in cryptography.

Peeter Laud: Transforming out private conditionals in programs for secure multiparty computation platforms

Slides from the talk [pdf]

Abstract: Secure multiparty computation (SMC) platforms like Sharemind are provided with an application programming language that abstracts away from underlying cryptography. The language does not abstract away from one detail - the SMC protocols do not hide the execution trace of the program, hence one cannot branch on private values. One can only perform the computations in both branches and obliviously merge them afterwards; this transformation is supported on some platforms. Hence the application performs many operations, the result of which is afterwards discarded.

In this talk we present an optimization that looks for common functionality in different branches and tries to merge them together, thereby reducing the total number of operations the application has to perform.

Joint work with Alisa Pankova.

Olaf Maennel: The future of cyber security exercises: more than just education?

Slides from the talk [pdf]

Abstract: The Internet has become part of our critical communication infrastructure and has revolutionised the lives of many people. However, security in cyberspace is still an underdeveloped field. This is partially due to the fact that the Internet was developed without a clear security concept in mind and also partially due to the fact that it is lucrative now for criminals to find security holes. Overall, cyber security is a critical skill for everyone using the Internet.

We start this talk by improving cyber security training courses. Practical hands-on training courses have proven very valuable in teaching basic concepts, but it?s hard to setup and prepare high-quality courses. Among the problems is that each lab needs a realistic environment, configured with a magnitude of services and consisting of complex network technology. To recognise the true value of such labs, we need to reduce the complexity of building, configuring, deploying and monitoring those emulated networks.

We argue that this can be achieved by translation from a high-level network design into a concrete set of router and service configurations that automatically deploy onto several emulation platforms. We will then continue to show that such a system is not only be beneficial for teaching cyber security, but can also be used as a large-scale security evaluation platform that studies novel technology in the context of a realistic network environment. We conclude by outlining how such a high-level configuration framework may change how networks are configured in the future and thus lead towards an Internet design that has a security concept in mind.

Alisa Pankova: Precomputed verification of multiparty protocols with honest majority

Slides from the talk [pdf]

Abstract: We present a generic method for turning passively secure protocols into protocols secure against covert attacks. We use beaver triples to make it possible to verify a protocol execution by running it locally on shares. The method adds a longer preprocessing phase and a short post-execution verification phase to the protocol that allows a misbehaving party to escape detection only with negligible probability. The execution phase, after which the computed protocol result is already available for parties, has only negligible overhead added by our method. We present our result for three parties, but it should be possible to extend it to any number of parties. Differently from our previous results, the verification can be easily adjusted to computation on rings, not only on fields, and hence it can be more easily applied to existing secure multiparty computation platforms.

Joint work with Peeter Laud.

Sander Siim: Combining secret sharing and garbled circuits for efficient private IEEE 754 floating-point computations

Slides from the talk [pdf]

Abstract: Two of the major branches in secure multi-party computation research are secret sharing and garbled circuits. This work succeeds in combining these to enable seamlessly switching to the technique more efficient for the required functionality. As an example, we add garbled circuits based IEEE 754 floating-point numbers to a secret sharing environment achieving very high efficiency and the first, to our knowledge, fully IEEE 754 compliant secure floating-point implementation.

Joint work with Pille Pullonen.

Tanel Tammet: Sightsmap: calculating popularity and meaning from crowd-sourced geodata

Abstract: I'll give an overview of the sightsmap.com project, in particular the dimensions of place popularity and the tagging algorithms using photo titles as input. I'll also give a brief overview about the related analysis methods using mobile positioning.

Dominique Unruh: Quantum position verification in the random oracle model

Abstract: We present a quantum position verification scheme in the random oracle model. In contrast to prior work, our scheme does not require bounded storage/retrieval/entanglement assumptions. We also give an efficient position-based authentication protocol. This enables secret and authenticated communication with an entity that is only identified by its position in space.

Presented at CRYPTO 2014.

Tarmo Uustalu: Runners for your computations

Slides from the talk [pdf]

Abstract: What structure is required of a set so that computations in a given notion of computation can be run statefully with this set as the state space? Some answers: To be able to serve stateful computations, a set must carry the structure of a lens; for running interactive I/O computations statefully, a "responder-listener" structure is necessary etc. I will observe that, in general, to be a runner of computations for an algebraic theory (defined as a set equipped with a monad morphism between the corresponding monad and the state monad for this set) is the same as to be a comodel of this theory, ie a coalgebra of the corresponding comonad. I will work out a number of instances. I will also compare runners to handlers.

Jri Vain: Provably correct model-based testing

Slides from the talk [pdf]

Abstract: Automated software testing is an increasing trend for improving the productivity and quality of software development processes. That, in turn, rises issues of trustability and conclusiveness of automatically generated tests and testing procedures. The main contribution of this paper is the methodology and tools of proving the correctness of tests for remote testing of systems with time constraints. To demonstrate the feasibility of the approach we show how the abstract conformance tests are generated, verified and made practically executable on distributed model-based testing platform dTron.

Ral Vicente: Magnets, machines, brains

Abstract: In this talk I will highlight some connections between the physics of magnets, artificial neural networks, and brains that have contributed to a better understanding of complex phenomena in each of them.

Niccol Veltri: Two set-based implementations of quotients in type theory

Slides from the talk [pdf]

Abstract: We present and compare two different implementations of quotient types in Intensional Type Theory. We first introduce quotients as particular inductive types following the extension of Calculus of Constructions with quotient types from Martin Hofmann's 2005 PhD thesis. Then we give an impredicative encoding of quotients. This implementation is reminiscent of Church numerals and more generally of encodings of inductive types in Calculus of Constructions.

Vesal Vojdani: Static analysis of priority scheduled programs

Abstract: I describe some recent progress in our research into static analysis of embedded controllers in the automotive domain. We previously described how standard analysis techniques can be applied to interrupt-driven priority scheduling [POPL '11]. We were extremely happy until our project partners evaluated our analysis in their industrial use cases. As it happens, despite the wonderful set of synchronization mechanisms provided by the priority-scheduled operating system, programmers often used their own hand-written synchronization idioms. Instead of acquiring locks, they rely on programming logic and the state of program variables to ensure mutually exclusive access to shared data. In order to cope, we present a method to analyze programs using value-dependent synchronization [VMCAI '14].

Joint work with Martin Schwarz, Helmut Seidl and Kalmer Apinis.

Peeter Laud
Helger Lipmaa
Tarmo Uustalu
Varmo Vene
Viimane uuendus 20.2.2015