08/04/2014: Talk by Frank Kelly (Cambridge University)

Title: Efficient advert assignment
Time: 14:00
Location: Conference room, building Alpha
Type: Research result
Speaker: Frank Kelly
Abstract: 
In current Ad-auctions, there is an information asymmetry between the platform and advertisers: the platform typically knows more than an advertiser about the search being conducted, such as information about the searcher. Hence the platform can potentially choose prices and an allocation that depends on the platform’s additional information. In contrast, the advertiser has to rely on more coarse-grained information, perhaps just the search terms of a query together with a crude categorization of the searcher.

We show that the information asymmetry can be used to develop a simple mechanism for advert assignment and pricing that incentivizes truthful bidding and encourages convergence to a unique Nash equilibrium that is socially optimal.

This is joint work with Peter Key and Neil Walton.

Short Bio: 
Frank Kelly is Professor of the Mathematics of Systems in the University of Cambridge, and Master of Christ’s College. He was elected a Fellow of the Royal Society in 1989, and a Foreign Member of the National Academy of Engineering in 2012. In 2013 he was awarded a CBE for services to mathematical sciences.
His main research interests are in random processes, networks and optimization. He is especially interested in applications to the design and control of networks and to the understanding of self-regulation in large-scale systems.

Frank Kelly has received several prizes for his work. In 1979 he won the Davidson Prize of the University of Cambridge. In 1989 he was awarded the Guy Medal in Silver of the Royal Statistical Society. He was awarded the 1991 Lanchester Prize of the Institute for Operations Research and the Management Sciences, and in 1997 the Naylor Prize of the London Mathematical Society. In 2005 he received the IEEE Koji Kobayashi Computers and Communications Award, in 2008 the John von Neumann Theory Prize of INFORMS, in 2009 the SIGMETRICS Achievement Award and the Gold Medal of the Association of European Operational Research Societies, in 2011 the Beale Medal of the Operational Research Society, in 2013 the INFORMS Saul Gass Expository Writing Award and in 2015 the Alexander Graham Bell Medal of the IEEE. He has been awarded Honorary Doctorates by Heriot-Watt University and by Eindhoven University of Technology.

He served as Director of the Statistical Laboratory in the University of Cambridge from 1991 to 1993. He has served on the Scientific Board of HP’s Basic Research Institute in Mathematical Sciences, the Scientific Council of EURANDOM, the Conseil Scientifique of France Telecom, and the Council of the Royal Society. He has chaired the Advisory Board of the Royal Institution/University of Cambridge Mathematics Enrichment Project, and the Management Committee of the Isaac Newton Institute for Mathematical Sciences.

He spent the academic year 2001-2 as a visiting professor at Stanford University. From 2003 to 2006 he served as Chief Scientific Adviser to the United Kingdom’s Department for Transport. He was chair of the Council for the Mathematical Sciences from 2010 to 2013, and is a member of the RAND Europe Council of Advisors.

07/04/2014: Talk by Pietro Ferrara (IBM Research)

Title: MorhpDroid: Fine-grained Privacy Verification
Time: 14:00
Location: Meeting Room, building Zeta
Type: Research result
Speaker: Pietro Ferrara
Abstract: 
Mobile devices are rich in sensors, such as a Global Positioning System (GPS) tracker, microphone and camera, and have access to numerous sources of personal information, including the device ID, contacts and social data. This richness increases the functionality of mobile apps, but also creates privacy threats. As a result, different solutions have been proposed to verify or enforce privacy policies. A key limitation of existing approaches is that they reason about privacy at a coarse level, without accounting for declassification rules, such that the location for instance is treated as a single unit of information without reference to its many fields. As a result, legitimate app behaviors — such as releasing the user’s city rather than exact address — are perceived as privacy violations, rendering existing analyses overly conservative and thus of limited usability.

