Towards Certifiably Correct
Java Card Applets
Alessandro Coglio
joint work with:
Matthias Anlauff David Cyrluk
Li-Mei Gilham Lambert Meertens
Kestrel Institute
IFIP WG 2.1 Meeting #60 (May 2005)
Java
Java
Enterprise Edition
Standard Edition
Java
S
I
Z
E
Micro Edition
chip
Card
plastic
substrate
smart
cards
authentication,
banking,
telephony,
health care,
…
Standard Edition
Java
• language
?
•  API
Card

Java Card
program
Java
bytecode
program
JAVA
COMPILER
Java Card
applet
JAVA CARD
CONVERTER
(checks subset & API)
...
APPLET
...
JAVA CARD RUNTIME
ENVIRONMENT (JCRE)
BYTECODE
INTERPRETER
API
LIBRARY
SMART CARD HW/OS
Java Card applet

Java web applet
typically
written
by hand
Java Card
program
somewhat
low-level
 error-prone
applet
spec
Java Card
program
AutoSmart
(automatic generator of smart card applets)
applet
spec
AUTOSMART
for
• high assurance
• productivity
Java Card
program
AutoSmart
(automatic generator of smart card applets)
applet
spec
applet
spec
AUTOSMART
Java Card
program
AUTOSMART
Java Card
program
AutoSmart
(automatic generator of smart card applets)
applet
spec
AUTOSMART
Java Card
program
proof
CHECKER
yes/no
smaller & simpler
than AutoSmart
 easier to trust
