A figura 7.11 apresenta uma visão geral das máquinas que compõem a implementação e as suas principais dependências.
Figura 7.11: Visão geral dos módulos principais do desenvolvimento Passport.
O desenvolvimento dos serviços oferecidos pela aplicação é apresentado na parte central da figura (Passport_JC, Passport_JC_FF_ref, Passport_JC_imp). A implementação importa (cláusula IMPORTS) diversas máquinas que auxiliam na implementação dos serviços. As má- quinas FileSystem, FileIndex, KeyStore, PassportCrypto e PassportUtil e suas implementações foram derivadas de classes correspondentes da aplicação de código-aberto JMRTD. A seguir, descreve-se de forma resumida cada um desses componentes.
FileIndex e FileSystem FileIndex contém uma operação getFileIndex que, dado um identifica- dor de arquivo, retorna o seu índice correspondente. O módulo FileSystem, por sua vez, possui uma operação que modela o retorno de um arquivo, dado o seu identificador.
KeyStore Possui operações para armazenar e retornar as chaves KENC e KMAC necessárias ao
PassportCrypto Contém diversos serviços úteis ao BAC e a outros protocolos do passaporte, permitindo encriptar, decriptar, gerar resumo criptográfico, verificar resumo, gerar cha- ves, e computar o contador de sessão.
PassportUtil implementa serviços diversos, que possibilitam, por exemplo, a troca dos valores armazenados em duas sequências de bytes e o retorno do menor entre dois valores. É utilizado pelo serviço processMutualAuthenticate.
É importante destacar outra categoria de máquinas importadas, as máquinas de biblioteca, utilizadas para encapsular o estado da implementação. Na figura, destacam-se as máquinas que modelam sequência (LM_SEQ_x), cujas implementações variam conforme o tipo de dados da sequência ou restrições impostas (número de elementos, tipo dos elementos, etc.). As máqui- nas de sequência refinam as variáveis volState (estado volátil), rnd (número randômico) e ssc (contador de sessão). Por sua vez, a máquina LM_BYTE encapsula o estado de 1 byte, refinando perState. Por fim, a biblioteca LM_SHORT_FILE é utilizada para armazenar o conteúdo da variável selectedFile, um valor short restrito a um índice de arquivo.
A figura 7.12 exibe as máquinas vistas, importadas e o invariante da implementação, que liga o estado abstrato às variáveis correspondentes das máquinas de biblioteca. Observa-se que todas as máquinas importadas devem receber um prefixo (nome de instância) que, no código Java Cardgerado, será o nome do objeto Java criado.
IMPLEMENTATION Passport_JC_imp REFINES Passport_JC_FF_ref
SEES JByte, JShort, JBoolean, APDU_Properties, ISO7816,
Passport_Context, FileSystem_Context, Passport_JC_FF_Context IMPORTS per_state.LM_BYTE, sel_file.LM_SHORT_FILE,
vol_state.LM_SEQ_0, jc_rnd_var.LM_SEQ_1, jc_ssc_var.LM_SEQ_1,
fileSystem.FileSystem, passportUtil.PassportUtil, crypto.PassportCrypto, keyStore.KeyStore, ISOException.ISOException, randomData.RandomData, apdu.Apdu, Util.Util
INVARIANT jc_perState= per_state.num_byte ∧ jc_volState= vol_state.bt_seq ∧ jc_selectedFile= sel_file.num_short ∧ jc_rnd= jc_rnd_var.bt_seq ∧ jc_ssc= jc_ssc_var.bt_seq
Figura 7.12: Máquinas referenciadas e especificação do estado da implementação Pass- port_JC_imp.
No caso das máquinas da API Java Card do KitSmart, utilizou-se as especificações ISOException, APDU, Util e RandomData, assim como foi feito para o refinamento Pass- port_JC_FF_ref. O uso dessas máquinas permite a verificação do uso correto das operações quanto aos tipos de dados utilizados, restrições aos valores desses tipos e quanto à necessidade
da aplicação prévia de outras operações, como no caso das operações de recepção e envio de dados da máquina Apdu. Dessa forma, ao ser gerado o código Java Card, os métodos serão chamados com o tipos corretos e na ordem adequada.
O invariante da implementação relaciona as variáveis abstratas com o estado das máqui- nas de biblioteca. Por exemplo, jc_perState = per_state.num_byte liga a variável de estado jc_perStateà variável num_byte da máquina LM_BYTE. Assim, toda operação sobre jc_perState será efetuada por meio das operações da máquina LM_BYTE, atualizando ou consultando a va- riável num_byte. De forma semelhante, o mesmo é feito para os outros componentes do estado da especificação Passport_JC_imp. A seção 7.7.2 a seguir apresenta o refinamento concreto das operações processGetChallenge e processSelectFile.
7.7.2 Operações processGetChallenge e processSelectFile
Nesta seção apresenta-se a implementação das operações processGetChallenge e process- SelectFile. Algumas partes dos códigos foram omitidas para deixá-los menos extensos e para que a explicação concentre-se nos aspectos mais relevantes.
data_out← processGetChallenge (apdu_p, protectedAPDU, data_in) = VAR le_val,v_st, per_st, bf, bf_offset, jc_rnd, apdu_state, out IN
bf← apdu.getBuffer; v_st← vol_state.getFirst;
per_st← per_state.get_num; jc_rnd← jc_rnd_var.getSeq; IF v_st = MUTUAL_AUTHENTICATED THEN
ISOException.throwIt(ex_processGetChallenge0)
ELSIF ¬ (per_st = HAS_MUTUAL_AUTHENTICATION_KEYS) THEN ISOException.throwIt(ex_processGetChallenge1)
ELSE (...)
le_val← Util.getShort(data_in, cast_short (0)) (...)
randomData.generateData(jc_rnd, 0, le_val); //Geração do número randômico (...)
IF sum_short(cast_short(0), le_val) ≤ size(jc_rnd) ∧ sum_short(cast_short(0), le_val) ≤ size(bf) ∧ bf_offset≥ 0 ∧ bf 6= [] ∧ sum_short(bf_offset, le_val) ≤ size(bf)
THEN
out← Util.arrayCopyNonAtomic(jc_rnd, cast_short(0), bf, bf_offset, le_val); jc_rnd_var.setSeq (jc_rnd) //Atualização da variável de estado
ELSE
ISOException.throwIt(SW_INTERNAL_ERROR) END;
vol_state.set(CHALLENGED); //Atualização do estado da aplicação data_out:= jc_rnd //Retorno do número gerado
END END;
Figura 7.13: Passport_JC_imp - operação concreta processGetChallenge.
Na operação processGetChallenge (figura 7.13), após a verificação das restrições de estado inclusas no modelo full function, vê-se a obtenção do valor tamanho esperado da resposta (le) diretamente do array data_in através da operação getShort da máquina Util da api Java Card (le_val ← Util.getShort(data_in, cast_short (0))). Posteriormente, a sequência aleatória de 8
bytesé gerada e armazenada na variável local jc_rnd, com o auxílio da operação generateData da máquina RandomData (randomData.generateData (jc_rnd, 0, le_val)). O valor local é então utilizado na atualização do estado global (jc_rnd_var.setSeq (jc_rnd)).
Observa-se que a cópia da variável jc_rnd no buffer apdu é o primeiro passo para retorná-la ao cliente. Para tanto, utiliza-se a operação arrayCopyNonAtomic da máquina Util. Ela recebe o valor de jc_rnd, o buffer apdu (bf ), os índices a partir dos quais a cópia dos valores é efetivada (cast_short (0) e bf_offset) e quantos bytes serão copiados (le_val). Observe que o arquivo só será copiado no buffer caso diversas restrições sejam atendidas, tais como o fato do buffer não ser vazio (bf 6= []) e a quantidade de bytes inseridos a partir de bf_offset não ultrapassar o tamanho do buffer (sum_short(bf _offset,le_val) ≤ size(bf )). A abordagem de antecipar os erros que possam surgir pela aplicação de operações com valores incorretos é utilizada durante toda implementação para assegurar a robustez do desenvolvimento.
Caso a geração tenha sido bem-sucedida, o estado global do passaporte é atualizado para CHALLENGED(vol_state.set(CHALLENGED)) e o valor do número randômico é retornado em data_out (data_out := jc_rnd). Destaca-se que o código de envio de data_out ao cliente, comum a todas as operações que retornam informações, encontra-se inserido no método process da implementação Applet.
processSelectFile (apdu_p, data_in) = VAR v_st, per_st,bf, lc_data, fid, file IN
v_st← vol_state.getFirst; per_st ← per_state.get_num; bf← apdu.getBuffer; vol_state.set(NO_FILE_SELECTED); IF per_st = LOCKED THEN ISOException.throwIt(ex_processSelectFile0) ELSIF ¬ (v_st = MUTUAL_AUTHENTICATED) THEN ISOException.throwIt(ex_processSelectFile1) ELSE fid:= data_in(1); lc_data:= cast_byte(8);
IF (fid ≥ EF_DG1_INDEX ∧ fid ≤ SOS_LOG_INDEX) THEN file← fileSystem.getFile(fid); IF (file 6= []) THEN sel_file.set_num(fid); vol_state.set(FILE_SELECTED) ELSE ISOException.throwIt(SW_FILE_NOT_FOUND) END ELSE ISOException.throwIt(SW_INTERNAL_ERROR) END END END;
Figura 7.14: Passport_JC_imp - operação concreta processSelectFile.
Ressalta-se que a operação processSelectFile (figura 7.14) não retorna nenhuma informação por meio do buffer. Sua funcionalidade principal é atualizar o arquivo selecionado (a variável
de estado selectedFile) com o valor fornecido pela aplicação host. Em seu modelo concreto, após as verificações de estado, o identificador do arquivo é obtido do primeiro byte do pa- râmetro data_in (fid := data_in(1)). Na sequência do código de processSelectFile é feita a leitura do arquivo, caso o identificador esteja na faixa correta (file ← fileSystem.getFile(fid), e a atualização das informações do estado relativa à seleção do arquivo (sel_ f ile.set_num(fid) e vol_state.set(FILE_SELECTED)).
Na seção 7.7.3 a seguir descreve-se o componente da implementação que refina o modelo da classe Applet da API Java Card e realiza o processamento das chamadas aos serviços do desenvolvimento Passport_JC.