Tag Archives: Security

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.

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

16/04/2014 – Talk by Silvia Signorato

Title:  Le indagini informatiche nel procedimento penale: analisi, valutazioni, prospettive.
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Silvia Signorato

Nell’attuale società globalizzata l’informatica permea ormai quasi ogni ambito del reale. Pressoché inevitabile, quindi, che pure la criminalità si avvalga dell’informatica per la commissione di reati. Al riguardo, si pensi solo a phishing, pedopornografia on line, diffamazioni commesse su social network, cyberstalking, adescamento di minori in Internet, violazione di diritto d’autore, istigazione on line al suicidio, in un crescendo di reati che non può non destare allarme sociale. 

A fronte della commissione di simili reati, anche le indagini penali divengono informatiche e sempre più spesso gli elementi di prova sono rappresentati da digital evidence.
Il seminario intende offrire un quadro introduttivo al tema delle indagini informatiche nel procedimento penale.
In tale ottica, anzitutto verranno tracciate le coordinate della disciplina vigente in materia; in secondo luogo, saranno esaminate le più rilevanti questioni giuridiche che derivano dall’impiego dell’informatica nell’ambito delle indagini penali; infine, verranno evidenziate le inedite prospettive delle investigazioni informatiche.

19/03/2014 – Talk by Andriana E. Gkaniatsou

Title:  Towards the automated analysis of low-level cryptographic protocols
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Andriana E. Gkaniatsou (U. of Edinburgh)
In this talk we discuss the problem of the automated analysis of reversed engineered low-level cryptographic protocols. Such analysis is difficult, as most of such protocol implementations are proprietary and confidential.
Our proposal is to consider the analysis as an inference problem and use knowledge repair techniques to fix possible mismatches. We discuss our thoughts towards this problem, and some working examples based on real card implementations.

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.

20/11/2013 – Talk by Wilayat Khan

Title:  Automatic and Robust Client-Side Protection for Cookie-Based Sessions
Time: 11:00
Location: Meeting room
Type: Research Result
Speaker: Wilayat Khan
Abstract: Session cookies constitute one of the primary attack targets
against client authentication on the Web, hence modern web browsers
implement native protection mechanisms for them based on the Secure
and HttpOnly flags. While there is a general understanding about the
effectiveness of these defences, no formal result has so far proved about
the security guarantees they convey.

In this work, we have provided the first such result, with a mechanized
proof of non-interference assessing the robustness of the Secure and
HttpOnly cookie flags against both web and network attacks. We have
mechanized the proofs using the interactive theorem prover Coq.
Furthermore, we have developed CookiExt, a browser extension
that provides client-side protection against session hijacking based on
appropriate flagging of session cookies and automatic redirection over
HTTPS for HTTP requests carrying such cookies. Our solution improves
over existing client-side defences by combining protection against both
web and network attacks, while at the same time being designed so as
to minimise its effects on the user’s browsing experience.

22.03.2013 – Talk by Pedro Adão

Title: Computationally Sound Verification of the NSL Protocol via Computationally Complete Symbolic Attacker
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Pedro Adão

We show that the recent technique of computationally complete symbolic attackers  proposed by Bana and Comon-Lundh for computationally sound verification of security protocols is powerful enough to verify actual protocols.  In their work,  Bana and Comon-Lundh presented only the general framework, but they did not introduce sufficiently many axioms to actually prove protocols.We present a  set of  axioms—some generic axioms that are computationally sound for all PPT  algorithms, and two specific axioms that are sound for CCA2 secure encryptions—and illustrate the power of this technique by giving the first computationally sound  verification (secrecy and authentication) via symbolic attackers of the  NSL Protocol  that does not need any further restrictive assumptions about the  computational implementation. These axioms are entirely modular, and not particular to the NSL protocol hence can be reused in the proofs of security for many other security protocols.Joint work with Gergei Bana and Hideki Sakurada

Open postdoc fellowship

We are seeking to recruit a post-doc fellow to conduct integrative theoretical and experimental research in modelling principles and analysis techniques for distributed and pervasive systems.

