SmartCardModelingGemplusResearchLab详解.pptVIP

Smart Card ModelingGemplus Research Lab Outline Motivations The B Method Java Card Mechanisms: Verifier Interpreter Firewall Conclusions Motivations Applications are developed by the card provider in a secure environment, Drawbacks: time consuming costly New security problems Applications are no more developed under card issuer control, Na?ve implementation can ease DPA attacks, Any application provider can introduce a Trojan Horse in the card, New attacks can arise (denial of services…), Information can be exchanged between application, Use faulty platform implementation Two security levels Platform security Traditional means, Use of formal methods. = Models of the platform security modules Application security There is a need for a global security policy Flow control (data and/or code sharing) Resources consumption (memory, CPU, method calls...) = Static analysis of applet configurations (part of the CMS) The B method A formal Method Based on the mathematical set theory (variables, sets, relations, etc..), Generation of proof obligations, Theorem prover Supported by CASE tools (AtelierB, B Toolkit..) Used in industrial applications (RATP Meteor automatic subway, SNCF TGV Speed train control The B Method - Machine The B Method - Proof Obligation The B Method - Refinement Smart Card Modeling B Method Verifier Interpreter Firewall The Byte Code Verifier The Java byte code is compiled for the Java Virtual Machine. The Java byte code may be corrupted intentionally or not. Need to perform checks before its execution by the interpreter: Flow controls Type correctness Flow Control and Type Correctness A state is defined by: The pc (program counter) The type stack The type frame The properties to be checked are Confinement Stack access Initialization Type correctness Our Approach of the Model Model a Defensive Machine. Extract runtime checks by successive refinements. De-synchronize verification and execution process. Split the defensive machine in two par