Transcript Formal specification of Gemplus’ electronic purse case study

Formal specification of
Gemplus’ electronic purse
case study
Néstor Cataño & Marieke Huisman
INRIA Sophia-Antipolis
{ncatano, mhuisman}@sophia.inria.fr
The electronic purse
• Developed by trainee at Gemplus
• Goal: develop more complex
application, using object-oriented
features
• Revision by members research lab and
new trainee
• Result: not completely finished, not fully
representative
Software documentation
• Management & history of the
development
• Clear, concise and unambiguous
• Correspondance with implementation
Some Fragments from
LoyaltiesTable
//
//
//
/*
huge modifications on 31/07/2000
now, we handle AID objects instead of byte arrays that represents them.
that way, we gain some space, and code is clearer.
the purse stores in this object the loyalties that are allowed to communicate
with it*/
class LoyaltiesTable {
////////////////
ATTRIBUTES
////////////////
// temporarily modified by RM on 26/07/2000 for memory reason
// private final static byte NB_MAX
= (byte)20;
private final static byte NB_MAX
= (byte)3;
…
/* suppress all the entries of the loyalty specified by aid */
void delLoyalty(AID aid) {…}
…
/* suppress the notification of the loyalty specified by aid*/
void removeNotification(AID aid) {…}
Software documentation
• Management & history of the
development
• Clear, concise and unambiguous
• Correspondance with implementation
• Formal specification
• And verification
Difficult and labour-intensive
This talk
• Different approaches to formal
specification and verification
• Static checking (lightweight formal
methods)
• The electronic purse case study
• Static checking of the electronic purse:
class invariants
Specification language
• Close to programming language
Eiffel, JML, ESC/Java, Jass
• Expressions from programming
language
with specification-specific constructs
(forall, exists, implication etc.)
Checking techniques
• Run-time checking (Eiffel, JML, Jass)
• Full verification
(syntactic or (Jive)
semantic) (LOOP)
• Static checking (ESC/Java)
Static checking with ESC/Java
• Compaq Research (Leino et al.)
• Focus on finding common program
errors (nullpointers, array index out of
bounds)
• Proof obligations to dedicated theorem
prover (assume - assert pairs)
• Issues warnings
Static checking with ESC/Java
ESC/Java =
Compromise
between
soundness,
completeness,
and
efficiency
ESC/Java pragmas
•
•
•
•
•
•
•
•
Preconditions (requires)
Postconditions (ensures)
Exceptional postconditions (exsures)
Modifies clause
Class invariants
Implication, quantification
Value expression in pre-state (\old(E))
Result value of method (\result)
The electronic purse
• Supports debit, credit and currency
change operations
• Interaction with loyalty, card issuer and
terminal
• Packages: utils, pacapinterfaces and
purse
The purse package
• PurseApplet: installation, (de)selection,
communication with terminal
• Purse:
– implements basic functionalities
– keeps track of balance, transactions,
currency changes, loyalties
The purse package
• AccessControl: restricted set of users
for certain operations
• Currencies
• Cryptographic concepts
Writing the specification
• For each method: requires, ensures,
exsures, modifies
• First basic classes (utils), then more
application-specific
• Appropriate class invariants, e.g.
restricting domain of instance variables
Writing the specification
• Discrepancies between documentation
and implementation
Writing the specification
• Discrepancies between documentation
and implementation
Writing the specification
• Discrepancies between documentation
and implementation
• Usage of existing API specification
Writing the specification
• Discrepancies between documentation
and implementation
• Usage of existing API specification
• .spec files for e.g. visa and crypto
classes
Writing the specification
• Discrepancies between documentation
and implementation
• Usage of existing API specification
• .spec files for e.g. visa and crypto
classes
• Avoid warnings as much as possible,
but still full specification
Class invariants
Restrict state space of a class
– reference never null pointer
//@ invariant purse != null;
– variable within a certain range
/*@ invariant decPart
decPart
invariant intPart
intPart
*/
>= 0 &&
< PRECISION;
>= 0 &&
< MAX_DECIMAL_NUMBER;
Easy to write, easy to check
Enumeration types
/* the transaction status*/
public static final byte INDETERMINE
= (byte)0;
. . .
/* the
public
/* the
public
transaction status*/
static final byte TYPE_CREDIT
transaction status*/
static final byte TYPE_DEBIT
= (byte)50;
= (byte)51;
. . .
/* the transaction type: debit or credit*/
private byte type;
/* the transaction type: debit or credit*/
private byte type;
. . .
/* set all this transaction attributes to 0*/
void reset() {
isValid = false;
number = (short)0;
type = INDETERMINE;
typeProduit = (short)0;
. . .
}
Enumeration types
/*@ invariant condition
condition
condition
condition
condition
==
==
==
==
==
FREE ||
LOCKED ||
SECRET_CODE ||
SECURE_MESSAGING ||
(SECRET_CODE |
SECURE_MESSAGING) */
public AccessCondition() {
super();
// commented by Rodolphe Muller on 16/06/2000
// strange to set the condition here to 0 and to
// FREE above
setCondition((byte)0);
}
NB. FREE == (byte)1;
Avoiding dead code
switch(condition) {
case FREE: ...
case SECRET_CODE: ...
case SECURE_MESSAGING: ...
case SECRET_CODE | SECURE_MESSAGING: ...
case LOCKED: ...
default:
//@ assert false;
t = AccessConditionException.C_C_INVALIDE;
AccessConditionException.throwIt(t);
}
Other problems
• Incorrect coding
• Forgetting variable modifiers (final)
• Underspecified documentation
Is MAX_DECIMAL_NUMBER.999 legal?
And how do you round it?
• Superfluous methods (isNegatif())
• Complex and undocumented
datastructures (with incorrect corrections)
Complete specification
Available from
http://www-sop.inria.fr/lemme/
verificard/electronic_purse
Conclusions
• Using lightweight formal methods,
applications can be improved
• Class invariants make implicit
assumptions explicit and check them
• Case study convinced Gemplus to look
at JML and ESC/Java
• ESC/Java useful, but possibilities for
improvement
Complete specification
Available from
http://www-sop.inria.fr/lemme/
verificard/electronic_purse
Writing the specification
/*@ modifies M;
requires true;
ensures Q;
exsures (E) !P;
*/
void m () {
. . .
}
Writing the specification
Offensive
/*@ modifies M;
requires P;
ensures Q;
exsures (E) false;
*/
void m () {
. . .
}
Defensive
/*@ modifies M;
requires true;
ensures Q;
exsures (E) !P;
*/
void m () {
. . .
}
Experiences with ESC/Java
• Pleasant tool, easy to work with
• Specifications written by nonexperienced user
• Two/three months work all together
Suggestions for ESC/Java
specification language
• Richer specification language
modifies \nothing, modifies \field_of(E)
• Extra quantifiers
• Run-time exceptions without explicit
throws clause
• Use of pure methods in specifications
Example specification
modifies sessionNumber, date.jour, date.mois,
date.annee, heure.heure, heure.minute;
modifies ancienneDevise, nouvelleDevise, isValid, status;
modifies id[*], terminalTC[*], terminalSN[*] ;
requires es != null ;
requires es.id != terminalTC & es.id != terminalSN &
es.terminalTC != terminalSN;
ensures sessionNumber == es.sessionNumber ;
ensures ancienneDevise == es.ancienneDevise ;
ensures nouvelleDevise == es.nouvelleDevise ;
ensures isValid == es.isValid ;
ensures status == es.status ;
ensures (\forall int i;0 <= i & i < ID_LENGTH ==>
es.id[i] == id[i]);
ensures (\forall int i;0 <= i & i < TTC_LENGTH ==>
es.terminalTC[i] == terminalTC[i]);
ensures (\forall int i;0 <= i & i < TSN_LENGTH ==>
es.terminalSN[i] == terminalSN[i]);
exsures (TransactionException e)
e._reason
e._reason ==
== TransactionException.BUFFER_FULL
TransactionException.BUFFER_FULL &&
&&
JCSystem._transactionDepth == 1;
exsures (NullPointerException) false;
exsures (ArrayIndexOutOfBoundsException) false;
And as we would like it to be...
modifies sessionNumber, date.jour, date.mois,
date.annee, heure.heure, heure.minute;
modifies ancienneDevise, nouvelleDevise, isValid,
status;
modifies id[*], terminalTC[*], terminalSN[*] ;
requires es != null ;
requires es.id != terminalTC & es.id != terminalSN &
es.terminalTC != terminalSN;
ensures this.equal(es);
exsures (TransactionException e)
e._reason == TransactionException.BUFFER_FULL
&& JCSystem._transactionDepth == 1;
exsures (NullPointerException) false;
exsures (ArrayIndexOutOfBoundsException) false;
NO Verification of modifies
clauses
Specification
/*@ modifies x;
accepted
ensures x == 3;
*/
void m()
{ x = 3;
n (); }
Missing modifies clause
void n() { x = 4; }
Modifies clauses
• Implementation of modifiable checker
• Extension of JML
• Static checking technique, based on
syntax
• Neither sound, nor complete
• Fully described in separate paper
(ask Néstor or me)
Future work
• Develop application with annotations
from scratch
• Extension to multi-threading
• Automated verification technique for
termination of loops
• Cryptographic aspects of the
specification