[go: up one dir, main page]

Béguelin, 2004 - Google Patents

Formal specification of GlobalPlatform Card Security Requirements

Béguelin, 2004

View PDF
Document ID
1654527494795768220
Author
Béguelin S
Publication year

External Links

Snippet

This report presents a formal specification of the security and functional requirements for GlobalPlatform cards as defined in [Glo01] and [Glo03]. The formalization is given using the notation of the B-method, which has already been applied in the SmartCard industry with …
Continue reading at pfa12.free.fr (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/445—Programme loading or initiating
    • G06F9/44589—Programme code verification, e.g. Java bytecode verification, proof-carrying code
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/455—Emulation; Software simulation, i.e. virtualisation or emulation of application or operating system execution engines
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/4421—Execution paradigms
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/70—Protecting specific internal or peripheral components, in which the protection of a component leads to protection of the entire computer
    • G06F21/71—Protecting specific internal or peripheral components, in which the protection of a component leads to protection of the entire computer to assure secure computing or processing of information
    • G06F21/77—Protecting specific internal or peripheral components, in which the protection of a component leads to protection of the entire computer to assure secure computing or processing of information in smart cards
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/46—Multiprogramming arrangements
    • G06F9/468—Specific access rights for resources, e.g. using capability register
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
    • G06F21/52—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems during program execution, e.g. stack integrity ; Preventing unwanted data erasure; Buffer overflow
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G06F8/43—Checking; Contextual analysis
    • G06F8/436—Semantic checking
    • G06F8/437—Type checking
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/60—Protecting data
    • G06F21/62—Protecting access to data via a platform, e.g. using keys or access control rules
    • G06F21/6218—Protecting access to data via a platform, e.g. using keys or access control rules to a system of files or objects, e.g. local or distributed file system or database
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06Q—DATA PROCESSING SYSTEMS OR METHODS, SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q20/00—Payment architectures, schemes or protocols
    • G06Q20/30—Payment architectures, schemes or protocols characterised by the use of specific devices
    • G06Q20/34—Payment architectures, schemes or protocols characterised by the use of specific devices using cards, e.g. integrated circuit [IC] cards or magnetic cards
    • G06Q20/357—Cards having a plurality of specified features
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/20—Handling natural language data
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2221/00—Indexing scheme relating to security arrangements for protecting computers, components thereof, programs or data against unauthorised activity

Similar Documents

Publication Publication Date Title
Besson et al. Model checking security properties of control flow graphs
Darvas et al. A theorem proving approach to analysis of secure information flow
Mantel et al. Controlled declassification based on intransitive noninterference
US7181725B1 (en) Method for verifying safety properties of java byte code programs
Hennessy et al. Information flow vs. resource access in the asynchronous pi-calculus
Hedin et al. Timing aware information flow security for a javacard-like bytecode
Bieber et al. Checking secure interactions of smart card applets: Extended version
Barthe et al. Security types preserving compilation
Stenzel A formally verified calculus for full Java Card
Avvenuti et al. Java bytecode verification for secure information flow
Casset Development of an embedded verifier for java card byte code using formal methods
Chetali et al. Industrial use of formal methods for a high-level security evaluation
Barthe et al. Tool-assisted specification and verification of the JavaCard platform
Hansen et al. Non-interference and erasure policies for java card bytecode
Bieber et al. Checking secure interactions of smart card applets
Kirchner et al. Analysis of rewrite-based access control policies
Béguelin Formal specification of GlobalPlatform Card Security Requirements
Warnier Language Based Security for Java and JML
Requet et al. Application of the B formal method to the proof of a type verification algorithm
Barthe et al. Validation of the JavaCard platform with implicit induction techniques
Bernardeschi et al. Using standard verifier to check secure information flow in java bytecode
Barthe et al. Compositional verification of secure applet interactions
Requet AB model for ensuring soundness of a large subset of the Java Card virtual machine
Béguelin Formalisation and verification of the globalplatform card specification using the b method
Veschetti et al. A Formal Modeling Language for Smart Contracts