Paper Info
Title
Certifying an embedded remote method invocation protocol
Abstract
This paper describes an approach to formally prove that an implementation of the Java Card Remote Method Invocation protocol on smart cards fulfills its functional and security specification. For that, we refine the specification in two intermediate formal models: the functional specification and the high level design. These two models are both defined upon an existing complete formal model of the Java Card virtual machine, allowing to formalize all the security requirements. We focus on certifying the Java code portion since the native portion has been handled in a previous work. The correctness is showed to be preserved while composing the native and Java codes. Our refinement scheme has been designed to fulfill the requirements of a high-level Common Criteria security evaluation.
Year
DOI
Venue
2008
10.1145/1363686.1363777
SAC
Keywords
Field
DocType
java code portion,intermediate formal model,java card remote method,functional specification,existing complete formal model,security specification,java card virtual machine,embedded remote method invocation,security requirement,high-level common criteria security,java code,virtual machine,java card,smart card,embedded software,formal verification
Programming language,Java annotation,Computer science,Correctness,Smart card,Common Criteria,Java Card,Java,Functional specification,Formal verification
Conference
Citations 
PageRank 
References 
1
0.39
5
Authors
2
Name
Order
Citations
PageRank
June Andronick190342.66
Quang-Huy Nguyen2304.14