applet
spec
written in
SmartSlang
AUTOSMART
Java Card
program
SmartSlang
(smart card specification language)
SmartSlang
SmartSlang
(smart card specification language)
domain-specific language
domain = smart cards
i.e. constructs specialized to smart card applications
under design
basic version done,
many additional constructs planned
precise semantics
in terms of state machines
applet : Command  State  Response  State
but no formal background necessary
SmartSlang
SmartSlang
example: e-wallet
SmartSlang example: e-wallet
expressive type system
type Balance = Int(0,MAX_BALANCE);
e.g. integer ranges
type Amount = Int(1,MAX_AMOUNT);
1000000
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
state { Balance balance }
(vs. byte/short/int in JC)
• capture semantics (short,
• automatic mapping short)
to JC types
int
e.g. Balance  short
Amount  byte
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
pervasive change
} else {
in Java Card code
respond EXCEEDED_BALANCE;
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
state { Balance balance } explicit state components
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
respond EXCEEDED_BALANCE;
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
state { Balance balance }
explicit symbolic commands
with high-level parameters
(vs. APDU bytes in JC)
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
respond EXCEEDED_BALANCE;
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
state { Balance balance }
• familiar to
developers
• “superset of
subset of Java”
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
simple Java-like
} else {
expressions &
respond EXCEEDED_BALANCE;
statements
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
state { Balance balance }
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
respond EXCEEDED_BALANCE; explicit responses
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
all type safety
checked statically
(conservatively)
• catches user errors
state { Balance balance }
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount; type-safe assignment
} else {
respond EXCEEDED_BALANCE;
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
all type safety
checked statically
(conservatively)
• catches user errors
state { Balance balance }
command credit(Amount amount) {
balance = balance + amount;
type-safe assignment
user gets warning
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
all type safety
checked statically
const MAX_BALANCE = 10000;
(conservatively)
const MAX_AMOUNT = 100;
• catches user errors
• no runtime errors
state { Balance balance }
(e.g. array access)
• type checker uses
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) { automated reasoning
balance = balance + amount; type-safe assignment
} else {
no such thing in JC!
respond EXCEEDED_BALANCE;
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
state { Balance balance }
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
declarative APDU encoding (vs.
respond EXCEEDED_BALANCE;
explicit decoding/dispatch in JC)
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
lengthy, error-prone JC
decoding/dispatching code
automatically generated
SmartSlang example: e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
state { Balance balance }
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
respond EXCEEDED_BALANCE;
amount encoded as byte
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
const EXCEEDED_BALANCE = 0x6A84;
...
JC code to handle user
input data errors
(e.g. if amount > 100)
automatically generated
e-wallet
example
example
e-wallet
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
state { Balance balance }
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const BALANCE_BYTES = ubytes(MAX_BALANCE).length;
const AMOUNT_BYTES = ubytes(MAX_AMOUNT).length;
state {
Balance balance
}
init() {
balance = 0;
} bytes {};
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
respond EXCEEDED_BALANCE;
}
} apdu {CLA,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
respond
EXCEEDED_BALANCE;
SmartSlang
spec
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
command debit(Amount amount) {
if (balance - amount >= 0) {
balance = balance - amount;
} else {
respond NEGATIVE_BALANCE;
}
} apdu {CLA,0x40,0,0,ubytes[AMOUNT_BYTES](amount),0};
command getBalance() {
respondok ubytes[BALANCE_BYTES](balance);
} apdu {CLA,0x50,0,0,{},BALANCE_BYTES};
const CLA = 0x80;
const EXCEEDED_BALANCE = 0x6A84;
const NEGATIVE_BALANCE = 0x6A85;
const EXCEEDED_BALANCE = 0x6A84;
...
e-wallet example
package pkg;
import javacard.framework.*;
import javacard.security.*;
import javacardx.crypto.*;
class Wallet extends Applet {
size(code)
= ~ 3–4
size(spec)
static
static
static
static
static
static
static
final
final
final
final
final
final
final
short MAX_BALANCE = 10000;
short MAX_AMOUNT = 100;
short BALANCE_BYTES = 2;
short AMOUNT_BYTES = 1;
short EXCEEDED_BALANCE = 0x6A84;
byte CLA = (byte)0x80;
short NEGATIVE_BALANCE = 0x6A85;
short balance;
static byte[] _aux1;
~ 150
lines
byte[] inData;
short inDataLength; // always <= 255
private A (byte[] initpar, short off, byte len) {
_aux1 = new byte[2];
inData = new byte[255]; // command data is 255 bytes max
balance = 0;
register(initpar,(short)(off + 1),initpar[off]);
}
public boolean select () {
return true;
}
~ 40 lines
public void process (APDU apdu) {
if (selectingApplet()) return;
byte[] buffer = apdu.getBuffer();
if (buffer[ISO7816.OFFSET_CLA] != (byte)0x80)
ISOException.throwIt(ISO7816.SW_CLA_NOT_SUPPORTED);
switch (buffer[ISO7816.OFFSET_INS]) {
case 0x30:
credit(apdu);
return;
case 0x40:
debit(apdu);
return;
case 0x50:
getBalance(apdu);
return;
default:
ISOException.throwIt(ISO7816.SW_INS_NOT_SUPPORTED);
}
}
const MAX_BALANCE = 10000;
const MAX_AMOUNT = 100;
void credit (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) || (buffer[ISO7816.OFFSET_P2] != 0))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength = nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (inDataLength != 1)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
short amount = nonNegativeByte(inData[0]);
if ((amount < 1) || (amount > 100))
ISOException.throwIt(ISO7816.SW_WRONG_DATA);
if ((short)(balance + amount) <= MAX_BALANCE)
balance = (short)(balance + amount);
else
ISOException.throwIt((short)EXCEEDED_BALANCE);
}
type Balance = Int(0,MAX_BALANCE);
type Amount = Int(1,MAX_AMOUNT);
const BALANCE_BYTES = ubytes(MAX_BALANCE).length;
const AMOUNT_BYTES = ubytes(MAX_AMOUNT).length;
state {
Balance balance
}
init() {
balance = 0;
} bytes {};
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
respond EXCEEDED_BALANCE;
}
} apdu {CLA,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
command debit(Amount amount) {
if (balance - amount >= 0) {
balance = balance - amount;
} else {
respond NEGATIVE_BALANCE;
}
} apdu {CLA,0x40,0,0,ubytes[AMOUNT_BYTES](amount),0};
void debit (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) || (buffer[ISO7816.OFFSET_P2] != 0))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength = nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (inDataLength != 1)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
short amount = nonNegativeByte(inData[0]);
if ((amount < 1) || (amount > 100))
ISOException.throwIt(ISO7816.SW_WRONG_DATA);
if ((short)(balance - amount) >= 0)
balance = (short)(balance - amount);
else
ISOException.throwIt((short)NEGATIVE_BALANCE);
}
AUTOSMART
command getBalance() {
respondok ubytes[BALANCE_BYTES](balance);
} apdu {CLA,0x50,0,0,{},BALANCE_BYTES};
void getBalance (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) || (buffer[ISO7816.OFFSET_P2] != 0))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
short requiredLe = BALANCE_BYTES;
short receivedLe = nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (receivedLe == 0)
receivedLe = 256;
if (receivedLe != requiredLe) {
short swLow = (short)(requiredLe & 0xff);
ISOException.throwIt((short)(ISO7816.SW_CORRECT_LENGTH_00 + swLow));
}
byte[] _aux1 = Wallet._aux1;
ubytes((short)2,balance,_aux1);
sendOutgoingData(apdu,_aux1);
return;
}
const CLA = 0x80;
const EXCEEDED_BALANCE = 0x6A84;
const NEGATIVE_BALANCE = 0x6A85;
static void ubytes(short n, short i, byte[] result) {
for (short k = (short)(n - 1); k >= 0; k--) {
result[k] = (byte) (i & 0xff);
i = (short) (i >>> 8);
}
}
SmartSlang spec
static short nonNegativeByte(byte b) {
return (b < 0 ? (short)(b + 256) : b);
}
void receiveIncomingData(APDU apdu) {
byte[] buffer = apdu.getBuffer();
short totalRead = 0;
short chunkRead = apdu.setIncomingAndReceive();
do {
// error if too little or too much data:
if (chunkRead == 0 ||
(short) (totalRead + chunkRead) > inDataLength)
ISOException.throwIt(ISO7816.SW_WRONG_DATA);
// transfer from APDU buffer to inData array:
Util.arrayCopy(buffer,ISO7816.OFFSET_CDATA,
inData,totalRead,chunkRead);
// increment counter:
totalRead += chunkRead;
// get more data if necessary:
if (totalRead != inDataLength)
chunkRead = apdu.receiveBytes(ISO7816.OFFSET_CDATA);
} while (totalRead < inDataLength);
}
void sendOutgoingData(APDU apdu, byte[] data) {
apdu.setOutgoing();
apdu.setOutgoingLength((short)data.length);
apdu.sendBytesLong(data,(short)0,(short)data.length);
}
public static void install(byte[] initpar, short off, byte len) {
new Wallet(initpar,off,len);
}
}
(actual files; font size 2)
Java
Card
code
e-wallet
Java Card code
e-wallet
...
void credit (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) ||
(buffer[ISO7816.OFFSET_P2] != 0))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength =
nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (inDataLength != 1)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
short amount = nonNegativeByte(inData[0]);
if ((amount < 1) || (amount > 100))
ISOException.throwIt(ISO7816.SW_WRONG_DATA);
Java
if ((short)(balance + amount) <= MAX_BALANCE)
balance = (short)(balance + amount);
Card
else
code
ISOException.throwIt((short)EXCEEDED_BALANCE);
}
...
...
void credit (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) ||
(buffer[ISO7816.OFFSET_P2] != 0))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength =
nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (inDataLength != 1)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
short amount = nonNegativeByte(inData[0]);
if ((amount < 1) || (amount > 100))
ISOException.throwIt(ISO7816.SW_WRONG_DATA);
if ((short)(balance + amount) <= MAX_BALANCE)
balance = (short)(balance + amount);
else
ISOException.throwIt((short)EXCEEDED_BALANCE);
}
...
e-wallet Java Card code
...
void credit (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) ||
(buffer[ISO7816.OFFSET_P2] != 0))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength =
nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (inDataLength != 1)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
short amount = nonNegativeByte(inData[0]);
if ((amount < 1) || (amount > 100))
ISOException.throwIt(ISO7816.SW_WRONG_DATA);
if ((short)(balance + amount) <= MAX_BALANCE)
interesting
balance = (short)(balance + amount);
computation else
ISOException.throwIt((short)EXCEEDED_BALANCE);
}
...
e-wallet Java Card code
...
void credit (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) ||
(buffer[ISO7816.OFFSET_P2] != 0))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength =
nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
APDU
checking if (inDataLength != 1)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
& decoding
receiveIncomingData(apdu);
short amount = nonNegativeByte(inData[0]);
if ((amount < 1) || (amount > 100))
ISOException.throwIt(ISO7816.SW_WRONG_DATA);
if ((short)(balance + amount) <= MAX_BALANCE)
balance = (short)(balance + amount);
else
ISOException.throwIt((short)EXCEEDED_BALANCE);
}
...
SmartSlang counterpart
...
command credit(Amount amount) {
if (balance + amount <= MAX_BALANCE) {
balance = balance + amount;
} else {
respond EXCEEDED_BALANCE;
}
} apdu {0x80,0x30,0,0,ubytes[AMOUNT_BYTES](amount),0};
...
SmartSlang example: PKI
SmartSlang
SmartSlang example: PKI
type
type
type
type
Key = RSAPrivateKey(1024); built-in key types
Message = Byte[1024/8];
automatic mapping to JC API classes
Pin = Byte[8];
PinState = enum {blocked, notVerified(Int(1,3)), ...};
state { Key key, Pin pin, PinState pinState, ... }
command privSignDecrypt(Message msg) {
if (pinState != verified) {
respond SW_SECURITY_NOK;
} else {
respondok decrypt(key,msg);
}
} apdu {0x80,0x42,0,0,msg,1024/8};
secure command putPIN(Pin newPin) {
pin = newPin;
pinState = notVerified(3);
} apdu {0x80,0x22,0,0,newPin,0};
...
SmartSlang example: PKI
type
type
type
type
Key = RSAPrivateKey(1024);
Message = Byte[1024/8];
Pin = Byte[8];
PinState = enum {blocked, notVerified(Int(1,3)), ...};
state { Key key, Pin pin, PinState pinState, ... }
command privSignDecrypt(Message msg) {
if (pinState != verified) {
respond SW_SECURITY_NOK;
built-in cryptographic functions
} else {
respondok decrypt(key,msg); (vs. multiple API method calls in JC)
}
• simple
} apdu {0x80,0x42,0,0,msg,1024/8};
secure command putPIN(Pin newPin) {
pin = newPin;
pinState = notVerified(3);
} apdu {0x80,0x22,0,0,newPin,0};
...
• automatic mapping
to JC API method calls
SmartSlang example: PKI
type
type
type
type
Key = RSAPrivateKey(1024);
Message = Byte[1024/8];
(# tries left)
Pin = Byte[8];
PinState = enum {blocked, notVerified(Int(1,3)), ...};
enumeration
types
state { Key key, Pin pin, PinState pinState, ... }
command privSignDecrypt(Message msg) {
if (pinState != verified) {
respond SW_SECURITY_NOK;
} else {
respondok decrypt(key,msg);
}
} apdu {0x80,0x42,0,0,msg,1024/8};
secure command putPIN(Pin newPin) {
pin = newPin;
pinState = notVerified(3);
} apdu {0x80,0x22,0,0,newPin,0};
...
• with arguments
• automatic mapping
to byte constants +
auxiliary variables
for arguments in JC
SmartSlang example: PKI
type
type
type
type
Key = RSAPrivateKey(1024);
Message = Byte[1024/8];
Pin = Byte[8];
PinState = enum {blocked, notVerified(Int(1,3)), ...};
state { Key key, Pin pin, PinState pinState, ... }
command privSignDecrypt(Message msg) {
if (pinState != verified) {
respond SW_SECURITY_NOK;
} else {
spread change in
respondok decrypt(key,msg);
Java Card code
}
} apdu {0x80,0x42,0,0,msg,1024/8};
construct for Global Platform
secure command putPIN(Pin newPin) { secure channels (vs. multiple
pin = newPin;
API method calls in JC)
pinState = notVerified(3);
} apdu {0x80,0x22,0,0,newPin,0};
...
• simple, localized
• automatic mapping to
JC API method calls
SmartSlang example: PKI
type
type
type
type
Key = RSAPrivateKey(1024);
Message = Byte[1024/8];
Pin = Byte[8];
PinState = enum {blocked, notVerified(Int(1,3)), ...};
state { Key key, Pin pin, PinState pinState, ... }
command privSignDecrypt(Message msg) {
if (pinState != verified) {
decryption result computed on the
respond SW_SECURITY_NOK;
} else {
fly and returned (vs. pre-allocated
respondok decrypt(key,msg); intermediate storage in JC)
}
• simple functional model
} apdu {0x80,0x42,0,0,msg,1024/8};
secure command putPIN(Pin newPin) {
pin = newPin;
pinState = notVerified(3);
} apdu {0x80,0x22,0,0,newPin,0};
...
• automatic mapping to
pre-allocated intermediate
storage in JC
automatic static storage
management is significant
advantage for smart cards!
PKI example
example PKI
type
type
type
type
Key = RSAPrivateKey(1024);
Message = Byte[1024/8];
Pin = Byte[8];
PinState = enum {blocked, notVerified(Int(1,3)), ...};
const K EY_SI ZE = 1024 ; // in bi ts
type Ke yStat e = rec { Bool isExp onent Set, Bool isMo dulus Set};
const M SG_SI ZE = KEY_ SIZE / 8; // in byt es
type Me ssage = B yte[M SG_SI ZE];
const P IN_SI ZE = 8;
type Pi n = B yte[ PIN_S IZE];
const M AX_TR IES = 3;
type Pi nStat e = enum {unse t, no tVeri fied (Int( 1,MAX _TRIE S)), veri fied, bloc ked};
const M AX_CE RT_S IZE = 1000 ; // in by tes
type Ce rtifi cate = By te[0. .MAX_ CERT_ SIZE ];
const M AX_CE RT_C HUNK_ SIZE = 100 ; // in b ytes
type Ce rtifi cate Chunk = By te[1. .MAX_ CERT _CHUN K_SIZ E];
const M AX_PR OP_S IZE = 200; // i n byt es
type Pr opert ies = Byt e[0.. MAX_P ROP_S IZE] ;
type Ap pletS tate = en um {p erson aliza tion , dep loyme nt, u pdati ng};
state {
RSAPr ivate Key( KEY_S IZE) key,
KeySt ate
keySt ate,
Pin
pin,
PinSt ate
pinSt ate,
Int(0 ,MAX_ CERT _SIZE )
certS ize,
Certi ficat e
certi ficat e,
Prope rties
prope rties ,
Int(0 ,MAX_ CERT _SIZE )
certB ytesS ent,
Apple tStat e
apple tStat e
}
state { Key key, Pin pin, PinState pinState, ... }
invaria nt ap plet State != d eploy ment || ( certB ytesS ent < = (ce rtif icate ).len gth-1 );
init() {
/* Th e cur rent defi nitio n of Smart Slan g req uires ever y sta te c ompon ent t o be
initi alize d in the initi aliza tion bloc k. Th is is a bi t art ific ial f or
certa in st ate compo nents that are real ly in itial ized by co mman ds, e .g. k eys,
forci ng us to use m eanin gless valu es l ike a ll 0s . We may c hang e the
defin ition of Smart Slang to n o lon ger requi re al l sta te co mpon ents to be
initi alize d in the initi aliza tion bloc k, wh ile l eavin g the req uirem ent t hat
every stat e co mpone nt mu st be init iali zed b efore it i s use d fo r the firs t
time. Besi des avoid ing a rtifi cial init ializ ation s, th is ch ange woul d sup port
bette r sem anti c che cking of t he Sm artS lang spec, beca use p resu mably a ke y
shoul dn't be u sed b efore it i s ass igne d a n on-al l-0s value . */
key
= RSA Priva teKey (KEY_ SIZE )
( repea t(0,K EY_SI ZE/8 ), re peat( 0,KEY _SIZE /8)) ;
keySt ate
= Key State (fals e,fal se);
pin
= rep eat(0 ,8);
pinSt ate
= uns et;
certS ize
= 0;
certi ficat e
= {};
prope rties
= {};
certB ytesS ent = 0;
apple tStat e
= per sonal izati on;
} bytes {};
command putE xpon ent(B yte[K EY_SI ZE/8] exp ) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
key = RSAP riva teKey (KEY_ SIZE) (exp , ke y.mod ulus) ;
keySt ate = Key State (tru e, ke yStat e.is Modul usSet );
// we may exte nd Sm artSl ang w ith d irec t ass ignme nts t o rec ord compo nents :
// ke y.exp onen t = e xp;
// ke yStat e.is Expon entSe t =tr ue;
} apdu {CLA, INS _PUT_ EXP, P1, P 2, ex p, 0 };
command privSignDecrypt(Message msg) {
if (pinState != verified) {
respond SW_SECURITY_NOK;
} else {
respondok decrypt(key,msg);
}
} apdu {0x80,0x42,0,0,msg,1024/8};
command putM odul us(By te[KE Y_SIZ E/8] mod) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
key = RSAP riva teKey (KEY_ SIZE) (key .exp onent , mod );
keySt ate = Key State (key State .isEx pone ntSet , tru e);
} apdu {CLA, INS _PUT_ MOD, P1, P 2, mo d, 0 };
command putP IN(P in p) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
pin = p;
pinSt ate = not Verif ied(M AX_TR IES);
} apdu {CLA, INS _PUT_ PIN, P1, P 2, p, 0};
command putC erti ficat eSize (Int( 1,MAX _CER T_SIZ E) si ze) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
certS ize = siz e;
certi ficat e = {};
} apdu {CLA, INS _CERT _SIZE , P1, P2, ubyt es[2] (size ), 0} ;
command putC erti ficat eChun k(Cer tific ateC hunk certC hunk) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
if (c ertSi ze = = 0) { res pond SW_CE RT_S IZE_U NSET; }
if (c ertif icat e.len gth + cert Chunk .len gth > cert Size)
{ r espon d SW _CERT IFICA TE_TO O_LAR GE; }
certi ficat e = certi ficat e ++ certC hunk ;
} apdu {CLA, INS _PUT_ CERT, P1, P2, c ertC hunk, 0};
command putP rope rties (Prop ertie s pro p) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
prope rties = p rop;
} apdu {CLA, INS _PUT_ PROP, P1, P2, p rop, 0};
command unbl ockP IN() {
if (a pplet Stat e != updat ing) { res pond SW_W RONG_ STATE ; }
pinSt ate = not Verif ied(M AX_TR IES);
} apdu {CLA, INS _UNBL OCK, P1, P 2, {} , 0} ;
command depl oy() {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
if (k eySta te
= = Key State (tru e,tru e)
&& p inSta te
! = uns et
&& c ertSi ze
!= 0
&& c ertif icat e.len gth = = cer tSize
&& p roper ties
! = {}) {
app letSt ate = dep loyme nt;
} els e {
res pond SW_U NFINI SHED_ PERSO NALIZ ATIO N;
}
} apdu {CLA, INS _DEPL OY, P 1, P2 , {}, 0};
command upda te() {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
apple tStat e = updat ing;
} apdu {CLA, INS _UPDA TE, P 1, P2 , {}, 0};
command getC erti ficat eChun k() {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
Certi ficat eChu nk ch unk;
if (c ertif icat e.len gth - cert Bytes Sent >= M AX_CE RT_CH UNK_S IZE) {
chu nk = cert ifica te[ce rtByt esSen t,MA X_CER T_CHU NK_SI ZE];
cer tByte sSen t = c ertBy tesSe nt + MAX_ CERT_ CHUNK _SIZE ;
} els e {
chu nk = cert ifica te[ce rtByt esSen t..c ertif icate .leng th-1] ;
cer tByte sSen t = c ertif icate .leng th;
}
if (c ertif icat e.len gth - cert Bytes Sent >= M AX_CE RT_CH UNK_S IZE) {
res pond {chu nk, S W1_MO RE_DA TA, M AX_C ERT_C HUNK_ SIZE} ;
} els e if (cer tific ate.l ength - ce rtBy tesSe nt > 0) {
res pond {chu nk, S W1_MO RE_DA TA, c erti ficat e.len gth - cert Byte sSent };
} els e /* cert ifica te.le ngth == ce rtBy tesSe nt */ {
cer tByte sSen t = 0 ; // reset
res pondo k ch unk;
}
} apdu {CLA, INS _GET_ CERT, P1, P2, { },
(cer tifi cate. lengt h - c ertBy tesS ent > = MAX _CERT _CHUN K_SI ZE) ?
MAX_ CERT _CHUN K_SIZ E : c ertif icat e.len gth - cert Bytes Sent };
command getP rope rties () {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
respo ndok prop ertie s;
} apdu {CLA, INS _GET_ PROP, P1, P2, { }, p roper ties. lengt h};
command pinV erif y(Pin p) {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
switc h (pi nSta te) {
cas e ver ifie d: {
r espon dok;
}
cas e not Veri fied( tries Left) : {
i f (p == p in) {
pinS tate = ve rifie d;
resp ondo k;
} else if (trie sLeft > 1) {
pinS tate = no tVeri fied( tries Left - 1) ;
resp ond {{}, SW1_W RONG_ PIN, trie sLeft };
} else {
pinS tate = bl ocked ;
resp ond SW_PI N_BLO CKED;
}
}
cas e blo cked : {
r espon d SW _PIN_ BLOCK ED;
}
cas e uns et: {
/ / can not happe n -- could be p rove d usi ng st ate i nvari ants
}
}
} apdu {CLA, INS _VERI FY, P 1, P2 , p, 0};
command pinV erif ied() {
if (a pplet Stat e != deplo yment ) {
switc h (pi nSta te) {
cas e ver ifie d: {
r espon dok;
}
cas e not Veri fied( tries Left) : {
r espon d {{ }, SW 1_TRI ES_LE FT,
}
cas e blo cked : {
r espon d SW _PIN_ BLOCK ED;
}
cas e uns et: {
/ / can not happe n -- could be
}
}
} apdu {CLA, INS _VERI FIED, P1, P2,
r espo nd SW _WRON G_STA TE; }
t ries Left} ;
p rove d usi ng st ate i nvari ants
{ }, 0 };
command priv Sign Decry pt(Me ssage msg) {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
if (p inSta te ! = ver ified ) {
res pond SW_S ECURI TY_NO K;
} els e {
res pondo k rs a(key ,msg) ;
}
} apdu {CLA, INS _SIGN _DEC, P1, P2, m sg, MSG_S IZE};
const C LA = 0x80 ;
const P 1 = 0 ;
const P 2 = 0 ;
const
const
const
const
const
const
const
const
const
const
const
const
const
const
I NS_PU T_EX P
I NS_PU T_MO D
I NS_PU T_PI N
I NS_CE RT_S IZE
I NS_PU T_CE RT
I NS_PU T_PR OP
I NS_UN BLOC K
I NS_DE PLOY
I NS_UP DATE
I NS_GE T_CE RT
I NS_GE T_PR OP
I NS_VE RIFY
I NS_VE RIFI ED
I NS_SI GN_D EC
=
=
=
=
=
=
=
=
=
=
=
=
=
=
0x44 ;
0x46 ;
0x22 ;
0x3A ;
0x38 ;
0x58 ;
0x24 ;
0x70 ;
0x72 ;
0x36 ;
0x56 ;
0x20 ;
0x26 ;
0x42 ;
secure command putPIN(Pin newPin) {
pin = newPin;
pinState = notVerified(3);
} SmartSlang
apdu {0x80,0x22,0,0,newPin,0};
spec
const S W_WRO NG_S TATE
= 0x 6985;
const S W_CER TIFI CATE_ TOO_L ARGE
= 0x 6A80;
const S W_UNF INIS HED_P ERSON ALIZA TION = 0x 6985;
const S W_PIN _BLO CKED
= 0x 6983;
const S W_SEC URIT Y_NOK
= 0x 6982;
const S W_CER T_SI ZE_UN SET
= 0x 6985;
const S W1_WR ONG_ PIN
= 0x 63;
const S W1_TR IES_ LEFT
= 0x 63;
const S W1_MO RE_D ATA
= 0x 63;
select {
certB ytesS ent = 0; // re set
}
deselec t {
if (p inSta te = = ver ified ) {
pin State = n otVer ified (MAX_ TRIES );
}
}
...
PKI example
package pkg;
import javac ard. frame work. *;
import javac ard. secur ity.* ;
import javac ardx .cryp to.*;
class A exte nds Apple t {
}
stati c fin al s hort KEY_S IZE = 1024 ;
stati c fin al b yte P IN_SI ZE = 8;
stati c fin al b yte M AX_TR IES = 3;
void getCertificateChunk (APDU apdu)
{
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != P1) || (buffer[ISO7816.OFFSET_P2] != P2))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
short requiredLe = MAX_CERT_CHUNK_SIZE;
short receivedLe = A.nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (receivedLe == 0)
receivedLe = 256;
if (receivedLe != requiredLe)
{
short swLow = (short)(requiredLe & 0xff);
ISOException.throwIt((short)(ISO7816.SW_CORRECT_LENGTH_00 + swLow));
}
if (appletState != AppletState.deployment)
ISOException.throwIt(SW_WRONG_STATE);
if ((short)(certificate.size() - certBytesSent) >= MAX_CERT_CHUNK_SIZE)
{
A.subarrayFromLength(certificate,
certBytesSent,
MAX_CERT_CHUNK_SIZE,
chunk,
(short)0,
false);
certBytesSent = (short)(certBytesSent + MAX_CERT_CHUNK_SIZE);
}
else
{
A.subarrayFromLength(certificate,
certBytesSent,
(short)(((certificate.size() - 1)
- certBytesSent)
+ 1),
chunk,
(short)0,
false);
certBytesSent = certificate.size();
}
if ((short)(certificate.size() - certBytesSent) >= MAX_CERT_CHUNK_SIZE)
{
sendOutgoingData(apdu, chunk.data, chunk.len);
ISOException.throwIt(Util.makeShort(SW1_MORE_DATA,
MAX_CERT_CHUNK_SIZE));
}
else
if ((short)(certificate.size() - certBytesSent) > 0)
{
sendOutgoingData(apdu, chunk.data, chunk.len);
ISOException.throwIt(Util.makeShort(SW1_MORE_DATA,
(byte)(certificate.size()
- certBytesSent)));
}
else
{
certBytesSent = 0;
sendOutgoingData(apdu, chunk.data, chunk.len);
return;
}
}
stati c fin al s hort MAX_C ERT_S IZE = 100 0;
stati c fin al b yte M AX_CE RT_CH UNK_S IZE = 100 ;
~ 240 lines
const K EY_SI ZE = 1024 ; // in bi ts
type Ke yStat e = rec { Bool isExp onent Set, Bool isMo dulus Set};
const M SG_SI ZE = KEY_ SIZE / 8; // in byt es
type Me ssage = B yte[M SG_SI ZE];
const P IN_SI ZE = 8;
type Pi n = B yte[ PIN_S IZE];
const M AX_TR IES = 3;
type Pi nStat e = enum {unse t, no tVeri fied (Int( 1,MAX _TRIE S)), veri fied, bloc ked};
const M AX_CE RT_S IZE = 1000 ; // in by tes
type Ce rtifi cate = By te[0. .MAX_ CERT_ SIZE ];
const M AX_CE RT_C HUNK_ SIZE = 100 ; // in b ytes
type Ce rtifi cate Chunk = By te[1. .MAX_ CERT _CHUN K_SIZ E];
const M AX_PR OP_S IZE = 200; // i n byt es
type Pr opert ies = Byt e[0.. MAX_P ROP_S IZE] ;
type Ap pletS tate = en um {p erson aliza tion , dep loyme nt, u pdati ng};
state {
RSAPr ivate Key( KEY_S IZE) key,
KeySt ate
keySt ate,
Pin
pin,
PinSt ate
pinSt ate,
Int(0 ,MAX_ CERT _SIZE )
certS ize,
Certi ficat e
certi ficat e,
Prope rties
prope rties ,
Int(0 ,MAX_ CERT _SIZE )
certB ytesS ent,
Apple tStat e
apple tStat e
}
stati c fin al s hort MAX_P ROP_S IZE = 200 ;
stati c fin al s hort SW_WR ONG_S TATE = 0x 6985;
stati c fin al b yte C LA = (byte )0x80 ;
stati c fin al b yte I NS_PU T_EXP = 0x 44;
stati c fin al b yte P 1 = 0 ;
stati c fin al b yte P 2 = 0 ;
stati c fin al b yte I NS_PU T_MOD = 0x 46;
stati c fin al b yte I NS_PU T_PIN = 0x 22;
stati c fin al b yte I NS_CE RT_SI ZE = 0x3a ;
stati c fin al s hort SW_CE RT_SI ZE_UN SET = 0x6 985;
size(code)
=~3
size(spec)
stati c fin al s hort SW_CE RTIFI CATE_ TOO_ LARGE = 0x 6a80;
stati c fin al b yte I NS_PU T_CER T = 0 x38;
stati c fin al b yte I NS_PU T_PRO P = 0 x58;
stati c fin al b yte I NS_UN BLOCK = 0x 24;
stati c fin al s hort SW_UN FINIS HED_P ERSO NALIZ ATION = 0x 6985;
stati c fin al b yte I NS_DE PLOY = 0x7 0;
stati c fin al b yte I NS_UP DATE = 0x7 2;
stati c fin al b yte S W1_MO RE_DA TA = 0x63 ;
void getProperties (APDU apdu)
{
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != P1) || (buffer[ISO7816.OFFSET_P2] != P2))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
short requiredLe = properties.size();
short receivedLe = A.nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (receivedLe == 0)
receivedLe = 256;
if (receivedLe != requiredLe)
{
short swLow = (short)(requiredLe & 0xff);
ISOException.throwIt((short)(ISO7816.SW_CORRECT_LENGTH_00 + swLow));
}
if (appletState != AppletState.deployment)
ISOException.throwIt(SW_WRONG_STATE);
sendOutgoingData(apdu, properties.data, properties.len);
return;
}
stati c fin al b yte I NS_GE T_CER T = 0 x36;
stati c fin al b yte I NS_GE T_PRO P = 0 x56;
stati c fin al b yte S W1_WR ONG_P IN = 0x63 ;
stati c fin al s hort SW_PI N_BLO CKED = 0x 6983;
stati c fin al b yte I NS_VE RIFY = 0x2 0;
stati c fin al b yte S W1_TR IES_L EFT = 0x6 3;
stati c fin al b yte I NS_VE RIFIE D = 0 x26;
stati c fin al b yte I NS_SI GN_DE C = 0 x42;
RSAPr ivate Key key;
KeySt ate k eySt ate;
byte[ ] pin ;
PinSt ate p inSt ate;
short cert Size ;
ByteV ector cer tific ate;
ByteV ector pro perti es;
short cert Byte sSent ;
byte apple tSta te;
init() {
/* Th e cur rent defi nitio n of Smart Slan g req uires ever y sta te c ompon ent t o be
initi alize d in the initi aliza tion bloc k. Th is is a bi t art ific ial f or
certa in st ate compo nents that are real ly in itial ized by co mman ds, e .g. k eys,
forci ng us to use m eanin gless valu es l ike a ll 0s . We may c hang e the
defin ition of Smart Slang to n o lon ger requi re al l sta te co mpon ents to be
initi alize d in the initi aliza tion bloc k, wh ile l eavin g the req uirem ent t hat
every stat e co mpone nt mu st be init iali zed b efore it i s use d fo r the firs t
time. Besi des avoid ing a rtifi cial init ializ ation s, th is ch ange woul d sup port
bette r sem anti c che cking of t he Sm artS lang spec, beca use p resu mably a ke y
shoul dn't be u sed b efore it i s ass igne d a n on-al l-0s value . */
key
= RSA Priva teKey (KEY_ SIZE )
( repea t(0,K EY_SI ZE/8 ), re peat( 0,KEY _SIZE /8)) ;
keySt ate
= Key State (fals e,fal se);
pin
= rep eat(0 ,8);
pinSt ate
= uns et;
certS ize
= 0;
certi ficat e
= {};
prope rties
= {};
certB ytesS ent = 0;
apple tStat e
= per sonal izati on;
} bytes {};
stati c byt e[] exp;
command putE xpon ent(B yte[K EY_SI ZE/8] exp ) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
key = RSAP riva teKey (KEY_ SIZE) (exp , ke y.mod ulus) ;
keySt ate = Key State (tru e, ke yStat e.is Modul usSet );
// we may exte nd Sm artSl ang w ith d irec t ass ignme nts t o rec ord compo nents :
// ke y.exp onen t = e xp;
// ke yStat e.is Expon entSe t =tr ue;
} apdu {CLA, INS _PUT_ EXP, P1, P 2, ex p, 0 };
priva te A (byt e[] i nitpa r, sh ort o ff, byte len) {
key = (R SAPr ivate Key)K eyBui lder. buil dKey( KeyBu ilder .TYPE _RSA _PRIV ATE,
(shor t)102 4,
false );
key State = n ew Ke yStat e();
pin = A. byte Array New(( short )8);
pin State = n ew Pi nStat e();
cer tific ate = new Byte Vecto r((sh ort) 0,(sh ort)1 000);
pro perti es = new ByteV ector ((sho rt)0 ,(sho rt)20 0);
chu nk = new ByteV ector ((sho rt)1, (sho rt)10 0);
_au x2 = A.by teArr ayNew ((sho rt)12 8);
_au x1 = A.by teArr ayNew ((sho rt)12 8);
msg = A. byte Array New(( short )128) ;
pro p = n ew B yteVe ctor( (shor t)0,( shor t)200 );
cer tChun k = new B yteVe ctor( (shor t)1, (shor t)100 );
p = A.by teAr rayNe w((sh ort)8 );
mod = A. byte Array New(( short )128) ;
exp = A. byte Array New(( short )128) ;
inD ata = new byte [255] ; // comma nd d ata i s 255 byte s max
rsa Ciphe r = Ciphe r.get Insta nce(C iphe r.ALG _RSA_ NOPAD ,fals e);
A.r epeat ((by te)0, (sho rt)12 8, _a ux1, (sho rt)0) ;
A.r epeat ((by te)0, (sho rt)12 8, _a ux2, (sho rt)0) ;
A.m akeRS APri vateK ey((s hort) 1024, _au x1, _ aux2, key) ;
key State .isE xpone ntSet = fa lse;
key State .isM odulu sSet = fal se;
A.r epeat ((by te)0, (sho rt)8, pin, (sh ort)0 );
pin State .ele m = P inSta te.un set;
cer tSize = 0 ;
cer tific ate. setSi ze((s hort) 0);
pro perti es.s etSiz e((sh ort)0 );
cer tByte sSen t = 0 ;
app letSt ate = App letSt ate.p erson aliz ation ;
reg ister (ini tpar, (sho rt)(o ff + 1), initp ar[of f]);
}
stati c byt e[] mod;
stati c byt e[] p;
}
stati c byt e[] msg;
stati c byt e[] _aux1 ;
stati c byt e[] _aux2 ;
stati c Byt eVec tor c hunk;
byte[ ] inD ata;
}
stati c Cip her rsaCi pher;
command putC erti ficat eSize (Int( 1,MAX _CER T_SIZ E) si ze) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
certS ize = siz e;
certi ficat e = {};
} apdu {CLA, INS _CERT _SIZE , P1, P2, ubyt es[2] (size ), 0} ;
command putC erti ficat eChun k(Cer tific ateC hunk certC hunk) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
if (c ertSi ze = = 0) { res pond SW_CE RT_S IZE_U NSET; }
if (c ertif icat e.len gth + cert Chunk .len gth > cert Size)
{ r espon d SW _CERT IFICA TE_TO O_LAR GE; }
certi ficat e = certi ficat e ++ certC hunk ;
} apdu {CLA, INS _PUT_ CERT, P1, P2, c ertC hunk, 0};
command unbl ockP IN() {
if (a pplet Stat e != updat ing) { res pond SW_W RONG_ STATE ; }
pinSt ate = not Verif ied(M AX_TR IES);
} apdu {CLA, INS _UNBL OCK, P1, P 2, {} , 0} ;
command getC erti ficat eChun k() {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
Certi ficat eChu nk ch unk;
if (c ertif icat e.len gth - cert Bytes Sent >= M AX_CE RT_CH UNK_S IZE) {
chu nk = cert ifica te[ce rtByt esSen t,MA X_CER T_CHU NK_SI ZE];
cer tByte sSen t = c ertBy tesSe nt + MAX_ CERT_ CHUNK _SIZE ;
} els e {
chu nk = cert ifica te[ce rtByt esSen t..c ertif icate .leng th-1] ;
cer tByte sSen t = c ertif icate .leng th;
}
if (c ertif icat e.len gth - cert Bytes Sent >= M AX_CE RT_CH UNK_S IZE) {
res pond {chu nk, S W1_MO RE_DA TA, M AX_C ERT_C HUNK_ SIZE} ;
} els e if (cer tific ate.l ength - ce rtBy tesSe nt > 0) {
res pond {chu nk, S W1_MO RE_DA TA, c erti ficat e.len gth - cert Byte sSent };
} els e /* cert ifica te.le ngth == ce rtBy tesSe nt */ {
cer tByte sSen t = 0 ; // reset
res pondo k ch unk;
}
} apdu {CLA, INS _GET_ CERT, P1, P2, { },
(cer tifi cate. lengt h - c ertBy tesS ent > = MAX _CERT _CHUN K_SI ZE) ?
MAX_ CERT _CHUN K_SIZ E : c ertif icat e.len gth - cert Bytes Sent };
AUTOSMART
command getP rope rties () {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
respo ndok prop ertie s;
} apdu {CLA, INS _GET_ PROP, P1, P2, { }, p roper ties. lengt h};
command pinV erif y(Pin p) {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
switc h (pi nSta te) {
cas e ver ifie d: {
r espon dok;
}
cas e not Veri fied( tries Left) : {
i f (p == p in) {
pinS tate = ve rifie d;
resp ondo k;
} else if (trie sLeft > 1) {
pinS tate = no tVeri fied( tries Left - 1) ;
resp ond {{}, SW1_W RONG_ PIN, trie sLeft };
} else {
pinS tate = bl ocked ;
resp ond SW_PI N_BLO CKED;
}
}
cas e blo cked : {
r espon d SW _PIN_ BLOCK ED;
}
cas e uns et: {
/ / can not happe n -- could be p rove d usi ng st ate i nvari ants
}
}
} apdu {CLA, INS _VERI FY, P 1, P2 , p, 0};
command pinV erif ied() {
if (a pplet Stat e != deplo yment ) {
switc h (pi nSta te) {
cas e ver ifie d: {
r espon dok;
}
cas e not Veri fied( tries Left) : {
r espon d {{ }, SW 1_TRI ES_LE FT,
}
cas e blo cked : {
r espon d SW _PIN_ BLOCK ED;
}
cas e uns et: {
/ / can not happe n -- could be
}
}
} apdu {CLA, INS _VERI FIED, P1, P2,
=
=
=
=
=
=
=
=
=
=
=
=
=
=
static void subarrayFromLength(ByteVector vec, short i, short n, ByteVector result, short offset, boolean setSize) {
if (setSize) result.setSize(n);
Util.arrayCopy(vec.data,i,result.data,offset,n);
}
static void getRSAExponent(RSAPrivateKey key, byte[] result) {
key.getExponent(result,(short)0);
}
static void getRSAModulus(RSAPrivateKey key, byte[] result) {
key.getModulus(result,(short)0);
}
static void assign(byte[] source, byte[] target, short offset) {
short len = (short) source.length;
Util.arrayCopy(source,(short)0,target,offset,len);
}
static boolean equals(byte[] arr1, byte[] arr2) {
short len = (short) arr1.length;
if (arr2.length != len) return false;
for (short i = 0; i < len; i++)
if (arr1[i] != arr2[i]) return false;
return true;
}
static byte[] byteArrayNew(short size) {
return new byte[size];
}
static void repeat(byte elem, short n, byte[] result, short offset) {
Util.arrayFillNonAtomic(result,offset,n,elem);
}
static void makeRSAPrivateKey
(short len, byte[] exponent, byte[] modulus, RSAPrivateKey result) {
result.setExponent(exponent,(short)0,(short)len);
result.setModulus(modulus,(short)0,(short)len);
}
static short nonNegativeByte(byte b) {
return (b < 0 ? (short)(b + 256) : b);
}
void receiveIncomingData(APDU apdu) {
byte[] buffer = apdu.getBuffer();
short totalRead = 0;
short chunkRead = apdu.setIncomingAndReceive();
do {
// error if too little or too much data:
if (chunkRead == 0 ||
(short) (totalRead + chunkRead) > inDataLength)
ISOException.throwIt(ISO7816.SW_WRONG_DATA);
// transfer from APDU buffer to inData array:
Util.arrayCopy(buffer,ISO7816.OFFSET_CDATA,
inData,totalRead,chunkRead);
// increment counter:
totalRead += chunkRead;
// get more data if necessary:
if (totalRead != inDataLength)
chunkRead = apdu.receiveBytes(ISO7816.OFFSET_CDATA);
} while (totalRead < inDataLength);
}
static void rsa(Key key, byte[] data, byte[] result) {
short sizeInBytes = (short) (key.getSize() / 8);
rsaCipher.init(key,Cipher.MODE_ENCRYPT);
rsaCipher.doFinal(data,(short)0,sizeInBytes,result,(short)0);
}
void sendOutgoingData(APDU apdu, byte[] data) {
sendOutgoingData(apdu, data, (short)data.length);
}
void sendOutgoingData(APDU apdu, byte[] data, short len) {
apdu.setOutgoing();
apdu.setOutgoingLength(len);
apdu.sendBytesLong(data,(short)0,len);
}
public static void install(byte[] initpar, short off, byte len)
throws ISOException {
new A(initpar,off,len);
}
}
class KeyState {
boolean isExponentSet;
boolean isModulusSet;
KeyState () { }
}
class PinState {
static final byte unset = 0;
static final byte notVerified = 1;
static final byte verified = 2;
static final byte blocked = 3;
byte elem;
byte notVerified_arg = 1;
PinState () { }
}
class AppletState {
static final byte personalization = 0;
static final byte deployment = 1;
static final byte updating = 2;
}
class VectorBase {
short len;
r espo nd SW _WRON G_STA TE; }
void putMo dulu s (AP DU ap du)
{
b yte[] buf fer = apdu .getB uffer ();
i f ((b uffe r[ISO 7816. OFFSE T_P1] != P1) | | (bu ffer[ ISO78 16.O FFSET _P2] != P2 ))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _P1P2 );
i nData Leng th = A.non Negat iveBy te(b uffer [ISO7 816.O FFSET _LC] );
i f (in Data Lengt h != 128)
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _LENG TH);
r eceiv eInc oming Data( apdu) ;
U til.a rray Copy( inDat a, (s hort) 0, m od, ( short )0, i nData Leng th);
i f (ap plet State == A pplet State .dep loyme nt)
ISOE xcep tion. throw It(SW _WRON G_ST ATE);
A .getR SAEx ponen t(key , _au x1);
A .make RSAP rivat eKey( (shor t)102 4, _ aux1, mod, key) ;
k eySta te.i sExpo nentS et = keySt ate. isExp onent Set;
k eySta te.i sModu lusSe t = t rue;
}
t ries Left} ;
p rove d usi ng st ate i nvari ants
{ }, 0 };
void putPI N (A PDU a pdu)
{
b yte[] buf fer = apdu .getB uffer ();
i f ((b uffe r[ISO 7816. OFFSE T_P1] != P1) | | (bu ffer[ ISO78 16.O FFSET _P2] != P2 ))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _P1P2 );
i nData Leng th = A.non Negat iveBy te(b uffer [ISO7 816.O FFSET _LC] );
i f (in Data Lengt h != 8)
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _LENG TH);
r eceiv eInc oming Data( apdu) ;
U til.a rray Copy( inDat a, (s hort) 0, p , (sh ort)0 , inD ataLe ngth );
i f (ap plet State == A pplet State .dep loyme nt)
ISOE xcep tion. throw It(SW _WRON G_ST ATE);
A .assi gn(p , pin , (sh ort)0 );
p inSta te.e lem = PinS tate. notVe rifi ed;
p inSta te.n otVer ified _arg = MAX _TRI ES;
}
const C LA = 0x80 ;
const P 1 = 0 ;
const P 2 = 0 ;
I NS_PU T_EX P
I NS_PU T_MO D
I NS_PU T_PI N
I NS_CE RT_S IZE
I NS_PU T_CE RT
I NS_PU T_PR OP
I NS_UN BLOC K
I NS_DE PLOY
I NS_UP DATE
I NS_GE T_CE RT
I NS_GE T_PR OP
I NS_VE RIFY
I NS_VE RIFI ED
I NS_SI GN_D EC
publi c voi d pr ocess (APD U apd u)
{
i f (se lect ingAp plet( ))
retu rn;
b yte[] buf fer = apdu .getB uffer ();
i f (bu ffer [ISO7 816.O FFSET _CLA] != CLA)
ISOE xcep tion. throw It(IS O7816 .SW_ CLA_N OT_SU PPORT ED);
s witch (bu ffer[ ISO78 16.OF FSET_ INS] )
{
ca se I NS_PU T_EXP :
pu tExpo nent( apdu) ;
re turn;
ca se I NS_PU T_MOD :
pu tModu lus(a pdu);
re turn;
ca se I NS_PU T_PIN :
pu tPIN( apdu) ;
re turn;
ca se I NS_CE RT_SI ZE:
pu tCert ifica teSiz e(apd u);
re turn;
ca se I NS_PU T_CER T:
pu tCert ifica teChu nk(ap du);
re turn;
ca se I NS_PU T_PRO P:
pu tProp ertie s(apd u);
re turn;
ca se I NS_UN BLOCK :
un block PIN(a pdu);
re turn;
ca se I NS_DE PLOY:
de ploy( apdu) ;
re turn;
ca se I NS_UP DATE:
up date( apdu) ;
re turn;
ca se I NS_GE T_CER T:
ge tCert ifica teChu nk(ap du);
re turn;
ca se I NS_GE T_PRO P:
ge tProp ertie s(apd u);
re turn;
ca se I NS_VE RIFY:
pi nVeri fy(ap du);
re turn;
ca se I NS_VE RIFIE D:
pi nVeri fied( apdu) ;
re turn;
ca se I NS_SI GN_DE C:
pr ivSig nDecr ypt(a pdu);
re turn;
de faul t:
IS OExce ption .thro wIt(I SO78 16.SW _INS_ NOT_S UPPOR TED) ;
}
}
void putEx pone nt (A PDU a pdu)
{
b yte[] buf fer = apdu .getB uffer ();
i f ((b uffe r[ISO 7816. OFFSE T_P1] != P1) | | (bu ffer[ ISO78 16.O FFSET _P2] != P2 ))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _P1P2 );
i nData Leng th = A.non Negat iveBy te(b uffer [ISO7 816.O FFSET _LC] );
i f (in Data Lengt h != 128)
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _LENG TH);
r eceiv eInc oming Data( apdu) ;
U til.a rray Copy( inDat a, (s hort) 0, e xp, ( short )0, i nData Leng th);
i f (ap plet State == A pplet State .dep loyme nt)
ISOE xcep tion. throw It(SW _WRON G_ST ATE);
A .getR SAMo dulus (key, _aux 1);
A .make RSAP rivat eKey( (shor t)102 4, e xp, _ aux1, key) ;
k eySta te.i sExpo nentS et = true;
k eySta te.i sModu lusSe t = k eySta te.i sModu lusSe t;
}
command priv Sign Decry pt(Me ssage msg) {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
if (p inSta te ! = ver ified ) {
res pond SW_S ECURI TY_NO K;
} els e {
res pondo k rs a(key ,msg) ;
}
} apdu {CLA, INS _SIGN _DEC, P1, P2, m sg, MSG_S IZE};
const
const
const
const
const
const
const
const
const
const
const
const
const
const
static void concat(ByteVector vec1, ByteVector vec2, ByteVector result, short offset, boolean setSize) {
short len1 = vec1.size();
short len2 = vec2.size();
if (setSize) result.setSize((short)(len1+len2));
Util.arrayCopy(vec2.data,(short)0,result.data,(short)(len1+offset),len2);
if (vec1.data != result.data)
Util.arrayCopy(vec1.data,(short)0,result.data,offset,len1);
}
publi c voi d de selec t ()
{
i f (pi nSta te.el em == PinS tate. veri fied)
{
pi nSta te.el em = PinSt ate.n otVe rifie d;
pi nSta te.no tVeri fied_ arg = MAX _TRIE S;
}
}
command depl oy() {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
if (k eySta te
= = Key State (tru e,tru e)
&& p inSta te
! = uns et
&& c ertSi ze
!= 0
&& c ertif icat e.len gth = = cer tSize
&& p roper ties
! = {}) {
app letSt ate = dep loyme nt;
} els e {
res pond SW_U NFINI SHED_ PERSO NALIZ ATIO N;
}
} apdu {CLA, INS _DEPL OY, P 1, P2 , {}, 0};
command upda te() {
if (a pplet Stat e != deplo yment ) { r espo nd SW _WRON G_STA TE; }
apple tStat e = updat ing;
} apdu {CLA, INS _UPDA TE, P 1, P2 , {}, 0};
static void assign(ByteVector source, ByteVector target, short offset, boolean setSize) {
short len = source.size();
if (setSize) target.setSize(len);
Util.arrayCopy(source.data,(short)0,target.data,offset,len);
}
publi c boo lean sele ct ()
{
c ertBy tesS ent = 0;
r eturn tru e;
}
command putP rope rties (Prop ertie s pro p) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
prope rties = p rop;
} apdu {CLA, INS _PUT_ PROP, P1, P2, p rop, 0};
}
void privSignDecrypt (APDU apdu)
{
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != P1) || (buffer[ISO7816.OFFSET_P2] != P2))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength = A.nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (inDataLength != 128)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
Util.arrayCopy(inData, (short)0, msg, (short)0, inDataLength);
if (appletState != AppletState.deployment)
ISOException.throwIt(SW_WRONG_STATE);
if (pinState.elem != PinState.verified)
ISOException.throwIt(SW_SECURITY_NOK);
else
{
A.rsa(key, msg, _aux1);
sendOutgoingData(apdu, _aux1);
return;
}
}
short inDa taLe ngth; // a lways <= 2 55
command putP IN(P in p) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
pin = p;
pinSt ate = not Verif ied(M AX_TR IES);
} apdu {CLA, INS _PUT_ PIN, P1, P 2, p, 0};
}
void pinVerified (APDU apdu)
{
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != P1) || (buffer[ISO7816.OFFSET_P2] != P2))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
if (appletState != AppletState.deployment)
ISOException.throwIt(SW_WRONG_STATE);
switch (pinState.elem)
{
case PinState.verified:
return;
case PinState.notVerified:
byte triesLeft = pinState.notVerified_arg;
ISOException.throwIt(Util.makeShort(SW1_TRIES_LEFT, triesLeft));
case PinState.blocked:
ISOException.throwIt(SW_PIN_BLOCKED);
case PinState.unset:
stati c Byt eVec tor c ertCh unk;
stati c Byt eVec tor p rop;
command putM odul us(By te[KE Y_SIZ E/8] mod) {
if (a pplet Stat e == deplo yment ) { r espo nd SW _WRON G_STA TE; }
key = RSAP riva teKey (KEY_ SIZE) (key .exp onent , mod );
keySt ate = Key State (key State .isEx pone ntSet , tru e);
} apdu {CLA, INS _PUT_ MOD, P1, P 2, mo d, 0 };
~ 700
lines
void pinVerify (APDU apdu)
{
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != P1) || (buffer[ISO7816.OFFSET_P2] != P2))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength = A.nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (inDataLength != 8)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
Util.arrayCopy(inData, (short)0, p, (short)0, inDataLength);
if (appletState != AppletState.deployment)
ISOException.throwIt(SW_WRONG_STATE);
switch (pinState.elem)
{
case PinState.verified:
return;
case PinState.notVerified:
byte triesLeft = pinState.notVerified_arg;
if (A.equals(p, pin))
{
pinState.elem = PinState.verified;
return;
}
else
if (triesLeft > 1)
{
pinState.elem = PinState.notVerified;
pinState.notVerified_arg = (byte)(triesLeft - 1);
ISOException.throwIt(Util.makeShort(SW1_WRONG_PIN,
triesLeft));
}
else
{
pinState.elem = PinState.blocked;
ISOException.throwIt(SW_PIN_BLOCKED);
}
case PinState.blocked:
ISOException.throwIt(SW_PIN_BLOCKED);
case PinState.unset:
stati c fin al s hort SW_SE CURIT Y_NOK = 0 x6982 ;
invaria nt ap plet State != d eploy ment || ( certB ytesS ent < = (ce rtif icate ).len gth-1 );
ISOException.throwIt(SW_WRONG_STATE);
if ((((((keyState.isExponentSet == true)
&& (keyState.isModulusSet == true))
&& (pinState.elem != PinState.unset))
&& (certSize != 0))
&& (certificate.size() == certSize))
&& (properties.size() != 0))
appletState = AppletState.deployment;
else
ISOException.throwIt(SW_UNFINISHED_PERSONALIZATION);
void update (APDU apdu)
{
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != P1) || (buffer[ISO7816.OFFSET_P2] != P2))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
if (appletState != AppletState.deployment)
ISOException.throwIt(SW_WRONG_STATE);
appletState = AppletState.updating;
}
stati c fin al s hort MSG_S IZE = 128;
0x44 ;
0x46 ;
0x22 ;
0x3A ;
0x38 ;
0x58 ;
0x24 ;
0x70 ;
0x72 ;
0x36 ;
0x56 ;
0x20 ;
0x26 ;
0x42 ;
void putCe rtif icate Size (APDU apdu )
{
b yte[] buf fer = apdu .getB uffer ();
i f ((b uffe r[ISO 7816. OFFSE T_P1] != P1) | | (bu ffer[ ISO78 16.O FFSET _P2] != P2 ))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _P1P2 );
i nData Leng th = A.non Negat iveBy te(b uffer [ISO7 816.O FFSET _LC] );
i f (in Data Lengt h != 2)
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _LENG TH);
r eceiv eInc oming Data( apdu) ;
s hort size = Ut il.ma keSho rt(in Data [0], inDat a[1]) ;
i f ((s ize < 1) || (s ize > 1000 ))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _DATA );
i f (ap plet State == A pplet State .dep loyme nt)
ISOE xcep tion. throw It(SW _WRON G_ST ATE);
c ertSi ze = size ;
c ertif icat e.set Size( (shor t)0);
}
const S W_WRO NG_S TATE
= 0x 6985;
const S W_CER TIFI CATE_ TOO_L ARGE
= 0x 6A80;
const S W_UNF INIS HED_P ERSON ALIZA TION = 0x 6985;
const S W_PIN _BLO CKED
= 0x 6983;
const S W_SEC URIT Y_NOK
= 0x 6982;
const S W_CER T_SI ZE_UN SET
= 0x 6985;
const S W1_WR ONG_ PIN
= 0x 63;
const S W1_TR IES_ LEFT
= 0x 63;
const S W1_MO RE_D ATA
= 0x 63;
select {
certB ytesS ent = 0; // re set
}
void putCe rtif icate Chunk (APD U apd u)
{
b yte[] buf fer = apdu .getB uffer ();
i f ((b uffe r[ISO 7816. OFFSE T_P1] != P1) | | (bu ffer[ ISO78 16.O FFSET _P2] != P2 ))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _P1P2 );
i nData Leng th = A.non Negat iveBy te(b uffer [ISO7 816.O FFSET _LC] );
i f ((i nDat aLeng th < 1) || (inD ataL ength > 10 0))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _LENG TH);
r eceiv eInc oming Data( apdu) ;
U til.a rray Copy( inDat a, (s hort) 0, c ertCh unk.d ata, (shor t)0, inDa taLen gth);
i f (ap plet State == A pplet State .dep loyme nt)
ISOE xcep tion. throw It(SW _WRON G_ST ATE);
i f (ce rtSi ze == 0)
ISOE xcep tion. throw It(SW _CERT _SIZ E_UNS ET);
i f ((s hort )(cer tific ate.s ize() + c ertCh unk.s ize() ) > c ertS ize)
ISOE xcep tion. throw It(SW _CERT IFIC ATE_T OO_LA RGE);
A .conc at(c ertif icate , cer tChun k, c ertif icate , (sh ort)0 , fa lse);
}
deselec t {
if (p inSta te = = ver ified ) {
pin State = n otVer ified (MAX_ TRIES );
}
}
void putPr oper ties (APDU apdu )
{
b yte[] buf fer = apdu .getB uffer ();
i f ((b uffe r[ISO 7816. OFFSE T_P1] != P1) | | (bu ffer[ ISO78 16.O FFSET _P2] != P2 ))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _P1P2 );
i nData Leng th = A.non Negat iveBy te(b uffer [ISO7 816.O FFSET _LC] );
i f ((i nDat aLeng th < 0) || (inD ataL ength > 20 0))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _LENG TH);
r eceiv eInc oming Data( apdu) ;
U til.a rray Copy( inDat a, (s hort) 0, p rop.d ata, (shor t)0, inDa taLen gth);
i f (ap plet State == A pplet State .dep loyme nt)
ISOE xcep tion. throw It(SW _WRON G_ST ATE);
A .assi gn(p rop, prope rties , (sh ort) 0, fa lse);
}
SmartSlang spec
void unblo ckPI N (AP DU ap du)
{
b yte[] buf fer = apdu .getB uffer ();
i f ((b uffe r[ISO 7816. OFFSE T_P1] != P1) | | (bu ffer[ ISO78 16.O FFSET _P2] != P2 ))
ISOE xcep tion. throw It(IS O7816 .SW_ WRONG _P1P2 );
i f (ap plet State != A pplet State .upd ating )
ISOE xcep tion. throw It(SW _WRON G_ST ATE);
p inSta te.e lem = PinS tate. notVe rifi ed;
p inSta te.n otVer ified _arg = MAX _TRI ES;
}
void deploy (APDU apdu)
{
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != P1) || (buffer[ISO7816.OFFSET_P2] != P2))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
if (appletState == AppletState.deployment)
(actual files; font size 1)
void setSize(short newSize) {
len = newSize;
}
short size() {
return len;
}
}
class ByteVector extends VectorBase {
byte[] data;
ByteVector(short minLen, short maxLen) {
data = A.byteArrayNew(maxLen);
setSize(minLen);
}
}
Java
Card
code
PKI PKI
Java Card code
...
static byte[] _aux1;
static Cipher rsaCipher;
...
rsaCipher = Cipher.getInstance(Cipher.ALG_RSA_NOPAD,false);
_aux1 = new byte[(short)128];
...
void privSignDecrypt (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) ||
(buffer[ISO7816.OFFSET_P2] != 0))
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
inDataLength = nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
if (inDataLength != 128)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
Util.arrayCopy(inData,(short)0,msg,(short)0,inDataLength);
if (pinState.elem != PinState.verified)
ISOException.throwIt(SW_SECURITY_NOK);
Java
else {
rsaCipher.init(key,Cipher.MODE_DECRYPT);
Card
rsaCipher.doFinal(msg,(short)0,(short)128,_aux1,(short)0);
code
sendOutgoingData(apdu, _aux1);
return;
}
}
...
...
static byte[ ] _a ux1;
static Ciphe r rs aCiph er;
...
rsaCi pher = Ci pher. getIn stanc e(Cip her. ALG_R SA_NO PAD,f alse) ;
_aux1 = ne w by te[(s hort) 128];
...
void pr ivSig nDec rypt (APDU apdu ) {
byte[ ] buf fer = apd u.get Buffe r();
if (( buffe r[IS O7816 .OFFS ET_P1 ] != 0) | |
( buffe r[IS O7816 .OFFS ET_P2 ] != 0))
ISO Excep tion .thro wIt(I SO781 6.SW_ WRON G_P1P 2);
inDat aLeng th = nonN egati veByt e(buf fer[ ISO78 16.OF FSET_ LC]);
if (i nData Leng th != 128)
ISO Excep tion .thro wIt(I SO781 6.SW_ WRON G_LEN GTH);
recei veInc omin gData (apdu );
Util. array Copy (inDa ta,(s hort) 0,msg ,(sh ort)0 ,inDa taLen gth);
if (p inSta te.e lem ! = Pin State .veri fied )
ISO Excep tion .thro wIt(S W_SEC URITY _NOK );
else {
rsa Ciphe r.in it(ke y,Cip her.M ODE_D ECRY PT);
rsa Ciphe r.do Final (msg, (shor t)0,( shor t)128 ,_aux 1,(sh ort)0 );
sen dOutg oing Data( apdu, _aux 1);
ret urn;
}
}
...
PKI Java Card code
...
intermediate
static byte[] _aux1;
static Cipher rsaCipher;
storage
pre-allocation
...
rsaCipher = Cipher.getInstance(Cipher.ALG_RSA_NOPAD,false);
_aux1 = new byte[(short)128];
...
void privSignDecrypt (APDU apdu) {
byte[] buffer = apdu.getBuffer();
if ((buffer[ISO7816.OFFSET_P1] != 0) ||
(buffer[ISO7816.OFFSET_P2] != 0))
APDU
ISOException.throwIt(ISO7816.SW_WRONG_P1P2);
checking inDataLength
= nonNegativeByte(buffer[ISO7816.OFFSET_LC]);
& decoding if (inDataLength != 128)
ISOException.throwIt(ISO7816.SW_WRONG_LENGTH);
receiveIncomingData(apdu);
Util.arrayCopy(inData,(short)0,msg,(short)0,inDataLength);
if (pinState.elem != PinState.verified)
ISOException.throwIt(SW_SECURITY_NOK); arrays accessed within
else {
bounds by construction
interesting rsaCipher.init(key,Cipher.MODE_DECRYPT);
computation rsaCipher.doFinal(msg,(short)0,(short)128,_aux1,(short)0);
sendOutgoingData(apdu, _aux1);
return;
code for “respondok decrypt(key,msg)”
}
}
...
SmartSlang counterpart
command privSignDecrypt(Message msg) {
if (pinState != verified) {
respond SW_SECURITY_NOK;
} else {
respondok decrypt(key,msg);
}
} apdu {0x80,0x42,0,0,msg,1024/8};
SmartSlang
example: PIN construct
SmartSlang
SmartSlang example: PIN construct
(under design)
identifier (there may be multiple PINs)
pin p {
length 8; in bytes (determines strength)
maxtries 3; before blocking
that require
APDU header
for
protect {privSignDecrypt, commands
to be verified
first
to verify
getCertificate}; PIN command
PIN) for
apdu verify {0x80,0x20,0,0}; PIN (data
APDU=header
apdu set {0x80,0x22,0,0} secure; command to (re)set
}
use secure channel
PIN (data = PIN)
implicit state variables, commands,
and checks in other commands
(tentative syntax)
SmartSlang example: PIN construct
(under design)
pin p {
length 8;
pin
p {
maxtries
3;
length
protect8;
{privSignDecrypt,
maxtries 3;
getCertificate};
protect
{privSignDecrypt,
apdu verify
{0x80,0x20,0,0};
getCertificate};secure;
apdu set {0x80,0x22,0,0}
} apdu verify {0x80,0x20,0,0};
apdu set {0x80,0x22,0,0} secure;
}
similar high-level constructs planned for
• challenge-response authentication
• piecewise data read/write
• key establishment
•…
estimated
 code
