[HGI-News] HGI-Seminar, Montag 16.04.2007: Formal Analysis of Security APIs

[Newsletter des Horst Görtz Instituts]

              Dr. Graham Steel, University of Edinburgh

            Montag 16. April 2007, 13:15 Uhr IC 4 / 39-41

                  Formal Analysis of Security APIs

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 code from gaining access to
the sensitive 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.



_____________________________________________________________________________
Die Webseite des HGI-Seminars mit allen Informationen zu vergangenen und
zukünftigen Vorträgen: http://www.hgi.rub.de/deutsch/lehrangebot/seminar.html