Skip to Main content Skip to Navigation
Conference papers

SawjaCard: A Static Analysis Tool for Certifying Java Card Applications

Frédéric Besson 1 Thomas Jensen 1 Pierre Vittet 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper describes the design and implementation of a static analysis tool for certifying Java Card applications, according to security rules defined by the smart card industry. Java Card is a dialect of Java designed for programming multi-application smart cards and the tool, called SawjaCard, has been specialised for the particular Java Card programming patterns. The tool is built around a static analysis engine which uses a combination of numeric and heap analysis. It includes a model of the Java Card libraries and the Java Card firewall. The tool has been evaluated on a series of industrial applets and is shown to au-tomate a substantial part of the validation process.
Document type :
Conference papers
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-01093327
Contributor : Frédéric Besson <>
Submitted on : Wednesday, December 10, 2014 - 3:11:04 PM
Last modification on : Friday, July 10, 2020 - 4:21:20 PM
Long-term archiving on: : Wednesday, March 11, 2015 - 11:15:56 AM

File

sawjacard.pdf
Files produced by the author(s)

Identifiers

Citation

Frédéric Besson, Thomas Jensen, Pierre Vittet. SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. 21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. pp.51 - 67, ⟨10.1007/978-3-319-10936-7_4⟩. ⟨hal-01093327⟩

Share

Metrics

Record views

2960

Files downloads

369