Project “Formal Specification for Secured Software System” has been approved!

The project entitled “Formal Specification for Secured Software System” has been approved for funding. We would like to congratulate prof. Agostino Cortesi who is the Italian principal investigator and prof. Nabendu Chaki who is the Indian principal investigator. The objective of the project is to investigate whether security policies of a (possibly safety critical) system could be integrated into the formal requirement specification using formal methods, in order to detect ambiguities and inconsistencies within the specification phase in Software development life-cycle. The funding will cover the costs of researchers’ mobility between India and Italy.

14/02/2017 – Talk by Ivan Stojic

Title: Algorithms for stationary analysis of stochastic Petri nets
Time: 12:30
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Ivan Stojic
Abstract:
Stochastic Petri nets (SPN) are a Markovian formalism for qualitative and quantitative analysis of discrete event dynamic systems. Among other uses, they have been used extensively in performance evaluation of telecommunication systems, computer systems and networks. Analysis of steady-state behaviour of an SPN model usually requires stationary analysis of a continuous-time Markov chain (CTMC) underlying the SPN, whose state space for many practical models is too large to be analysed by direct methods. This serious drawback is shared with many other modeling formalisms and is usually referred to as state space explosion. Usually simulation can be employed to analyse such models. An alternative is to restrict the SPN formalism to product-form SPNs, a class of nets whose unnormalised stationary probability distribution can be obtained in closed form, making stationary analysis much simpler. In this thesis we present algorithms for stationary analysis of SPN models based on efficient encoding of state spaces and transition functions by multi-valued decision diagrams, an efficient data structure. After a short introduction to SPNs and their steady-state analysis, we start with simulation of SPNs and present an algorithm for perfect sampling of SPNs that can be used to directly obtain samples from the stationary distribution. After this, we turn to product-form SPNs and present an algorithm for computation of normalising constant, needed for the normalisation of stationary probabilities in the analysis of product-form models.

15/02/2017 – Talk by Fabiana Zollo

Title: Social Dynamics on Online Social Media: A Data Science Approach
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Fabiana Zollo
Abstract:
Information, rumors, debates shape and reinforce the perception of reality and heavily impact public opinion. Indeed, the way in which individuals influence each other is one of the foundational challenges in several disciplines such as sociology, social psychology, and economics. In particular, on online social networks users tend to select information that is coherent to their system of beliefs and to form polarized groups of like-minded people –i.e, echo chambers– where they reinforce and polarize their pre-existing opinions. Such a context exacerbates misinformation, which has traditionally represented a political, social, and economic risk. In this talk we explore how we can understand social dynamics by analyzing massive data on Facebook. By means of a tight quantitative analysis on 376 millions users we characterize the anatomy of news consumption on a global scale. We show that users tend to focus on a limited set of pages (selective exposure) eliciting a sharp and polarized community structure among news outlets. Moreover, we find similar patterns around the Brexit –the British referendum to leave the European Union– debate, where we observe the spontaneous emergence of two well segregated and polarized groups of users around news oultets. Our findings provide interesting insights about the determinants of polarization and the evolution of core narratives on online debating, and highlight the crucial role of data science techniques to understand and map the information space on online social media. The main aim of this research stream is to identify non-trivial proxies for the early detection of massive (mis)informational cascades. Furthermore, by combining users traces we are able to draft the main concepts and beliefs of the core narrative of an echo chamber and its related perceptions.

21/12/2016 – Talk by Alvise Spanò

Title: Lw: a new general-purpose programming language
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Alvise Spanò
Abstract:
e introduce Lw, a new general purpose, statically typed, strict, impure, functional language supporting cutting-edge features and advanced forms of polymorphism for writing robust, reusable and succinct code. It integrates state-of-the-art advancements in the field of programming languages together with a number of novel bits which makes it ideal for writing big as well as small programs: each heavyweight declarative language construct offers an inferred lightweight counterpart, allowing programmers to design large software architectures that seamlessly coexist with more script-like code.

Among its highlights: type and kind inference, System-F types and first-class polymorphism, open-world overloading with automatic context-dependant resolution, implicit function parameters and controlled dynamic scoping, Generalized Algebraic Datatypes (GADTs), row types for polymorphic variants and records, powerful kind system supporting higher-order polymorphism and kind polymorphism, first-class modules and much more.

Resolution of type constraints is central to many language mechanisms, which, combined with overloading, leads to a form of static dispatching that can either be automatic or assisted by the programmer; dually, row-typed records are subject to dynamic dispatching by nature and enables structural subtyping – a.k.a. sound duck typing. And here lies one of Lw’s most notable and novel features: users can turn type constraints into records and viceversa anytime by using a pair of special inject/eject operators, converting a non-first-class entity which basically resembles a dictionary into a first-class record value, and the other way round. This makes two worlds communicate: the world of static resolution and the world of dynamic resolution. Languages out there typically do not define a clear symmetry in this respect; plus, a lot of boilterplate code is often required for switching between the two worlds, when possible at all.
In Lw this symmetry is crucial and explitly designed, encouraging code reuse.

