SPARK é uma linguagem de programação formalmente definida baseada na linguagem de programação Ada, destinada ao desenvolvimento de software de alta integridade utilizado em sistemas onde a operação previsível e altamente confiável é essencial. Ela facilita o desenvolvimento de aplicações que exigem segurança de funcionamento (safety), segurança da informação (security) ou integridade de negócios. Encontrou aplicação principalmente na computação em tempo real e em sistemas embarcados onde questões de criticidade de segurança ou segurança computacional são primordiais.

Originalmente, existiam três versões do SPARK (SPARK83, SPARK95, SPARK2005), baseadas em Ada 83, Ada 95 e Ada 2005, respectivamente.

Uma quarta versão, o SPARK 2014, baseada em Ada 2012, foi lançada em 30 de abril de 2014. O SPARK 2014 é uma reformulação completa da linguagem e suporta ferramentas de verificação de software.

A linguagem SPARK consiste em um subconjunto bem definido da linguagem Ada que utiliza contratos para descrever a especificação de componentes de uma forma adequada tanto para verificação estática quanto dinâmica. O SPARK também foi projetado para eliminar todas as construções da linguagem que possam causar comportamento imprevisível.

No SPARK83/95/2005, os contratos são codificados em comentários de Ada e, portanto, são ignorados por qualquer compilador Ada padrão, mas são processados pelo Examiner do SPARK e suas ferramentas associadas. Essas versões anteriores focam na verificação estática de contratos.

O SPARK 2014, em contrapartida, utiliza a sintaxe integrada de aspectos do Ada 2012 para expressar contratos, trazendo-os para o núcleo da linguagem. A principal ferramenta para o SPARK 2014 (GNATprove) baseia-se na infraestrutura do GNAT/GCC e reutiliza quase todo o front-end do GNAT Ada 2012.

Visão geral técnica O SPARK utiliza os pontos fortes de Ada enquanto tenta eliminar todas as suas potenciais ambiguidades e construções inseguras. Os programas em SPARK são, por projeto, destinados a ser inequívocos, e exige-se que seu comportamento não seja afetado pela escolha do compilador Ada. Esses objetivos são alcançados em parte pela omissão de alguns dos recursos mais problemáticos de Ada (como o multitarefa paralelo irrestrito) e em parte pela introdução de contratos que codificam as intenções e os requisitos do projetista da aplicação para determinados componentes de um programa.

A combinação dessas abordagens permite que o SPARK atenda aos seus objetivos de projeto, que são:

solidez lógica definição formal rigorosa semântica simples segurança poder expressivo verificabilidade requisitos de recursos (espaço e tempo) limitados requisitos mínimos de sistema em tempo de execução (runtime)

Um membro da equipe da Praxis afirmou: "Nossa taxa de defeitos com o Spark é pelo menos 10 vezes, às vezes 100 vezes menor do que aquelas criadas com outras linguagens."

Exemplos de contratos Considere a especificação de subprograma em Ada abaixo:

procedure Increment (X : in out Counter_Type);

Em Ada pura, isso poderia incrementar a variável X em um ou em mil; ou poderia definir algum contador global para X e retornar o valor original do contador em X; ou poderia não fazer nada com X.

Com o SPARK 2014, contratos são adicionados ao código para fornecer mais informações sobre o que um subprograma realmente faz. Por exemplo, a especificação acima pode ser alterada para:

procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X);

Isso especifica que o procedimento Increment não utiliza nenhuma variável global (nem atualização nem leitura) e que o único item de dados utilizado no cálculo do novo valor de X é apenas X.

Alternativamente, a especificação pode ser escrita como:

procedure Increment (X : in out Counter_Type) with Global => (In_Out => Count), Depends => (Count => (Count, X), X => null);

Isso especifica que Increment usará a variável global Count no mesmo pacote que Increment, que o valor exportado de Count depende dos valores importados de Count e X, e que o valor exportado de X não depende de nenhuma variável, sendo derivado apenas de dados constantes.

Se o GNATprove for então executado na especificação e no corpo correspondente de um subprograma, ele analisará o corpo do subprograma para construir um modelo do fluxo de informações. Esse modelo é então comparado com o que foi especificado pelas anotações e quaisquer discrepâncias são relatadas ao usuário.

Essas especificações podem ser ainda mais estendidas pela asserção de várias propriedades que precisam ser válidas quando um subprograma é chamado (pré-condições) ou que serão válidas assim que a execução do subprograma for concluída (pós-condições). Por exemplo, ao escrever:

procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X), Pre => X < Counter_Type'Last, Post => X = X'Old + 1;

Isso agora especifica não apenas que X é derivado somente de si mesmo, mas também que antes de Increment ser chamado, X deve ser estritamente menor que o último valor possível de seu tipo (para garantir que o resultado nunca cause estouro de inteiro) e que depois X será igual ao valor inicial de X mais um.

Condições de verificação O GNATprove também pode gerar um conjunto de condições de verificação (VCs). Elas são usadas para estabelecer se certas propriedades são válidas para um determinado subprograma. No mínimo, o GNATprove gerará VCs para estabelecer que todos os erros em tempo de execução não podem ocorrer dentro de um subprograma, tais como:

índice de arranjo fora do intervalo (out of range) violação de intervalo de tipo divisão por zero estouro numérico (overflow)

Se uma pós-condição ou qualquer outra asserção for adicionada a um subprograma, o GNATprove também gerará VCs que exigem que o usuário demonstre que essas propriedades são válidas para todos os caminhos de execução possíveis através do subprograma.

