de la plate-forme Java Card (2008)
École Doctorale Stic, Spécialité Informatique, Guillaume Dufay, Erik Poll, ...
Quelle meilleure opportunité que cette thèse, qui marque l’achèvement des études universitaires, pour exprimer mes plus vifs remerciements à mes parents? Je ne leur serais probablement jamais...
Formal Methods for Smartcard Security (2008)
Gilles Barthe, Guillaume Dufay
Abstract. Smartcards are trusted personal devices designed to store and process confidential data, and to act as secure tokens for providing access to applications and services. Smartcards are widely...
Virtual machines, such as the Java Virtual Machine, Java Card Virtual (2008)
Gilles Barthe, Inria Sophia Antipolis, Guillaume Dufay
Abstract. Bytecode verification is one of the key security functions of several architectures for mobile and embedded code, including Java, Java Card, and.NET. Over the last few years, its formal...
Verifying Resource Access Control on Mobile Interactive Devices (2008)
Frédéric Besson, Guillaume Dufay, Thomas Jensen, David Pichardie, Inria Rennes, U. Rennes
A model of resource access control is presented in which the access control to resources can employ user interaction to obtain the necessary permissions. This model is inspired by and improves on the...
A Formal Model of Access Control for Mobile Interactive Devices (2006)
Besson, Frédéric, Dufay, Guillaume, Jensen, Thomas
Abstract. This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model...
A Formal Model of Access Control for Mobile Interactive Devices (2006)
Besson, Frédéric, Dufay, Guillaume, Jensen, Thomas
This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model is...
A Formal Model of Access Control for Mobile Interactive Devices (2006)
Besson, Frédéric, Dufay, Guillaume, Jensen, Thomas
This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model is...
A Formal Model of Access Control for Mobile Interactive Devices (2006)
Frédéric Besson, Guillaume Dufay, Thomas Jensen
Abstract. This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model...
A Formal Model of Access Control for Mobile Interactive Devices (2006)
Frédéric Besson, Guillaume Dufay, Thomas Jensen
Abstract. This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model...
Privacy-sensitive information flow with JML (2005)
Guillaume Dufay, Amy Felty, Stan Matwin
Abstract. In today’s society, people have very little control over what kinds of personal data are collected and stored by various agencies in both the private and public sectors. We describe an...
Privacy-sensitive information flow with JML (2005)
Guillaume Dufay, Amy Felty, Stan Matwin
Abstract. In today’s society, people have very little control over what kinds of personal data are collected and stored by various agencies in both the private and public sectors. We describe an...
A Formal Executable Semantics of the JavaCard Platform (2001)
Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard Serpette
Abstract. We present a formal executable speci cation of two crucial JavaCard platform components, namely the Java Card Virtual Machine (JCVM) and the ByteCode Veri er (BCV). Moreover, we relate both...
Formalization in Coq of the Java Card Virtual Machine
Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard Serpette, Simão Sousa, Shen-Wei Yu
Introduction Java has quickly become a standard for Internet and, through Java Card, for smartcard programming, putting security issues at stake. Yet recent research has unveiled several problems in...