Embedding formally proved code in a smart card: converting B to C

Author

Requet, Antoine ; Bossu, Gaelle

Author_Institution

Gemplus Res. Lab., Bertagne, France

fYear

2000

fDate

2000

Firstpage

15

Lastpage

22

Abstract

Smart cards are small embedded devices with strong security requirements. To fulfil those requirements, formal methods appear as promising techniques. The B method has already been used to model smart-card components. However, smart cards have also very strong programming constraints, both for memory usage and computing power. Currently, the code generated from a B specification does not meet those constraints. This paper presents some classical optimisation techniques that are well-suited for B specifications and that need to be included within a code generator to embed this generated code

Keywords

C language; embedded systems; optimising compilers; program verification; security of data; smart cards; specification languages; B specifications; B to C conversion; code embedding; code generator; computing power; embedded devices; formal methods; formally proved code; memory usage; optimisation techniques; programming constraints; security requirements; smart cards; Certification; Distributed power generation; Information security; Information systems; Java; Laboratories; Memory management; Operating systems; Random access memory; Smart cards;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Engineering Methods, 2000. ICFEM 2000. Third IEEE International Conference on

Conference_Location

York

Print_ISBN

0-7695-0822-7

Type

conf

DOI

10.1109/ICFEM.2000.873801

Filename

873801