^October November – 2011 ^December

In recent years the computing industry has been showing a growing interest in distributed computing frameworks as the only way to achieve the massive scale, high reliability and continuous availability that are required by enterprise data centers and cloud computing infrastructure. This talk will focus on research we did on the Virtual Synchrony framework of Birman and Jones. We created an axiomatic model for their framework that enables a great simplification of the description of failure behaviors in the cluster and very precise proofs of the correctness of their protocols.

Applying Software Engineering and Formal Verification Methods to Biological Systems Studies of biological systems are often facilitated by diagram models that summarize the current understanding of underlying mechanisms. The increasing complexity of our understanding of biology necessitates computational models that can extend these representations to include their dynamic behavior. I will present progress on foundations and tools, towards enabling biologists and modelers to construct high-level theories and models of biological systems using formal visual languages, capturing biological hypotheses, inferred mechanisms, and experimental results. I will describe some of the applications (assuming no background in biology) and outline challenges and future research directions.

In this talk I will present state of the art algorithms for solving combinatorial optimization tasks defined over graphical models (Bayesian networks, Markov networks, and constraint networks) and demonstrate their performance on a variety of benchmarks. Specifically I will present branch and bound and best-first search algorithms which explore the AND/OR search space over graphical models and will demonstrate the gain obtained by exploiting problem’s decomposition (using AND nodes), equivalence (by caching) and irrelevance (via the power of new lower bound heuristics such as mini-buckets). The impact of additional principles such as exploiting determinism via constraint propagation, the use of good initial upper bounds generated via stochastic local search and the variable orderings ideas may be discussed, as time permits. Current research is in extending the algorithms into distributed/parallel solving, anytime solutions, m-best solutions, and dvanced heuristic generations. Joint work with Radu Marinescu.

The current state of the art in the development of search methodologies is focused around the design of bespoke systems, which are specifically tailored to a particular situation or organisation.Such bespoke systems are necessarily created by human experts, and so they are relatively expensive. Some of the research at the ASAP research group, at the University of Nottingham, is concerned with how to build intelligent systems which are capable of automatically building new systems. In other words to automate some of the creative process, to make it less expensive by being less reliant on human expertise. In this talk, I will present some work we have recently published on the automatic design of heuristics, particularly for two dimensional stock cutting problems. The research shows that genetic programming can be used to evolve novel heuristics which are at least as good as human designed heuristics for this problem. Research into the automatic design of heuristics could represent a change in the role of the human expert, from designing a heuristic methodology, to designing a search space within which a good heuristic methodology is likely to exist. The computer then takes on the more tedious task of searching that space, while we can focus on the creative aspect of designing it.

The problem of multi-robot patrol has become a canonical problem in multi-robot, in which a team of mobile robots is required to jointly visit some target area in order to monitor change in state. The goal of the robots can vary from optimizing point-visit frequency, to maximizing the chances of detecting an adversary that tries to pass through the patrol path undetected. In this talk I will describe theoretical results that are used as a baseline for my work, in which strategies for the patrolling robots can be found efficiently based on, among others, a Markovian modeling of the world. I will then describe various adaptations of the theoretical results to handle real world constraints, among them description of new patrolling strategies, reevaluation of coordination restrictions, and development of new adversarial models.

Approximating an arbitrary graph by a simpler structure while preserving some properties of the original graph, is a very active research direction that has found numerous applications.In this talk we will discuss the problem of finding a spanning tree that preserves the distances of the original graph on average, up to a universal constant. Based on joint work with Ittai Abraham and Yair Bartal.

Detection and containment of unknown malware are challenging tasks. Typically the detection is performed by experts who use anomaly detection systems or Honeypots-based systems. Such a detection process is very slow and it is not suited for detection of rapidly propagating threats such as worms. In this research we propose to automate the detection process by introducing an innovative distributed framework for detection and containment of new malware. The framework consists of distributed agents that are installed in several client computers and a Centralized Decision Maker module (CDM) that interacts with the agents. The new detection process is performed in two phases. In the first phase agents detect potential malware on local machines and send their detection results to the CDM. In the second phase, the CDM builds a propagation graph for every potential malware. These propagation graphs are compared to known malware propagation characteristics in order to determine whether the potential malware is indeed a malware. All the agents are notified of a final decision in order to start the containment process. Another contribution of this study is a method for detecting new malicious executables locally. It is based on monitoring run-time system calls and comprises the following steps: (a) in an offline training phase, finding a set of (not necessary consecutive) system call sequences that are characteristic only to malicious files, when such malicious files are executed, and storing said sequences in a database; (b) in a real time detection phase, for each running executable, continuously monitoring its issued system calls and comparing them with the stored sequences of system calls within the database to determine whether there exists a match between a portion of the sequence of the run-time system calls and one or more of the database sequences, and when such a match is found, declaring said executable as malicious. In addition to the collaborative detection, the method can be used for independent (local) malware detection, replacing (or in addition to) traditional antivirus software.

Protection of personal information is one of the most challenging problems in emerging information society. The traditional approach, based on purely organizational protection seems to be insufficient – it became clear that personal data protection should be backed by technical mechanisms working in automatic way, independently of human behavior. One of the recent ideas in this area is restricted identification introduced by German authorities. New electronic personal identity documents in Germany are equipped with a cryptographic protocol that supports anonymous identification. The idea is based on the notion of independent sectors of activity. The cryptographic protocol implemented there provides unlinkable passwords created with strong asymmetric cryptography from a single secret key of the user. This approach differs from anonymous credentials in the sense that a single person may have only one pseudonym in a given sector for the lifetime of a given personal identity document. In particular, no Sybil attack is possible. We present related solutions for different anonymity scenarios, such as access to personal medical information or contacts with law enforcement authorities. Despite some differences these solutions build together a common framework for unlinkable authentication in different sectors. We also provide reduction proofs supporting unlinkability claims. joint work with: P.Kubiak, L.Krzywiecki, Jun Shao, M.Koza concern results presented at IEEE CCNC 2011 and to be presented at INTRUST 2011