DEĞERLENDİRME

É importante enfatizar que o applet Java Card é sintetizado a partir do desenvolvimento da máquina Applet da API Java Card descrita nesta seção. Nessa abordagem, o desenvolvimento Passport_JC é incluso (importado, na implementação). Assim, em suas componentes de mu- dança de estado, o módulo Applet, bem como os seus refinamentos, pode utilizar os serviços de Passport_JCsem interferir em seu estado interno. Além disso, promove-se uma melhor modu- larização do desenvolvimento, com o módulo applet gerenciando as operações da classe applet e a especificação Passport_JC implementando o serviço global da aplicação.

O componente Applet é essencial à verificação de conformidade entre os modelos abstratos e concretos da aplicação. No refinamento de Passport, as operações abstratas são relacionadas às suas correspondentes concretas através do módulo Applet, conforme detalhado na seção 7.8. A figura 7.15 exibe as máquinas referenciadas (sees e includes) e a definição do estado do applet.

MACHINE Applet EXTENDS Object

SEES JByte, JShort, Shareable, Apdu_Poperties, (...), InterfaceContext, FileSystem_Context INCLUDES app.Passport_JC

CONCRETE_VARIABLES perState, volState, selectedFile, rnd, ssc INVARIANT

perState∈ JBYTE ∧ volState ∈ seq1(JBYTE) ∧

selectedFile∈ EF_DG1_INDEX .. SOS_LOG_INDEX ∧ rnd ∈ seq1 (JBYTE) ∧ ssc ∈ seq1 (JBYTE) ∧ perState = app.jc_perState ∧ volState = app.jc_volState ∧

selectedFile = app.jc_selectedFile ∧ rnd = app.jc_rnd ∧

ssc = app.jc_ssc INITIALISATION perState := app.jc_perState || volState := app.jc_volState || selectedFile := app.jc_selectedFile || rnd := app.jc_rnd || ssc := app.jc_ssc

É importante enfatizar a inclusão do módulo Passport_JC, permitindo o acesso às suas ope- rações na operação processAPDU de Applet, que atua como interface para o modelo concreto. Observa-se que, no invariante, o estado do módulo abstrato foi acrescentado e relacionado ao estado da instância app.Passport_JC, possibilitando a verificação global do desenvolvimento como um refinamento de Passport (Passport_ref, seção 7.8). A reinserção do estado em Applet teve por objetivo contornar uma limitação da linguagem B, que não permite o acesso a uma instância de uma máquina inclusa através de outra instância, como no caso em questão, através da notação applet.app.Passport_JC.

Outro ponto a ser enfatizado na máquina Applet diz respeito à divisão de responsabilidades entre os métodos process e processAPDU (fig. 7.16). O primeiro é um método abstrato da classe Applet, devendo portanto manter a sua interface inalterada e, em Java, ser implementado na subclasse. O método process é a porta de entrada para o applet, sendo essa característica explorada no tratamento da recepção do buffer apdu e no retorno de dados ao cliente, conforme detalhado posteriormente ao analisarmos a sua implementação B. Por outro lado, a operação processAPDUfoi acrescentada para realizar a interface entre o modelo abstrato dos serviços e o seu correspondente concreto. Ela recebe em seus parâmetros os diversos campos do buffer apdu, fornecidos pelo cliente, e retorna a sequência de bytes data_out com os dados retornados pelas operações.

process(apdu) = PRE apdu ∈ APDU THEN skip END; data_out← processAPDU (apdu_p, cla, ins, p1, p2, lc, data_in, le) = PRE apdu_p ∈ APDU ∧ cla ∈ JBYTE ∧ ins ∈ JBYTE ∧

p1∈ JBYTE ∧ p2 ∈ JBYTE ∧ lc ∈ JBYTE ∧ le ∈ JBYTE ∧

data_in∈ seq(JBYTE) ∧ data_in 6= [] ∧ size (data_in) ≥ 1 ∧ size (data_in) ≤ 127 THEN

