Enforcing High-Level Security Properties for Applets

Mariela Pavlova; Gilles Barthe; Lilian Burdy; Marieke Huisman; Jean-Louis Lanet

doi:10.1007/1-4020-8147-2_1

Enforcing High-Level Security Properties for Applets

Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

13 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Smart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France
Editors	Jean-Jacques Quisquater, Pierre Paradinas, Yves Deswarte, Anas Abou El Kalam
Publisher	Springer
Pages	1-16
Number of pages	16
DOIs	https://doi.org/10.1007/1-4020-8147-2_1
Publication status	Published - 2004
Externally published	Yes
Event	IFIP 18th World Computer Congress, WCC 2004 - Toulouse, France Duration: 22 Aug 2004 → 27 Aug 2004 Conference number: 18

Publication series

Name	IFIP International Federation for Information Processing book series
Publisher	Kluwer/Springer
Volume	153

Conference

Conference	IFIP 18th World Computer Congress, WCC 2004
Abbreviated title	WCC 2004
Country/Territory	France
City	Toulouse
Period	22/08/04 → 27/08/04

Access to Document

10.1007/1-4020-8147-2_1

Cite this

Pavlova, M., Barthe, G., Burdy, L., Huisman, M., & Lanet, J.-L. (2004). Enforcing High-Level Security Properties for Applets. In J.-J. Quisquater, P. Paradinas, Y. Deswarte, & A. A. E. Kalam (Eds.), Smart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France (pp. 1-16). (IFIP International Federation for Information Processing book series; Vol. 153). Springer. https://doi.org/10.1007/1-4020-8147-2_1

Pavlova, Mariela ; Barthe, Gilles ; Burdy, Lilian et al. / Enforcing High-Level Security Properties for Applets. Smart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France. editor / Jean-Jacques Quisquater ; Pierre Paradinas ; Yves Deswarte ; Anas Abou El Kalam. Springer, 2004. pp. 1-16 (IFIP International Federation for Information Processing book series).

@inproceedings{7422a57894964fb6b2e7457f7bc942b3,

title = "Enforcing High-Level Security Properties for Applets",

abstract = "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.",

author = "Mariela Pavlova and Gilles Barthe and Lilian Burdy and Marieke Huisman and Jean-Louis Lanet",

year = "2004",

doi = "10.1007/1-4020-8147-2_1",

language = "English",

series = "IFIP International Federation for Information Processing book series",

publisher = "Springer",

pages = "1--16",

editor = "Jean-Jacques Quisquater and Pierre Paradinas and Yves Deswarte and Kalam, {Anas Abou El}",

booktitle = "Smart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France",

address = "Germany",

note = "IFIP 18th World Computer Congress, WCC 2004, WCC 2004 ; Conference date: 22-08-2004 Through 27-08-2004",

}

Pavlova, M, Barthe, G, Burdy, L, Huisman, M & Lanet, J-L 2004, Enforcing High-Level Security Properties for Applets. in J-J Quisquater, P Paradinas, Y Deswarte & AAE Kalam (eds), Smart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France. IFIP International Federation for Information Processing book series, vol. 153, Springer, pp. 1-16, IFIP 18th World Computer Congress, WCC 2004, Toulouse, France, 22/08/04. https://doi.org/10.1007/1-4020-8147-2_1

Enforcing High-Level Security Properties for Applets. / Pavlova, Mariela; Barthe, Gilles; Burdy, Lilian et al.
Smart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France. ed. / Jean-Jacques Quisquater; Pierre Paradinas; Yves Deswarte; Anas Abou El Kalam. Springer, 2004. p. 1-16 (IFIP International Federation for Information Processing book series; Vol. 153).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Enforcing High-Level Security Properties for Applets

AU - Pavlova, Mariela

AU - Barthe, Gilles

AU - Burdy, Lilian

AU - Huisman, Marieke

AU - Lanet, Jean-Louis

N1 - Conference code: 18

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

U2 - 10.1007/1-4020-8147-2_1

DO - 10.1007/1-4020-8147-2_1

M3 - Conference contribution

T3 - IFIP International Federation for Information Processing book series

SP - 1

EP - 16

BT - Smart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France

A2 - Quisquater, Jean-Jacques

A2 - Paradinas, Pierre

A2 - Deswarte, Yves

A2 - Kalam, Anas Abou El

PB - Springer

T2 - IFIP 18th World Computer Congress, WCC 2004

Y2 - 22 August 2004 through 27 August 2004

ER -

Pavlova M, Barthe G, Burdy L, Huisman M, Lanet JL. Enforcing High-Level Security Properties for Applets. In Quisquater JJ, Paradinas P, Deswarte Y, Kalam AAE, editors, Smart Card Research and Advanced Applications VI, IFIP 18th World Computer Congress, TC8/WG8.8 TC11/WG11.2 Sixth International Conference on Smart Card Research and Advanced Applications (CARDIS), 22-27 August 2004, Toulouse, France. Springer. 2004. p. 1-16. (IFIP International Federation for Information Processing book series). doi: 10.1007/1-4020-8147-2_1

Enforcing High-Level Security Properties for Applets

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this