Previous TCS Seminar Series

---

For a list of current TCS Seminars, click here.

---

TCS Seminar Series Fall 2011

• 15 Dec 2011 at 10:15 in room 1537
  Modern SAT Solving: CDCL and Inprocessing
  (Matti Järvisalo, University of Helsinki)

  Boolean satisfiability (SAT) has become an attractive approach to solving hard decision and optimization problems arising from artificial intelligence, knowledge representation, and various industrially relevant domains. The success of the SAT-based approach relies heavily on the development of increasingly robust and efficient SAT solvers. This talk gives a two-part overview of the current state-of-the-art SAT solver technology based on the conflict-driven clause learning (CDCL) paradigm. In the first part, I will provide a basic overview of the most important components of CDCL SAT solvers today. The second part of the talk concentrates on the important aspect of practical preprocessing for SAT and the inprocessing SAT solving paradigm in which more extensive reasoning is interleaved with the core satisfiability search (not only before search). I will review some of the most successful SAT preprocessing techniques, and give an overview of our recent work (joint work with Armin Biere and Marijn Heule) on developing new reasoning techniques for pre- and inprocessing.

  The seminar will be 2*45 minutes with a 15 minute break.

• 07 Dec 2011 at 13:15 in room 1537
  An additive combinatorics approach to the log-rank conjecture in communication complexity
  (Noga Zewi, Technion, Haifa)

  For a {0,1}-valued matrix M let CC(M) denote he deterministic communication complexity of the boolean function associated with M. The log-rank conjecture of Lovasz and Saks [FOCS 1988] states that CC(M) <= log^c(rank(M)) for some absolute constant c where rank(M) denotes the rank of M over the field of real numbers.

  We show that CC(M) <= c rank(M)/ logrank(M) for some absolute constant c, assuming a well-known conjecture from additive combinatorics, known as the Polynomial Freiman-Ruzsa (PFR) conjecture.

  Our proof is based on the study of the "approximate duality conjecture" which was recently suggested by Ben-Sasson and Zewi [STOC 2011] and studied there in connection to the PFR conjecture. First we improve the bounds on approximate duality assuming the PFR conjecture. Then we use the approximate duality conjecture (with improved bounds) to get the aforementioned upper bound on the communication complexity of low-rank martices, and this part uses the methodology suggested by Nisan and Wigderson [Combinatorica 1995].

  Joint work with Eli Ben-Sasson and Shachar Lovett.

  The talk will be 2*45 minutes with the first 45 minutes intended for a general audience.

• 05 Dec 2011 at 13:15 in room 1537
  Robust set-valued prediction in games
  (Jörgen Weibull, Handelshögskolan, Stockholm)

  Game theory has transformed economics and greatly influenced other social and behavioral sciences. The central solution concept used in applications is that of Nash equilibrium. Yet Nash equilibria can be fragile and Nash equilibrium play does not generally follow from assumptions of rationality or of evolution. It is here argued that an exploration of methods for robust set-valued prediction in games is called for, and some such approaches and avenues for future research are discussed.

• 24 Nov 2011 at 13:15 in room 4523
  Integrity Protection for Authorized Changes - Sanitizable Signatures with Transparency or Detectability
  (Heinrich Pöhls, University of Passau, Germany)

  Sanitizable Signature Schemes enhance Digital Signatures by allowing the signer to allow a third-party called the sanitizer to make authorized changes to signed document. I will introduce our newest results on re-definition of the security properties Transparency and Detectability for Sanitizable Signatures. Transparency has been defined already by G. Ateniese, D. H. Chou, B. de Medeiros, and G. Tsudik in their 2005 ESORIC's paper titled "Sanitizable signatures". Transparency in a nutshell means that a verifier cannot distinguish with a probability better than 0.5 between a sanitized and an original version of a signed document.

  We have introduced and formalized the notion of detectability, which captures that a verifier will always be able to detect a sanitization. This still allows an authorized change to be verified, but it becomes detectable. In this talk I will explain the security properties of sanitizable signatures and show some applications. Finally, I will introduce the legal implications of transparency, which we circumvent by using a detectable sanitizable signature scheme.

• 14 Nov 2011 at 13:15 in room 4523
  Sampling Massive Online Graphs: Challenges, Techniques, and Applications to Facebook
  (Maciej Kurant, University of California, Irvine)

  Online Social Networks (OSNs) have recently emerged as a new killer application, and are of interest to a number of communities, ranging from computer science and engineering to social sciences. Because of their sheer size (Facebook alone has more than 800 million active users), OSNs are widely studied today based on *samples* collected through measurements of publicly available information. In this talk, I will give an overview of our recent work on sampling OSNs.

  First, I will discuss how to efficiently crawl a friendship graph to collect a representative sample of its *nodes*. To this end, I will introduce two novel techniques: (i) "Multigraph Sampling" that exploits different relations between nodes, and (ii) "Stratified Weighted Random Walk" that preferentially crawls nodes more relevant to our measurement. I will evaluate these techniques on real-life OSNs, such as Facebook and LastFM. This will also allow me to study some basic characteristics of these OSNs, e.g., the privacy awareness in Facebook.

  Second, I will focus on *topology* rather than on nodes alone. Breadth First Search (BFS) is a natural and widely used sampling technique in this context. Unfortunately, BFS is subject to nontrivial and often very significant biases, which I quantify analytically. As a viable alternative, I propose to study a "coarse-grained" version of the underlying topology, and I show how to estimate it based on a sample of nodes. Finally, I will apply this methodology to Facebook to obtain a global country-to-country friendship network (more examples available at geosocialmap.com).

  This work is joint with Athina Markopoulou, Minas Gjoka, and Carter Butts at the University of California, Irvine and with Patrick Thiran at EPFL, Lausanne. Parts of this work appear in IEEE INFOCOM 2010, ITC 2010, ACM SIGMETRICS 2011 and IEEE JSAC 2011.

• 24 Oct 2011 at 13:15 in room 1537
  The Landscape of Structural Graph Parameters
  (Michail Lampis, KTH CSC)

  In traditional computational complexity we measure algorithm running times as functions of one variable, the size of the input. Though in this setting our goal is usually to design polynomial-time algorithms, most interesting graph problems are unfortunately believed to require exponential time to solve exactly.

  Parameterized complexity theory refines this by introducing a second variable, called the parameter, which is supposed to quantify the “hardness” of each specific instance. The goal now becomes to confine the combinatorial explosion to the parameter, by designing an algorithm that runs in time polynomial in the size of the input, though inevitably exponential in the parameter. This will allow us to tackle instances where the parameter value is much more modest than the input size, which will happen often if the parameter is chosen well.

  Of course, this setting is rather general and there are countless ways in which one may attempt to measure the hardness of specific instances, depending on the problem. The parameterized graph algorithms literature has been dominated for a long time by a very successful notion called treewidth, which measures graph complexity by quantifying a graph's similarity to a tree. However, more recently the study of alternative graph parameters and widths has become more popular. In this (self-contained) talk we will attempt to explore the algorithmic properties of treewidth, its related graph width parameters, as well as other graph invariants which may serve as measurements of a graph's complexity such as Vertex Cover, or Max-Leaf number. We will focus especially on general results which prove tractability for whole classes of problems characterized by expressibility in certain logics, results often referred to as "algorithmic meta-theorems".

• 10 Oct 2011 at 13:15 in room 1537
  An Anonymity Framework for SaaS
  (Ricardo Puttini, University of Brasília)

  Cloud computing technology has recently experienced rapid growth and continuous adoption. Enterprises are evermore taking advantage of its dynamicity and ubiquity. However, migrating strategic services to the cloud has put embracing companies in a fragile spot. Entrusting key business knowledge to cloud service providers and consequently relinquishing any claims to complete privacy is the tradeoff applied to adopters of the technology. This happens because the cloud computing service model called SaaS (Software as a Service) makes use of service contracts that inherently give the service provider access to unreasonable amounts of information regarding the consumer’s business. The service consumer has, then, no option but to trust the service provider. Because of that, there emerges a demand for a reliable, private and economically viable framework for cloud service consumption.

  Our contribution unfolds as a privacy aware environment for cloud service consumption with a payment mechanism for maintaining the commercially feasibility of the SaaS service model. Regarding the supporting of privacy, anonymity techniques are employed both in service contract and network levels. As for the payment methods, encryption algorithms in the area of blind signatures complete the proposed framework.

• 27 Sep 2011 at 10:15 in room 1537
  Increasing availability in a p2p storage system through a truthful taxation mechanism
  (Krzysztof Rzadca, University of Warsaw, Poland)

  In peer-to-peer storage systems, peers replicate each others' data in order to increase availability. If the matching is done centrally, the algorithm can optimize data availability in an equitable manner for all participants. However, if matching is completely decentralized, peers' selfishness can greatly alter the results, leading to performance inequities that can render the system unreliable and thus ultimately unusable.

  In this presentation, we show game-theoretic mechanisms that reduce the price of anarchy, i.e., the relative loss of efficiency in the decentralized matching scenario. The mechanism "taxes" the highly-available peers. A fraction of their replication slots is used by a centralized algorithm to replicate data of weakly-available peers. We prove the conditions under which the mechanism is incentive-compatible, i.e., no peer gains by artificially lowering its availability. We also experimentally show that the mechanism renders the system usable, as the data availability of weakly-available peers increases by approximately two orders of magnitude.

• 26 Sep 2011 at 16:15 in room 1537
  Codes tailor-made for distributed networked storage
  (Anwitaman Datta, NTU Singapore)

  Redundancy is essential for fault-tolerance in distributed networked storage systems – which are ubiquitous and come in diverse flavors (e.g., p2p storage, data-centers). Erasure codes provide orders of magnitude better performance than replication in terms of fault-tolerance/storage overhead trade-offs, however traditional erasure codes incur high overhead for recreating lost redundancy in the system. This cardinal drawback has led to a recent flurry in designing codes which are tailor-made with the nuances of distributed storage systems in mind. In this talk, we will provide a brief overview of some such proposed codes, concluding with self-repairing codes.

  More details can be found at: http://sands.sce.ntu.edu.sg/CodingForNetworkedStorage/

• 19 Sep 2011 at 13:15 in room 4523
  A little advice can be very helpful
  (Arkadev Chattopadhyay, University of Toronto)

  Proving superpolylogarithmic lower bounds for dynamic data structures has remained an open problem despite years of research. Recently, Patrascu proposed an exciting new approach for breaking this barrier via a two player communication model in which one player gets private advice at the beginning of the protocol. He gave reductions from the problem of solving an asymmetric version of set-disjointness in his model to a diverse collection of natural dynamic data structure problems in the cell probe model. He also conjectured that, for any hard problem in the standard two-party communication model, the asymmetric version of the problem is hard in his model, provided not too much advice is given.

  We prove several surprising results about his model. We show that there exist Boolean functions requiring linear randomized communication complexity in the two-party model, for which the asymmetric versions in Patrascu's model have deterministic protocols with exponentially smaller complexity. For set-disjointness, which also requires linear randomized communication complexity in the two-party model, we give a deterministic protocol for the asymmetric version in his model with a quadratic improvement in complexity. These results demonstrate that Patrascu's conjecture, as stated, is false. In addition, we show that the randomized and deterministic communication complexities of problems in his model differ by no more than a logarithmic multiplicative factor.

  We also prove lower bounds in some restricted versions of this model for natural functions such as set-disjointness and inner product. All of our upper bounds conform to these restrictions.

  This is joint work with J. Edmonds, F. Ellen and T. Pitassi.

• 16 Sep 2011 at 10:15 in room 1537
  How Unique and Traceable are Usernames?
  (Daniele Perito, INRIA, France)

  Usernames are ubiquitously used for identification and authentication purposes on web services and the Internet at large, ranging from the local-part of email addresses to identifiers in social networks. Usernames are generally alphanumerical strings chosen by the users and, by design, are unique within the scope of a single organization or web service. In this paper we investigate the feasibility of using usernames to trace or link multiple profiles across services that belong to the same individual. The intuition is that the probability that two usernames refer to the same physical person strongly depends on the “entropy” of the username string itself. Our experiments, based on usernames gathered from real web services, show that a significant portion of the users’ profiles can be linked using their usernames. In collecting the data needed for our study, we also show that users tend to choose a small number of related usernames and use them across many services. To the best of our knowledge, this is the first time that usernames are considered as a source of information when profiling users on the Internet.

• 12 Sep 2011 at 13:15 in room 1537
  Algorithmic analysis and complexity lower bounds
  (Rahul Santhanam, University of Edinburgh)

  I will discuss some connections between analysis of algorithms for satisfiability and complexity lower bound techniques. First I will present an algorithm for Formula-SAT which runs in time 2^{n-\Omega(n)} on formulae of linear size. The analysis of the algorithm relies on the method of random restrictions, originally used to prove formula size lower bounds. Then I will sketch a connection between the Neciporuk lower bound technique in concrete complexity and the algorithmic technique of memoization. If time permits, I will show that the published analyses of some well-known algorithms for satisfiability are tight, and pose some questions about further connections in this vein.

• 05 Sep 2011 at 13:15 in room 1537
  Hardness amplification for polynomial threshold proof systems
  (Trinh Huynh, University of Washington)

  Using known results from multiparty number-on-forehead communication complexity, we exhibit a simple hardness amplification method that converts any t-CNF formula of large rank complexity in Resolution, for constant t, into a new related formula requring large rank and tree-like size complexity in much stronger proof systems, namely polynomial threshold proof systems, which consist of all systems for proving propositional tautologies by manipulating degree-k polynomial inequalities (collectively denoted as Th(k) proof systems). This method works for any k<loglog n, where n is the size of the formula. These include Gomory-Chvatal cutting-planes (CP) (as a special case of Th(1)) and Lovasz-Schrijver systems (as special cases of Th(2)). This method thus yields new rank and tree-like size lower bounds for a large number of natural formulas in these systems, whereas previously, lower bounds for only a handful of problems were known.

  For every even constant t>5, we also obtain strong integrality gap results for the MAX-t-SAT problem for Th(1) systems, which include CP. We also show that Th(k) systems are strictly stronger than Th(k-1) systems, for every k<loglog n, in terms of rank and tree-like size.

  This is joint work with Paul Beame and Toniann Pitassi.

• 22 Aug 2011 at 15:30 in room 1537
  Monotonicity testing and shortest-path routing on the cube
  (Arie Matsliah, IBM Haifa Research Laboratory and Technion - Israel Institute of Technology)

  How many edges does one need to remove from a directed n dimensional cube to disconnect t disjoint source-sink vertex pairs? We show a construction where removing t/\sqrt{n} edges suffices. This answers a decade-old question of Lehman and Ron related to monotonicity testing, and gives a stronger counterexample to Szymanski's conjecture on hypercube routing.

  The presentation is self-contained and elementary.

  Based on a joint work with Jop Briet, Sourav Chakraborty and David Garcia-Soriano.

