Tag Archives: Security

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
Abstract:
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:
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
Abstract:

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)

Abstract:

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)

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