Publication


A Formal Security Model of the Infineon SLE 88 Smart Card Memory Management

Proceedings of ESORICS 2003


Author: David von Oheimb, Georg Walter, Volkmar Lotz
Year: 2003
Publisher: Springer LNCS
CR Classification: D.2.4, F.1.2, H.2.0
CR General Terms: Security, Reliability, Theory, Verification
Abstract: The Infineon SLE 88 is a smart card processor that offers strong protection mechanisms. One of them is a memory management system, typically used for sandboxing application programs dynamically loaded on the chip. High-level (EAL5+) evaluation of the chip requires a formal security model.

We formally model the memory management system as an Interacting State Machine and prove, using Isabelle/HOL, that the associated security requirements are met. We demonstrate that our approach enables an adequate level of abstraction, which results in an efficient analysis, and points out potential pitfalls like non-injective address translation.


Copyright © 2003 Springer-Verlag.
This paper has been published by Springer LNCS.
Conference version and journal version (which includes a detailed description of the ISM semantics) available in PDF format.
Slides


BibTeX-Entries:

@inproceedings{SLE88MM03, author = {Oheimb, David von and Walter, Georg and Lotz, Volkmar}, title = {A Formal Security Model of the Infineon {SLE 88} Smart Card Memory Management}, booktitle = {Proc.\ of the $8^{\rm th}$ European Symposium on Research in Computer Security (ESORICS)}, publisher = {Springer}, series = {LNCS}, volume = {2808}, year = 2003, note = {\url{http://ddvo.net/papers/SLE88_MM.html}}, CRClassification = {D.2.4, F.1.2, H.2.0}, CRGenTerms = {Security, Reliability, Theory, Verification}, abstract = { The Infineon SLE 88 is a smart card processor that offers strong protection mechanisms. One of them is a memory management system, typically used for sandboxing application programs dynamically loaded on the chip. High-level (EAL5+) evaluation of the chip requires a formal security model. We formally model the memory management system as an Interacting State Machine and prove, using Isabelle/HOL, that the associated security requirements are met. We demonstrate that our approach enables an adequate level of abstraction, which results in an efficient analysis, and points out potential pitfalls like non-injective address translation. } } @article{SLE88MM05, author = {Oheimb, David von and Lotz, Volkmar and Walter, Georg}, title = {{Analyzing SLE 88 memory management security using Interacting State Machines}}, journal = {International Journal of Information Security}, publisher = {Springer}, year = 2005, volume = {4}, number = {3}, pages = {155--171}, note = {\url{http://www.springerlink.com/index/10.1007/s10207-004-0057-5}; preprint: \url{http://ddvo.net/papers/SLE88_MM.html}} }