Skip to Main content Skip to Navigation
New interface
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 metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Frédéric Besson Connect in order to contact the contributor
Submitted on : Wednesday, December 10, 2014 - 3:11:04 PM
Last modification on : Wednesday, February 2, 2022 - 3:50:48 PM
Long-term archiving on: : Wednesday, March 11, 2015 - 11:15:56 AM


Files produced by the author(s)



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⟩



Record views


Files downloads