20/12/2016 – Talk by Giovanni Bernardi

Title: Robustness against Consistency Models with Atomic Visibility
Time: 13:30
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Giovanni Bernardi
Abstract:To achieve scalability, modern Internet services often rely on distributed databases with consistency models for transactions weaker than serializability. At present, application programmers often lack techniques to ensure that the weakness of these consistency models does not violate application correctness. We present criteria to check whether applications that rely on a database providing only weak consistency are robust, i.e., behave as if they used a database providing serializability. When this is the case, the application programmer can reap the scalability benefits of weak consistency while being able to easily check the desired correctness properties. Our results handle systematically and uniformly several recently proposed weak consistency models, as well as a mechanism for strengthening consistency in parts of an application.

30/11/2016 – Talk by Moreno Ambrosin (University of Padova)

Title: Secure and Scalable Services for the Internet of Things, and Past and Ongoing Effort in the Security of Software-Defined Networking
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Moreno Ambrosin
Abstract:
In recent years, the advent of Internet of Things (IoT) is populating the world with billions of low cost heterogeneous interconnected devices. IoT devices are quickly penetrating in many aspects of our daily lives, and enabling new innovative services, ranging from fitness tracking, to factory automation. Unfortunately, their wide use, as well as their low-cost nature, make IoT devices also an attractive target for attackers, which may exploit them to perform DoS attacks, or violate the privacy of end users. Furthermore, the potentially very large scale of IoT systems makes the use of existing security solutions unfeasible.
In this talk I will give an overview of our research effort in defining secure and scalable protocols and mechanisms for IoT services, and in particular for: (1) efficient and secure device management at large scale (commands and software distribution, and device sanity check); and (2) privacy-preservation in three representative IoT-enabled services and tasks: location-based services, advanced metering infrastructures, and decentralized consensus in a multi-agent systems. Finally, in the last part of this talk I will briefly introduce past, and ongoing research work of our group in Software-Defined Networking security.

15/11/2016 – Talk by Andrea Marin

Title: Fair workload distribution for multi-server systems with pulling strategies
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Andrea Marin
Abstract:
In this talk we present the paper that has received the best paper award at the conference Valuetools 2016.

We consider systems with a single queue and multiple parallel servers. Each server fetches a job from the queue immediately after completing its current work. We propose a pulling strategy that aims at achieving a fair distribution of the number of processed jobs among the servers. We show that if the service times are exponentially distributed then our strategy ensures that in the long run the expected difference among the processed jobs at each server is finite while maintaining a reasonable throughput.
We give the analytical expressions for the stationary distribution and the relevant stationary performance indices like the throughput and the system’s balance.
Interestingly, the proposed strategy can be used to control the join-queue length in fork-join queues and the analytical model gives the closed form expression of the performance indices in saturation.

Best Paper Award Valuetools 2016

The paper entitled:
“Fair workload distribution for multi-server systems with pulling strategies”
authored by Andrea Marin and Sabina Rossi has been awarded with the “best paper award” at Valuetools 2016.

Congratulations to the authors!

08/11/2016 – Talk by Filippo Cavallin

Title: Multi-Step Discrete Time Process Algebra (MuPA)
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Filippo Cavallin
Abstract:
We consider Discrete Time Markov Chains with synchronous behaviour, i.e. models in which multiple events may occur at each recorded time in the model. This is based on a conceptual model in which the discrete times are sampling points when the system is observed and at each instant all events that have occurred since the previous observation point will be noted. We propose the first process algebra which is capable of capturing such systems and demonstrate its application to discrete time queues both in isolation and forming networks.

05/10/2016 – Talk by Stefano Calzavara

Title: Theory and Practice of CSP
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Stefano Calzavara
Abstract:Content Security Policy (CSP) is a recent W3C standard introduced to prevent and mitigate the impact of content injection vulnerabilities on websites. In this talk we present a systematic, large-scale analysis of the effectiveness of the current CSP deployment, focusing on four key aspects: browser support, website adoption, correct configuration and constant maintenance. Our analysis shows that browser support for CSP is largely satisfactory, with the exception of few notable issues, but unfortunately there are several shortcomings relative to the other three aspects. CSP appears to have a rather limited deployment as yet and, more crucially, existing policies exhibit a number of weaknesses and misconfiguration errors. Moreover, content security policies are not regularly updated to ban insecure practices and remove unintended security violations. We finally discuss how formal methods are an effective tool to substantiate the claims of our empirical evaluation.