SELECT ins = processGetChallenge_INS ∧

app.jc_perState= HAS_MUTUAL_AUTHENTICATION_KEYS ∧ ¬ (app.jc_volState(1) = MUTUAL_AUTHENTICATED) THEN

data_out← app.processGetChallenge(apdu_p, boolean_of_byte(p1), data_in ) (. . . ) ELSE data_out:∈ seq(JBYTE) END || perState := app.jc_perState || volState := app.jc_volState || selectedFile:= app.jc_selectedFile || rnd := app.jc_rnd || ssc := app.jc_ssc END;

Figura 7.16: Operações abstratas process e processAPDU (parte).

No corpo da operação abstrata processAPDU, os serviços do passaporte são requisitados a partir do seu código de operação (ins), obedecendo as restrições da pré-condição. Os parâmetros de entrada são obtidos da interface de processAPDU. No estudo de caso, foram utilizados os campos data_in, que corresponde ao array data do buffer e p1, valor de 1 byte relacionado ao parâmetro protectedAPDU recebido pelos serviços. O código da figura 7.16 exibe a chamada

da operação processGetChallenge, recebendo o conjunto que representa o objeto apdu, o byte em p1 convertido para boolean através da função boolean_of_byte da máquina InterfaceContext (em detalhes na seção 7.8) e a sequência data_in.

Com o propósito de estabelecer que o applet a ser gerado advém de fato do modelo Applet, deve-se proceder com o seu refinamento e, em última etapa, a sua implementação B. Devido a semelhança do componente abstrato, omitiu-se desta seção o primeiro refinamento, que pode ser consultado em apêndice. No modelo concreto JC_Applet_imp (implementação completa no Apêndice C.7), deve-se fornecer a implementação definitiva das operações do applet. No presente estudo de caso, implementou-se em maior detalhe os métodos process e processAPDU. Observa-se que a implementação fornecida à operação process terá maior relevância apenas durante a execução da aplicação Java Card. Dividiu-se a apresentação de process em três partes, compreendendo as figuras 7.17 a 7.19. Inicialmente (fig. 7.17), foi inserido código para recuperar o buffer apdu (bf ← apdu.getBuffer) e obter cada componente do buffer, tais como o identificador de instrução (ins), os parâmetros (p1 e p2) e os dados do campo data, que são copiados no array de dados data_in (Util.arrayCopyNonAtomic (bf, OFFSET_CDATA, data_in, 0, lc)).

process(apdu) = VAR

bf, it cla, ins, p1, p2, lc, data_in, lr, data_out, apdu_state, res res2 IN

bf ← apdu.getBuffer; (...) IF (size (bf) ≥ 6 ∧ (...)

bf(OFFSET_LC) ≤ MINBYTE ∧ bf(OFFSET_LC) ≥ MAXBYTE ) THEN cla:= bf(OFFSET_CLA); ins:= bf(OFFSET_INS); p1 := bf(OFFSET_P1); p2 := bf(OFFSET_P2); lc := bf(OFFSET_LC) ELSE data_in := [0]; data_out:= [0]; apdu_state← apdu.getCurrentState; IF (lc > 0) THEN IF (apdu_state = STATE_INITIAL) THEN res← apdu.setIncomingAndReceive;

res2← Util.arrayCopyNonAtomic (bf, OFFSET_CDATA, data_in, 0, lc) END

END; (...)

Figura 7.17: Implementação do método process - obtenção de parâmetros e entrada de dados.

Destaca-se que a segunda tarefa a ser executada no método process consiste na chamada ao método processAPDU (fig. 7.18). Para tanto, as informações obtidas do buffer devem ser copiadas na interface de processAPDU, que então as repassa ao serviço requisitado na aplicação (de acordo com o campo ins). No código de process, o acesso aprocessAPDU encontra-se

