Séminaires
Séminaire du 17 décembre 2010
Lieu
ENS de Cachan, amphi Fonteneau (bâtiment d'Alembert): comment y aller
Programme
14h00-15h00: G. Steel (INRIA), "Attacking and Fixing PKCS#11 Security Tokens", Joint work with M. Bortolozzo, M. Centenaro, and R. Focardi
Abstract: We show how to extract sensitive cryptographic keys from a variety of commercially available tamper resistant cryptographic security tokens and smartcards, exploiting vulnerabilities in their RSA PKCS#11 based APIs. The attacks are performed by Tookan, an automated tool we have developed, which reverse-engineers the particular token in use to deduce its functionality, constructs a model of its API for a model checker, and then executes any attack trace found by the model checker directly on the token. We describe the operation of Tookan and give results of testing the tool on 18 commercially available tokens: 10 were vulnerable to attack, while the other 8 had severely restricted functionality. Response from manufacturers has varied from registering the vulnerability with MITRE and announcing a patch programmed (see e.g.http://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2010-3321) too a complete lack of response. We discuss how Tookan may be used to verify patches to insecure devices, and give a secure configuration that we have implemented in a patch to a software token simulator. This is the first such configuration to appear in the literature that does not require any new cryptographic mechanisms to be added to the standard. We comment on lessons for future key management APIs..
15h00-15h30 : H. Djafri, ENS de Cachan, "An Expressive Language for Statistical Verification of Stochastic Models", joint work with P. Ballarini, M. Duflot, S. Haddad and N. Pekergin
Abstract: Being inspired by existing stochastic logic, such as, the Continuous Stochastic Logic CSL and its following action-state asCSL and timed automata CSLTA evolutions, SHAL extends them in two respects: firstly it targets a much broader class of stochastic models (i.e. DESP rather than Markov chains); secondly it increases the expressiveness of verification by allowing to capture sophisticated dynamics expressed in terms of multivariate conditions. A formula of SHAL consists of a Linear Hybrid Automaton (LHA) and an expression. The LHA selects prefixes of relevant execution paths of a DESP and collects information along the paths. The result of the formula verification is the evaluation of an expression of the considered path random variable. A statistical engine is then employed for the confidence-interval estimation of the expected value of the expression associated to an LHA. We illustrate the SHAL approach by means of some examples and experimental results obtained through a prototype software tool for SHAL verification.