DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

Formal Analysis of Security APIs

Graham Steel PhD, Post Doctoral Research Associate,
University of Edinburgh

Monday (!), November 27th, Time: 15:00 - 16:00
IT University of Copenhagen, Rued Langgaards Vej 7, auditorium 3

Abstract:

Cash machines (ATMs) and other critical parts of the electronic payment infrastructure contain tamper-proof hardware security modules (HSMs), which protect highly sensitive data such as the keys used to obtain personal identification numbers (PINs). These HSMs have a restricted API that is designed to prevent malicious intruders from gaining access to the data. However, several attacks have been found on these APIs, as the result of painstaking manual analysis by experts such as Mike Bond and Jolyon Clulow.

At the University of Edinburgh, a project is underway to formalise and mechanise the analysis of these APIs. This talk will present some API attacks, and our efforts to generalise them and capture them formally, using theorem provers, protocol analysis tools, and the PRISM probabilistic model checker.

Scientific host: Carsten SchŘermann. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org