Requirements: Applicants must hold a Ph.D degree in Computer Science or related subject before the application deadline. The successful candidate will submit a scientifically excellent research proposal,  relevant to the topics of the call, and display:

  • Scientific knowledge across the relevant subjects,
  • Technical competence and a strong publication record,
  • Team working skills,
  • Leadership experience,
  • Ability to organize her/him self and others.

Funding: is for one year, renewable, at approximately 24,000 Euro gross, including mobility allowances (that corresponds to around 21,000 Euro net). The fellowship is expected to start in May / June 2013

See this page for full detalis.

18.12.2012 – Talk by Michele Mazzucco

Title: Revenue Maximization Problems in Commercial Data Centers

Date: 18/12/2012
Time: 1:00 pm
Location: Sala riunioni
Type: industrial application
Speaker: Michele Mazzucco (Demonware, Dublin)


As IT systems are becoming more and more important, one of the main concerns is that users may face major breakdowns and eventually incur major costs if computing systems do not meet the expected performance requirements: customers expect reliability and performance guarantees, while under-performing systems loose revenues. For example, it has been reported that Amazon tried delaying the page generation by 100 ms and found out that even very small delays would result in substantial and costly drops in revenue (1% sales drop for 100 ms delay). In this talk I will discuss some performance models aiming at optimizing the revenue earned by IT providers running ‘jobs’ subject to Quality of Service (QoS) constraints. The presentation is divided into two parts. In the first part I will analyze a business model where the QoS guarantees are formally defined through Service Level Agreements (SLAs), and thus the provider is liable to pay a penalty every time the promised performance level is not met. Experimental results show that revenues can be dramatically improved by imposing suitable conditions for accepting incoming traffic, and that the proposed policies perform well under different traffic conditions.

In the second part of the presentation I will discuss two queueing models for power and performance. The main difference compared to the first part of the talk is that now the QoS is implicit, and thus customers simply leave the system (or wait) if it under-performs, while the provider also takes into account the energy consumed by servers when deciding how many servers to allocate.

Michele Mazzucco graduated in Computer Science at the University of Bologna and obtained his PhD at the University of Newcastle under the supervision of prof. Mitrani. His main reserach interests include models for the performance evaluation and optimization of data centers. He has published in major conferences and journals on topics such as cloud computing and green computing. Since 2012, he works for Demonware.

DemonWare is an Irish software development company and a subsidiary of Activision Blizzard. DemonWare’s products enable games publishers to outsource their networking requirements, allowing them to concentrate on playability. The organisation has offices in Dublin, Ireland; and Vancouver, Canada.Primary products developed by DemonWare include the “DemonWare State Engine” and “Matchmaking+”. The State Engine is a high-performance state synchronization C++ programming framework that eliminates the need to reinvent netcode multiplayer games. Matchmaking+ provides services for multiplayer games such as matchmaking, user profiling, and gaming statistics. DemonWare’s main product has been used to support the development of several online games of success, among which Call of Duty.

12.12.2012 – Tutorial by Stefano Calzavara

Title: An introduction to stochastic process algebras and quantitative security analysis

Date: 12/12/2012
Time: 3:00 pm
Location: Sala riunioni
Type: review of literature
Speaker: Stefano Calzavara (Ca’ Foscari, Venice)

Stochastic process algebras are a popular and convenient specification tool, which have proven successful in many applications from the areas of performance modeling, bioinformatics, and security. However, approaching the world of stochastic process algebras is a nontrivial task, since the very foundations of such models are rather peculiar and the well-known formal machinery of classical (non-deterministic) process algebras does not properly fit them. In this talk we analyze stochastic process algebras from the point of view of the programming languages community, and we try to motivate and understand some apparently weird design choices underlying their development. We then focus on an application of stochastic process algebras to security verification and we propose a personal understanding of the challenges behind such task. We argue that, as the foundations of stochastic process algebras depart from those of classical process algebras, also the approach to their verification may probably benefit from a change of perspective.

Prerequisites: Some notions on process algebras and formal methods may help in appreciating the contents, but the seminar is self-contained.