spec = ~ 7–8
SmartSlang
is SmartSlang just a macro language?
is AutoSmart just a macro expander?
is SmartSlang just a macro language?
is AutoSmart just a macro expander?
NO:
•
•
•
•
•
•
expressive types, statically checked
automated reasoning
automatic static storage management by type analysis
APDU decoding/checking
non-local mapping of spec constructs into code
…
inside AutoSmart
AutoSmart
applet
spec
AUTOSMART
applet
code
inside AutoSmart
applet SPEC
CODE applet
spec CHECKERAUTOSMART
GENERATOR code
checked
applet
spec
applet
spec
parses spec
parser generated from grammar
via our own parser generator
checksSPEC
type safety
CHECKER
includes
Fourier-Motzkin decision
procedure for linear arithmetic
checks other properties
e.g. restrictions to allow generation
of code to check and decode APDUs
checked
applet
spec
CODE GENERATOR
SMARTSLANG

LOGIC
SmartSlang
applet represented
in logic
provable correctness?
SmartSlang
Java Card
semantics
semantics
in logic
in logic
formal relationship
provable correctness
applet
code
JAVA CARD

LOGIC
Java Card
applet represented
in logic
applet represented
in logic
applet represented
in logic
applet represented
in logic
applet represented
in logic
Metaslang, the
specification language
of
which is a form of
higher-order logic
other choices are possible
applet represented
in logic
?
applet
applet
selection
command (APDU)
response (APDU)
applet
deselection
what is observable?
initialization
(w/ params.)
selection
command (APDU)
response (APDU)
initialization
(w/ params.)
applet
deselection
type Event = |
|
|
|
initialize InitParam
process Command * Response
select
deselect
type Command = ...
type Response = ...
type InitParam = ...
including erroneous ones
selection
command (APDU)
response (APDU)
applet
initialization
(w/ params.)
deselection
type Event = |
|
|
|
initialize InitParam
process Command * Response
select
deselect
type Trace = (Nat
Nat -> Event)
Event | orderOK?
op orderOK? : (Nat -> Event) -> Boolean
def orderOK? tr =
embed? initialize (tr 0) &&
...
selection
command (APDU)
response (APDU)
applet
initialization
(w/ params.)
deselection
type Event = |
|
|
|
initialize InitParam
process Command * Response
select
deselect
type Trace = (Nat -> Event) | orderOK?
type Applet = Set Trace
type Set a = a -> Boolean
Applets = spec
type Event = |
|
|
|
initialize InitParam
process Command * Response
select
deselect
type Trace = (Nat -> Event) | orderOK?
type Applet = Set Trace
endspec
Applet = spec
import Applets
Applets = spec
type Event = |
|
op applet : Applet |
def applet = ...
|
endspec
initialize InitParam
process Command * Response
select
deselect
type Trace = (Nat -> Event) | orderOK?
type Applet = Set Trace
endspec
Applet = spec
Applet’ = spec
import Applets
import Applets
type Aux
op aux : Aux
...
type Aux’
op aux’ : Aux’
...
op applet : Applet
def applet = ...
op applet’ : Applet
def applet’ = ...
endspec
endspec
Applet = spec
import Applets
Applet’ = spec
import Applets
type Aux
op aux : Aux
... = spec
Applet
type Aux’
op aux’ : Aux’
...
Applet’
= spec
op
applet
: Applet
import
Applets
def applet = ...
type Aux
endspec
op aux : Aux
...
op
applet’
: Applet
import
Applets
def applet’ = ...
type Aux’
endspec
op aux’ : Aux’
...
op applet : Applet
def applet = ...
op applet’ : Applet
def applet’ = ...
endspec
endspec
Applet = spec
Applet’ = spec
import Applets
import Applets
type Aux
op aux : Aux
...
type Aux’
op aux’ : Aux’
...
op applet : Applet
def applet = ...
op applet’ : Applet
def applet’ = ...
endspec
endspec
FormalRelationship = spec
endspec
Applet = spec
Applet’ = spec
import Applets
import Applets
type Aux
op aux : Aux
...
type Aux’
op aux’ : Aux’
...
op applet : Applet
def applet = ...
op applet’ : Applet
def applet’ = ...
endspec
endspec
FormalRelationship = spec
import Applet
endspec
Applet’ = spec
import Applets
type Aux’
op aux’ : Aux’
...
op applet’ : Applet
def applet’ = ...
endspec
FormalRelationship = spec
import Applet, Applet’
endspec
applets have same
observable behavior
FormalRelationship = spec
import Applet, Applet’
theorem applet = applet’
endspec
Applet = spec
import Applets
type Aux
op aux : Aux
...
op applet : Applet
def applet = ...
defined in terms
of SmartSlang
endspec
FormalRelationship = spec
import Applet, Applet’
theorem applet = applet’
endspec
SmartSlang
SmartSlang
SmartSlang
SmartSlang = spec
type
type
type
...
type
Expression = ...
Statement = ...
Command = ...
(simplified)
(abstract)
syntax
Spec = ...
op wellFormed? : Spec -> Boolean
def wellFormed? = ...
type WFSpec = Spec | wellFormed?
static
semantics
type Value = ...
type State = ...
op expSem : Expression -> (State -> Value)
op stmSem : Statement -> (State -> State)
...
endspec
dynamic
semantics
SmartSlang = spec
SSApplets = spec
type Expression = ...
import SmartSlang
type Statement = ...
type Command = ...
...
type Spec = ...
endspec
op wellFormed? : Spec -> Boolean
def wellFormed? = ...
type WFSpec = Spec | wellFormed?
type Value = ...
type State = ...
op expSem : Expression -> (State -> Value)
op stmSem : Statement -> (State -> State)
...
endspec
Applets = spec
SSApplets = spec
type Event = ...
type Applets
Trace = ...
import SmartSlang,
type Applet = ...
endspec
endspec
SSApplets = spec
import SmartSlang, Applets
op appletOf : WFSpec -> Applet
def appletOf = ...
endspec
SSApplet = spec
import SSApplets
op appletSpec : WFSpec
def appletSpec = ...
op applet : Applet
def applet = appletOf appletSpec
endspec
SSApplets = spec
import SmartSlang, Applets
op appletOf : WFSpec -> Applet
def appletOf = ...
endspec
SSApplet = spec
import SSApplets
op appletSpec : WFSpec
def appletSpec = ...
op applet : Applet
def applet = appletOf appletSpec
endspec
SmartSlang
spec
PARSER
abstract
syntax
tree
(.ssl file)
x+1
+
x
SSApplet = spec
import SSApplets
op appletSpec : WFSpec
def appletSpec = ...
op applet : Applet
def applet = appletOf appletSpec
endspec
META
1
Metaslang
expression
e:Spec
plus(var “x”,
const 1)
SmartSlang
spec
PARSER
abstract
syntax
tree
META
(.ssl file)
Metaslang
expression
e:Spec
SSApplet = spec
import SSApplets
op appletSpec : WFSpec
def appletSpec = ...
op applet : Applet
def applet = appletOf appletSpec
endspec
COPY &
PASTE
SmartSlang
spec
PARSER
abstract
syntax
tree
META
(.ssl file)
Metaslang
expression
e:Spec
Spec
e
SSApplet = spec
import SSApplets
op appletSpec : WFSpec
def appletSpec =
op applet : Applet
def applet = appletOf appletSpec
endspec
COPY &
PASTE
WFSpec < Spec
subtype proof obligation:
wellFormed? e
SmartSlang
spec
abstract
syntax
tree
PARSER
Metaslang
expression
e:Spec
SS  MS
Metaslang
SSApplet = spec spec
import SSApplets
proof
obligation
op appletSpec : WFSpec
def appletSpec = e
op applet : Applet
def applet = appletOf appletSpec
endspec
META
COPY &
PASTE
(previously showed)
applet
spec
SMARTSLANG

