2004 | OriginalPaper | Buchkapitel
Enforcing High-Level Security Properties for Applets
verfasst von : Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet
Erschienen in: Smart Card Research and Advanced Applications VI
Verlag: Springer US
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Typically, such policies are described as high-level security properties, stating for example that no pin verification must take place within a transaction.Behavioural interface specification languages, such as JML (Java Modeling Language), have been successfully used to validate functional properties of smart card applications. However, high-level security properties cannot directly be expressed in such languages. Therefore, this paper proposes a method to translate high-level security properties into JML annotations. The method synthesises appropriate annotations and weaves them throughout the application. In this way, security policies can be validated using existing tools for JML. The method is general and applies to a large class of security properties.To validate the method, it has been applied to several realistic examples of smart card applications. This allowed us to find violations against the documented security policies for some of these applications.