Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

SawjaCard: A Static Analysis Tool for Certifying Java Card Applications

  • Conference paper
Static Analysis (SAS 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8723))

Included in the following conference series:

  • 737 Accesses

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 automate a substantial part of the validation process.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Common Criteria for Information Technology Security Evaluation (2012)

    Google Scholar 

  2. Ahrendt, W., et al.: The KeY system: Integrating Object-Oriented Design and Formal Methods. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 327–330. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Barthe, G., Burdy, L., Charles, J., Grégoire, B., Huisman, M., Lanet, J.-L., Pavlova, M.I., Requet, A.: JACK - A Tool for Validation of Security and Behaviour of Java Applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 152–174. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In: POPL, pp. 269–282. ACM Press (1979)

    Google Scholar 

  5. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: POPL, pp. 84–96. ACM Press (1978)

    Google Scholar 

  7. Demange, D., Jensen, T., Pichardie, D.: A Provably Correct Stackless Intermediate Representation for Java Bytecode. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 97–113. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Éluard, M., Jensen, T.P.: Secure Object Flow Analysis for Java Card. In: CARDIS, pp. 97–110. USENIX (2002)

    Google Scholar 

  9. Éluard, M., Jensen, T., Denne, E.: An Operational Semantics of the Java Card Firewall. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol. 2140, pp. 95–110. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  10. ETSI Project Smart Card Platform. Smart Cards; UICC Application Programming Interface (UICC API) for Java CardTM

    Google Scholar 

  11. Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: OOPSLA, pp. 302–312. ACM (2003)

    Google Scholar 

  12. GlobalPlatform Inc. GlobalPlatform Card Composition Model Security Guidelines for Basic Applications (2012)

    Google Scholar 

  13. Graf, J., Hecker, M., Mohr, M.: Using JOANA for Information Flow Control in Java Programs - A Practical Guide. In: ATPS 2013. LNI, vol. 215, pp. 123–138. GI (2013)

    Google Scholar 

  14. Hansen, R.R., Siveroni, I.: Towards Verification of Well-Formed Transactions in Java Card Bytecode. Electr. Notes Theor. Comput. Sci. 141(1), 145–162 (2005)

    Article  Google Scholar 

  15. Hind, M.: Pointer Analysis: Haven’t We Solved This Problem Yet? In: PASTE 2001, pp. 54–61. ACM (2001)

    Google Scholar 

  16. Hubert, L.: A non-null annotation inferencer for Java bytecode. In: PASTE, pp. 36–42. ACM (2008)

    Google Scholar 

  17. Hubert, L., Barré, N., Besson, F., Demange, D., Jensen, T., Monfort, V., Pichardie, D., Turpin, T.: Sawja: Static Analysis Workshop for Java. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 92–106. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  18. Huisman, M., Gurov, D., Sprenger, C., Chugunov, G.: Checking Absence of Illicit Applet Interactions: A Case Study. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 84–98. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. IBM. The T.J. Watson Libraries for Analysis (Wala), http://wala.sourceforge.net

  20. Le Pallec, P., Diallo, S., Simon, T., Saif, A., Briot, O., Picard, P., Bensimon, M., Devisme, J., Eznack, M.: Cardlet Development Guidelines. AFSCM (2012)

    Google Scholar 

  21. Leavens, G.T., Kiniry, J.R., Poll, E.: A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, p. 37. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Lhoták, O., Hendren, L.J.: Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation. ACM Trans. Softw. Eng. Methodol. 18(1) (2008)

    Google Scholar 

  23. Might, M., Shivers, O.: Improving flow analyses via GammaCFA: abstract garbage collection and counting. In: ICFP, pp. 13–25. ACM (2006)

    Google Scholar 

  24. Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)

    Article  MATH  Google Scholar 

  25. Miné, A.: Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  26. Mostowski, W.: Formalisation and Verification of Java Card Security Properties in Dynamic Logic. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 357–371. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  27. Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5) (2007)

    Google Scholar 

  28. Siveroni, I.: Operational semantics of the Java Card Virtual Machine. J. Log. Algebr. Program. 58(1-2), 3–25 (2004)

    Article  MATH  Google Scholar 

  29. Smaragdakis, Y., Bravenboer, M., Lhoták, O.: Pick your contexts well: understanding object-sensitivity. In: POPL, pp. 17–30. ACM (2011)

    Google Scholar 

  30. Spoto, F.: The Nullness Analyser of julia. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 405–424. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  31. Spoto, F.: Precise null-pointer analysis. Software and System Modeling 10(2), 219–252 (2011)

    Article  Google Scholar 

  32. Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L.J., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: CASCON, p. 13. IBM (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria, Rennes, France

    Frédéric Besson, Thomas Jensen & Pierre Vittet

Authors
  1. Frédéric Besson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Jensen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pierre Vittet
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Westfälische Wilhelms-Universität Münster, FB 10, Einsteinstraße 62, 48149, Münster, Germany

    Markus Müller-Olm

  2. Institut für Informatik, Technische Universität München, 12, Boltzmannstr. 3, 85748, Garching, Germany

    Helmut Seidl

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Besson, F., Jensen, T., Vittet, P. (2014). SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. In: Müller-Olm, M., Seidl, H. (eds) Static Analysis. SAS 2014. Lecture Notes in Computer Science, vol 8723. Springer, Cham. https://doi.org/10.1007/978-3-319-10936-7_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10936-7_4

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10935-0

  • Online ISBN: 978-3-319-10936-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation