Tag Archives: formal methods

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

27/04/2016 – Tutorial day

Tutorial day

The ACADIA research centre organisms a tutorial day on hot topics in computer science.
Date: 27/04/2016
Location: Conference room, building Alpha, Scientific campus


- 11:00-13:00  Dale Miller (Ecole Polytechnique, Paris, France): ”Communicating and trusting formal proofs”

- 14:00-17:00 Young Im Cho (Gachon Univ., Seoul, Korea): ”Intelligent IoT Platforms for Smart City”

Abstract 1 (Communicating and trusting formal proofs)

In the mist of feeling insecure with our electronic communications, we can take solace in the advice that we can “trust the math” behind cryptography. Faced with concerns over the safety of fly-by-wire planes and self-driving cars, we should be able to find solace in the fact that some parts of our safety critical systems have been proved formally correct: that is, we should be able to “trust the proof”. The
way formal proofs are built today, however, makes trusting them difficult. While proof assistants are used to build formal proofs, those proofs are often locked to that assistant. Formal proofs produced by one proof assistant cannot usually be checked and trusted by another proof assistant nor by a future version of itself. Thus, one of the components of the scientific method that ensures trust-reproducibility – is missing from proof checking.
The field of proof theory, as initiated by Gentian in the 1930′s, has identified a great deal of structure in formal proofs. Given recent developments in this topic, it is now possible to apply what we know
about proofs in theory to what we would like to have for proofs in practice. To that end, I will present the Foundational Proof Certificates framework for defining the semantics of proof evidence.
Since such definitions are executable, it is possible to build proof checkers that can check a wide range of formal proofs. In this scheme, the logic engine that executes such definitions is the only thing that needs to be trusted. Since such a logic engine is based on well-known computational logic topics, anyone can write a logic engine in their choice of programming language and hardware in order for them to build a checker they can trust. I will also overview some of the consequences of defining proofs in this manner: provers can become networked far more richly than they are currently and both libraries and marketplaces of proofs are enabled in a technology independent


Abstract 2 (Intelligent IoT Platforms for Smart City)

Machine-to-Machine communications (M2M) is a phenomenon that has been proceeding quietly in the background, and it is coming into the phase where explosion of usage scenarios in businesses will happen. Sensors, actuators, RFID/NFC tags, vehicles, and intelligent machines all have
the ability to communicate. The number of M2M connections is continuously increasing, and it has been predicted to see billions of machines interconnected in a near future. M2M applications provide
advantages in various domains from building, energy, healthcare, industrial, transportation, retail, security to environmental services. This fast-growing ecosystem is leading M2M towards a promising future, however M2M market expansion opportunities are not straight forward.
M2M is suffering from the highly fragmented vertical domain specific approach, which has increased the R&D cost in each specific domain. In fact, various vertical M2M solutions have been designed independently and separately for different applications, which inevitably impacts or even impedes large-scale M2M deployment. The existence of multiple manufacturers, the lack of a common M2M Service Capability Layer and no clarity about what can be achieved have all combined to leave the field of M2M communications closer to dream than reality.
To reduce the standardization gap which exist between M2M domains, the ETSI Technical committee M2M defined an end to end M2M service platform with the intermediate service layer that are key components of the horizontal M2M solution. This standards based platform follows a RESTful approach with open interfaces to enable developing services and applications independently of the underlying network, thus easing the deployment of vertical applications for an effective interoperability, and facilitating innovation across industries.
The following topics will be covered by the tutorial:
- IoT basics
- Smart City basics
- IoT international platform focusing on OneM2M reference model
- Components and model description for IoT platform
- Examples in detail
- Case studies and demonstration etc.

02/03/2016 – Talk by Filippo Cavallin

Title:  Cronization: a method to pass from Continuous Time to Discrete Time Automata
Time: 14:00
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Filippo Cavallin
Discrete and Continuous Time automata are important formalisms to model and analyze systems such queuing and telecommunication networks. The stationary performance analysis of these automata requires the computation of the steady-state distribution of their underlying Markov chains. Sometimes for the analysis is more convenient to pass from continuous to discrete time. The main methods are focused on the underlying Markov chains and not on the automatas. To preserve the transitions with labels and the synchronization between them, we will introduce a method to pass from a continuous time stochastic automaton (SA) to a probabilistic Input/Output automaton (PIOA). This method is a bijection from continuous to discrete time and it allows us to switch between the two different types of automata and it preserves the parallel composition.

27/10/2015 – Talk by Jean-Michel Fourneau (Université de Versailles Saint Quintin)

Title: Discrete Time Stochastic Automata Network with Steady-State Product Form distribution
Time: 13:00
Location: Meeting Room, building Zeta
Type: Research result
Speaker: Jean-Michel Fourneau
Abstract: We present some sufficient conditions for a discrete time Stochastic Automata Networks (SAN) to have a steady-state distribution which has a multiplicative form. The proofs are based on algebraic properties of the tensor operations associated with SAN. Some examples are given.
Bio sketch: J.M. Fourneau is Professor of Computer Science at the University of Versailles St. Quentin, France. He was formerly with Ecole Nationale des Telecommunications, Paris and University of Paris XI Orsay as an Assistant Professor. He graduated in Statistics and Economics from Ecole Nationale de la Statistique et de l’Administation Economique, Paris and he obtained is Ph.D. and his habilitation in Computer Science at the University of Paris XI Orsay in 1987 and 1991 respectively. He is the Head of the Performance Evaluation team within PRiSM laboratory at Versailles University and his recent research interests are algorithmic performance evaluation, Stochastic Automata Networks, G-networks, stochastic bounds, and application to high speed networks, and all optical networks.

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

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.

20/03/2014 – Talk by Paul-Andre Mellies

Title:  The free dialogue category with sums: an algebraic approach to game semantics
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Paul-Andre Mellies (CNRS, Paris Diderot))
In this talk, I will give a direct combinatorial description of the free dialogue category with sums
as a category with dialogue games as objects and with innocent strategies as morphisms.
I will then explain how to apply this result in order to construct a functor from the category
of dialogue games and innocent strategies to the category of coherence spaces and cliques.
One obtains in this way another proof of the positionality theorem of innocent strategies,
which establishes moreover that the halting positions of an innocent strategy form a clique.

27/11/2013 – Talk by Stefano Calzavara

Title:  Formalizing and Enforcing Web Session Integrity
Time: 11:00
Location: Meeting room
Type: Research Result
Speaker: Stefano Calzavara
Enforcing protection at the browser side has recently become a popular approach for securing web authentication, even when web application developers do not follow recommended security guidelines. Though interesting, existing attempts in the literature only address specific classes of attacks, and thus fall short of providing robust foundations to reason on web authentication security. In this talk we provide such foundations, by introducing a novel notion of web session integrity, which allows us to capture many existing attacks and spot some new ones. We then discuss FF+, a security-enhanced model of a web browser that provides a full-fledged and provably sound enforcement of web session integrity. We leverage our theory to develop SessInt, a prototype extension for Google Chrome implementing the security mechanisms formalized in FF+.   SessInt provides a level of security very close to FF+, while keeping an eye at usability and user experience.