Nos bastidores, o GNATprove usa a linguagem intermediária e o gerador de VCs Why3, e os provadores de teoremas CVC4, Z3 e Alt-Ergo para descarregar as VCs. O uso de outros provadores (incluindo verificadores de prova interativos) também é possível por meio de outros componentes do conjunto de ferramentas Why3.

História Os primórdios da tecnologia remontam a 1987, com base em trabalhos realizados na Universidade de Southampton. A primeira versão do SPARK (baseada em Ada 83) foi produzida na universidade, com patrocínio do Ministério da Defesa do Reino Unido, por Bernard Carré e Trevor Jennings. O nome SPARK derivou de SPADE Ada Kernel, em referência ao subconjunto SPADE da linguagem de programação Pascal.

Posteriormente, a linguagem foi progressivamente estendida e refinada, primeiro pela Program Validation Limited e depois pela Praxis Critical Systems Limited. Em 2004, a Praxis Critical Systems Limited mudou seu nome para Praxis High Integrity Systems Limited, e o trabalho no SPARK continuou. Em janeiro de 2010, a empresa tornou-se Altran Praxis.

No início de 2009, a Praxis formou uma parceria com a AdaCore e lançou o SPARK Pro sob os termos da GPL. Isso foi seguido em junho de 2009 pelo SPARK GPL Edition 2009, voltado para as comunidades de software livre e de código aberto (FOSS) e acadêmica.

Em janeiro de 2013, a Altran-Praxis mudou seu nome para Altran, que em abril de 2021 tornou-se Capgemini Engineering (após a fusão da Altran com a Capgemini).

A primeira versão Pro do SPARK 2014 foi anunciada em 30 de abril de 2014, sendo rapidamente seguida pela edição SPARK 2014 GPL, voltada para as comunidades acadêmica e de software livre.

Aplicações industriais O SPARK tem sido empregado em uma série de aplicações industriais no mundo real. Incorporá-lo o mais cedo possível no processo de projeto é considerado geralmente como a abordagem que oferece o resultado mais favorável.

Sistemas relacionados à segurança de funcionamento O SPARK tem sido utilizado em diversos sistemas críticos de segurança de alto perfil, cobrindo aviação comercial (o Ship/Helicopter Operational Limits Instrumentation System, motores a jato da série Rolls-Royce Trent, o sistema ARINC ACAMS, o Lockheed Martin C130J), aviação militar (Eurofighter Typhoon, Harrier GR9, AerMacchi M346), gerenciamento de tráfego aéreo (sistema NATS iFACTS do Reino Unido), setor ferroviário (inúmeras aplicações de sinalização), médico (o dispositivo de assistência ventricular LifeFlow) e aplicações espaciais (o projeto CubeSat da Vermont Technical College).

Em termos dos processos de aprovação necessários para tais sistemas, o SPARK foi utilizado para certificação em conformidade com o padrão de defesa do Reino Unido (DEFSTAN) 00-55, bem como com a DO-178B Nível A e ITSEC E6.

Sistemas relacionados à segurança da informação O SPARK também tem sido empregado no desenvolvimento de sistemas seguros. Entre os usuários estão a Rockwell Collins (soluções entre domínios Turnstile e SecureOne), o desenvolvimento da autoridade certificadora original do MULTOS, o demonstrador Tokeneer da NSA, a estação de trabalho multinível secunet, o microkernel de separação Muen e o criptografador de dispositivos de bloco Genode. Outro caso foi a implementação de uma autoridade de certificação segura para o cartão de valor armazenado produzido pela Mondex International, no qual a notação Z foi usada como precursora da codificação em SPARK.

Em agosto de 2010, Rod Chapman, engenheiro principal da Altran Praxis, implementou o Skein, um dos candidatos ao SHA-3, em SPARK. Após cuidadosa otimização, ele conseguiu fazer com que a versão em SPARK rodasse apenas cerca de 5 a 10% mais lenta que a implementação em C. Melhorias posteriores no middle-end de Ada no GCC (implementadas por Eric Botcazou da AdaCore) eliminaram a diferença, com o código SPARK alcançando exatamente o mesmo desempenho do C.

A NVIDIA também adotou o SPARK para a implementação de firmware crítico para a segurança. Obtendo êxito nisso, a empresa adicionou o SPARK para projetos adicionais relacionados a firmware e iniciou treinamentos internos no uso da tecnologia SPARK.

Em 2020, Rod Chapman reimplementou a biblioteca criptográfica TweetNaCl em SPARK 2014. A versão em SPARK da biblioteca possui uma prova autoativa completa de segurança de tipos, segurança de memória e algumas propriedades de correção, mantendo algoritmos em tempo constante em toda a extensão. O código SPARK também é significativamente mais rápido que o TweetNaCl.

Ver também Notação Z Java Modeling Language Referências

Leitura adicional

Ligações externas Site da comunidade SPARK 2014 Website do SPARK Pro Website do SPARK Libre (GPL) Edition Altran Correctness by Construction: A Manifesto for High-Integrity Software Safety-Critical Systems Club do Reino Unido Comparação com uma linguagem de especificação em C (Frama C) Página do projeto Tokeneer Lançamento público do Muen Kernel Projeto LifeFlow LVAD Projeto VTU CubeSat

Categoria:Linguagens de programação concorrentes Categoria:Linguagens de programação procedurais Categoria:Linguagens de programação criadas no século XX Categoria:Universidade de Southampton