Videre arbeid

Na presente seção detalha-se a especificação abstrata da aplicação de passaporte eletrônico JMRTD. Ela é a base para a criação da especificação Java Card que será inserida no cartão (seção 7.5), assim como é a partir da interface das operações deste módulo que é traduzida, de forma automatizada, a API para a aplicação host. Este e outros módulos importantes que compõem o desenvolvimento do passaporte podem ser consultados em detalhes no apêndice C.

As máquinas referenciadas e a definição dos componentes de estado da especificação são apresentados na figura 7.2. Na cláusula SEES são inseridas as especificações dos tipos primiti- vos de Java do KitSmart (JByte, JShort e JBoolean) e máquinas de contexto (Passport_Context e FileSystem_Context) que incluem constantes que são utilizadas na especificação abstrata e em seus refinamentos.

Observa-se que a única máquina inclusa na especificação abstrata é a máquina FileSystem, que modela, através da operação getFile, a obtenção de um arquivo da estrutura de dados LDS do passaporte. Tendo em vista simplificar o modelo decidiu-se uniformizar a representação dos arquivos como uma sequência de 8 bytes.

MACHINE Passport SEES

JByte, JShort, JBoolean, Passport_Context, FileSystem_Context INCLUDES

fileSystem.FileSystem VARIABLES

perState, volState, selectedFile, rnd, ssc INVARIANT

perState∈ JBYTE ∧ volState∈ seq1(JBYTE) ∧ size (volState) = 1 ∧

selectedFile∈ EF_DG1_INDEX .. SOS_LOG_INDEX ∧ rnd∈ seq1 (JBYTE) ∧ ssc∈ seq1 (JBYTE) INITIALISATION perState:= PER_STATE_INIT || volState:= [NO_FILE_SELECTED] || selectedFile:= EF_DG1_INDEX || rnd := [0, 0, 0, 0, 0, 0, 0, 0] || ssc := [0, 0, 0, 0, 0, 0, 0, 0] OPERATIONS (...)

Figura 7.2: Máquina Passport - máquinas referenciadas e variáveis de estado.

Em relação às variáveis de estado, cumpre observar que a variável perState representa o estado atual da aplicação que deve ser armazenado no cartão de forma persistente, ou seja, que deve ser mantido entre diferentes sessões de comunicação. Por outro lado, volState armazena o estado que pode ser modificado a cada sessão de uso da aplicação, mas não necessita ser pre- servado entre elas. A variável selectedFile armazena o índice do último arquivo selecionado, que pode ser um entre dezenove índices de arquivos. Por sua vez, o componente do estado rndguarda o número randômico gerado após a chamada à operação getChallenge. Por fim, a variável ssc é o contador de sessão, inicializado com o estabelecimento do BAC e incrementado a cada nova sessão de comunicação entre o terminal e o cartão. O contador de seção, na espe- cificação oficial, é um valor armazenado em um array de bytes. No desenvolvimento Passport

essa representação foi preservada ao tipá-lo como uma sequência de bytes.

Ressalta-se que no código Java Card da aplicação de passaporte eletrônico, o estado per- sistente é inicializado simplesmente com o valor 0 (zero). Na especificação B, criou-se o es- tado PER_STATE_INIT para representar essa situação inicial. Apenas para deixá-la em um estado consistente, a variável selectedFile recebeu o valor de um dos arquivos do passaporte (EF_DG1_INDEX). A efetiva indicação de que um arquivo está autorizado para ser requi- sitado depende do estado da variável volState. Na situação inicial, ela é inicializada com NO_FILE_SELECTED, indicando que nenhum arquivo foi requisitado ainda para seleção. Por fim, as sequências de byte rnd e ssc tem cada byte inicializado com o valor zero (0), uma vez que elas recebem valores significativos apenas através da chamada às operações getChallenge e processMutualAuthenticate, respectivamente.

Com respeito às operações, inicialmente destaca-se a operação processGetChallenge (fi- gura 7.3), utilizada na geração de um número randômico (challenge), requisito essencial para o processo de autenticação do protocolo BAC, conforme descrito na seção 7.3.1. Ela recebe dois parâmetros, a saber, protectedAPDU, indicando se a comunicação entre as aplicações deve ser protegida e le, que se refere ao tamanho esperado da resposta, nesse caso, do número randô- mico a ser gerado (normalmente, 8 bytes). A operação tem como pré-condições que as chaves iniciais de autenticação mútua tenham sido geradas (perState= HAS_MUTUAL_AUTHENTICATION_KEYS) e