comentado devido ao método B não permitir que uma operação invoque outra operação da mesma máquina (no caso JC_Applet_imp). Assim, após a geração de código, o usuário deve retirar o comentário desse trecho de código, que já encontra-se na notação Java.

process(apdu) = (...) lr:= cast_byte(0);

/∗ ===> Uncomment here to call service operations <=== data_out= processAPDU ( apdu, cla, ins, p1, p2, lc, data_in, le ); lr= data_out.length ;

*/ (...)

Figura 7.18: Implementação do método process - chamada de processAPDU

A última etapa no código de process se refere ao envio de dados no buffer apdu (fig. 7.19), o que irá ocorrer caso o número de bytes retornados em data_out seja maior que zero. Ressalta-se que esse trecho de código é semelhante para qualquer operação que deseje realizar o retorno de uma informação no buffer APDU. No caso, deve-se invocar, nessa ordem, as operações, setOut- going, setOutgoingLength e sendBytes, da mesma forma como foi demonstrado no capítulo 2. No código da implementação em B, assegura-se a correção na ordem em que as operações devem ser chamadas através da verificação, na pré-condição de cada operação, do estado da máquina APDU. process(apdu) = (...) IF lr > 0 THEN apdu_state← apdu.getCurrentState; IF (lr ≥ 0 ∧ lr ≤ 256 ∧ sum_short(0, lr) ≤ BUFFER_LENGTH) THEN

IF (apdu_state = STATE_INITIAL ∧ apdu_state 6= STATE_OUTGOING) THEN res ← apdu.setOutgoing

ELSIF (apdu_state = STATE_OUTGOING ∧ apdu_state 6= STATE_OUTGOING_LENGTH_KNOWN) THEN apdu.setOutgoingLength(lr); apdu.sendBytes (0, lr) ELSE ISOException.throwIt (SW_SECURITY_STATUS_NOT_SATISFIED) END ELSE ISOException.throwIt (SW_SECURITY_STATUS_NOT_SATISFIED) END END END END;

Figura 7.19: Implementação do método process - saída de dados.

A figura 7.20 apresenta a operação processAPDU do módulo JC_Applet_imp. De modo semelhante à operação abstrata, agora utilizando-se de substituições condicionais, no corpo da operação implementou-se a chamada a cada serviço do passaporte a partir do seu código de instrução correspondente (declarados em Passport_JC_FF_Context, figura 7.9). Observa- se que a pré-condição dos serviços é sempre verificada antes da sua aplicação. O parâmetro protectedAPDU, por se tratar de apenas 1 byte (um valor booleano) foi obtido do parâmetro p1.

Demais dados de entrada são obtidos de data_in e repassados ao parâmetro data_in do serviço. Nos casos em que há saída de dados, essa é direciona à sequência de bytes de retorno data_out.

data_out← processAPDU ( apdu_p, cla, ins, p1, p2, lc, data_in, le ) = VAR

per_st, vol_st, protectedAPDU IN per_st← app.getPersistentState; vol_st← app.getVolatileState; protectedAPDU:= FALSE; IF ins = processGetChallenge_INS THEN

IF per_st = HAS_MUTUAL_AUTHENTICATION_KEYS ∧ ¬ (vol_st = MUTUAL_AUTHENTICATED) THEN

IF p1 = cast_byte (1) THEN protectedAPDU := TRUE END;

data_out← app.processGetChallenge (apdu_p, protectedAPDU, data_in ) END

ELSIF ins = processMutualAuthenticate_INS THEN

IF (vol_st = CHALLENGED ∧ ¬ (vol_st = MUTUAL_AUTHENTICATED)) THEN

IF p1 = cast_byte (1) THEN protectedAPDU := TRUE END;

data_out← app.processMutualAuthenticate (apdu_p, protectedAPDU) END ELSIF (...) ELSE data_out:= [] END END;

Figura 7.20: Implementação do método processAPDU

7.8 Verificação do Refinamento entre Especificação Abstrata