Security-by-Contract for Java Card 2.x.x*

Java Card is a technology that could enable open multi-application smart cards.

Applications on these cards:

1. Can be loaded or removed after card issuance;
2. Can come from different providers;
3. Can interact providing enhanced services to the card holder.

Think of cards for everyday use:

• ePurse + Ticketing applications downloadable in every city the user visits;
• Credit card + Loyalty applications for every major airline alliances/hotel chains;
• All the shop loyalty applications on one card.

Unfortunately, the Java Card middleware itself is not flexible enough to enable these cards

• Security policy for application-interactions is hardcoded in the application code 
  • Already a bad idea from a security point of view;
•  If an application wants to change the list of trusted callers it needs to be reinstalled
  • Reinstallation is just not a good solution for smart cards, as it often will require recertification of the card;
  • No smart card vendor can afford recertification of all millions of cards each evolving differently.

We propose a Security-by-Contract framework embedded into the Java Card platform and integrated with the card manager.
This framework can enable loading time verification of security policies of each application, thus ensuring that the card is always in a secure state across evolutions.

You can find more details about the Security-by-Contract framework for Java Card here:

• "Load time on-card application certification for Java Card: The Security-by-Contract scheme for multi-application Java Card cards"
  A short white paper that summarizes the idea of the Security-by-Contract scheme for Java Card and the proof-of-concept implementation results ( .pdf)
• ''Security-by-Contract for Open Multi-Application Smart Cards''
  Presentation at eSmart'2011 with the overview of the SxC idea, architecture and some details of the implementation ( .pdf)
• ''Load Time Security Verification''
  Paper about the Claim Checker component of the framework at ICISS'2011 ( .pdf  )
• ''Load Time Security Verification. The Claim Checker. Technical report  DISI-11-471''
  Technical report with the full version of the ICISS'2011 paper ( .pdf)
• ''Implementation requirements and specification of the Policy Checker component. Technical report DISI-11-455''
  Technical report with the algorithms and data structures of the Policy Checker component ( .pdf)
• ''A Load Time Policy Checker for Open Multi-Application Smart Cards''
  Paper about a proof-of-concept implementation as an applet of the Policy Checker component at POLICY'2011 ( .pdf)
• ''Extended Abstract: Embeddable Security-by-Contract Verifier for Java Card''
  Short paper summarizing the SxC scheme and the implementation details ( .pdf)

Or contact me via email (gadyatskaya AT dit.unitn.it)

* Work is partially supported by the EU under grant EU-FP7-FET-IP-Secure Change.