TCS Seminar Series Spring 2011

• 20 June 2011 13:15 room 1537
  Internet Privacy: Who gathers data and how, and what can be done about it
  (Balachander Krishnamurthy, AT&T research)

  For the last few years we have been examining the leakage of privacy on the Internet: how information related to individual users is aggregated as they browse seemingly unrelated Web sites. Thousands of Web sites across numerous categories, countries, and languages were studied to generate a privacy "footprint". Our results show increasing aggregation of user-related data by a steadily decreasing number of entities. I will present results from three studies on leakage of personally identifiable information (PII) via Online Social Networks (both traditional and mobile OSNs) and popular non-OSN sites. I will discuss various options on what can be done about this serious problem.

• 30 May 2011 13:15 room 1537
  The complexity of conservative valued CSPs
  (Stanislav Živný, University College, Oxford, UK)

  We study the complexity of valued constraint satisfaction problems (VCSP). A problem from VCSP is characterised by a constraint language, a fixed set of cost functions over a finite domain. An instance of the problem is specified by a sum of cost functions from the language and the goal is to minimise the sum. Under the unique games conjecture, the approximability of finite-valued VCSPs is well-understood (Raghavendra [FOCS’08]). However, there is no characterisation of finite-valued VCSPs, let alone general-valued VCSPs, that can be solved exactly in polynomial time, thus giving insights from a combinatorial optimisation perspective.

  In this talk, I'll show Schaefer-like dichotomy theorem for general-valued constraint languages including all unary cost functions over arbitrary domains (such languages are called conservative). This work generalises several previous results, including an algorithm from Cohen et al. [TCS'08], and dichotomies for Boolean languages (Cohen at al. [AIJ'06]), Min-Cost Hom (Takhanov [STACS'10]), and Max-CSPs (Deineko et al. [JACM'08]). Compared to Deineko et al. [JACM'08], our results do not involve any computer-assisted search.

  Joint work with V. Kolmogorov.

• 16 May 2011 10:15 room 1537
  Short Propositional Refutations for Dense Random 3CNF Formulas
  (Iddo Tzameret, Tsinghua University, Beijing, China)

  This is a talk about propositional proofs and satisfiability. First, I am going to give a short high level introduction to proof complexity. Then, I will show that almost all 3CNF formulas with high enough clause-to-variable ratio have short propositional refutations, already in a fairly weak propositional proof system.

  No prior knowledge in proof complexity is assumed.

  Joint work with Sebastian Muller. (For more details see: http://iiis.tsinghua.edu.cn/~tzameret/3CNF-tcz.pdf)

  The talk is intended to last for about 60 minutes.

• 02 May 2011 13:15 room 1537
  Balanced Partitions of Trees
  (Andreas Feldmann)

  We study the k-BALANCED PARTITIONING problem in which the vertices of a graph are to be partitioned into k sets of size at most \ceiling{n/k} each while minimising the cut-size, which is the number of edges connecting vertices in different sets. The problem on general graphs is well studied, while no results are known for restricted graph classes.

  We initiate the research on restricted graph classes by focusing on trees. We show that approximating the cut-size is APX-hard even if the maximum degree of the tree is bounded by a constant. If instead the diameter of the tree is bounded by a constant, we show that it is NP-hard to approximate the cut-size within n^c , for any constant c < 1. On the positive side we show that if the constraint on the balance of the sets is relaxed such that at most (1 + \epsilon) n/k vertices are allowed in any of the k sets, then (for constants \epsilon > 0) there is a polynomial time approximation scheme that computes a partition with a cut-size of at most that of an optimal balanced solution.

• 28 Apr 2011 13:15 room 1537
  Approximating Graphic TSP by Matchings
  (Tobias Moemke, KTH CSC)

  We present a framework for approximating the metric TSP based on a novel use of matchings. Traditionally, matchings have been used to add edges in order to make a given graph Eulerian, whereas our approach also allows for the removal of certain edges leading to a decreased cost.

  For the TSP on graphic metrics (graph-TSP), the approach yields a 1.461-approximation algorithm with respect to the Held-Karp lower bound. For graph-TSP restricted to a class of graphs that contains degree three bounded and claw-free graphs, we show that the integrality gap of the Held-Karp relaxation matches the conjectured ratio 4/3. The framework allows for generalizations in a natural way and also leads to a 1.586-approximation algorithm for the traveling salesman path problem on graphic metrics where the start and end vertices are prespecified.

  The talk will be approximately 2*45 min and somewhat technical.

• 04 Apr 2011 15:15 room 1537
  Neutrality Based Symmetric Cryptanalysis
  (Shahram Khazaei, KTH CSC)

  Cryptographic primitives are the basic components of any cryptographic tool. Block ciphers, stream ciphers and hash functions are the fundamental primitives of symmetric cryptography. In symmetric cryptography, the communicating parties perform essentially the same operation and use the same key, if any.

  This presentation concerns cryptanalysis of stream ciphers and hash functions based on my findings during my Ph.D. studies at Swiss Federal Institute of Technology, Lausanne, Switzerland (EFPL). The main contribution of this work is introducing the concept of probabilistic neutrality for the arguments of a function, a generalization of the definition of neutrality. This concept finds application in cryptanalysis. An input argument of a given function is called neutral if it does not affect the output of the function. This simple idea has already been implicitly used in key recovery cryptanalysis of block ciphers and stream ciphers. However, in 2004, Biham and Chen explicitly used the idea of neutrality to speed up collision finding algorithms for hash functions. We call an input argument of a function probabilistic neutral if it does not have a "significant" influence on the output of the function. Simply stated, it means that if the input argument is changed, the output of the function stays the same with a probability "close" to one. We will exploit the idea of probabilistic neutrality to assess the security of several stream ciphers and hash functions. To the best of our knowledge, this is the first time that the probabilistic neutrality has found diverse applications in cryptanalysis.

• 11 Mar 2011 13:15 room 4523
  Behavioral specifications of object-oriented components: How do trace-based and model-based techniques compare?
  (Arnd Poetzsch-Heffter, University of Kaiserslautern)

  The literature distinguishes between trace-based and state-based specification techniques for object-oriented components. Trace-based techniques describe behavior in terms of the message histories of components. State-based specifications explain component behavior by defining how the state is changed by method calls and what the returned results are. The state space can either be abstract or concrete. Abstract states are used to model the behavior without referring to the implementation. Concrete states are expressed by the underlying implementation. State-based specifications are usually described in terms of pre- and postconditions of methods.

  In this talk, we investigate the relationship between trace-based specifications and specifications based on abstract states for sequential, object-based components. We present a technique for specifying interaction patterns of components and show that the technique allows to formulate both trace-based and state-based specifications. In particular, we illustrate how callbacks can be handled. We define the semantics of specifications in terms of transition systems and discuss how different specifications can be compared.

• 07 Feb 2011 13:15 room 1537
  Taming Code Explosion in Supercompilation
  (Peter Jonsson, Luleå University of Technology)

  Clear and concise programs written in functional programming languages often suffer from poor performance compared to their counterparts written in imperative languages such as Fortran or C. Supercompilation is a program transformation that can mitigate many of these problems by removing intermediate structures and performing program specialization.

  Unfortunately supercompilation sometimes also suffer from the problem of code explosion. This results in huge binaries which might hurt the performance on a modern processor. We present a revised supercompilation algorithm that is fast enough to speculatively supercompile expressions and discard the result if it turned out bad. This allows us to supercompile large parts of the imaginary and spectral parts of nofib in a matter of seconds while keeping the binary size increase below 5%.

• 04 Feb 2011 10:15 room 1537
  Resident Evil: After-Life Vulnerabilities in Firefox. A Study on Firefox Evolution, its Vulnerabilities, and its Fixes
  (Fabio Massacci, University of Trento)

  I will discuss the interplay between the evolution of Firefox source code and its vulnerabilities over six major versions (v1.0, v1.5, v2.0, v3.0, v3.5, and v3.6) spanning almost ten years of development, and integrating a numbers of sources (NVD, CVE, MFSA, Firefox CVS).

  Somewhat surprisingly we found out that a large fraction of today's vulnerabilities apply to code from older versions no longer mantained. We call these after-life vulnerabilities. This somewhat contradicts and somewhat confirms the Milk-or-Wine study of Ozment and Schechter as we did not found enough evidence that most vulnerabilities are foundational while they are still more than they should.

  The surprise will be spelled out after digging into a new metric which we call the LOC's market share (as opposed to the software or version market share), where we are able to show that old code is still very much in use both in terms of instances and as global codebase: versions might be replaced in the span of 6 months but we actually use the same code of 10 years ago.

  This is empirical evidence that the software-evolution-as-security solution (patching software and automatic updates) might not work, and that vulnerabilities will have to be mitigated by other means.

  Joint Work with S. Neuhaus and V. H. Nguyen.

• 31 Jan 2011 10:15 room D4448 (D-building, next to D42)
  From Trusted Systems to the Smart Grid
  (Klaus Kursawe, Radboud University Nijmegen)

  In this presentation, I will cover several layers of trust implementation from essential building blocks to architecture questions. We will start with mechanism used to implement secure hardware building blocks, then moving up to basic security services such as key establishment protocols for restricted devices, and ending in distributed security architectures. The presentation will finish with latest activities in Smart-Grid security, with a special emphasis on privacy protection in this context.

• 27 Jan 2011 10:15 room 4523
  Securing Mobile Unattended WSNs against a Mobile Adversary
  (Roberto di Pietro, Department of Mathematics, Roma Tre University)

  Wireless Sensor Networks (WSNs) security is complicated by the lack of inexpensive tamper resistant hardware in commodity sensors. Indeed, once an adversary compromises a sensor, all memory and forms of storage become exposed, along with all secrets. Thereafter, any cryptographic remedy ceases to be effective. Regaining sensor security after compromise (i.e., intrusion-resilience) is a formidable challenge.

  Prior approaches that rely on either (1) the presence of an on-line trusted third party (sink), or (2) the availability of a True Random Number Generator (TRNG) on each sensor, cannot be adopted in large-scale Unattended Wireless Sensor Networks (UWSNs), composed of low-cost commodity sensors and characterized by the intermittent presence of a sink.

  In this talk, we explore intrusion resilience in Mobile UWSNs in the presence of a powerful mobile adversary. We show how the choice of the sensor mobility model influences intrusion resilience with respect to this adversary. We also explore self-healing protocols that require only local communication. Results indicate that sensor density and neighborhood variability are the two key parameters affecting intrusion resilience. Findings are supported by extensive analyses and simulations.

• 14 Jan 2011 10:15 room 4523
  Security by degrees: the process of security risk and trust management
  (Simon Foley, Department of Computer Science, University College Cork, Ireland)

  A challenge to securing open systems is the process of assuring robustness to failure due to threats that exploit vulnerabilities in design, implementation and deployment. The provision of this assurance assumes that: requirements are understood; threats are properly identified, and the right security controls are available to mitigate the threats. Notwithstanding the challenge of verifying security of a complex system, what happens in practice is that requirements are misunderstood, threats are misidentified and security controls selection is limited. This talk discusses insights to these problems and offers some solutions based on my research in trust management and security configuration management.

• 12 Jan 2011 15:15 room 1537
  Femtocells - A femtostep to the holy grail
  (Prof. Jean-Pierre Seifert, Deutsche Telekom Laboratories, TU Berlin)

  Mobile network operators are adapting femtocells in order to simplify their network architecture for increased coverage, performance, and greater revenue opportunities. While emerging as a new low-cost technology which assures best connectivity, it has also introduced a range of new potential security risks for the mobile network operators. We analyze these security issues and demonstrate the weaknesses of femtocell security. First, we describe and demonstrate weaknesses in the location verification techniques that create problems for various important services such as lawful interception services, emergency call services, and the operator's business. Next, we outline several security flaws that allow attackers to gain root access or install malicious applications on the femtocell, and to remain undetected even when it has connected to the operator's network. Furthermore, we experimentally evaluated and showed a wide range of possible threats to femtocells; including compromise of femtocell credentials; physical, configuration, and protocol attacks; attacks on the core network; user data and identity privacy attacks. Experimental results suggest that location security methods are insufficient to avoid femtocell misuse. In addition, the vulnerabilities we found suggest that commercially available femtocells fail to fulfill 3GPP security requirements and could expose operator network elements to the attacker. Our findings and successful attacks exhibit the need for further research to bridge the gap between theoretical and practical security of femtocell devices.

TCS Seminar Series Fall 2010

• 13 Dec 2010 13:15 room 4523
  Network coding and guessing games
  (Klas Markström, Umeå university)

  In a network coding problem there are multiple senders who each wants to send a message to some receiver in a network. In traditional information transfer protocols bottlenecks may appear when several different messages which need to pass through a given router arrive there at the same time. In network coding this problem is solved by letting the routers transform the messages, in such a way that the receivers can compute their intended message from a set of arrive messages. Soren Riis found an equivalent formulation for the problem of finding optimal network coding protocols in terms of a guessing game on a graph, and this also turned out to be equivalent to a problem in circuit complexity. In this talk I will discuss some results by myself and Demetres Christofides which determine the optimal solutions to these games and, using linear programming and entropy, also present a conjecture on the optimal values for all undirected graphs.

• 29 Nov 2010 13:15 room 1537
  On the Semantics of Local Characterizations for Linear-Invariant Properties
  (Jakob Nordström, KTH CSC)

  A property of functions on a vector space is said to be linear-invariant if it is closed under linear transformations of the domain. Linear-invariant properties are some of the most well-studied properties in the field of property testing. Testable linear-invariant properties can always be characterized by so-called local constraints, and of late there has been a rapidly developing body of research investigating the testability of linear-invariant properties in terms of their descriptions using such local constraints. One problematic aspect that has been largely ignored in this line of research, however, is that syntactically distinct local characterizations need not at all correspond to semantically distinct properties. In fact, there are known fairly dramatic examples where seemingly infinite families of properties collapse into a small finite set that was already well-understood.

  In this work, we therefore initiate a systematic study of the semantics of local characterizations of linear-invariant properties. For such properties the local characterizations have an especially nice structure in terms of forbidden patterns on linearly dependent sets of vectors, which can be encoded formally as matroid constraints. We develop techniques for determining, given two such matroid constraints, whether these constraints encode identical or distinct properties, and show for a fairly broad class of properties that these techniques provide necessary and sufficient conditions for deciding between the two cases. We use these tools to show that recent (syntactic) testability results indeed provide an infinite number of infinite strict hierarchies of (semantically) distinct testable locally characterized linear-invariant properties.

  Joint work with Arnab Bhattacharyya, Elena Grigorescu, and Ning Xie

• 15 Nov 2010 13:15 room 4523
  Structural Properties of Hard Problem Instances
  (Tobias Mömke, KTH CSC)

  Most of the hardness results for NP-hard problems are derived for worst-case scenarios and in many cases it is not clear whether the actual problem instances arising in practical applications exhibit this worst-case behavior. A recent branch of algorithmic research aims at a more fine-grained analysis of the hardness of optimization problems. The main idea behind this analysis is to find some parameter according to which one can classify the hardness of problem instances. In this spirit, we characterize instances for the metric TSP according to the solution computed by Hoogeveen's 5/3-approximation algorithm for the problem to find a Hamiltonian path with prespecified ends in the same metric graph. Our analysis reveals that the sets of the hardest instances of both problems for Christofides' and Hoogeveen's algorithm are disjoint in the sense that any instance is guaranteed to allow at least one of the two algorithms to achieve a significantly improved approximation ratio. In particular, any input instance that leads to a $5/3$-approximation with Hoogeveen's algorithm enables us to find an optimal solution for the traveling salesman problem.

• Oct 20 2010 13:15 room 1537
  A counter-example guided abstraction refinement scheme for parameterized verification.
  (Ahmed Rezine, Uppsala Univerity)

  I will introduce ''monotonic abstraction'' as an approach to verify systems with an arbitrary number of concurrent and communicating processes, i.e., parameterized systems. Monotonic abstraction is particularly successful in automatic verification of safety properties for parameterized systems. The main drawback is that it sometimes generates spurious counter-examples.

  I will describe a counterexample-guided abstraction refinement (CEGAR) framework for monotonic abstraction. The CEGAR algorithm automatically extracts from each spurious counterexample a set of configurations called a ''Safety Zone'' and uses it to refine the abstract transition system of the next iteration. This approach gave encouraging results and allowed the verification of several parameterized systems.

• Oct 18 2010 13:15 room 1537
  On the Relative Strength of Pebbling and Resolution
  (Jakob Nordström, KTH CSC)

  In the early 70s, combinatorial pebble games played on directed acyclic graphs were introduced as a way of studying programming languages and compiler construction. These games found a broad range of applications in computational complexity theory and were extensively studied in the 70s and 80s.

  Somewhat surprisingly, the last decade has seen a revival of interest in pebble games in the context of proof complexity. In particular, pebbling has proven a very useful tool for understanding time-space trade-offs. Very roughly, what one can do is to encode instances of the pebble game as propositional logic formulas, and then argue that these formulas (almost) inherit the pebbling properties of the underlying graphs.

  The crux of the matter here is what "almost" means. Graphs and formulas are very different objects, and the reductions we have between the two are far from tight. In this work, we introduce a new flavour of pebbling that gives better reductions than were previously known. We also construct graph families for which the gap in the current reductions does not matter. There are still a number of problems regarding space complexity and time-space trade-offs that, although simple to state, remain wide open, however, and time permitting we will discuss some of these problems.

  This talk is intended to be roughly 45 minutes long and to be completely self-contained. In particular, no prerequisites in proof complexity or pebbling are required. The talk is based on a paper that appeared in the Conference on Computational Complexity 2010.

• Sept 27 2010 13:15 room 1537
  Virtualization and Security
  (Christian Gehrmann, Swedish Institute of Computer Science)

  Part I: Background to Virtualization and Security

  Virtualization is becoming increasingly popular. In this talk we give a brief overview of the technologies behind virtualization. In particular we discuss the security challenges and opportunities in virtualized systems.

  Part II: Hypervisors for security in embedded systems

  Security threats on consumer devices such as mobile phones are increasing as the software platforms become more open and complex. Therefore, hypervisors, which bring potential new secure services to embedded systems, are becoming increasingly important. We look into how to design hypervisor-based security architecture for an advanced mobile phone and compare with alternative approaches such as the ARM TrustZone technology.

• Sept 23 13:15 1537
  Non-deterministic Matrices and their Applications
  (Anna Zamansky, Tel-Aviv University)

  One of the main principles of classical and many-valued logic is truth-functionality: the truth-value assigned to a complex formula is uniquely determined by the truth-values of its subformulas. In commonsense reasoning, however, an agent often needs to deal with inherently non-deterministic phenomena: partially unknown information, faulty devices and ambiguity of natural language are only a few cases in point. It is clear that non-determinism, the very essence of which is contradictory to the principle of truth-functionality, cannot be captured by classical or many-valued logics. One possible solution is to borrow the idea of non-deterministic computations from automata and computability theory and to apply it to evaluations of formulas. This leads to the introduction of Non-deterministic Matrices (Nmatrices), which are a generalization of standard many-valued matrices, in which the truth-value of a complex formula is chosen non-deterministically out of a certain set of options. Although applicable to a much wider family of logics, finite Nmatrices have all the advantages of ordinary finite-valued semantics. In fact, there are many useful (propositional) logics that have no finite ordinary semantics, but do have finite non-deterministic semantics, and are thus decidable.

  In this talk we survey the theory and a number of applications of Nmatrices in different areas. One such application is in the area of paraconsistent logics, which are logics that allow non-trivial inconsistent theories and are useful for reasoning with inconsistent information. Nmatrices can be used to provide simple and modular semantics for a large family of paraconsistent logics known as Logics of Formal Inconsistency. Another application of Nmatrices is in proof theory: there is a remarkable correspondence between two-valued Nmatrices and important syntactic properties, such as as cut-elimination, invertibility of rules, etc. in a natural class of Gentzen-type systems called Canonical Calculi.

TCS Seminar Series Spring 2010

• May 27 2010 13:15 room 1537
  Hardness of 3Lin over the reals
  (Subhash Khot, New York University)

  TBA

• May 19 2010 10:00 4423
  Cryptographic Hash Functions: Theory and Practice
  (Bart Preneel, Katholieke Universiteit Leuven)

  The first designs of cryptographic hash functions date back to the late 1970s. In the early 1990s, MD5 and SHA-1 were deployed in an ever increasing number of applications; as a consequence, hash functions became the "Swiss army knifes" of cryptography. In spite of the importance of hash functions, only limited effort was spent on studying their formal definitions and foundations. In 2004 Wang et al. perfected differential cryptanalysis to a point that finding collisions for MD5 became very easy; for SHA-1 a substantial reduction of the security margin was obtained. This breakthrough has resulted in a flurry of research, resulting in new constructions and a growing body of foundational research. NIST announced in November 2007 that it would organize the SHA-3 competition, with as goal to select a new hash function family by 2012. From the 64 candidates submitted by October 2008, 14 have made it to the second round. This talk presents an overview of the state of hash functions 30 years after their introduction; it also discusses the progress of the SHA-3 competition.

• May 12 2010 11:00 room 4423
  Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions
  (Jakob Nordström, MIT CSAIL)

  In recent years, deciding if a CNF formula is satisfiable has gone from a theoretical question to a practical approach for solving real-world problems. For current state-of-the-art satisfiability algorithms, typically based on resolution and clause learning, the two main bottlenecks are the amounts of time and memory used. Understanding time and memory consumption of SAT-solvers, and how these resources are related to one another, is therefore a question of considerable interest.

  Roughly a decade ago, it was asked whether proof complexity had anything intelligent to say about this question, corresponding to the interplay between size and space of proofs. In this talk, I will explain how this question can be answered almost completely by combining two tools, namely good old pebble games on graphs, studied extensively in the 70s and 80s, and a new, somewhat surprising, theorem showing how the hardness of CNF formulas can be amplified simply by making variable substitutions.

  This talk is based partly on my PhD thesis, presented with the Ackermann Award 2009, and partly on some subsequent papers. Most of it is joint work with Eli Ben-Sasson. The talk will be self-contained, so no background is needed.

• April 26 2010 13:15 room 1537
  CFlow: A security-preserving cryptography-implicit compiler for distributed programs
  (Gurvan Le Guernic, KTH CSC)

  In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues. We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract information-flow policy for accessing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing. We build a translation from well-typed source programs and policies to cryptographic implementations. To establish its correctness, we develop a cryptographic type system for a target probabilistic language. Our typing rules enforce the correct usage of cryptographic primitives against active adversaries; from an information-flow viewpoint, they capture controlled forms of robust declassification and endorsement. We show type soundness for a variant of the non-interference property, then show that our translation preserves typability. We rely on concrete primitives and hypotheses for cryptography, stated in terms of probabilistic polynomial-time algorithms and games. We model these primitives as commands in our target language. Thus, we develop a uniform language-based model of security, ranging from computational non-interference for probabilistic programs down to standard cryptographic hypotheses.

• Jan 25 2010 13:15 4523
  En introduktion till OWASP -- The Open Web Application Security Project
  (John Wilander, Omegapoint / Chapter leader OWASP Sweden)

  En introduktion till den världsomspännande, ideella säkerhetscommunityn OWASP. Genom vår ständigt växande wiki, öppna projekt, gratis böcker och konferenser så arbetar OWASP för högre säkerhet i applikationsutveckling. Mest kända är vi för vår topp tio-lista över de största säkerhetsriskerna i webbapplikationer (OWASP Top 10) men vi har många andra strängar på lyran:

  • OpenSAMM -- en metod för införande av Security Development Lifecycle
  • OWASP Testing Guide -- en gratis bok om säkerhetstestning
  • ESAPI, Enterprise Security API -- ett säkerhets-API i Java
  • JBroFuzz, Orizon, Anti-Samy -- ett antal öppna säkerhetsverktyg
  • Webgoat -- en övningsapplikation för att lära sig om säkerhetsfel

TCS Seminar Series Fall 2009

• Dec 03 2009 10:15 1537
  Introduction to Supercompilation
  (Peter Jonsson, Luleå)

  High levels of abstraction, the possibility to reason about software components in isolation, and the ability to compose different components together are crucial to improve productivity in software development. A pure functional language gives the ability to reason equationally about programs, along with features such as higher-order functions that aid programmer productivity. While these mechanisms increase productivity they also come with a problem known as the 'abstraction penalty': as the programmer increases the abstraction level to deal with system complexity, the performance of the resulting program decreases.

  I will show, through examples, how the abstraction penalty can be automatically removed through supercompilation. Anyone who has taken a basic course in functional programming should be able to follow my examples. I will briefly survey previous work and identify some open problems.

• Dec 01 2009 13:15 1537
  A Refined State Monad, with applications to capability-based access control
  (Johannes Borgström, )

  Behavioural type and effect systems regulate properties such as adherence to object and communication protocols, dynamic security policies, avoidance of race conditions, and many others. Typically, each system is based on some specific syntax of constraints, and is checked with an ad hoc solver.

  Instead, we advocate types refined with first-order logic formulas as a basis for behavioural type systems, and general purpose automated theorem provers as an effective means of checking programs.

  To illustrate this approach, we give type systems for two related notions of permission-based access control: stack inspection and history-based access control. These type systems are both instances of a refined state monad.

  Our main technical result is a safety theorem stating that no assertions fail when running a well-typed program.

• Oct 29 2009 09:00 MDI-Torget
  Evolving Contracts
  (Gerardo Schneider, Chalmers)

  Any formalism to describe contracts must be able to capture evolvability over time, and also to correlate such evolutions to changes in the environment or in the behavior of the parties involved in contracts. Yet, few works have focused on the general problem of verifying evolvable contracts.

  In this talk I will present ongoing work on the definition of an abstract theory of dynamic contracts, including some preliminary results concerning verification of static and dynamic contracts. Starting from a very general view of contracts as syntactic entities that characterize sets of traces, I show how to accomodate two essential ingredients of dynamic contracts: spillover, which characterizes the remains of a clause when it is withdrawn from a contract, and power, which characterizes when a principal is entitled to perform a change in a contract. Although the technical development is carried in an abstract setting, I will illustrate our definitions and results using contract languages for rights and obligations; these languages, despite their simplicity, share many essential features with other formalisms for digital right management and access control, and are therefore representative of the potential interest of our approach.

  (Joint work with Gilles Barthe and Gordon Pace)

• Tuesday August 25, 14.00, room 1537:
  PeerSoN: Privacy-Preserving P2P Online Social Networks
  (Sonja Buchegger, Deutsche Telekom Laboratories)

  Online Social Networks like Facebook, MySpace, Xing, etc. have become extremely popular. Yet they have some limitations that we want to overcome for a next generation of social networks: privacy concerns and requirements of Internet connectivity, both of which are due to web-based applications on a central site whose owner has access to all data.

  To overcome these limitations, we envision a paradigm shift from client-server to a peer-to-peer infrastructure coupled with encryption so that users keep control of their data and can use the social network also locally, without Internet access. This shift gives rise to many research questions intersecting networking, security, distributed systems and social network analysis, leading to a better understanding of how technology can support social interactions.

  Our project consists of several parts. One part is to build a peer-to-peer infrastructure that supports the most important features of online social networks in a distributed way. We have written a first prototype to test our ideas. Another part is concerned with encryption, key management, and access control in such a distributed setting. Extending the distributed nature of the system, we investigate how to integrate such peer-to-peer social networking with ubiquitous computing and delay-tolerant networks, to enable direct exchange of information between devices and to take into account local information.

TCS Seminar Series Spring 2009

• Monday May 25, 13.15, room 1537 (Lindstedtsvägen 5, floor 5):
  Three holy grails of programming models
  (Joachim Parrow, Uppsala Universitet)

  I shall discuss three important paradigms for formulating models of programming languages, the technical problems involved in unifying them, and how it connects to recent work joint with Jesper Bengtson, Magnus Johansson and Björn Victor to appear at LICS '09. This will also serve to put the pi-calculus in perspective by explaining its underlying motivations and real achievements and limitations. The intended audience should have a reasonable grasp on programming but needs not be familiar with any particular formalmodels.

• Wednesday May 27, 10.15, room 4423 (Lindstedtsvägen 5, floor 4):
  Game Theory with Costly Computation
  (Rafael Pass, Cornell University)

  We develop a general game-theoretic framework for reasoning about strategic agents performing possibly costly computation. In this framework, many traditional game-theoretic results (such as the existence of a Nash equilibrium) no longer hold. Nevertheless, we can use the framework to provide psychologically appealing explanations to observed behavior in well-studied games (such as finitely repeated prisoner's dilemma and rock-paper-scissors). Furthermore, we provide natural conditions on games sufficient to guarantee that equilibria exist.

  As an application of this framework, we consider a notion of game-theoretic implementation of mediators in computational games. We show that a special case of this notion is equivalent to a variant of the traditional cryptographic definition of protocol security; this result shows that, when taking computation into account, the two approaches used for dealing with deviating players in two different communities---Nash equilibrium in game theory, and zero-knowledge simulation in cryptography---are intimately connected.

  Joint work with Joe Halpern.

• Wednesday May 27, 13.15, room 1537 (Lindstedtsvägen 5, floor 5):
  Quantitative Social Choice Theory
  (Elchanan Mossel, UC Berkeley / Weizmann Institute of Science)

  I will survey recent results giving quantitative versions of theorems in economics regarding social choice (voting) functions. The focus of the talk will be a quantitative proof of Arrow's Impossibility Theorem. The proof is based on new combinatorial arguments coupled with use of an inverse hyper-contractive estimate by Borell and non-linear invariance principles.

TCS Seminar Series Fall 2008

• Friday December 12, 13.15, room 1537:
  Reducing Behavioural Properties to Structural Properties of Programs with Procedures
  (Dilian Gurov, Theory Group, KTH CSC)

  (Joint work with Marieke Huisman, University of Twente)

  There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. This talk presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with procedures, and properties expressed in a fragment of the modal mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. We discuss several applications of the characterisation, in particular compositional verification for behavioural properties, based on maximal models.

• Friday November 28, 10.00 (NB! no academic quarter!), room 4523 (Lindstedtsvägen 5, floor 5):
  Nearly spherical cubes
  (Ryan O'Donnell, School of Computer Science, Carnegie Mellon University)

  What is the least surface area of a shape that tiles d-dimensional space when shifted by all vectors in the integer lattice? A unit cube is such a shape, and has surface area 2d. On the other hand, any such shape must have volume 1 and hence surface area at least that of the volume-1 ball, namely about sqrt(2 pi e) sqrt(d). We nearly close the gap, using a randomized construction to show that there exists a tiler with surface area at most 4 pi sqrt(d). The problem was originally motivated by questions in computational complexity theory; our construction generalizes a discretized solution given by Raz in the complexity-theory setting.

• Tuesday October 7, 15.15, room 1537:
  Security Policy Enforcement through Transactional Memory Introspection
  (Úlfar Erlingsson, School of Computer Science, Reykjavík University)

  Correct enforcement of authorization policies is a difficult task, especially for multi-threaded software. Even in carefully-reviewed code, unauthorized access may be possible in subtle corner cases. This talk introduces Transactional Memory Introspection (TMI), a novel reference monitor architecture that builds on Software Transactional Memory-a new, attractive alternative for writing correct, multi-threaded software. TMI may be seen as an early language-based security result in a promising new area that is both well-suited to formalization and can also hold large practical benefits

  TMI facilitates correct security enforcement by simplifying how the reference monitor integrates with software functionality. In particular, TMI can help ensure complete mediation of security-relevant operations, eliminate race conditions related to security checks, and simplify handling of authorization failures. The talk will present the design, implementation, and initial formalization of TMI-based reference monitors. The talk also describes the results of our initial experiments, which confirm the value of the TMI architecture and that it incurs only acceptable runtime overhead.

• Friday September 12, 10.15, room 1439:
  A clearer picture of approximation resistance
  (Per Austrin, Theory Group, KTH CSC)

  A constraint satisfaction problem (CSP) is said to be approximation resistant if it is hard to approximate within a factor better than what is obtained by a random assignment. We talk about recent progress on characterizing approximation resistant CSPs.

  Based on joint works with Johan Håstad and Elchanan Mossel.

---

TCS Seminar Series Spring 2008

• Monday March 31, 13.00, room 1537:
  A Transformation from the Fibonacci to the Galois Non-Linear Feedback Shift Registers
  (Professor Elena Dubrova, ECS/ICT/KTH)

  Conventional Non-Linear Feedback Shift Registers (NLFSRs) use the Fibonacci configuration in which the feedback is applied to the first bit only. In this paper, we show how to transform a Fibonacci NLFSR into an equivalent NLFSR in the Galois configuration, in which the feedback can potentially be applied to every bit. Such a transformation reduces the depth of the circuits implementing feedback functions, thus decreasing the propagation time and increasing the throughput. The practical significance of the presented technique is that is makes possible increasing (in some cases doubling) the keystream generation speed of any Fibonacci NLFSR-based stream cipher with no area penalty.

• Wednesday January 8, 10.15, room 4523:
  Structural Operational Semantics for Computational Effects
  (John Power, Reader, Dept. of Computer Science, University of Bath)

  (joint with Gordon Plotkin)

  In seeking a unified study of computational effects, a fundamental task is to give a unified structural operational semantics, together with an adequate denotational semantics for it, in such a way that, for the leading examples of computational effects, the general definitions are consistent with the usual operational semantics for the relevant effects. One can readily produce a unified operational semantics that works fine for examples that include various forms of nondeterminism and probabilistic nondeterminism. But that simple semantics fails to yield a sensible result in the vitally important case of state or variants of state. The problem is that one must take serious account of coalgebraic structure. I shall not formally enunciate a general operational semantics and adequacy theorem in this talk, but I shall explain the category theory that supports such a semantics and theorem. I shall investigate, describe, and characterise a kind of tensor of a model and a comodel of a countable Lawvere theory, calculating it in leading examples, primarily involving state. Ultimately, this research supports a distinction between what one might call coalgebraic effects, such as state, and algebraic effects, such as nondeterminism

---

TCS Seminar Series Fall 2007

• WENNER-GREN FOUNDATIONS DISTINGUISHED LECTURE
  Wednesday November 21, 15:00, room D3
  Cryptography in Financial Transactions: Current Practice and Future Directions
  (Professor Jacques Stern, Ecole Normale Supérieure and CNRS)

  In this talk I will briefly describe the history of cryptography and explain how it became an area of scientific research, served by a strong community both in academia and in the industry.

  Next I will cover two case studies.

  The first is related to banking cards and payment terminals and the second to Internet banking. In both cases, I will show how cryptographic tools crafted within the research community in the past thirty years entered the picture and how cryptographers were able to provide stronger and stronger levels of security.

  While applications are now stable in the first area, there is more to come in the second.

• Monday October 15, 15:15, room 4523:
  Optimal Bounds for Predecessor Search and the First Separation between Linear and Polynomial Space
  (Mikkel Thorup, AT&T Labs Research)

  (joint work with Mihai Patrascu from STOC'06 and SODA'07)

  We develop a new technique for proving cell-probe lower bounds for static data structures. Previous lower bounds used a reduction to communication games, which was known not to be tight by counting arguments. We give the first lower bound for an explicit problem which breaks this communication complexity barrier. In addition, our bounds give the first separation between polynomial and near linear space. Such a separation is inherently impossible by communication complexity.

  Using our lower bound technique and new upper bound constructions, we obtain tight bounds for searching predecessors among a static set of integers. We determine the optimal query time for any combination of space and word size w. In particular, we show that the classic van Emde Boas search time of O(log w) cannot be improved, even if we allow randomization. This is a separation from polynomial space, since Beame and Fich [STOC'99] give a predecessor search time of O(log w / log log w) using quadratic space.

• Monday October 8, 13:15, room 1537:
  Beating Semidefinite Programming Means Beating The Unique Games Conjecture
  (Per Austrin, Theory Group, KTH CSC)

  During the last few years, there have been several results of the form "if the Unique Games Conjecture is true, then problem X can not be approximated better than what is achieved by algorithm Y, based on semidefinite programming", indicating a strong connection between the UGC and the limitations of SDP-based approximation algorithms.

  For 2-CSP problems in particular this connection has been very evident, with the optimal parameters for the hardness reductions for Max Cut and Max 2-Sat coming directly from the analysis of the best SDP-based approximation algorithms for the problems.

  We generalize these results, by considering an arbitrary boolean 2-CSP (or more generally, an arbitrary nonnegative objective function on two boolean variables), and show that a set of "obstructions" towards obtaining a good rounding procedure for the SDP relaxation can be translated into a matching UG-hardness result. We also show that, under a certain conjecture on the nature of worst-case angles for the SDP relaxation, this result is tight. This conjecture is supported by all previous results for specific 2-CSPs.

  The talk will be 45 minutes long and will be held in English.

• Tuesday October 2, 13:15, room 4523:
  Model Checking Network Applications
  (Cyrille Artho, AIST, Japan)

  This tutorial addresses a new model checking technique for networked applications. Such applications could not be model checked by traditional techniques, as multiple processes cannot be checked in normal (single-process) software model checkers. Our approach is to convert processes into threads and to model network communication using a special library and model checker extensions. Other approaches include the usage of stubs or a special cache that can serialize the state space exploration tree.

• Monday September 10, 13:15, room 1537:
  Generating Propagators for Finite Set Constraints
  (Christian Schulte, Department of Electronic, Computer, and Software Systems, KTH ICT)

  Constraint programming is a successful and widely used method for solving combinatorial optimization problems. An essential ingredient for any constraint programming system are propagators implementing constraints performing strong constraint propagation.

  Ideally, programming propagators as implementations of constraints should be an entirely declarative specification process for a large class of constraints: a high-level declarative specification is automatically translated into an efficient propagator.

  This talk introduces the use of existential monadic second-order logic as declarative specification language for finite set propagators. The approach taken is to automatically derive projection propagators (involving a single variable only) implementing constraints described by formulas. By this, we transfer the ideas of indexicals to finite set constraints while considerably increasing the level of abstraction available with indexicals. We show soundness and completeness of the derived propagators and present a runtime analysis, including techniques for efficiently executing projectors for n-ary constraints.

  Joint work with:

  • Guido Tack, Programming Systems Lab, Saarland U, Germany
  • Gert Smolka, Programming Systems Lab, Saarland U, Germany

  ---

  TCS Seminar Series Spring 2007

  • Wednesday June 27, 13:15, room 1537:
    Towards modular verification of concurrent object-oriented programs
    (Marieke Huisman, INRIA Sophia Antipolis)

    Modular static verification of concurrent object-oriented programs remains a challenge. This talk discusses the impact of concurrency on the use of standard program-logic-based verification techniques.

    Atomicity of methods is often advocated as a solution to the problem of verification of multithreaded programs. However, we show that in a design-by-contract framework atomicity in itself is not sufficient, because it does not consider specifications. Instead, we propose to use the notion of stability of method contracts, to allow sound modular reasoning about method calls. A contract is stable if it cannot be broken by interferences from concurrent threads.

    We explain why stability of contracts cannot always be shown directly, and we speculate about different approaches to prove stability. One approach that we will detail further is the use of an annotation system to describe object capacities and locking policies. The annotation system can be used to specify how many threads simultaneously can access an object. The annotation system distinguishes between read-write accesses and read-only accesses, thus offering fine-grained concurrency control. The locking policy of an object describes which locks must be held, before accessing it. The annotation system can express how ownership may be transferred or split between different threads.

    The information that is given by the annotations can be exploited to verify other properties of the application. In particular, if an object is known to be local to a thread, sequential verification techniques can be used to verify functional correctness of its methods. We finish by outlining how a proof obligation generator for sequential programs can be extended to one for concurrent programs by using stability information.

    This talk does not present a full technical solution to the problem, but instead describes work in progress. It shows how the verification problem can be decomposed into several smaller subproblems. For each subproblem, a solution is sketched, but the technical details still need to be worked out.

    (Joint work with Clement Hurlin)

  • Thursday June 14, 13:15, room 1537:
    Logic-based Specification and Verification of Multi-Agent Systems
    (Alessio Lomuscio, Department of Computing, Imperial College London)

    Multi-agent systems are open, highly-autonomous systems whose components act rationally, independently or interacting with their peers, to achieve their design objectives. While several formalisms in Artificial Intelligence have been developed in the past to represent multi-agent systems, the issue of their automatic verification has acquired prominence only very recently. In this talk I will try to discuss some of my own contribution to this area. In particular I will survey some recent work on a family of temporal, epistemic, correctness, ATL logics as well as symbolic model checking techniques (both obdd- and sat-based) for their verification. I will discuss current research directions and, present brief demonstrations of MCMAS, a specialised model checker for temporal, epistemic, ATL logics.

  • Wednesday April 25, 13:15, room 1537:
    Towards the Engineering of Modular Software for Increased Predictability
    (Michel Schellekens, Centre for Efficiency-Oriented Languages, University College Cork)

    We focus in this talk on two main methods used in academia and industry to optimize/evaluate software: worst-case and average-case analysis. These methods can be used in a variety of contexts for optimization purposes. For instance in a Real-Time context, to efficiently budget resources, and in embedded systems, for optimizing power consumption.

    A crucial property for the predictability of software is modularity, i.e. the capacity to predict the behaviour of software from the behaviour of its components. It is shown that the worst-case measure typically does not allow for exact modularity. Current Real-Time approaches to static worst-case analysis are discussed in this light. On the other hand, we show that the average-case measure does possess inherent modularity. We show how this modularity can be exploited, based on a redesign of standard data structuring operations, to track the distribution of the data states throughout a computation. This approach in turn has enabled the specification of the novel programming language MOQA, implemented in Java 5.0, and its associated timing tool DISTRI-TRACK. MOQA (MOdular Quantitative Analysis), essentially a suite of data structure operations for modular design, is guaranteed to be modular w.r.t. the average-case time measure. This is not the case for general purpose programming languages and in particular for current languages geared towards automated average-case analysis.

    The approach links several, thus far largely separate, areas together, including Semantics, Complexity, Analysis of Algorithms and Real-Time Language design. The corresponding unified foundation for algorithmic analysis has led to the solution of bottle-neck problems in automated average-case timing (open problems on dynamic algorithms, first investigated by Knuth) and has given rise to novel algorithms.

    The talk focuses on the intuitions underlying the approach and should be accessible to anyone with a standard undergraduate background in the Analysis of Algorithms. The talk touches on some core issues which will be discussed in the book ``A Modular Calculus for the Average Cost of Data Structuring'', to appear with Springer.

  • Monday March 5, 13:15, room 1537:
    Computational Aspects of Random Boolean Networks
    (Elena Dubrova, KTH ICT)

    Research on networks becomes essential to all branches of sciences as we struggle to interpret the data coming from neurobiology, genomics, economics, ecology, and the Internet. Random Boolean Networks (RBNs) were introduced by Kaufmann in 1969 in the context of gene expression and fitness landscapes. They were applied to the problems of cell differentiation, immune response, evolution, and neural networks. They have also attracted the interest of physicists due to their analogy with the disordered systems studied in statistical mechanics, such as the mean field spin glass. An RBN is a synchronous Boolean automaton. Each vertex has k predecessors, selected at random, and an associated Boolean function of k variables. Kauffman has shown that it is possible to tune the parameters of an RBN so that the network exhibits self-organized critical behavior ensuring both stability and evolutionary improvements. Statistical features of self-organized RBNs match the characteristics of living cells. This talk focuses on computational aspects of RBNs. First, we give an introduction to random Boolean networks and show how they can be used for modeling of gene regulatory networks of living cells. Then, we describe three basic steps of the analysis of dynamical behavior of RBNs: redundancy removal, partitioning, and computation of attractors. Finally, we discuss open problems and outline prospectives of RBNs.

  • Joint TCS/CIAM Seminar
    Tuesday February 27, 15:15-17:00, room D3:
    Security and Cryptography in Mobile Wireless Networks
    (Mats Näslund, Ericsson Research)

    In the first half of the talk I will give an overview of the security functions and cryptography used in today's GSM (2G) and UMTS (3G) networks. I will also describe some cryptographic attacks on 2G security, largely due to 'security by obscurity' approaches used in the past. This has led to rethinking the security design principles, and in the second half I will present the new data authentication algorithm for UMTS which in a formal setting can be proven to be (unconditionally) secure. The only pre-requisites are basic understanding of finite fields.

  • Tuesday January 23, 13:15, room 1537:
    Learning of timed systems
    (Olga Grinchtein, Uppsala University)

    We present an algorithm for constructing a timed-automaton model of a system from information obtained by observing its external behavior. The construction of models from observations of system behavior can be seen as a learning problem. For finite-state reactive systems, it means to construct a (deterministic) finite automaton from the answers to a finite set of membership queries, each of which asks whether a certain word is accepted by the automaton or not. This problem is well understood, e.g., by the work by Angluin. We extend this approach to learning of timed systems, modeled by deterministic event-recording automata. Our construction deviates from previous work and that of Angluin in that it first constructs a so called timed decision tree from observations of system behavior. When sufficiently many observations have been recorded, this decision tree is folded into an event-recording automaton.

    joint work with Bengt Jonsson and Paul Pettersson

  ---

  TCS Seminar Series Autumn 2006

• Monday December 11, 10:15, room 4523 (NB! Not the usual time and place):
  Higher Level Fusion For Catastrophic Events
  (Galina L. Rogova PhD, Encompass Consulting, USA)

  The core purpose of higher level fusion (situation and threat assessment) is to infer and approximate the characteristics and critical events of the environment in relation to specific goals, capabilities and policies of the decision makers. The higher level fusion processes utilize fused data about objects of interest, dynamic databases, maps, and expert knowledge, and opinion for context processing. The result of higher level fusion is a coherent composite picture of the current and predicted situation, which provides human experts with essential information to help them understand and control the situation, and act effectively to mitigate its impact. Situation and threat assessment processing has to be adaptive to resource and time constraints, new and uncertain environments, and reactive to uncertain and unreliable heterogeneous inputs.

  The presentation will discuss major challenges, specific requirements, and approaches to designing higher level fusion processes as applied to the problem of crisis management.

  The higher level fusion processing described in the presentation exploits synergy between cognitive work analysis and ontological analysis of the specific domain, developed within the framework of a formal ontology. The combination of cognitive work analysis and ontology provides a formally structured and computationally tractable domain representation capturing the basic structures of relevant objective reality and users’ domain knowledge and requirements. This domain representation further serves as a basis for generating domain specific situational hypotheses and high-level reasoning about these hypotheses. The dynamic situational picture is built by analyzing spatial and temporal relations of the situational entities and entity aggregations at different levels of granularity, and their dynamics provided within the overall situational context. Special attention is paid to "inference for best explanation" aimed at discovery of the underlying causes of observed situational entities and their behavior. Belief Based Argumentation system, a reasoning framework considered, represents a generalization of Probabilistic Argumentation System. It allows for allocating rational belief in hypotheses about the environment by utilizing given knowledge to find and combine arguments in favor of and against them.

  The presented methodology also includes multi-step inter-level and intra-processing information exchange comprising a quality control and a belief update steps.

• Monday November 20, 13:15, room 1537:
  Counting Set Covers
  (Andreas Björklund, Lund Institute Of Technology)

  In a Set Cover problem we are given a ground set U of size n and a family S of size m of subsets of U and we want to know if U can be covered by k of the sets from S. We give two related algorithms which are stronger than applying dynamic programming over all subsets of U.

  1. We demonstrate a simple technique solving the problem in space $\poly(n,\log m)$ and time $\poly(n,\log m)m2^n$ which actually counts the number of solutions.
  2. We show that with exponential space we can count the solutions in time $\poly(n,\log m)(m+2^n)$ which gives us the fastest algorithms for Chromatic Number and Domatic Number known to date.

  Based on two recent papers with Thore Husfeldt announced at ICALP 2006 and FOCS 2006. The seminar will be roughly 45 minutes long.

• Monday October 2, 13:15, room 1537:
  BitTorrent
  (Stefan Nilsson, Theory Group, KTH CSC)

  BitTorrent är ett filöverföringsprotokoll som gör det möjligt att med mycket små serverresurser distribuera stora filer till många användare på kort tid. I det här föredraget kommer jag att beskriva hur protokollet fungerar, berätta hur Bram Cohen uppfann det och diskutera dess skalbarhet, säkerhet och begränsningar.

  Seminariet blir ca 45 minuter långt.

  ---

  TCS Seminar Series Spring 2006

  • Wednesday June 21, 15:15, room 1537:
    Cybersecurity and its limitations
    (Andrew Odlyzko, University of Minnesota)

    Network security is terrible, and we are constantly threatened with the prospect of imminent doom. Yet such warnings have been common for the last two decades. In spite of that, the situation has not gotten any better. On the other hand, there have not been any great disasters either. To understand this paradox, we need to consider not just the technology, but also the economics, sociology, and psychology of security. Any technology that requires care from millions of people, most very unsophisticated in technical issues, will be limited in its effectiveness by what those people are willing and able to do. The interactions of human society and human nature suggest that security will continue being applied as an afterthought. We will have to put up with the equivalent of bailing wire and chewing gum, and to live on the edge of intolerable frustration. However, that is not likely to block development and deployment of information technology, because of the non-technological protection mechanisms in our society.

    The talk will be roughly 60 minutes long.

  • Thursday June 15, 10:15, room 1537:
    A Framework for Sequential Planning in Multi-Agent Settings
    (Piotr Gmytrasiewicz, Department of Computer Science, University of Illinois at Chicago)

    This work extends the framework of partially observable Markov decision processes (POMDPs) to multi-agent settings by incorporating the notion of agent models into the state space. Agents maintain beliefs over physical states of the environment and over models of other agents, and they use Bayesian updates to maintain their beliefs over time. The solutions map belief states to actions. Models of other agents may include their belief states and are related to agent types considered in games of incomplete information. We express the agents' autonomy by postulating that their models are not directly manipulable or observable by other agents. We show that important properties of POMDPs, such as convergence of value iteration, the rate of convergence, and piece-wise linearity and convexity of the value functions carry over to our framework. Our approach complements a more traditional approach to interactive settings which uses Nash equilibria as a solution paradigm. We seek to avoid some of the drawbacks of equilibria which may be non-unique and do not capture off-equilibrium behaviors. We do so at the cost of having to represent, process and continuously revise models of other agents. Since the agent's beliefs may be arbitrarily nested, the optimal solutions to decision making problems are only asymptotically computable. However, approximate belief updates and approximately optimal plans are computable. We illustrate our framework using a simple application domain, and we show examples of belief updates and value functions.

  • Thursday June 8, 13:15, room 1537:
    Narrow Proofs May Be Spacious: Separating Space and Width in Resolution
    (Jakob Nordström, Theory Group, KTH CSC)
    [slides ]

    Resolution is a proof system for proving tautologies in propositional logic. It works by showing that the negation of a tautology, encoded as a CNF formula, is unsatisfiable. There is only one derivation rule, namely that from the clauses C ∨ x and D ∨ ¬ x we can resolve on the variable x to derive the resolvent clause C ∨ D. A resolution proof refutes an unsatisfiable formula F by deriving the empty clause 0, i.e., the clause with no literals, from F.

    Because of its simplicity, resolution is well adapted to proof search algorithms. Many real-world automated theorem provers are based on resolution. It is also perhaps the single most studied propositional proof system from a theoretical point of view in the area of proof complexity.

    The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is, intuitively, the maximal number of clauses one needs to keep in memory while verifying the proof. Both of these measures have previously been studied and related to the resolution refutation size of unsatisfiable CNF formulas. Also, the refutation space of a formula has been proven to be at least as large as the refutation width, but it has been open whether space can be separated from width or the two measures coincide asymptotically. We prove that there is a family of k-CNF formulas for which the refutation width in resolution is constant but the refutation space is non-constant, thus solving a problem mentioned in several previous papers.

    Our result has been published as ECCC Report TR05-066, and an extended abstract appeared in STOC '06 (co-winner of Danny Lewin Best Student Paper Award).

    The talk will be given in Swedish or English depending on the participants, and is intended to last for 2x45 minutes.

  • Wednesday May 31, 13:15, room 1537:
    Confluent Markov Chains
    (Parosh Abdulla, Department of Information Technology, Uppsala University)

    We consider infinite-state discrete Markov chains which are confluent: each computation will almost certainly either reach a defined set F of final states, or reach a state from which F is not reachable. Confluent Markov chains include probabilistic extensions of several classical computation models such as Petri nets, Turing Machines, and communicating finite-state machines.

    For confluent Markov chains, we consider three different variants of the reachability problem and the repeated reachability problem: The qualitative problem, i.e., deciding if the probability is one (or zero); the approximate quantitative problem, i.e., computing the probability up-to arbitrary precision; and the exact quantitative problem, i.e., computing probabilities exactly.

    We also study the problem of computing the expected reward (or cost) of runs until reaching the final states, where rewards are assigned to individual runs by computable reward functions.

  • Monday May 8, 13:15, room 1537:
    Cryptography in mobile networks
    (Mats Näslund, Ericsson Research)

    Cryptography in mobile networks has over the last 15 years gone from security-by-obscurity to a more sound approach of using publicly scrutinized algorithms. I will give a brief history of cryptography in GSM and UMTS, and then focus on some quite interesting new algorithms for UMTS that have recently been developed by ETSI SAGE. In particular, the new integrity algorithm is based on an (unconditionally) provably secure construction. It is based on quite old but nice (and easy) results by Carter and Wegman, which for some reason have not started to see wider deployment until recently.

  • Tuesday May 2, 13:15, room 1537:
    CoverTranslator - from Haskell to First Order Logic
    (Patrik Jansson, CSE Department, Chalmers University of Technology)

    The Cover project at Chalmers has been developing systems (theories, languages, libraries and tools) for software verification of Haskell programs. I will give a quick overview of the Cover project and present CoverTranslator in a little more detail. The translator takes as input Haskell programs with properties (defined in an embedded language), translates these into first order clauses and uses off-the-shelf FOL provers to prove the properties.

  • Thursday March 23, 13:15, room 1537:
    Cryptographically Sound Theorem Proving
    (Christoph Sprenger, Department of Computer Science, ETH Zurich)

    Tools for security protocol verification are traditionally based on Dolev-Yao models, which give the adversary complete control over the network and assume cryptography to be perfect. Recently, much research has been devoted to underpinning such symbolic protocol models with sound cryptographic foundations (possibly relaxing the perfect cryptography assumption).

    In this talk, I will describe a faithful embedding of the Dolev-Yao-style model of Backes, Pfitzmann, and Waidner (CCS 2003) in the theorem prover Isabelle/HOL. This model provides strong soundness guarantees in the sense of reactive simulatability: essentially arbitrary security properties proved in the symbolic model carry over to the cryptographic realization and this holds under active attacks and in arbitrary protocol environments. The main challenge in designing a practical formalization of this model is to cope with the complexity of providing such strong guarantees. We have reduced this complexity by abstracting the model into a sound, light-weight formalization that enables both concise property specifications and efficient application of our proof strategies and their supporting proof tools. This yields the first tool-supported framework for symbolically verifying security protocols that enjoys the strong cryptographic soundness guarantees provided by reactive simulatability.

  • Monday March 13, 13:15, room 1537:
    Compositional Verification of Sequential Programs with Procedures
    (Dilian Gurov, Theory Group, KTH CSC)

    I present a method for algorithmic, compositional verification of control flow based safety properties of sequential programs with procedures. The application of the method involves three steps: (1) decomposing the desired global property into local properties of the components, (2) proving the correctness of the property decomposition by using a maximal model construction, and (3) verifying that the component implementations obey their local specifications. I shall consider safety properties of the control flow behaviour of programs, as well as of the control flow structure.

    The compositional verification method builds on a technique proposed by Grumberg and Long who use maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. The generalisation of the maximal model technique to programs with recursion requires a refinement, since maximal applets are only guaranteed to exist for structural but not for behavioural properties. I therefore present a mixed, two-level approach where local assumptions are structural, while the global guarantee is behavioural.

    The proposed verification method is applicable to arbitrary sequential programs with procedures. It is evaluated on an industrial case study taken from the smart card area. By separating the tasks of verifying global and local properties the method supports secure post-issuance loading of applets onto a smart card.

  • Monday February 27, 15:15 (NB! Not the usual time!), room 1537:
    Introduction to information flow analysis
    (Mads Dam, Theory Group, KTH CSC)

    In computer security, information flow analysis concerns the problem of determining whether, and, potentially, how much, information is flowing across security boundaries. Confidentiality and integrity, for instance, are easily modelled as information flow problems: For confidentiality the problem concerns flow of secret data to public domains, and for integrity the problem is dual, to prevent flow of insecure data to secure domains. In the talk I introduce the research area, state of the art and open issues, and cover some recent work in the area, including some by the speaker.

  • Monday February 13, 13:15, room 1537:
    Cryptographic Protocol Logic. A Synthetic Approach.
    (Simon Kramer, EPFL)

    I present my current work on CPL, a logic for reasoning about cryptographic protocols. CPL establishes truth on the grounds of evidence-based knowledge and spans the modal dimensions of knowledge, norms, space, and time.

    The contribution of my work is twofold:

    • cryptographically speaking, it is to formally define the meaning of cryptographic states of affairs in a cryptographically intuitive way, and to exhibit the hypotheses at the meta-level under which this is possible;
    • logically speaking, it is to define the new paradigms of evidence-based epistemic and spatio-temporal logic, and to illustrate these paradigms on the example of CPL.

  • Thursday January 26, 9:15, room 1537:
    Ontology Based Higher-Level Fusion
    (Mieczyslaw M. Kokar, Department of Electrical and Computer Engineering, Northeastern University, Boston)

    Higher-level fusion involves estimation of abstract entities - sometimes called "situations" - that can be represented as relations among objects, both physical and conceptual. Unlike features of physical objects, features of relations are not directly measured by any sensors. Instead, the existence of a relation is derived from a domain theory relevant to a specific scenario. In this talk, both theoretical and practical aspects of situation awareness and higher-level information fusion will be discussed. First, a motivational example will be given to demonstrate the importance of relations and to introduce the concept of situation. Then a formal mathematical definition of situation will be formulated and mapped to an ontological framework. This will be followed by a presentation of some methodological techniques and some technologies that are needed for establishing an ontological approach to higher level fusion processing. In conclusion, directions for both applications and research in the areas of ontologies and higher-level fusion will be discussed.

  ---

  TCS Seminar Series Autumn 2005

  • December 20, 13:15, room 1537:
    Spam fighting and The Complexity of Pebbling Graphs
    (Moni Naor, Weizmann Institute of Science)

    Consider the following simple technique for combatting spam:

    If I don't know you, and you want your e-mail to appear in my inbox, then you must attach to your message an easily verified "proof of computational effort", just for me and just for this message.

    To apply this approach one needs to be able to come up with computational problems where solving them requires significant expenditure of resources while verifying a solution can be done easily. In this talk I will introduce this approach and concentrate on the choice of computational problems for which most of the work is in retrieving information from memory. In particular I will describe the connection to pebbling problems.

    (Joint work with Cynthia Dwork and Hoeteck Wee.)

  • September 19, 10:15, room 1537:
    A compositional natural semantics and Hoare logic for low-level languages
    (Tarmo Uustalu, Institute of Cybernetics, Tallinn)

    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, based on a paper at SOS 2005.)

  • September 15, 13:15, room 1537:
    Web services security
    (Alan Abdulrahman)

    As the surrounding world changes, IT systems grow and become more complex. By providing everything in terms of service modules to internal and external users of an organization, these service modules can easily be regrouped and exchanged to provide new forms of services adapted to the new situation. This is the idea of service-oriented architectures. A set of specifications that provide means to communicate in a platform- and language-independent manner, are grouped under the concept of Web services, and provide a realization of serviceoriented architectures. Web services facilitate communication between partner organizations with entirely different underlying IT infrastructures by exchanging XML messages in a standardized manner.

    To address security in Web services environments, another set of specifications are being developed that goes under the name Web services security. These specifications include mechanisms for securing single messages, establishing and brokering trust relationships between organizations, putting security capabilities and constraints on Web services, establishing security contexts, federating identities across partner organizations, stating privacy policies, and subjecting Web services to fine-grained access control.

    This seminar will present in more detail the specifications that comprise Web services security. No more than basic knowledge on computer security mechanisms is required.

  ---

  TCS Seminar Series, spring 2005

  • June 17, 10:15, room 4329 (seminar room at Media):
    Efficient Publicly Verifiable Mix-net for Long Inputs
    (Jun Furukawa, NEC Corporation, Japan)

    A mix-net is a multi-party protocol that takes a list of cryptotexts and outputs the list of corresponding cleartexts in random order. No individual mix-server knows the secret key of the cryptosystem used or the resulting random permutation. The main application of mix-nets is to implement electronic elections.

    We propose here the first efficient publicly verifiable hybrid mix-net. In order to achieve this goal, we have newly developed an IND-ME-CCA secure scheme of multiple encryption using hybrid encryption and a perfect zero-knowledge argument for shuffle-and-decryption of ElGamal ciphertexts. Although the resulting mix-net does not provide full public verifiability of the hybrid decryption in the case when a user and a mixer collude, the best adversary can do is to switch the input between a valid and an invalid one. The resulting scheme is efficient enough to treat large scale electronic questionnaires of long messages as well as voting with write-ins. The scheme is provably secure if we assume random oracles, semantic security of a one-time symmetric-key cryptosystem, and intractability of decision Diffie-Hellman problem.

  • June 15, 13:15, room 1537:
    Answering distance queries in directed graphs using fast matrix multiplication
    (Uri Zwick, Tel Aviv University, Israel)

    Let G=(V,E,w) be a weighted directed graph with integer edge weights of absolute value at most M. We show that G can be preprocessed in O*(Mn^w) time, where w<2.376 is the exponent of fast matrix multiplication, such that subsequently each distance d(u,v) in the graph can be computed exactly in O(n) time. As a very special case, we obtain an O*(Mn^w) time algorithm for the SINGLE SOURCE SHORTEST PATHS (SSSP) problem for directed graphs with integer weights of absolute value at most M. For sufficiently dense graph, with edge weights that are not too large, this improves upon the O*(mn^{1/2}log M) time algorithms of Gabow and Tarjan, and Goldberg.

    Joint work with Raphael Yuster.

  • May 25, 10:30, room 1537:
    Information Fusion from Databases, Sensors and Simulations - a Research Program in Cooperation with Industry
    (Sten F. Andler, University of Skövde)

    The University of Skövde is embarking on a research program, funded by the Knowledge Foundation, Sweden, in the area of Information Fusion from Databases, Sensors and Simulations. Information fusion entails the combination of data from multiple sources, to generate information that cannot be derived from the individual sources. There are several reasons for focusing on this. The area is of strategic importance for industry, defense, and public administration areas such as health care. A large number of industrial partners are supporting and participating in the development of the area. This work is related to two former programs, Mechatronic Systems and Learning Systems, previously funded by the Knowledge Foundation. Several research groups at the University of Skövde are active in different aspects of information fusion, adding to the strength to the program. The program covers the entire spectrum from sensors to decision support, i.e., from technical to human (cognitive and organizational) aspects, where decisions need to be based on different sources of information or where time is a critical factor and the decision support needs to be of highest possible quality, given the available information. Examples of the latter are when a company needs to act before a competitor does, or when a fighter pilot needs to act before his adversary does, i.e., when it is necessary to get inside the competitor's decision loop.

    The talk does not require prior knowledge of information fusion.

    • Slides (4.8 Mb, PDF format)
  • March 23, 13:15, room 1537:
    Controlled Linear Programming for Infinite Games
    (Henrik Björklund, Uppsala University)

    The controlled linear programming problem (CLPP) is a combinatorial optimization problem. An instance consists of a number of linear constraints of a certain form. A controller is allowed to select and discard constraints according to simple rules, with the goal of maximizing the optimal solution to the resulting linear program.

    The CLPP captures and generalizes parity, mean payoff, discounted payoff, and simple stochastic games. For its most general version, the exact complexity is still unknown, but several rich subclasses can be shown to belong to NP intersection coNP. In this talk we use linear algebra to characterize the properties of such subclasses, and prove a number of new results. We also identify sufficient conditions for a class to be solvable in randomized subexponential time.

  • March 11, 14:00, room 4523:
    Anonymous credentials
    (Jan Camenisch, IBM Zurich)

    A credential system allows users to obtain credentials from organizations and demonstrate possession of these credentials. An anonymous credential system further ensures that per se different transactions by the same user cannot be linked. Therefore anonymous credential systems are one of the corner stones to protect users' privacy in electronic transactions.

    This talk discusses anonymous credentials systems and generic yet efficient constructions for them.

  • March 7, 13:15, room 1537:
    Semantical investigations into BAN-like logics
    (Mads Dam, IMIT/KTH, joint work with Mika Cohen, IMIT/KTH)
    

    BAN-logic is an epistemic logic for verification of security protocols proposed by Burrows, Abadi and Needham in the late 80'es. From a practical point of view, BAN logic has turned out to be quite successful: Reasoning about cryptographic protocol in terms of principals knowledge is arguably very natural, and moreover, BAN logic produces short and informative derivations which can reveal quite subtle protocol errors. However, despite quite a number of attempts, the semantics of BAN logic has remained problematic. In the talk we pinpoint the rule of normality, essentially monotonicity of the epistemic modality, as the chief culprit: This rule is validated by all proposed semantics we know of, but by adding it to BAN logic intuitively absurd statements become derivable from intuitively correct ones without much trouble. To overcome this problem we propose to adopt an idea from counterpart semantics, namely to generalize the epistemic accessibility relation from a relation between local states to a relation between pairs of messages and local states, by systematically renaming content which is cryptographically inaccessible. We use this idea to build a new semantics for BAN logic which we claim avoids the problems of the previous semantics, and we show how the idea can be used to build semantics for richer logics up to and including first-order BAN logic. The latter is interesting, in particular, since it provides a framework in which existing semantics can be compared. Finally, if there is time, we will discuss soundness of the proposed cryptographic counterpart semantics.

  • January 18, 10:15, room 1537:
    Share conversion, pseudorandom secret-sharing and applications to secure distributed computing
    (Ivan Damgård, joint work with Ronald Cramer and Yuval Ishai)

    We present a method for converting shares of a secret into shares of the same secret in a different secret-sharing scheme using only local computation and no communication between players.

    We show how this can be combined with any pseudorandom function to create, from initially distributed randomness, any number of Shamir secret-sharings of (pseudo)random values without communication. We apply this technique to obtain efficient non-interactive protocols for secure computation of low-degree polynomials, which in turn give rise to other applications in secure computation and threshold cryptography. For instance, we can make the Cramer-Shoup threshold cryptosystem by Canetti and Goldwasser fully non-interactive, or assuming initially distributed randomness, we can compute any function securely in 2 rounds of communication.

    The solutions are practical only for a relatively small number of players. However, in our main applications the number of players is typically small, and furthermore it can be argued that no solution that makes a black-box use of a pseudorandom function can be more efficient.

  ---

  TCS Seminar Series, autumn 2004

  • 22 November, 13:15, room 1537:
    Difunctorial Semantics of Object Calculus: Towards Algebra of Objects
    (Johan Glimming, TCS/NADA)

    I will give an introduction to Abadi and Cardelli's object calculus, a typed system similar to simply typed lambda calculus but where objects, rather than functions, are the primitive syntactic entities. I give a denotational model for the first order object calculus (without subtyping) in the category pCpo of cpos and partial maps. The key novelty of this new model is its extensive use of recursively defined types, supporting self-application, to model objects. At a technical level, this entails using some sophisticated techniques such as Freyd's algebraic compactness to guarantee the existence of the denotations of the object types. The key feature/complexity is the mixed variance functors which are needed to model object types.

    I will show that a canonical recursion operator is inherent in this semantics. This operator can be useful in object-oriented programming: both in algebraic/coalgebraic formal methods and in capturing recurring abstractions in actual programs. The usefulness of the operator is witnessed by giving a straightforward translation of algebraic datatypes into so called wrapper classes. The talk concludes by comparing with Abadi and Cardelli's per semantics and by discussing current and future work.

    The work reported here is joint work with Neil Ghani at University of Leicester.

  • 25 October, 13:15, room 1537:
    Semidefinite programming
    (Anders Forsgren, KTH)

    Semidefinite programming has attracted interest in the computational complexity community as a tool for providing lower bounds on optimal values of certain combinatorial optimization problems. It has also become an important tool for solving many design problems in control and communications theory.

    The aim of this talk is to give an introduction to semidefinite programming. We start with a discussion on linear programming and duality. These results are then generalized to semidefinite programming, with discussion on important differences. The ability to solve semidefinite programs efficiently has been enhanced quite significantly by the development of interior methods. We give a basic description of interior methods. Finally, a few application examples are discussed.

  ---

  TCS Seminar Series, spring 2004

  • 7 May, 14:15, room 1537:
    Primitive Sets in Number Fields for Absolutely Optimal Black Box Secret Sharing
    (Ronald Cramer, BRICS, joint work with H.W. Lenstra Jr. and M. Stam.)

    A black box secret sharing scheme (BBSSS) for a threshold access structure is a linear secret sharing scheme that works for any finite abelian group. Introduced by Desmedt and Frankel, the problem has been rigourously analyzed by Cramer and Fehr.

    BBSSS can be based on number fields with certain properties. The approach by Desmedt and Frankel relies on number fields with large Lenstra constant, i.e.,number fields over which a "large" invertible Vandermonde matrix exists. The best known choices for these number fields lead to BBSSS with expansion factor O(n), where n is the number if players. The expansion factor corresponds to the length of each share, i.e., the number of group elements received from the dealer by each player. The solution of Cramer and Fehr achieves expansion factor O(log n), which is asymptotically optimal. It relies on low-degree number fields over which a pair of "large" Vandermonde matrices exists whose determinants are co-prime.

    We propose a new approach which aims at achieving an absolutely optimal solution. Our approach is based on low-degree number fields containing a "large primitive set." We give some experimental as well as some theoretical results.

  • 16 February, 10:15, room 1537:
    Optimization versus counting
    (Alex Samorodnitsky, Hebrew University of Jerusalem, joint work with Alexander Barvinok)

    There are two closely related algorithmic problems which we want to address. Given a finite set X and a cost function W on its elements, one may be interested in computing the cost of X - the total cost of its elements. The other question is to find an element of X of largest cost.

    For our purposes we must and will assume that the set X in question is endowed with a combinatorial structure that allows us to answer one of these questions efficiently, for any cost function W. Can this be of any use for the other question?

    It is not hard to see that if we can count (i.e. compute the total cost of X), then optimization becomes easy. For instance, it is possible to solve the Assignment problem (finding a maximal-weight perfect matching in a bipartite graph) by computing appropriate determinants. What about the other direction?

    It turns out that in a fairly general setting the two problems are 'equivalent'. This means that given an ability to optimize over a set one can estimate the total cost of the set. In fact, the estimates so obtained will be sufficiently precise to allow optimization.

    The proofs use several tools from probability and statistics, such as the concentration of measure in product spaces, large deviations, asymptotics of order statistics etc.

  • Måndagen 2 februari, 14:15, rum 1537:
    En (ganska) enkel krets som (oftast) sorterar
    (Hans Block)

    Seminariet refererar en artikel från 1990 av Tom Leighton och C. Greg Plaxton.

    Artikeln beskriver en parallell sorteringsmetod som bygger på den s.k. fjärilsturneringen. I denna får 2^k deltagare under k omgångar möta motståndare med samma mönster av förluster och segrar. Därför får spelare av liknande styrka tävla mot varandra, vilket bäddar för en snabb turnering.

    På k omgångar blir fjärilsturneringen inte färdig. Artikeln ger exakta uppskattningar av hur stor andel av indatapermutationerna som ger utdata med måttliga fel i sorteringsordningen.

    Genom att dela upp utdata från fjärilsturneringen i block och använda andra sorteringsmetoder på dessa skapar författarna en sorteringskrets som med mycket hög sannolikhet sorterar rätt.

    Den informationsteoretiska undre gränsen är 2 lg n - o(lg n) omgångar. Leighton - Plaxtons algoritm är 10-potenser bättre än tidigare rekord och tar 7,44 lg n omgångar. Går det att göra bättre?

  ---

  TCS Seminar Series, autumn 2003

  • Måndagen 15 december, 14:15, rum 1537:
    Bounded-Concurrent Secure Two-Party Computation in a Constant Number of Rounds
    (Rafael Pass, joint work with Alon Rosen)

    The original setting in which secure two-party protocols were investigated allowed the execution of a single instance of the protocol at a time. A more realistic setting, however, is one which allows the concurrent execution of protocols. In the concurrent setting, many two-party protocols are executed at the same time, involving many parties which may be talking with the same (or many) other parties simultaneously. This setting presents the new risk of a coordinated attack in which an adversary controls many parties, interleaving the executions of the protocols and choosing messages based on other partial executions of the protocol.

    In this work we consider the problem of constructing a general protocol for secure two-party computation in a way that preserves security under concurrent composition. In our treatment, we focus on the case where an a-priori bound on the number of concurrent sessions is specified before the protocol is constructed (a.k.a. bounded concurrency). We make no set-up assumptions.

    Lindell (STOC 2003) has shown that any protocol for bounded-concurrent secure two-party computation, whose security is established via black-box simulation, must have round complexity that is strictly larger than the bound on the number of concurrent sessions. In this talk I will show how to construct a (non black-box) protocol for realizing bounded-concurrent secure two-party computation in a constant number of rounds. The only previously known protocol for realizing the above task required more rounds than the pre-specified bound on the number of sessions (despite usage of non black-box simulation techniques).

    An extended abstract is available from the author's homepage http://www.nada.kth.se/~rafael/.

  • Måndagen 1 december, 14:15, rum 1537:
    More Efficient Queries in PCPs for NP and Improved Approximation Hardness of Maximum CSP
    (Lars Engebretsen, joint work with Jonas Holmerin)

    In the PCP model, a verifier is supposed to probabilistically decide if a given input belongs to some language by posing queries to a purported proof of this fact. The probability that the verifier accepts an input in the language given a correct proof is called the completeness c; the probability that the verifier rejects an input not in the language given any proof is called the soundness s. For a verifier posing q queries to the proof, the amortized query complexity is defined by q / log_2(c/s) if the proof is coded in binary. It is a measure of the average ``efficiency'' of the queries in the following sense: An ideal query should preserve the completeness and halve the soundness. If this were the case for all queries, the amortized query complexity would be exactly one.

    Samorodnitsky and Trevisan (STOC 2000) gave a q-query PCP for NP with amortized query complexity (1 + 2/sqrt{q} + epsilon) for any constant epsilon > 0. In this paper, we examine to what extent their result can be sharpened. In particular, we consider the dependency between the probability that a proof of an incorrect statement is accepted and the number of queries posed to the proof oracle.

    Our main result is a PCP for NP that queries q positions in the proof and has amortized query complexity (1 + sqrt{2/q} + epsilon). As an immediate corollary, we also obtain an improved hardness of approximation result for the Maximum q-CSP problem. As can be seen, our improvements are in the lower order term. It is, however, not possible to improve the amortized query complexity much more unless P=NP; a consequence of a result due to Trevisan (Algorithmica, 21(1):72--88, 1998) is that unless P=NP no PCP verifier for NP that queries q positions in the proof can have amortized query complexity 1 + 1/(q-1).

    Our improved construction uses the layered label cover problem recently introduced by Dinur et al. (STOC2003); based on such a label cover problem we devise a new ``outer verifier'' that allows us to construct an ``inner verifier'' that uses the query bits more efficiently than earlier verifiers.

  • Måndagen 17 november, 14:15, rum 1537:
    Effektiv aritmetik i ändliga kroppar av liten udda karaktäristik
    (Per Austrin)

    Vi studerar problemet att göra effektiva beräkningar (på binär hårdvara) i GF(p^n), där p är ett litet primtal skiljt från 2. Vissa primtal (t.ex. 3 och 5) av denna typ är av speciellt intresse i en del nya kryptosystem baserade på elliptiska kurvor. Utöver detta är problemet naturligtvis intressant ur ett rent teoretiskt perspektiv.

    Huvudidén är att operera på flera element i GF(p) parallellt genom att stoppa dem i samma maskinord. Motsvarande knep i GF(2^n) är både välkänt och tacksamt, eftersom addition här motsvaras av XOR.

    Vi ger övre gränser (samt ev. något handviftande argument om undre gränser) för hur mycket utrymme som behövs för varje GF(p)-element för att vi ska kunna operera på dem parallellt (d.v.s. väsentligen hur många vi kan klämma in i ett maskinord), och presenterar några prestandajämförelser från en faktisk implementation.

  • 27 oktober, 14:15, rum 4329 (Observera rummet, seminarierum vid media):
    Nyckel-revokerings protokoll
    (Mattias Johansson)

    Ett problem i samband med kommunikation inom grupper är att dynamiskt kontrollera medlemskap i gruppen, d.v.s. att lägga till nya medlemmar samt att utesluta gamla medlemmar. T.ex. vill man se till att före detta medlemmar inte längre kan lyssna på kommunikationen, och detta sköts med hjälp av kryptografiska nycklar. Så länge gruppen är liten kan man lösa detta genom att skicka ut nya nycklar till alla kvarvarande medlemmar på ett förhållandevis enkelt sätt, men när gruppstorleken växer blir detta snabbt mycket komplext och ohanterligt.

    Vi kommer att titta lite närmare på några av de protokoll som finns för att lösa detta problem, både naiva och mer effektiva. Bland de mer effektiva kan nämnas två som får extra mycket uppmärksamhet: Subset Difference (SD) och Logical Key Hierarchy (LKH). Inom ramen för en föreslagen verklig tillämpning, frågar vi oss också vilka krav det ger på revokerings protokollet och om det i dagsläget finns något praktiskt användbart alternativ till detta.

  • 26 September, 10:30, D35:
    Another attack on A5/1
    (Thomas Johansson, Lunds Tekniska Högskola)

    A5/1 is a stream cipher used in the GSM standard. Several time-memory trade-off attacks against A5/1 have been proposed, most notably the attack by Biryukov, Shamir and Wagner, which can break A5/1 in seconds using huge precomputation time and memory. We present a completely different attack on A5/1, based on ideas from correlation attacks. Whereas time-memory trade-off attacks have a complexity which is exponential with the shift register length, the complexity of the proposed attack is almost independent of the shift register length. Our implementation of the suggested attack breaks A5/1 in a few minutes using 2-5 minutes of conversation.

  ---

  TCS Seminar Series, spring 2003

  • 10 February, 13:00, room 1537:
    Språkteknikforskning på Nada eller Sagan om de fem oeniga taggarna
    (Viggo Kann och Jonas Sjöbergh, NADA, KTH)

    Första delen av seminariet kommer att ägnas åt en översikt över språkteknologiforskningen på Nada från 90-talets rättstavningsprojekt till dagens forskning om informationssökning med matrismetoder och grammatikgranskning för andraspråkssvenska. Som en del i det senare projektet ingår konstruktion av en supertaggare som med hjälp av fem oeniga taggare kan märka orden i en svensk text med ordklass och böjningsform bättre än någon av de enskilda taggarna. Om detta, och skapandet av en "extra oenig" taggare, handlar andra delen av seminariet.

  • 24 February, 13:00, room 1537:
    HUBIN: HUman Brain INformatics
    (Stefan Arnborg, NADA, KTH)

    Seminariet ger en överblick över detta medicinska tvärvetenskapliga forskningsprojekt som går ut på att skapa kunskap om sjukdomen schizofreni. Särskilt: Vilket problem ska lösas och vilka frågor är viktiga? Hur är det organiserat? Vilken information kan användas, och vad kan en datalog göra i sammanhanget? Inga specialistkunskaper förutsätts.

  • 10 Mars, 13:00, room 4523:
    (Icke-)approximerbarhet hos ekvationer över ändliga grupper
    (Jonas Holmerin, NADA, KTH)

    En ekvation över en ändlig grupp G är ett uttryck på formen w_1 w_2...w_k = 1_G, där varje w_i är en variabel, en inverterad variabel, eller konstant från G. En sådan ekvation är satisfierbar om det går att tilldela variablerna värden från G på ett sådant sätt att likheten realiseras.

    I detta seminarium behandlas problemet att samtidigt satisfiera så många som möjligt av en familj av ekvationer över en ändlig grupp G. Vi presenterar ett bevis för att det är NP-svårt att satisfiera mer än en andel 1/|G| av det optimala antalet ekvationer, eller med andra ord att problemet är NP-svårt att approximera inom |G|-epsilon för varje epsilon > 0. Motsvarande resultat var tidigare känt enbart för Abelska grupper (Håstad 2001).

    I seminariet skissar vi på en koppling mellan problemet att satisfiera maximalt antal ekvationer och så kallade PCPer ("Probabilistically Checkable Proofs"), som kan ses som ett slags spel mellan två personer, en verifierare och en bevisare, där bevisaren vill övertyga verifieraren om något påstående. Vi konstruerar ett sådant spel som motsvarar optimeringsproblemet ovan, och för att analysera detta spel använder vi sedan representationsteori för ändliga grupper.

    Arbetet har utförts tillsammans med Lars Engebretsen och Alexander Russell.

  • 24 Mars, 15:15, room 1537:
    Rekonsiliering och ortologianalys
    (Jens Lagergren, SBC/NADA, KTH)

    Att jämföra olika arters arvsmassa ger möjlighet att studera evolutionära mekanismer samt att överföra kunskap om en art till kunskap om en annan, tex från modellorganismer till människan. Tiden sedan ett par arter divergerade, eller mer generellt arträdet (det kantviktade träd som beskriver evolutionen av en mängd arter), är mycket relevant vid denna typ av jämförelser. Genduplikationer är en typ av mutation vars roll i skapandet av nya funktioner inte är klarlagd men trots detta är central i definition av "samma funktion" (ortologi).

    Vi ska titta på en probabilistisk modell för genduplikationer där ett genträd växer fram inuti ett arträd. En rekonsiliering är en beskrivning av en sådan framväxt. Givet ett arträd samt ett genträd så är likelihooden för en rekonsiliering sannolikheten att det är den rätta rekonsilieringen. Det visar sig att vi kan beräkna likelihooden m.h.a. dynamisk programmering. För att uppskatta posteriorifördelningen över rekonsilieringar så använder vi Markov Chain Monte Carlo tekniker.

  • 7 April, 13:00, room 1537:
    Bevisbar säkerhet och svåra predikat
    (Gustav Hast, NADA, KTH)

    Seminariet kommer handla om svåra predikat. Givet en funktion f och ett predikat P så är P svårt om det inte finns en algoritm som kan gissa värdet P(x), givet värdet av f(x), bättre än en slumpgissning. Vi kommer att gå igenom en känd konstruktion av ett svårt predikat som baseras på en godtycklig enkelriktad funktion (Goldreich och Levin, STOC '89).

    Konceptet svåra predikat kommer bland annat till användning när man ska bevisa säkerheten hos en pseudoslumptalsgeneratorer (PSG), ett viktigt kryptografiskt primitiv. Utdata från en PSG ska inte kunna skiljas från slump av motståndare som är begränsade av en viss tidsåtgång. Bevisgången är att reducera problemet att förutsäga värdet av ett svårt predikat till problemet att "knäcka" PSG:n. Här är effektiviteten hos reduktionen viktig eftersom den relaterar direkt till hur kraftfulla motståndare beviset fungerar på. Vi kommer även att ta upp en effektivare reduktion för specifika, men vanligt förekommande, användningsområden för PSG:er (Hast, EUROCRYPT 2003).

  • 28 April, 13:00, room 1537:
    Constructing Programs with Bird-Meertens Formalism
    (Johan Glimming, NADA, KTH)

    In this seminar we present Bird Meertens formalism, a mathematical tool for the construction of generic (datatype-parametric) programs. We define the formalism starting from the category FUN of sets and total functions, and explain how recursive datatypes are represented by fixpoints of functors. We define catamorphism and anamorphism as fundamental building blocks in the formalism, and then turn to concrete examples of program derivation. We conclude by describing our current research in the area.

  • 12 May, 13:00, room 1537:
    Reproducerbarhetsanalys av funktionella hjärnbilder
    (Jesper Fredriksson, NADA, KTH)

    Funktionell hjärnbildforskning har på relativt kort tid etablerats som ett stort forskningsområde med målet att skapa förståelse om det sista outforskade organet i människokroppen. Med hjälp av en PET eller fMRI scanner undersöker man mönster i förändringar av tex blodets syresättning.

    Men att dra slutsatser av den uppmätta signalen från scannern har visat sig svårt, av flera anledningar, och graden av reproducerbarhet mellan experiment är därför ofta dålig. I slutfasen av det europeiska databasprojektet NeuroGenerator (www.neurogenerator.org) försöker vi därför hitta statistiska metoder för att analysera graden av reproducerbarhet för insamlade PET och fMRI experiment.

    Under seminariet kommer jag att presentera problemet och gå igenom metoder som används för analysen av enstaka experiment, samt hur vi inom projektet attackerar problemet att göra en sammantagen analys av flera experiment som borde uppvisa gemensamma funktionella komponenter.

  • 26 May, 13:00, room 1537:
    Kvantinformationsteori
    (Göran Einarsson, S3, KTH)

    Informationsteori för kommunikation med kvantobjekt, t ex fotoner, har rönt stor uppmärksamhet under senare år. Kanalkapacitet för en sådan kommunikationskanal har studerats och felkorrigerande koder har presenterats. Seminariet behandlar principerna för kvantkommunikation illustrerad med en rad exempel. Tyngdpunkten ligger på transmission av klassiska data (vanliga ettor och nollor). Överföring av hemlig information (kvantkryptering) beskrivs.

  • 10 June, 13:00, room 1537:
    On the Complexity of Sphere Decoding in Digital Communications
    (Joakim Jalden, S3, KTH)

    Sphere Decoding, originally an algorithm to find vectors of short length in lattices, has recently been suggested by a number of authors as an efficient algorithm to solve various maximum likelihood (ML) detection problems in digital communication. Often the algorithm is referred to as an algorithm of polynomial complexity, and some papers have previously been published in communication literature in support of this claim. This is a somewhat surprising result, especially since the ML detection problem, in general, is known to be NP-hard. However, as will be argued in this talk by making some assumptions on the detection problems, these claims are probably not correct and the complexity of the algorithm is instead exponential

    It will in this talk be argued that, although always exponential, the complexity is strongly dependent on some parameters of the communication system, such as for example the signal to noise ratio (SNR). This will be done by first briefly discussing the differences between the detection problem and the related lattice problem to show what assumptions can be made about the detection problem. It will then be outlined how these assumptions lead to an exponential lower bound on the complexity of the algorithm. Also, numerical examples will be given to show the effect of different parameters on the complexity. Special attention will be given to how the algorithm benefits from a high SNR.

  ---

  TCS Seminar Series, autumn 2002

  • 10 December, 10:15, room 1537:
    On Some Approximation Algorithms of Magnús Halldórsson
    (Uri Feige, Weizmann Institute, Israel)

    Several approximation algorithms will be presented. A common theme for these algorithms is that they were either designed by Magnús Halldórsson (perhaps with coauthors), or are based on ideas that appeared in work of Magnús. Another common theme is that the algorithms have clever but simple proofs of correctness. Among the algorithms presented will be a recent algorithm with the current best approximation ratio for finding a maximum clique in a graph.

  • 15 November, 14:15, room E2:
    PRIMES is in P
    (Johan Håstad, NADA, KTH)

    Att avgöra om ett givet tal är ett primtal är ett grundläggande problem som dessutom är mycket viktigt bland annat i kryptografiska tillämpningar. Nyligen visade Agarwal, Kayal och Saxena att problemet går att lösa i deterministisk polynomisk tid; tidigare fanns algoritmer som krävde probabilistisk polynomisk tid samt algoritmer som bara kunde visas fungera korrekt under antagandet att vissa, obevisade, matematiska satser är sanna.

    Agarwals, Kayals och Saxenas resultat har fått stor uppmärksamhet över hela världen och är av stor teoretisk betydelse. I det här seminariet kommer vi att ge en bakgrund till problemet, beskriva dess lösning och till sist diskutera vilken betydelse resultatet har, både från ett teoretiskt och ett praktiskt perspektiv.

  ---

  TCS Seminar Series, spring 2002

  • 4 June, 14:15, room 1537:
    Approximationsalgoritmer för villkorsfamiljer på två variabler
    (Lars Engebretsen, NADA, KTH)

    En villkorsfunktion på två variabler, dvs en funktion från D×D till {0,1}, är r-reguljär ifall det för varje fix tilldelning till den ena variabeln finns exakt r tilldelningar till den andra variabeln som gör att villkoret är satisfierat. Genom att välja en slumpvis tilldelning till alla variablerna i en instans av ett r-reguljärt villkorsproblem gan man uppfylla en förväntad andel r/d av alla villkor, där d är storleken på domänen D.

    Vi använder semidefinit programmering för att konstruera en algoritm som uppfyller en förväntad andel r/d + Omega(d^-4) av det optimala antalet villkor. Arbetet har utförts tillsammans med Venkatesan Guruswami vid University of California at Berkeley.

  • 27 May, 14:15, room 1537:
    Handelsresandens problem i asymmetrisk graf
    (Anna Palbom, NADA, KTH)

    Handelsresandens problem med symmetrisk kostnadsfunktion är ett klassiskt datalogiproblem. Det är NP-svårt att lösa exakt, men när kostnadsfunktionen uppfyller triangelolikheten ger Christofides algoritm (1976) en lösning i polynomisk tid med vikt högst en faktor 3/2 från optimum.

    Versionen med asymmetrisk kostnadsfunktion som uppfyller triangelolikheten är inte lika välstuderad. Jag kommer att ge en översiktlig beskrivning av tidigare resultat och diskutera olika möjligheter till forskning kring handelsresandens problem med asymmetrisk kostnadsfunktion. Inga förkunskaper krävs.

  • 13 May, 15:00, room 4523:
    Tröskelkretsar och kommunikationskomplexitet
    (Mikael Goldman, NADA, KTH)

    Inom kretskomplexitet försöker man visa att problem är svåra genom att visa att det krävs stora kretsar för att lösa dem. Hur kraftfull en krets är beror, förutom storleken, på vilken typ av beräkningselement (grindar) kretsen är uppbyggd av.

    En majoritetsgrind med n indata ger utdata 1 om mer än hälften av indatabitarna är 1 och ger utdata 0 annars. Tröskelgrinden är en generalisering av majoritetsgrinden. Den beräknar en viktad summa av indatabitarna och ger utdata 1 om summan är större än ett visst tröskelvärde. Exempelvis kan man med en tröskelgrind jämföra två binärkodade heltal och avgöra vilket som är störst.

    Tröskelkretsar av konstant djup och polynomisk storlek har visat sig vara ganska kraftfulla, till skillnad från kretsar med AND- och OR-grindar med samma begränsningar på storlek och djup. De är de enklaste "naturliga" kretsar för vilka man inte kunnat visa några starka undre gränser förutom i vissa mycket begränsade fall (väsentligen för majoritetskretsar av djup två).

    Seminariet kommer att handla om en del av de övre och undre gränser som finns för tröskelkretsar. I samband med det kommer jag också att ta upp en annan beräkningsmodell där två eller flera spelare ska evaluera en funktion tillsammans. Kruxet är att ingen ensam spelare har tillgång till hela indatat, och målet är att evaluera funktionen genom att skicka så få och så små meddelanden som möjligt till andra deltagare. Kommunikationskomplexitet är ett användbart verktyg i många delar av komplexitetsteori, och i vårt fall visar det sig att problem som har hög kommunikationskomplexitet också kräver stora majoritetskretsar av djup två.

  • 22 April, 14:15, room 1537:
    Statistisk grammatikgranskning
    (Johnny Bigert, NADA, KTH)

    Grammatikgranskare är ofta användbara verktyg när man skriver stora mängder text. Traditionella språkgranskningsprogram (såsom Granska) hittar stavfel genom uppslagning i lexikon och grammatikfel genom att matcha skribentens text mot regler. Vissa vanliga typer av fel förblir dock oupptäckta eftersom de inte lämpar sig för att beskriva med regler och lexikon. Ett exempel på en sådan feltyp är stavfel som resulterar i befintliga ord.

    Trots att grammatik till sin natur är nära knutet till regler visar det sig att statistik kan hjälpa oss med dessa feltyper. Från stora mängder text kan man bygga statistik över vilka konstruktioner som är grammatiska i språket. Denna information används sedan för att avgöra vilka grammatiska konstruktioner som är osannolika i den text som ska grammatikgranskas.

    En statistisk grammatikgranskare har utvecklats tillsammans med Ola Knutsson på Nada. Jag kommer att berätta om de bakomliggande teorierna och hur statistisk grammatikkontroll kan komplettera en traditionell grammatikgranskare. En testversion finns integrerad i Granska på Granskaprojektets hemsida.

  • 15 April: Inget seminarium pga kurs.

  • 8 April: Viggo Kann har pedagogikseminarium 15:15 i D41.

  • 25 March, 14:15, room 1537:
    Bandbredd kontra frihet i interna videosystem
    (Lars Engebretsen, NADA, KTH)

    Om man på exempelvis ett hotell tillhandahåller filmer på en internkanal är det vanligt att man har en fix programtablå. Som gäst vill man däremot själv kunna välja när man ska titta på en viss film och man vill inte behöva vänta två timmar på nästa utsändning av filmen bara för att man råkat missa första kvarten.

    I det här seminariet kommer jag att prata om ovanstående problem ur ett datalogiskt perspektiv. Den modell jag kommer att behandla bygger på att det finns en central utsändningskälla och tunna klienter i varje TV-mottagare. Problemet blir då att tillhandahålla flexibilitet för tittarna utan att det går åt alltför mycket bandbredd i nätet.

    De resultat jag presenterar är frukterna av ett samarbete med Madhu Sudan vid MIT.

  • 11 March, 14:15, room 1537:
    Approximerbarheten hos problemet Minimum Hitting Set
    (Jonas Holmerin, NADA, KTH)

    Antag att vi har en mängd X och en familj C av delmängder till X, och vi vill välja ut en så liten delmängd S av X som möjligt under bivillkoret att varje mängd i C har något element med i S.

    Detta problem kallas för Minimum Hitting Set och är NP-svårt att lösa exakt. När ett problem är svårt att lösa är exakt är det naturligt att försöka hitta en lösning som är ganska bra. Vi säger att en algoritm approximerar ett problem inom en faktor c om den producerar en lösning som är högst en faktor c större än den optimala. Hur lätt det är att hitta approximativa lösningar varierar enormt mellan olika NP-svåra problem. Ett viktigt problem inom teoretisk datalogi är att utreda olika problems approximationsegenskaper.

    Det är känt att generella Minimum Hitting Set är rejält svårt att approximera. I detta seminarium koncentrerar vi oss på Minimum Hitting Set där mängderna i familjen C alla har samma storlek. Om mängderna har storlek k, säg, går detta problem att approximera inom en faktor k med en enkel algoritm. När k=2 är problemet ekvivalent med det välkända problemet Minimal Hörntäckning. Det tycks naturligt att problemt blir svårare när k växer, men upp till alldeles nyligen kunde man inte visa starkare icke-approximationsresultat för k>2 än för k=2.

    Vi diskuterar utveckligen för detta problem och visar att när k är högst 4 så är problemet NP-svårt att approximera inom en faktor 2.

  ---

  TCS Seminar Series, spring 2000

  • 13 June, 15:15, room 1537:
    Construction of Optimal Gadget Reductions
    (Gunnar Andersson, NADA, KTH)

    Reductions have played an important role in theoretical computer science since the development of the theory of NP-completeness. They have also been used in the domain of approximation algorithms. One such use is to transfer lower bounds, usually derived from probabilistic proof systems, from the original problem to other problems. In this context the cost of the reduction is important - a smaller cost leads to a stronger inapproximability result. In this talk we discuss the problem of finding the cheapest reductions and focus on the class of gadget reductions. It turns out that it in many cases is possible to obtain the best possible reductions by solving linear programs. Many strong inapproximability results have been derived using this technique.

  • 6 June, 13:15, room 1537:
    Probabilistic Verification of Multiple-Valued Functions
    (Elena Dubrova, Department of Electronics, KTH)

    This talk will describe a probabilistic method for verifying the equivalence of two multiple-valued functions. Each function is hashed to an integer code by transforming it to a integer-valued polynomial and the equivalence of two polynomials is checked probabilistically. The hash codes for two equivalent functions are always the same. Thus, the equivalence of two functions can be verified with a known probability of error, arising from collisions between inequivalent functions. Such a probabilistic verification can be an attractive alternative for verifying functions that are too large to be handled by deterministic verification methods.

  • 30 May, 15:15, room 1537:
    Some optimal inapproximability results
    (Johan Håstad, NADA, KTH)

    Using very efficient probabilistically checkable proofs (PCP) for NP we prove that unless NP=P, some simple approximation algorithms for basic NP-hard optimization problems are essentially optimal. In particular given a SAT formula with exactly 3 variables in each clause it is not hard to find an assignment that satisfies a fraction 7/8 of the clauses. We prove that (upto an arbitrary epsilon > 0) this is the best possible for a polynomial time approximation algorithm.

    In this talk we concentrate on the problem of given a linear system of equations mod 2, to satisfy the maximal number of equations. This problem is easy to approximate within a factor of 2 and we prove that this is essentially tight. This result is obtained by constructing a PCP that uses logarithmic randomness, reads 3 bits in the proof and accepts based on the exclusive-or of the these bits. This proof system has completeness 1-epsilon and soundness 1/2+epsilon, for any constant epsilon > 0.

  • 23 May, 15:15, room 1537:
    Strong Lower Bounds on the Approximability of Coloring
    (Lars Engebretsen, NADA, KTH)

    We describe how the reduction from PCPs to Maximum Clique can be extended to give hardness result for Coloring.

  • 16 May, 15:15, room 1537:
    Clique is Hard to Approximate
    (Jonas Holmerin, NADA, KTH)

    We discuss hardness results for Maximum Clique under different assumptions.

  ---

  TCS Seminar Series, autumn 1999

  • 15 december, 15:15, room E3:
    Efficient Manipulation of Boolean Functions with OBDDs
    (Christoph Meinel, Abteilung Informatik, Universität Trier)

    One of the main problems in chip design is the huge number of possible combinations of individual chip elements, leading to a combinatorial explosion as chips become more and more complex. New key results in theoretical computer science and in the design of data structures and efficient algorithms can be applied fruitfully here. The use and application of ordered binary decision digrams (OBDDs) has led to dramatic performance improvements in many computer-aided design projects. The talk provides an introduction to this interdisciplinary research area with an emphasis in computer-aided circuit design and verification.

  • 8 december, 15:00, room 1537:
    Svensk grammatikkontroll med både statistiska och lingvistiska metoder
    (Johan Carlberger och Viggo Kann, Nada, KTH)

    Om man ska få datorn att hitta grammatikfel i svenska texter så räcker det inte med att mata in Svenska Akademiens nya grammatik. Nej, bäst resultat har vi faktiskt fått genom att avstå från att göra en fullständig grammatisk analys av varje mening och istället uttnyttja ett par icke-lingvistiska metoder. Först ska varje ord i texten taggas, det vill säga märkas med ordklass och böjningsform. Detta gör vi med statistiska metoder och en Markovmodell. 97% av orden får rätt tagg och hela 91% av orden som inte finns i lexikonet taggas rätt. Sedan matchas en stor uppsättning granskningsregler mot den taggade texten, och ut kommer en lista med hittade grammatikfel och andra språkfel. I seminariet kommer vi att beskriva hur taggningen och regelmatchningen kan göras effektivt.

  • 24 November, 15:00, room 4523:
    Fourier and Abel in cooperation
    (Lars Engebretsen, Nada, KTH)

    In his work on the stationary heat distribution in a unit disc, Fourier introduced the method of expressing functions as series involving trigonometric functions. In Fourier's case, the functions were functions from the unit circle in R² to C, but the concept can be generalized. In this talk, we show that the approach can also be used for functions in the space L²(G), i.e., the space of functions from some finite Abelian group G to C.

  • 10 November, 15:00, room 1537:
    Sorting in time O(n log log n)
    (Stefan Nilsson, Nada, KTH)

    A fast algorithm for the "standard sorting problem" is presented. It sorts n word-sized integers on a unit-cost RAM in O(n log log n) worst-case time. The algorithm appeared in a rather inaccessible paper ("Sorting in linear time?" by A. Andersson, T. Hagerup, S. Nilsson, and R. Raman, STOC'95) but is actually quite simple.

  • 27 October, 15:00, room 1537:
    Bayes Rules!
    (Stefan Arnborg, Nada, KTH)

    Aristoteles beskrev induktionsproblemet - att generalisera från observationer - och erkände Sokrates som den som identifierade problemet. Det har varit centralt på olika sätt under hela filosofins historia. Bayes och Laplace kvantifierade osäkerheten i induktion med sannolikheter i Bayesiansk tolkning. Idag ser vi en ökande mängd 'intelligenta' datorbaserade system som gör observationer och försöker tolka dem, och Bayes har fått konkurrens av flera alternativa metoder. Därför är grundvalarna för induktion och inferens fortfarande högaktuella.

    Cox (Am Jour of Phys., 1946) försökte visa att Bayesianism är oundviklig om man vill räkna konsistent med osäker information. Iden är att alla rimliga alternativa osäkerhetsmått kan skalas om så att de omskalade osäkerheterna kombineras med multiplikation, som sannolikheter för oberoende storheter. Hans arbete har prisats och kritiserats i omgångar sedan dess. Speciellt har hans antaganden att osäkerhet graderas i ett kontinuum och att osäkerheter måste kombineras med en två gånger differentierbar funktion kritiserats. Antagandena föranleddes av Cox bevismetod och har senare mildrats.

    Vi har visat att det finns goda skäl att betrakta Bayesianism som oundviklig även i modeller med ett ändligt antal grader av osäkerhet, och med en oändlig men inte tät mängd osäkerheter. Några antaganden måste dock göras som inte förefaller helt oundvikliga. Dessa hänger samman med problemets natur och inte med den bevismetod som används, vilket framgår av motexempel. Vi kallar antagandena förfiningsbarhet, strikt monotonicitet och separerbarhet. För att bevisa våra satser använder vi dualitet och en utveckling av bevismetoder som använts av Janos Aczel för associativitetsekvationen. I de fall våra antaganden inte gäller kan man få olika varianter av possibilistisk logik och, som gränstagningsoperationer, icke-monoton logik.