In this talk, I will present MorphDroid, a novel static analysis algorithm that verifies mobile applications against fine-grained privacy policies. Such policies define constraints over combinations
of fine-grained units of private data. Specifically, through a novel design, MorphDroid tracks flows of fine-grained privacy units while addressing important challenges, including (i) detection of
correlations between different units (e.g. longitude and latitude) and (ii) modeling of semantic transformations over private data (e.g. conversion of the location into an address).
We have implemented MorphDroid, and present a thorough experimental evaluation atop the 500 top-popular Google Play applications in 2014.
Our experiments involve a spectrum of 5 security policies, ranging from a strict coarse-grained policy to a more realistic fine-grained policy that accounts for declassification rules. Our experiments show that the gap is dramatic, with the most conservative policy detecting violations in 171 of the applications (34%), and the more realistic policy flagging only 4 of the applications as misbehaved (< 1%). In addition, MorphDroid exhibits good performance with an average analysis time of < 20 seconds, where on average apps consist 1.4M lines of code.

Short Bio: 
Pietro has been an IBM Research Staff Member in the group of Mobile Enterprise Software led by Marco Pistoia since July 2013. His main research interest is sound static analysis via abstract interpretation. In particular, he is currently working on various security (mostly confidentiality) properties of mobile (mostly Android) programs. Before joining IBM Research, Pietro was a lecturer at ETH of Zurich in the Programming methodology group under the supervision of Peter Mueller from April 2009 to July 2013. In this period, he developed Sample, a generic static analyzer developed in Scala that has been applied to a large variety of properties and programming languages. Previously (from October 2005 to May 2009), he was a PhD student at the Ecole Polytechnique of Paris and the Università Ca’ Foscari of Venice, under the join supervision of Radhia Cousot and Agostino Cortesi.

01/04/2014 – Talk by M. Squarcina and M. Tempesta

Title: Surviving the Web: A Journey into Web Session Security
Time: 14:00
Location: Meeting Room, building Zeta
Type: Survey of literature
Speaker: Marco Squarcina and Mauro Tempesta
Abstract: In this talk we describe and classify web security properties, attacks and security solutions. We focus on client-side attacks against web sessions, i.e., attacks that target honest user clients establishing a session with a remote web server. We identify general security properties representative of web session security and we highlight the properties violated by the different attacks. We then survey existing security solutions and mechanisms that prevent or mitigate the attacks: for each security solution, we also evaluate the impact on usability, the compatibility with existing web sites and the ease of deployment. Finally, we identify a list of sound principles that, to some extents, have been taken into account by the designers of the surveyed solutions. We believe that these principles could be helpful for the development of innovative solutions approaching web security in a more systematic and comprehensive way.

20/03/2015 – Talk by Mohammed Abbadi

Title: Designing games with high performances in Casanova
Time: 12:30
Location: Meeting Room, building Zeta
Type: Research Result
Speaker: Mohammed Abbadi
Abstract: Making games is expensive and resource consuming. These costs include development and maintenance. In software engineering, the efficient design of solutions (e.g. the encapsulation) have been largely studied and it has been shown taht they help developers to keep game code readable and maintainable. Because of the bad performance that these solutions exhibit, developers chose to avoid them for faster highly coupled implementations. We present Casanova, a domain specific language oriented to game development. In Casanova, developers are guided to write game code using encapsulation. Through dependency analysis on code and the use of reversed indexes, Casanova performs optimization on source code so that the generated code is fast. We show that the resulting code is readable, maintainable, and fast, to the advantage of developers with limited resources.

24/03/2015 – Talk by Nathalie Peyrard

Title: Reinforcement learning-based design of sampling policies under cost constraints in Markov random fields. Application to weed map reconstruction
Time: 11:00
Location: Meeting Room, building Zeta
Type: Research Result
Speaker: Nathalie Peyrard (INRIA Toulouse)
Abstract:
Weeds are responsible for yield losses in arable fields, whereas the role of weeds in agro-ecosystem food webs and in providing ecological services has been well established. Innovative weed management policies have to be designed to handle this trade-off between production and regulation services. As a consequence, there has been a growing interest in the study of the spatial distribution of weeds in crops, as a prerequisite to management. Such studies are usually based on maps of weed species. The issues involved in building probabilistic models of spatial processes as well as plausible maps of the process on the basis of models and observed data are frequently encountered and important. As important is the question of designing optimal sampling policies that make it possible to build maps of high probability when the model is known. This optimization problem is more complex to solve than the pure reconstruction problem and cannot generally be solved exactly.

