Transcript Checking Secure Interactions of Smart Card Applets: extended version

Checking Secure Interactions of Smart
Card Applets: extended version
P. Bieber, J. Cazin, P. Girard, J. –L. Lanet, V. Wiels, and G. Zanon
Published in Journal of Computer Security
Presented By: Sruthi Bandhakavi
(Day 1)
27th Oct 2003
Contents of the paper



A security policy that associates levels to applet attributes and
methods.
A technique based on model checking to verify that actual information
flows between applets are authorized.
The approach is illustrated on applets involved in an electronic purse
running on Java enabled smart cards.
Goal: To provide techniques and tools for the Java Card issuer to verify
that new applets interact securely with already loaded applets.
What is a Java Card?

Java Card - A smart card capable of running Java programs.
The system architecture on the Java Card
Benefits of Java Card Technology

Interoperable

Secure

Multi-Application Capable

Dynamic

Open

Compatible with Existing Standards
Multi-application Smart Card

A smart card that can contain several functions.
Advantages of multi-application
smart cards




To reduce the number of cards in the users’ wallets
Allow the issuers to decrease the time-to-market, the development,
infrastructure and deployment costs or to update/add applications after
card issuance.
Allow the commercial synergies between partners and can lead to new
business opportunities. Ex: A credit card with an electronic purse and a
frequent flyer application.
More cost effective than several cards with single applications.
Participants

Issuer


Application provider (AP)




Designs the application for targeted card OS.
Negotiates with the issuer for downloading its application into the card.
Owner of the applet and applet’s data. (airways operating the frequent flyer
application).
Card Operator (CO)


Proposes the card to the user. (Bank)
Interacts with the card either to use an application or to perform an
administrative task. (Bank)
Card Holder(User)
Security issues

Platform level security




Application security



Applications segregation(OS Security)
Quality of security services offered by the platform (correctness of JVM,
tamper resistance, cryptographic algorithms, post issuance loading
mechanisms)
Issuers’ responsibility.
Under providers’ responsibility but relies on platform security.
OS must guarantee the security of the applications even though some
insecure applications are encountered by it.
Information flow security

Difficulties that arise from illegal data sharing inside a card.
Security Policies

Discretionary Security Policy


Application will be in charge of defining their own security policy, for
example, by providing access control lists to the OS using which the
propagation of data between applets is controlled.
Mandatory Security Policy

Card wide security policy necessary to solve the problem of re-sharing
shared objects.
Trust Relationships
Security Level lattice without Sharing
Security level lattice with unacceptable
sharing
Security level lattice with acceptable
sharing
Implementation Issues


Classifying the data objects and assigning
granularity.
Enforcing a security policy
Classification of data objects



Assign a security level to each data object.
In a given applet, label the objects with their
provider’s level. If an object is shared, assign the
level related to the shared data.
Authorized information flows in an applet will be from
lower labeled objects to higher ones.
Enforcing the security policy

Dynamically



Using a reference monitor, which will be called
each time an object reference is made by the
virtual machine.
Costly in memory and execution time.
Statically


By checking the correctness of information flows
between applets.
Done using security level set with a lattice
structure.
Applet Certification
Example of three applets sharing data
Lattice of security levels
Electronic Purse Functionalities
Electronic purse threats
Applet Interactions
Security Policy



Each applet provider is assigned a security level and we consider special levels
for shared data.

In our example we have a level for each applet: AF for Air France, P for
Purse and RC for RentaCar, AF+P for data shared by Air France and Purse,
etc.
The relation between levels ≤ is used to authorize or forbid information flows
between applets.

In the policy we consider, AF + P ≤ AF and AF + P ≤ P, this means that
information whose level is AF + P is authorized to flow towards information
whose level is P or AF.
The applets may only communicate through shared interfaces, directs flows
between levels AF, P and RC are forbidden.

AF !≤ P, P !≤ AF, AF !≤ RC, RC !≤ AF, P !≤ RC & RC !≤ P.
Authorized information flows

The levels together with the ≤ relation have a lattice structure,
so there are a bottom level public and top level private.
Secure Dependency Model



Applies to systems where applications might maliciously or
involuntarily, communicate confidential information to other
applications.
Ensures that dependencies between system objects cannot be
exploited to establish an indirect communication channel.
When applied to electronic purse, illicit interactions will be
detected by controlling the dependencies between objects of
the system.
Definitions

Set of Evolutions



Ev  Objects X Dates  Values
Set Objects X Dates is made of three disjoint subsets:




A program is described by a set of evolutions that associate a value
with each object at each date.
Input objects : not computed by the program
Output objects: computed by the program and are directly
observable
Internal objects: not observable.
Function lvl

Associates a security level with input and output objects.
Secure Dependency Property(SecDep)

Requires that the value of the output objects with security level l only
depends on the value of input objects whose security level is
dominated by l :
ot  Output, e  Ev, e’  Ev, e ~aut(ot) e’  e(ot) = e’(ot)
where aut(ot) = {o’t’  Input | t’ < t, lvl(o’t’ ) ≤ lvl(ot)} and
e ~aut(ot) e’ iff o’t’  aut(ot), e(o’t’ ) = e’ (o’t’ ) .


Cannot be directly proved by a model checker like SMV because it is
neither a safety or liveness property nor a refinement property.
So sufficient conditions of SecDep that are better handled by SMV are
looked up.
Definitions 2

Set dep(i, ot)


Program counter



Contains objects with date t-1 used by instruction at program location i to
compute the value ot .
Internal object such that pct-1 determines the current instruction used to
compute the value of ot .
Whenever and object is modified(i.e. ot-1 is different from ot ) then we
consider that pct-1 belongs to dep(i, ot).
Function lvldep


Associates a computed level with each object for each evolution.
If ot is an input object then lvldep(e, ot) = lvl(ot) otherwise
lvldep(e, ot) = max{lvldep(e, o’t-1) | o’t-1  dep(e(pct-1 ), ot) }
where max denotes the least upper bound in the lattice of levels.
Hypothesis 1.
The value of ot computed by the program is determined
by the values of objects in dep(e(pct-1 ), ot) :
ot  Output, e  Ev, e’  Ev,
e ~ dep(e(pct-1 ), ot) e’  e(ot) = e’(ot)
Theorem 1.
A program satisfies SecDep if the computed level of an
output object is always dominated by it security level:
ot  Output, e  Ev, lvldep(e, ot) ≤ lvl(ot)