Paper Info
Title
Formal verification of security properties of smart card embedded source code
Abstract
This paper reports on a method to handle the verification of various security properties of imperative source code embedded on smart cards. The idea is to combine two program verification approaches: the functional verification at the source code level and the verification of high level properties on a formal model built from the program and its specification. The method presented uses the Caduceus tool, built on top of the Why tool. Caduceus enables the verification of an annotated C program and provides a validation process that we used to generate a high level formal model of the C source code. This method is illustrated by an example extracted from the verification of a smart card embedded operating system.
Year
DOI
Venue
2005
10.1007/11526841_21
FM
Keywords
Field
DocType
annotated c program,source code level,smart card,security property,imperative source code,program verification approach,embedded source code,high level,formal model,high level property,formal verification,c source code,functional verification,source code,operating system,formal method,theorem proving
Functional verification,Programming language,Computer science,Intelligent verification,Verification,Runtime verification,Formal methods,High-level verification,Software verification,Formal verification
Conference
Volume
ISSN
ISBN
3582
0302-9743
3-540-27882-6
Citations 
PageRank 
References 
8
0.62
18
Authors
3
Name
Order
Citations
PageRank
June Andronick190342.66
Boutheina Chetali2595.68
Christine Paulin-Mohring354149.23