que o processo de autenticação não tenha sido previamente executado (¬ volState (1) = MU- TUAL_AUTHENTICATED). A operação deve armazenar internamente o número randômico gerado como uma sequência de bytes (rnd :∈ number) e retorná-lo ao cliente (rnd_val :∈ num- ber).

rnd_val← processGetChallenge (protectedAPDU, le) = PRE protectedAPDU∈ JBOOLEAN ∧ le∈ JSHORT ∧ perState= HAS_MUTUAL_AUTHENTICATION_KEYS ∧ ¬ (volState(1) = MUTUAL_AUTHENTICATED) THEN volState(1) := CHALLENGED || ANY number WHERE number= seq1(JBYTE) THEN

rnd:∈ number || rnd_val :∈ number END

END;

Figura 7.3: Máquina Passport - operação processGetChallenge.

finalizada através da chamada à operação processMutualAuthenticate (figura 7.4). Para tanto, a operação getChallenge deve ter sido previamente invocada (volState(1) = CHALLENGED) e o processo de autenticação ainda não deve ter sido requisitado para a seção de comunica- ção em curso (¬(volState (1) = MUTUAL_AUTHENTICATED)). A pós-condição deve levar a especificação para o estado MUTUAL_AUTHENTICATED e os bytes correspondentes aos nú- meros randômicos (RNDICC e RNDIFD) e à chave de autenticação KICC devem ser gerados e

retornados à aplicação host através da variável key_data.

key_data← processMutualAuthenticate (protectedAPDU)= PRE protectedAPDU∈ JBOOLEAN ∧ (volState(1) = CHALLENGED ∧ ¬ (volState(1) = MUTUAL_AUTHENTICATED)) THEN volState(1) := MUTUAL_AUTHENTICATED || ssc:∈ seq1(JBYTE) || key_data :∈ seq1(JBYTE) END;

Figura 7.4: Máquina Passport - operação processMutualAuthenticate.

As operações processSelectFile (figura 7.5) e processReadBinary (figura 7.6) especificam, respectivamente, a seleção e o retorno de um arquivo para o terminal de consulta. A primeira recebe um número (fid) representando um índice de arquivo, que deve estar dentro da faixa permitida (fid ∈ EF_DG1_INDEX .. SOS_LOG_INDEX).

processSelectFile (fid)= PRE

fid∈ EF_DG1_INDEX .. SOS_LOG_INDEX ∧ volState(1) = MUTUAL_AUTHENTICATED ∧ ¬ (perState = LOCKED) THEN CHOICE selectedFile:= fid || volState(1) := FILE_SELECTED OR volState(1) := NO_FILE_SELECTED END END;

Figura 7.5: Máquina Passport - operação selectFile.

As demais pré-condições que devem ser obedecidas para a correta aplicação da operação processSelectFiledizem respeito aos estados volátil e persistente. A primeira delas (volState(1) = MUTUAL_AUTHENTICATED) indica que é preciso que a autenticação entre o terminal e o cartão tenha sido estabelecida, o que é feito através da chamada às operações getChallenge e processMutualAuthenticate. Em relação ao estado persistente, o cartão não deve estar no estado bloqueado (perState = LOCKED). No corpo da operação, em uma aplicação bem sucedida, o

índice de arquivo é salvo na variável de estado selectedFile e o estado volátil é modificado para indicar que um arquivo foi selecionado (FILE_SELECTED). Caso contrário, o estado é atualizado para indicar que nenhum arquivo foi selecionado.

Estando o canal de comunicação segura entre o cliente e o cartão devidamente estabelecido e um identificador de arquivo selecionado (processSelectFile), a aplicação terminal pode requi- sitar o arquivo correspondente ao passaporte. O envio efetivo de um arquivo é feito através da operação processReadBinary (Figura 7.6), que obtém o arquivo por meio da operação getFile da máquina inclusa FileSystem, passando para ela o identificador armazenado na variável de estado selectedFile.

file← processReadBinary (protectedAPDU, le)= PRE protectedAPDU∈ JBOOLEAN ∧ le∈ JSHORT ∧ volState(1) = FILE_SELECTED THEN file← fileSystem.getFile(selectedFile) END;

Figura 7.6: Máquina Passport - operação processReadBinary.