LOGIC
SmartSlang
applet represented
in logic
applet
code
AUTOSMART
SmartSlang
semantics
in logic
Java Card
semantics
in logic
formal relationship
provable correctness
JAVA CARD

LOGIC
Java Card
applet represented
in logic
(previously showed)
applet
spec
SMARTSLANG

LOGIC
applet
code
AUTOSMART
SmartSlang
semantics
in logic
Java Card
semantics
in logic
JAVA CARD

LOGIC
fixed
SmartSlang
applet represented
in logic
formal relationship
provable correctness
Java Card
applet represented
in logic
applet
spec
SMARTSLANG

LOGIC
SmartSlang
applet represented
in logic
applet
code
AUTOSMART
Java Card
semantics
in logic
formal relationship
provable correctness
JAVA CARD

LOGIC
Java Card
applet represented
in logic
same for Java Card
Java Card
same for Java Card
JavaCard = spec
JCApplets = spec
type Expression = ...
import JavaCard, Applets
type Statement = ...
... : WFProgram -> Applet
op appletOf
type Program
def appletOf
= ... = ...
op wellFormed? : Program -> Boolean
def wellFormed? = ...
op WFProgram = Program | wellFormed?
JCApplet =type
specObject = ...
endspec
type Heap = ...
import JCApplets
type State = ...
op appletPrg
: WFProgram
type Exception
= ...
def appletPrg
= ...
op expSem
: Expression -> ...
op :stmSem
op applet
Applet: Statement -> ...
... = appletOf appletPrg
def applet
endspec endspec
same for Java Card
Java Card
program
PARSER
abstract
syntax
tree
META
(.java file)
Metaslang
expression
e:Program
JCApplet = spec
import JCApplets
op appletPrg : WFProgram
def appletPrg = ...
op applet : Applet
def applet = appletOf appletPrg
endspec
COPY &
PASTE
same for Java Card
Java Card
program
PARSER
abstract
syntax
tree
META
(.java file)
Metaslang
expression
e:Program
Program
e
JCApplet = spec
import JCApplets
op appletPrg : WFProgram
def appletPrg =
op applet : Applet
def applet = appletOf appletPrg
endspec
COPY &
PASTE
WFProgram < Program
subtype proof obligation:
wellFormed? e
same for Java Card
Java Card
program
abstract
syntax
tree
PARSER
Metaslang
expression
e:Program
JC  MS
Metaslang
JCApplet = spec spec
import JCApplets
proof
obligation
op appletPrg : WFProgram
def appletPrg = restrict e
op applet : Applet
def applet = appletOf appletPrg
endspec
META
COPY &
PASTE
(previously showed)
SmartSlang
spec
AUTO
SMART
Java Card
program
proof
CHECKER
yes/no
how does it
work exactly?
AUTO
SMART
AUTO
SMART
CHECKER
CHECKER
(not to scale)
SS
AUTO
SMART
JC
CHECKER
SS
SS  MS
prf
SPEC
CHECKER
AUTO
SMART
MS
y/n
prf
CODE
GENERATOR
CHECKER
=BEHAVIOR?
y/n
y/n
prf
JC
WELLFORMED?
WELLFORMED?
MS
JC  MS
AND
y/n
SS
prf
AUTO
SMART
prf
prf
JC
CHECKER
y/n
SS
prf
simple?
JC
CHECKER
y/n
SS
SS  MS
proof checker
for Metaslang
(unavoidable)
WELLFORMED?
MS
y/n
prf
CHECKER
=BEHAVIOR?
y/n
y/n
WELLFORMED?
JC
MS
JC  MS
AND
trivial
y/n
SS  MS
SS/JC
MS
SS/JC  MS
JC  MS
COPY &
PARSER
META
PASTE
SS/JC
relatively
simple
very
simple
MS
trivial
can be made simpler…
(previously showed)
SmartSlang’ = spec
SmartSlang = spec
import SmartSlang
type Expression = ...
type Statement = ...
type Command = ...
...
type Spec = ...
op wellFormed? : Spec -> Boolean
def wellFormed? = ...
type WFSpec = Spec | wellFormed?
endspec
type Value = ...
type State = ...
op expSem : Expression -> (State -> Value)
op stmSem : Statement -> (State -> State)
...
endspec
SmartSlang’ = spec
import SmartSlang
op parse : String -> Option Spec
def parse = ...
endspec
SmartSlang’ = spec
import SmartSlang
op parse : String -> Option Spec
def parse = ...
op denotesWFSpec? : String -> Boolean
def denotesWFSpec? str =
case parse str of
| Some spc -> wellFormed? spc
| None -> false
endspec
SmartSlang’ = spec
import
SmartSlang
SSApplets’
= spec
op import
parse :SmartSlang’,
String -> Option
Spec
Applets
def parse = ...
op denotesWFSpec? : String -> Boolean
def denotesWFSpec? str =
endspec
case parse str of
| Some spc -> wellFormed? spc
| None -> false
type WFSpecString = String | denotesWFSpec?
endspec
SSApplets’ = spec
import SmartSlang’, Applets
op appletOf : WFSpecString -> Applet
def appletOf = ...
endspec
SSApplet’ = spec
import SSApplets’
op appletStr : WFSpecString
def appletStr = ...
op applet : Applet
def applet = appletOf appletStr
endspec
as before but
spec  string
SmartSlang
spec
SSApplet’ = spec
import SSApplets’
op appletStr : WFSpecString
def appletStr = ...
op applet : Applet
def applet = appletOf appletStr
endspec
SmartSlang
spec
SS  MS
SSApplet’ = spec
import SSApplets’
op appletStr : WFSpecString
def appletStr = “
”
op applet : Applet
def applet = appletOf appletStr
endspec
subtype proof obligation:
denotesWFSpec? “
SmartSlang
spec
”
SmartSlang
spec
SS  MS
trivial
copy &
paste
SSApplet’ = spec
Metaslang
spec
import SSApplets’
op appletStr : WFSpecString
def appletStr = “
”
SmartSlang
spec
op applet : Applet
def applet = appletOf appletStr
endspec
SmartSlang
spec
SS  MS
Metaslang
spec
SmartSlang
Java Card
program
spec
trivial
copy &
paste
JC  MS
Metaslang
spec
proof obligations include parsing
(previously showed)
AUTOSMART
SS
SPEC
CHECKER
SS  MS
prf
MS
WELLFORMED?
CODE
GENERATOR
y/n
JC
AUTOSMART
SS
SPEC
CHECKER
CODE
GENERATOR
JC
(checked)
CODE
GENERATOR
SS
prf
y/n
JC
prf
JC  MS
WELLFORMED?
MS
(checked)
SS
SS  MS
MS
CODE
GENERATOR
JC
JC  MS
prf
=BEHAVIOR?
y/n
MS
SS
CODE
GENERATOR
CODE
GENERATOR
proof
JC
SS
CODE
GENERATOR
STEP 1
STEP 2
+
proof
JC
more steps  easier proofs
SS
CODE
GENERATOR
STEP 1
STEP 2
STEP 3
+
proof
STEP 4
JC
SS
STEP 1
within
SmartSlang
STEP 2.
. . .STEP
. . .3. . . STEP
. n
language
change
within
Java Card
declarative
transformations?
JC
example of transformation & proof
transformation
example of transformation & proof
e  e’
e.g.
x+0  x
(SS or JC expressions)
⊢ expSem
e = expSem e’
⊢ fa(a,x,y)
(proof depends on e and e’)
expSem x = expSem y =>
appletOf a = appletOf a[x/y]
(proved once
and for all)
instantiation + modus ponens
⊢ applet
= applet’
approach is more general
than smart card applets
L1
L1  L2
L2
languages L1 & L2
translation L1  L2
(possibly L1 = L2)
e.g. •
•
•
•
compilers
code generators
theorem prover interfaces
…
Descargar

Document