Analyzing SLE 88 memory management security using Interacting State Machines |
| |
Authors: | David von Oheimb Volkmar Lotz Georg Walter |
| |
Affiliation: | (1) Corporate Technology, Siemens AG, 81730 Munich, Germany;(2) Secure Mobile Solutions, Infineon AG, 81609 Munich, Germany |
| |
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 noninjective address translation. |
| |
Keywords: | Security Formal analysis Smart cards Memory management Isabelle/HOL |
本文献已被 SpringerLink 等数据库收录! |
|