Tag Archives: System Verification

03/12/2015 – Talk by Marco Squarcina

Title:  Run-time analysis of PKCS#11 attacks
Time: 13:30
Location: Acadia Lab, building Zeta
Type: Research Results
Speaker: Marco Squarcina
The goal of this talk is to report on the development of a tool aimed at the automatic detection of attacks against PKCS#11 devices. Instead of modifying or configuring the API, we propose a stateful run-time monitor which is able to track key usage over time, for the identification of operations that might result in the leakage of sensitive keys. We briefly report on the components developed for implementing the monitor and discuss new challenges and open issues.

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.

30/09/2013 – Talk by Giulia Costantini

Title: Lexical and Numerical Domains for Abstract Interpretation
Time: 10:00
Location: Meeting room
Type: PhD program result
Speaker: Giulia Costantini

The goal of this thesis is to contribute to the field of formal methods employed for the static verification of computer program properties. The context is the Abstract Interpretation framework, one of the various possible techniques to perform static analyses. In particular, we focus on the design of novel abstract domains to analyze the basic building blocks of computer programs: lexical and numerical variables, as well as relationships between variables. In order to provide experimental evidence of their actual applicability, we implemented our domains and we applied them to a suite of case studies.

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

25.01.2013 – Talk by Hoang Vu Tuan

Title: The PRISM tool and its applications
Time: 14:00
Location: Meeting room
Type: Tool presentation
Speaker: Hoang Vu Tuan

In this presentation, I will consider some models and show how it is possible to derive some meaningful properties by using the PRISM model checker. PRISM tool supports  four types of models whose underlying processes can be Discrete-time Markov chain (DTMC), Continuous-time
Markov chains (CTMC), Markov decision processes (MDP) and Probabilistic timed automata (PTA). For each of these classes, a set of properties can be analysed. The talk will rely on a case study to illustrate the PRISM functionalities. Specifically,  the Stable Matching problem will be addressed by applying the DTMC analysis.

10.01.2013 – Talk by Giovanni Bernardi

Title: Testing preorders for clients and peers

Date: 10/01/2012
Time: 1:00 pm
Location: Sala riunioni
Type: research talk
Speaker: Giovanni Bernardi (Trinity College, Dublin)

The must testing is a formalism that let us reason on the safety of  computations performed by two communicating parties; typically a  client (test) and a server (process). By using the must testing one can define three refinements that state when it is safe to replace servers, clients, or peers.
In this talk we explain the classic semantic characterisation of the must preorder for servers, and then we show how to generalise so as to characterise also the preorders for clients and peers.