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
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
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.

25/02/2015 Talk by Stefano Calzavara

Title: Compositional Typed Analysis of ARBAC Policies
Time: 14:00
Location: Meeting room
Type: Research Result
Speaker: Stefano Calzavara

Model-checking is a popular approach to the security analysis of ARBAC policies, but its effectiveness is hindered by the exponential explosion of the ways in which different users can be assigned to different role combinations. In this talk we propose a paradigm shift, based on the observation that, while verifying ARBAC by exhaustive state search is complex, realistic policies often have rather simple security proofs, and we propose to use types as an effective tool to leverage this simplicity. Concretely, we present a static type system to verify the security of ARBAC policies, along with a sound and complete type inference algorithm used to automate the verification process. We then introduce compositionality results, which identify sufficient conditions to preserve the security guarantees obtained by the verification of different sub-policies when these sub-policies are combined together: this compositional reasoning is crucial when policy administration is highly distributed and naturally supports the security analysis of evolving ARBAC policies. We evaluate our approach by implementing TAPA, a static analyser for ARBAC policies based on our theory, which we test on a number of relatively large, publicly available policies from the literature.

04/02/2015 – Talk by Wilayat Khan

Title: Web Session Security: Formal Verification, Client-Side Enforcement and Experimental Analysis
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Wilayat Khan

Web applications are the dominant means to provide access to millions of on-line  services and applications such as banking and e-commerce. To personalize users’  web experience, servers need to authenticate the users and then maintain their authentication state throughout a set of related HTTP requests and responses called a web session. As HTTP is a stateless protocol, the common approach, used by most of the web applications to maintain web session, is to use HTTP cookies. Each request belonging to a web session is authenticated by having the web browser to provide to the server a unique long random string, known as session identifier stored as cookie called session cookie. Taking over the session identifier gives full control over to the attacker and hence is an attractive target of the attacker to attack on the confidentiality and integrity of web sessions. The browser should take care of the web session security: a session cookie belonging to one source should not be corrupted or stolen or forced, to be sent with the requests, by any other source.

This research demonstrates that security policies can in fact be written down for both, confidentiality and integrity, of web sessions and enforced at the client side without getting any support from the servers and without breaking too many web applications. Moreover, the enforcement mechanisms designed can be proved correct within mathematical models of the web browsers. These claims are supported by

1) defining both, end-to-end and access control, security policies to protect web sessions;

2) introducing a new and using exiting mathematical models of the web browser extended with confidentiality and integrity security policies for web sessions;

3) offering mathematical proofs that the security mechanisms do enforce the security policies; and

4) designing and developing  prototype browser extensions to test that real-life web applications are supported.

28/01/2015 – Workshop on mobile agents and robots


January, 28th 9.30-12.30, Room 1, Bulding Z, Campus Scientifico


9.30-9.35 Workshop presentation.

9.35-10.20 Prof. Evangelos Kranakis Carleton University, Ottawa, Canada: “Evacuating Robots from an Unknown Exit in a Disk”.

Consider k mobile robots inside a circular disk of unit radius. The robots are required to evacuate the disk through an unknown exit point situated on its boundary. We assume all robots having the same (unit) maximal speed and starting at the centre of the disk. The robots may communicate in order to inform themselves about the presence (and its position) or the absence of an exit. The goal is for all the robots to evacuate through the exit in minimum time.

