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.
Partially supported by the EU as part of the VerifiCard project IST-2000-26328.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Barthe, G., Gurov, D., Huisman, M.: Compositional verification of secure applet interactions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 15–32. Springer, Heidelberg (2002)
Besson, F., Jensen, T., Le Métayer, D., Thorn, T.: Model checking security properties of control flow graphs. J. of Computer Security 9(3), 217–250 (2001)
Bouajjani, A., Fernandez, J.C., Graf, S., Rodriguez, C., Sifakis, J.: Safety for branching time semantics. In: Automata, Languages and Programming, pp. 76–92 (1991)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency Theory, pp. 135–150 (1997)
Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder - second generation of a Java model checker. In: Workshop on Advances in Verification (2000)
Bretagne, E., El Marouani, A., Girard, P., Lanet, J.-L.: Pacap purse and loyalty specification. Technical Report V 0.4, Gemplus (2000)
Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 545–623. North Holland, Amsterdam (2000)
Chugunov, G., Fredlund, L.-å., Gurov, D.: Model checking of multi-applet Java-Card applications. In: CARDIS 2002, pp. 87–95. USENIX Publications (2002)
Cleaveland, R., Parrow, J., Steffen, B.: A semantics based verification tool for finite state systems. In: Proc. 9th IFIP Symp. Protocol Specification, Verification and Testing (1989)
Corbett, J., Dwyer, M., Hatcliff, J., Robby: A language framework for expressing checkable properties of dynamic software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, Springer, Heidelberg (2000)
Hatcliff, J., Dwyer, M.: Using the Bandera tool set to model-check properties of concurrent Java software. Technical report, SAnToS Laboratory, Department of Computing and Information Sciences, Kansas State University (2000)
Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)
Polanský, D.: Verifying properties of infinite-state systems. Master’s thesis, Masaryk University, Faculty of Informatics, Brno (2000)
Sprenger, C., Gurov, D., Huisman, M.: Simulation logic, applets and compositional verification. Technical Report RR-4890, INRIA (2003)
Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a Java Optimization Framework. In: CASCON 1999, pp. 125–135 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huisman, M., Gurov, D., Sprenger, C., Chugunov, G. (2004). Checking Absence of Illicit Applet Interactions: A Case Study. In: Wermelinger, M., Margaria-Steffen, T. (eds) Fundamental Approaches to Software Engineering. FASE 2004. Lecture Notes in Computer Science, vol 2984. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24721-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-24721-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21305-5
Online ISBN: 978-3-540-24721-0
eBook Packages: Springer Book Archive