Checking Absence of Illicit Applet Interactions: A Case Study

Marieke Huisman; Dilian Gurov; Christoph Sprenger; Gennady Chugunov

doi:10.1007/978-3-540-24721-0_6

Checking Absence of Illicit Applet Interactions: A Case Study

Marieke Huisman, Dilian Gurov, Christoph Sprenger, Gennady Chugunov

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

21 Citations (Scopus)

Abstract

This paper presents the use of a method – and its corresponding tool set – for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional, thus supporting post-issuance loading of applets. The correctness of a global system property can algorithmically be inferred from local applet properties. Later, when loading applets on a card, the implementations are matched against these local properties, in order to guarantee the global property. The theoretical framework underlying our method has been presented elsewhere; the present paper evaluates its practical usability by means of an industrial case study. In particular, we outline the tool set that we have assembled to support the verification process, combining existing model checkers with newly developed tools, tailored to our method.

Original language	English
Title of host publication	Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings
Editors	Michel Wermelinger, Tiziana Margaria
Publisher	Springer
Pages	84-98
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-540-24721-0_6
Publication status	Published - 2004
Externally published	Yes
Event	7th International Conference on Fundamental Approaches to Software Engineering, FASE 2004 - Barcelona, Spain Duration: 29 Mar 2004 → 2 Apr 2004 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2984

Conference

Conference	7th International Conference on Fundamental Approaches to Software Engineering, FASE 2004
Abbreviated title	FASE 2004
Country/Territory	Spain
City	Barcelona
Period	29/03/04 → 2/04/04
Other	Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004

Access to Document

10.1007/978-3-540-24721-0_6

Cite this

Huisman, M., Gurov, D., Sprenger, C., & Chugunov, G. (2004). Checking Absence of Illicit Applet Interactions: A Case Study. In M. Wermelinger, & T. Margaria (Eds.), Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings (pp. 84-98). (Lecture Notes in Computer Science; Vol. 2984). Springer. https://doi.org/10.1007/978-3-540-24721-0_6

Huisman, Marieke ; Gurov, Dilian ; Sprenger, Christoph et al. / Checking Absence of Illicit Applet Interactions: A Case Study. Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings. editor / Michel Wermelinger ; Tiziana Margaria. Springer, 2004. pp. 84-98 (Lecture Notes in Computer Science).

@inproceedings{b186b582bf274f278a189d0f02735dc1,

title = "Checking Absence of Illicit Applet Interactions: A Case Study",

abstract = "This paper presents the use of a method – and its corresponding tool set – for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional, thus supporting post-issuance loading of applets. The correctness of a global system property can algorithmically be inferred from local applet properties. Later, when loading applets on a card, the implementations are matched against these local properties, in order to guarantee the global property. The theoretical framework underlying our method has been presented elsewhere; the present paper evaluates its practical usability by means of an industrial case study. In particular, we outline the tool set that we have assembled to support the verification process, combining existing model checkers with newly developed tools, tailored to our method.",

author = "Marieke Huisman and Dilian Gurov and Christoph Sprenger and Gennady Chugunov",

year = "2004",

doi = "10.1007/978-3-540-24721-0_6",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "84--98",

editor = "Michel Wermelinger and Tiziana Margaria",

booktitle = "Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings",

address = "Germany",

note = "7th International Conference on Fundamental Approaches to Software Engineering, FASE 2004, FASE 2004 ; Conference date: 29-03-2004 Through 02-04-2004",

}

Huisman, M, Gurov, D, Sprenger, C & Chugunov, G 2004, Checking Absence of Illicit Applet Interactions: A Case Study. in M Wermelinger & T Margaria (eds), Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2984, Springer, pp. 84-98, 7th International Conference on Fundamental Approaches to Software Engineering, FASE 2004, Barcelona, Spain, 29/03/04. https://doi.org/10.1007/978-3-540-24721-0_6

Checking Absence of Illicit Applet Interactions: A Case Study. / Huisman, Marieke; Gurov, Dilian; Sprenger, Christoph et al.
Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings. ed. / Michel Wermelinger; Tiziana Margaria. Springer, 2004. p. 84-98 (Lecture Notes in Computer Science; Vol. 2984).

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

TY - GEN

T1 - Checking Absence of Illicit Applet Interactions: A Case Study

AU - Huisman, Marieke

AU - Gurov, Dilian

AU - Sprenger, Christoph

AU - Chugunov, Gennady

N1 - Conference code: 7

PY - 2004

Y1 - 2004

N2 - This paper presents the use of a method – and its corresponding tool set – for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional, thus supporting post-issuance loading of applets. The correctness of a global system property can algorithmically be inferred from local applet properties. Later, when loading applets on a card, the implementations are matched against these local properties, in order to guarantee the global property. The theoretical framework underlying our method has been presented elsewhere; the present paper evaluates its practical usability by means of an industrial case study. In particular, we outline the tool set that we have assembled to support the verification process, combining existing model checkers with newly developed tools, tailored to our method.

AB - This paper presents the use of a method – and its corresponding tool set – for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional, thus supporting post-issuance loading of applets. The correctness of a global system property can algorithmically be inferred from local applet properties. Later, when loading applets on a card, the implementations are matched against these local properties, in order to guarantee the global property. The theoretical framework underlying our method has been presented elsewhere; the present paper evaluates its practical usability by means of an industrial case study. In particular, we outline the tool set that we have assembled to support the verification process, combining existing model checkers with newly developed tools, tailored to our method.

U2 - 10.1007/978-3-540-24721-0_6

DO - 10.1007/978-3-540-24721-0_6

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - 84

EP - 98

BT - Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings

A2 - Wermelinger, Michel

A2 - Margaria, Tiziana

PB - Springer

T2 - 7th International Conference on Fundamental Approaches to Software Engineering, FASE 2004

Y2 - 29 March 2004 through 2 April 2004

ER -

Huisman M, Gurov D, Sprenger C, Chugunov G. Checking Absence of Illicit Applet Interactions: A Case Study. In Wermelinger M, Margaria T, editors, Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings. Springer. 2004. p. 84-98. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-24721-0_6

Checking Absence of Illicit Applet Interactions: A Case Study

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this