A generic approach to spatial sampling for optimizing map construction, based on Markov random fields (MRF), is provided and applied to the problem of weed sampling for mapping. MRF offers a powerful representation for reasoning on large sets of random variables in interaction.In the field of spatial statistics, the design of sampling policies has been largely studied in the case of continuous variables, using tools from the geostatistics domain. In the MRF case with finite state space variables, some heuristics have been proposed for the design problem but no universally accepted solution exists, particularly when considering adaptive policies as opposed to static ones.The problem of designing an adaptive sampling policy in an MRF can be formalized as an optimization problem. By combining tools from the fields of Artificial Intelligence (AI) and Computational Statistics, an original algorithm is then proposed for approximate resolution. This generic procedure, referred to as Least-Squares Dynamic Programming (LSDP), combines an approximation of the value of a sampling policy based on a linear regression, the construction of a batch of MRF realizations and a backwards induction algorithm. Based on an empirical comparison of the performance ofLSDPwithexistingone-step-look-aheadsamplingheuristicsand solutionsprovidedbyclassicalAI algorithms, the following conclusions can be derived:

(i) a naïve heuristic consisting of sampling sites where marginals are the
most uncertain is already an efficient sampling approach;
(ii) LSDP outperforms all the classical approaches we have tested; and
(iii) LSDP outperforms the naïve heuristic approach in cases where sampling costs are not uniform over the set of variables or where sampling actions are constrained.

11/03/2015 – Talk by Robbe Block

Title: Spatial Fairness in Multi-Channel CSMA Line Networks
Time: 14:00
Location: Meeting Room, building Zeta
Type: Research Result
Speaker: Robbe Block (University of Antwerp)
Abstract:
In this talk we will consider a line of wifi-hotspots placed in a single line. Starting from earlier results, we will show the steady state of this system has a product form solution and using this product form, a fast method to calculate the per-hotspot throughput will be given. Furthermore, for a single channel setting it was shown in previous work that a simple formula could be used to achieve fairness among the different nodes in the network. It will be shown that the same formula still achieves fairness in the multi-channel setting in either heavy or low traffic conditions, but no such simple formula exists in general. However, through numerical experiments, we see that the fairness index of the multi-channel system still remains very close to one, meaning the simple formula eliminates most of the unfairness in the network.

04/03/2015 Talk by Filippo Cavallin

Title: Single TTL Cache with Reset under the Independent Reference Model
Time: 14:00
Location: Conference room, Building Alfa
Type: Research Result
Speaker: Filippo Cavallin
Abstract:
Cache systems based on a Time To Live (TTL) policy are becoming increasingly important especially in the field of Information-Centric Network design. In this kind of cache an element is kept in it unless it is not used (i.e., it does not receive any write/read request) for a certain period.
This model is less effective if there are some periods of inactivity of the system.
In this talk, after some brief explanations about G-Networks and PEPA language, we will evaluate the performance of a single TTL cache equipped with a refresh system that rejuvenates the timers of the elements stored. In this way we try to avoid the problem of under-utilization of the cache when traffic is low. We will show also that the equilibrium distribution function has a product-form expression under the Independent Reference Model. This allows us to efficiently compute the performance indices.

11/02/2015 Talk by Giordano Favro

Title: Graph easy classes of lambda terms
Time: 14:00
Location: Meeting room
Type: Research Result
Speaker: Giordano Favro
Abstract:
Lambda calculus is a formal systems which can also be used as an abstract programming language. It aims to describe some very general properties of programs in a very abstract setting. Objects of lambda calculus are the lambda terms and can be considered as computational processes. The problem of characterizing lambda-terms that represent an undefined computational process has interested researchers since the origin of lambda calculus:  we survey some results about this issue. In the second part of the talk we introduce the regular mute terms, a proper, decidable subset of the mute terms, a kind of lambda terms  that shows an high level of undefinedness. Graph models, a particular kind of models of lambda calculus, are introduced in order to present the main contribution of the talk: the set of regular mute terms is the union of an infinite number of non trivial graph easy sets.