We consider two models of communication between the robots: in non-wireless (or localcommunication model robots exchange information only when simultaneously located at the same point, and wireless communication in which robots can communicate one another at any time. We study the following question for different values of k: what is the optimal evacuation time for k robots? We provide algorithms and show lower bounds in both communication models for k=2 and k=3 thus indicating a difference in evacuation time between the two models. We also obtain almost-tight bounds on the asymptotic relation between evacuation time and team size, for large k. We show that in the local communication model, a team of k robots can always evacuate in time 3 + (2Π)/k, whereas at least 3 + (2Π)/k – O(k^{-2}) time is sometimes required. In the wireless communication model, time 3 + Π/k + O(k^{-4/3}) always suffices to complete evacuation, and at least 3+ Π/k is sometimes required. This shows a clear separation between the local and the wireless communication models.


10.25-11.10 Prof. Danny Krizanc Wesleyan University, Middletown, CT, U.S.A.: “The Dynamic Map Visitation Problem: Foremost Coverage of Time-varying Graphs.”

We consider the Dynamic Map Visitation Problem (DMVP), in which a team of agents must visit a collection of critical locations as quickly as possible, in an environment that may change rapidly and unpredictably during the agents’ navigation. We apply recent formulations of time-varying graphs (TVGs) to DMVP, shedding new light on the computational hierarchy R ⊃ B ⊃ P of TVG classes by analyzing them in the context of graph navigation. We provide hardness results for all three classes, and for several restricted topologies, we show a separation between the classes by showing severe inapproximability in R, limited approximability in B, and tractability in P. We also give topologies in which DMVP in R is fixed parameter tractable, which may serve as a first step toward fully characterizing the features that make DMVP difficult.

11.10-11.40 coffee break (registration is required).

11.40-12.10 PhD students demos with LEGO MINDSTORMS Robots.

23/10/2014 – Talk by Laurent Vuillon (Université de Savoie)

Title: From tilings to fibers: bio-mathematical aspects of fold plasticity
Time: 14:00
Location: Meeting room
Type: Research Result
Speaker: Laurent Vuillon (Université de Savoie)
Protein oligomers are made by the association of protein chains via intermolecular amino acid interactions (interaction between subunits) forming so called protein interfaces. This talk proposes mathematical concepts to investigate the shape constraints on the protein interfaces in order to promote oligomerization. First, we focus on tiling the plane (2 dimensions) by translation with abstract shapes. Using the fundamental Theorem of Beauquier-Nivat, we show that the shapes of the tiles must be either like a square or like a hexagon to tile the whole plane. Second, we look in more details at the tiling of a cylinder and discuss its relevancy in constructing protein fibers. The universality of such “building” properties are investigated through biological examples.

18/09/2014 – Talk by Soumya Sen

Title: Integrating XML with Data Warehouse
Time: 14:00
Location: Meeting room
Type: Research Result
Speaker: Soumya Sen
XML is the most widely used language in web environment. Many of the organizations maintain their semi-structured data in XML format for e-commerce and internet based applications. These XML data which are used to manage OLTP data can be processed further for analytical processing. Integration of XML and data warehouse for the innovation of business logic and to enhance decision making has therefore emerged as a demanding area of research interest. 
XML is semi-structured model where as majority of the OLAP are maintained through relational model. Thus the conversion is preferably aimed at Relational OLAP (ROLAP). The majority of the research work in this field is based on conversion of single XML schema to star or snowflake schema. A significant improvement is to consider multiple XML schemas and possibly identifying fact constellation.
However a major problem in existing research is the use of other intermediate tool, data structure or middleware to convert XML into data warehouse. The use of this extra entity slows down the process. Eliminating the presence of this entity is a good research challenge. XQuery, the query language on XML could be efficiently used to meet the challenge. A state of the art framework is presented to formalize a standard syntactical structure to construct lattice of cuboids from XML data as well performing the common OLAP operations using only XQuery.    

16/09/2014 – Talk by Lucia Gallina

Title: Formal Models for the Analyisis of Cloud Computing
Time: 12:00
Location: Meeting room
Type: Research Result
Speaker: Lucia Gallina
Cloud Computing is a smart solution aiming at effectively sharing massive computational resources on-line between multiple users. The key benefits of Cloud computing is virtualisation, provisioning and elasticity: clients see an infinite amount of virtual machines which they can lease on demand, responding to short-term application load, thus eliminating significant purchase and maintenance costs of private high-end computational infrastructure which would remain underutilised during off peak periods. This new paradigm creates a profitable market for cloud vendors who can simultaneously run client virtual machines on the same data centers, taking advantage of clever scheduling and resource provisioning. In the last few years, cloud computing had a great impact, and today companies such as Google, Amazon and Microsoft implement cloud solutions. However, there are still many open issues that have to be taken in consideration.
One of the main challenges is to invent precise resource provisioning technology, which is crucial in guaranteeing high performance and low-cost services. Indeed, resource allocation is organized with a pay as you go model, and it is fundamental to add or remove resources at a fine grain, ensuring the final users the services they are asking for, without delays, but at the same time without falling into over-provisioning, i.e., the under utilisation of the resources, which is a critical factor influencing the costs.

23/07/2014 – Talk by Wilayat Khan

Title: Client Side Web Session Integrity as a Non-Interference Property
Time: 11:00
Location: Meeting room
Type: Research Result
Speaker: Wilayat Khan

Because of the stateless nature of the HTTP protocol, web applications
that need to maintain state over multiple interactions with a client have
to implement some form of session management: the server needs to know to
what ongoing session (if any) incoming HTTP requests belong. Sessions are
usually implemented by means of session cookies, which are unpredictable
random identifier generated by the server at the start of a session.

Sessions can be attacked at network (e.g. sniffing), implementation (e.g.
script injection) and application layers. The attacks at the first two
layers are well-understood problems with well-understood solutions,
however, the problem of application-level session integrity is not yet
well-understood. An attack at application layer happens when a page in the
browser send malicious requests to any of the servers that the browser
currently has a session with, and that request will automatically get the
session cookie attached and hence will be considered as part of a
(possibly authenticated) session by the server, leading to CSRF attacks.
Moreover, malicious requests can also be sent by scripts included in or
injected by an attacker into a page from the same origin.

In this work, we refined our previous ideas to the classical
noninterference property as known from information flow security and
designed an information flow control technique that can enforce session
integrity in a more permissive and fine-grained way than access control