Quais linguagens são usadas para software crítico de segurança?[fechado]
https://stackoverflow.com/questions/243387
-
04-07-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianPergunta
Estou pesquisando o desenvolvimento de software crítico para a segurança e, em particular, quais os efeitos que a escolha da linguagem de programação tem nesse desenvolvimento.
Por favor, explique, em detalhes, quais idiomas são comumente usados e por quê.
Solução
Ada e FAGULHA (que é um dialeto Ada com alguns ganchos para verificação estática) são usados em círculos aeroespaciais para construir software de alta confiabilidade, como sistemas aviônicos.Há algo de ecossistema de ferramentas de verificação de código para essas linguagens, embora esta tecnologia também exista para idiomas mais convencionais também.
Erlang era projetado desde o início para escrevendo de alta confiabilidade código de telecomunicações.Ele foi projetado para facilitar a separação de preocupações para recuperação de erros (ou seja,o subsistema que gera o erro é diferente do subsistema que trata o erro).Também pode ser submetido a provas formais, embora esta capacidade não tenha realmente saído dos círculos de pesquisa.
Linguagens funcionais como Haskell podem ser submetidos a provas formais por sistemas automatizados devido à natureza declarativa da língua.Isso permite que códigos com efeitos colaterais sejam contidos em funções monádicas.Para uma prova formal de correção, pode-se presumir que o restante do código não faz nada além do que está especificado.
No entanto, essas linguagens são coletadas como lixo e a coleta de lixo é transparente para o código, portanto não pode ser raciocinada dessa maneira.Linguagens de coleta de lixo normalmente não são previsíveis o suficiente para aplicações difíceis em tempo real, embora haja um conjunto de pesquisas em andamento sobre coletores de lixo incrementais limitados no tempo.
Eiffel e seus descendentes têm suporte integrado para uma técnica chamada Projeto por contrato que fornece um mecanismo de tempo de execução robusto para incorporar pré e pós-verificações para invariantes. Embora Eiffel nunca tenha realmente pegado, o desenvolvimento de software de alta confiabilidade tende a consistir em escrever verificações e manipuladores para modos de falha antecipadamente, antes de realmente escrever a funcionalidade.
Embora C e C++ não foram projetados especificamente para esse tipo de aplicação, eles são amplamente utilizados para software embarcado e de segurança crítica por vários motivos.As principais propriedades dignas de nota são o controle sobre o gerenciamento de memória (que permite evitar a coleta de lixo, por exemplo), bibliotecas básicas de tempo de execução simples e bem depuradas e suporte a ferramentas maduras.Muitas das cadeias de ferramentas de desenvolvimento incorporadas em uso hoje foram desenvolvidas pela primeira vez nas décadas de 1980 e 1990, quando esta era a tecnologia atual e vêm da cultura Unix que prevalecia naquela época, portanto, essas ferramentas continuam populares para esse tipo de trabalho.
Embora o código de gerenciamento manual de memória deva ser cuidadosamente verificado para evitar erros, ele permite um grau de controle sobre os tempos de resposta do aplicativo que não está disponível em linguagens que dependem de coleta de lixo. O bibliotecas principais de tempo de execução das linguagens C e C++ são relativamente simples, maduras e bem compreendidas, portanto estão entre as plataformas mais estáveis disponíveis.A maioria, senão todas as ferramentas de análise estática usadas para Ada também suportam C e C++, e há muitas outras ferramentas semelhantes disponíveis para C.Há também diversos largamente usado C/C++ baseado ferramenta correntes;a maioria das cadeias de ferramentas usadas para Ada também vem em versões que suportam C e/ou C++.
Métodos Formais como Semântica Axiomática (PDF), Notação Z ou Comunicação de Processos Sequenciais permitem que a lógica do programa seja verificada matematicamente e são frequentemente usados no projeto de software crítico de segurança onde a aplicação é simples o suficiente para aplicá-los (normalmente sistemas de controle embarcados).Por exemplo, um dos meus ex-professores fez uma prova formal de correção de um sistema de sinalização para a rede ferroviária alemã.
A principal deficiência dos métodos formais é a sua tendência a crescer exponencialmente em complexidade em relação ao sistema subjacente que está sendo provado.Isto significa que existe um risco significativo de erros na prova, pelo que estão praticamente limitados a aplicações bastante simples.Métodos formais são amplamente usados para verificar a exatidão do hardware, pois os bugs de hardware são muito caros para corrigir, especialmente em produtos do mercado de massa.Desde o Bug Pentium FDIV, os métodos formais ganharam bastante atenção e foram usado para verificar a exatidão do FPU em todos os processadores Intel desde o Pentium Pro.
Muitas outras linguagens têm sido usadas para desenvolver software altamente confiável. Muitas pesquisas foram feitas sobre o assunto. Pode-se argumentar razoavelmente que metodologia é mais importante que a plataforma embora existam princípios como simplicidade e seleção e controle de dependências que podem impedir o uso de certas plataformas.
Como vários outros observaram, certas plataformas O/S possuem recursos para promover confiabilidade e comportamento previsível, como temporizadores de vigilância e tempos de resposta de interrupção garantidos.A simplicidade também é um forte impulsionador da confiabilidade, e muitos sistemas RT são deliberadamente mantidos muito simples e compactos. QNX (o único sistema operacional com o qual estou familiarizado, tendo trabalhado uma vez com um sistema de dosagem de concreto baseado nele) é muito pequeno e cabe em um único disquete.Por razões semelhantes, as pessoas que fazem OpenBSD - que é conhecido por sua segurança robusta e auditoria de código completa - também faz de tudo para manter o sistema simples.
EDITAR: Esta postagem tem alguns links para bons artigos sobre software crítico de segurança, em particular Aqui e Aqui.Parabéns a S.Lott e Adam Davis pela fonte.A história do THERAC-25 é um trabalho um tanto clássico neste campo.
Outras dicas
Para C++, o padrão de codificação C++ do Joint Strike Fighter (F-35) é uma boa leitura:
Eu acredito Ada ainda está em uso em alguns projetos governamentais que são de segurança e/ou missão crítica.Nunca usei o idioma, mas está na minha lista de “aprender”, junto com Eiffel.A Eiffel oferece Design By Contract, que supostamente melhora a confiabilidade e a segurança.
Em primeiro lugar, o software crítico de segurança segue os mesmos princípios que você veria nos campos clássicos da engenharia mecânica e elétrica.Redundância, tolerância a falhas e segurança contra falhas.
À parte, e como o postador anterior aludiu (e por algum motivo foi rejeitado), o fator mais importante para conseguir isso é que sua equipe tenha uma compreensão sólida de tudo o que está acontecendo.Nem é preciso dizer que um bom design de software de sua parte é fundamental.Mas também implica uma linguagem acessível, madura, bem suportada, para a qual existe muito conhecimento comunitário e desenvolvedores experientes disponíveis.
Muitos postadores já comentaram que o sistema operacional é um elemento-chave neste aspecto, o que é verdade porque deve ser determinístico (ver QNX ou VxWorks).Isso exclui a maioria das linguagens interpretadas que fazem coisas nos bastidores para você.
ADA é uma possibilidade, mas há menos ferramentas e suporte por aí e, mais importante, as pessoas estelares não estão tão prontamente disponíveis.
C++ é uma possibilidade, mas somente se você aplicar estritamente um subconjunto.Neste aspecto, é uma ferramenta do diabo, prometendo tornar a nossa vida mais fácil, mas muitas vezes fazendo demasiado,
C é ideal.É muito maduro, rápido, possui um conjunto diversificado de ferramentas e suporte, muitos desenvolvedores experientes por aí, multiplataforma e extremamente flexível, podem trabalhar próximos ao hardware.
Eu desenvolvi tudo, desde smalltalk até ruby, e aprecio e aproveito tudo o que linguagens superiores têm a oferecer.Mas quando estou desenvolvendo sistemas críticos, eu aguento a bala e fico com C.Na minha experiência (defesa e muitos dispositivos médicos de classes II e III) menos é mais.
Eu escolheria Haskell se fosse segurança acima de todo o resto.Proponho o haskell porque ele possui uma verificação de tipo estático muito rígida e promove uma programação onde você constrói peças de uma maneira que são muito fáceis de testar.
Mas então eu não me importaria muito com a linguagem.Você pode obter muito mais segurança sem comprometer tanto tendo seu projeto em condições gerais e trabalhando sem prazos.No geral, como ter todo o gerenciamento básico do projeto em funcionamento.Talvez eu me concentrasse em testes extensivos para garantir que tudo funcionasse como deveria, testes que cobrem todos os casos extremos e muito mais.
A linguagem e o sistema operacional são importantes, mas o design também.Tente mantê-lo básico, extremamente simples.
Eu começaria tendo o mínimo de informações de estado (dados em tempo de execução), para minimizar a chance de ficar inconsistente.Então, se você quiser ter redundância para fins de tolerância a falhas, certifique-se de ter maneiras infalíveis de recuperar os dados que ficam inconsistentes.A redundância sem uma forma de se recuperar da inconsistência é apenas procurar problemas.
Sempre tenha um substituto para quando as ações solicitadas não forem concluídas em um prazo razoável.Como se costuma dizer no controle de tráfego aéreo, uma autorização não reconhecida não é autorização.
Não tenha medo dos métodos de votação.Eles são simples e confiáveis, mesmo que possam desperdiçar alguns ciclos.Evite o processamento que depende apenas de eventos ou notificações, porque eles podem ser facilmente descartados, duplicados ou ordenados incorretamente.Como complemento à votação, eles estão bem.
Um amigo meu do projeto APOLLO comentou certa vez que sabia que eles estavam levando a sério quando decidiram confiar em pesquisas, em vez de eventos, embora o computador fosse terrivelmente lento.
P.S.Acabei de ler os padrões C++ Air Vehicle.Eles estão bem, mas parecem assumir que haverá muitas classes, dados, ponteiros e alocação dinâmica de memória.Isso é exatamente o que não deveria ser mais do que o absolutamente necessário.Deveria haver um czar da estrutura de dados com uma grande foice.
O sistema operacional é mais importante que o idioma.Use um kernel em tempo real como VxWorks ou QNX.Analisamos ambos para controlar robôs industriais e decidimos usar o VxWorks.Usamos C para o controle real do robô.
Para software verdadeiramente crítico, como sistemas de pouso automático de aeronaves, você deseja que vários processadores sejam executados de forma independente para verificar os resultados.
Ambientes em tempo real geralmente possuem requisitos "críticos de segurança".Para esse tipo de coisa, você poderia olhar para VxWorks, um popular sistema operacional em tempo real.Atualmente está em uso em diversas áreas, como aeronaves Boeing, componentes internos do BMW iDrive, controladores RAID e várias naves espaciais.(Confira.)
O desenvolvimento para a plataforma VxWorks pode ser feito com diversas ferramentas, dentre elas Eclipse, Bancada de trabalho, PONTUAÇÃO, e outros.C, C++, Ada e Fortran (sim, Fortran) são suportados, assim como alguns outros.
Já que você não fornece uma plataforma, eu diria C/C++.De qualquer forma, na maioria das plataformas em tempo real, você tem opções relativamente limitadas.
As desvantagens da tendência do C de permitir que você dê um tiro no próprio pé são compensadas pelo número de ferramentas para validar o código e pela estabilidade e mapeamento direto do código para os recursos de hardware da plataforma.Além disso, para qualquer coisa crítica, você não poderá confiar em software de terceiros que não tenha sido extensivamente revisado - isso inclui a maioria das bibliotecas - mesmo muitas daquelas fornecidas por fornecedores de hardware.
Como tudo será de sua responsabilidade, você deseja um compilador estável, comportamento previsível e um mapeamento próximo do hardware.
Aqui estão algumas atualizações para algumas ferramentas que eu ainda não tinha visto discutidas e com as quais tenho brincado ultimamente, que são bastante boas.
A infraestrutura do compilador LLVM, uma breve sinopse em sua página principal (inclui front-ends para C e C++.Front-ends para Java, Scheme e outras linguagens estão em desenvolvimento);
Uma infraestrutura de compilador - LLVM também é uma coleção de código-fonte que implementa a linguagem e estratégia de compilação.O primário componentes da infraestrutura LLVM são um front-end C & C++ baseado em GCC, um estrutura de otimização de tempo de link com um conjunto crescente de análises interprocessuais e transformações, back-ends estáticos para o X86, X86-64, PowerPC 32/64, ARM, Polegar, IA-64, Alpha, SPARC, MIPS e Arquiteturas CellSPU, um back-end que emite código C portátil, e um Compilador Just-In-Time para X86, X86-64, Processadores PowerPC 32/64 e um emissor para MSIL.
CCV;
VCC é uma ferramenta que comprova a correção de programas C simultâneos anotados ou encontra problemas neles.VCC estende C com recursos de design por contrato, como pré e pós-condição, bem como tipo Invariáveis.Os programas anotados são traduzido para fórmulas lógicas usando a ferramenta Boogie, que os passa para um solucionador SMT automatizado Z3 para verificar sua validade.
VCC usa o lançado recentemente Infraestrutura Comum do Compilador.
Ambas as ferramentas, LLVM ou VCC, são projetadas para suportar múltiplas linguagens e arquiteturas. Acredito que haja um aumento na codificação por contrato e outras práticas formais de verificação.
WPF (não a estrutura MS :), é um bom lugar para começar se você estiver tentando avaliar algumas das pesquisas e ferramentas recentes no espaço de validação de programas.
GT23 é o principal recurso, no entanto, para informações bastante atuais e específicas detalhes da linguagem de desenvolvimento de sistemas críticos.Eles cobrem tudo, desde Ada, C, C++, Java, C#, Scripting, etc...e ter pelo menos um conjunto decente de referência e orientação para atualizar informações sobre falhas e vulnerabilidades específicas do idioma.
Há muitas boas referências em http://www.dwheeler.com ("software de alta segurança").
Para itens automotivos, consulte o padrão MISRA C.C, mas você não pode usar mais de dois níveis de ponteiros e outras coisas assim.
adahome.com tem boas informações sobre Ada.Gostei deste tutorial de C++ para Ada: http://adahome.com/Ammo/cpp2ada.html
Para tempo real, Tom Hawkins fez algumas coisas interessantes sobre Haskell.Ver:ImProve (a linguagem incorpora um solucionador SMT para verificar as condições de verificação) e Atom (EDSL para programação simultânea em tempo real sem usar threads ou tarefas reais).
Uma linguagem que impõe padrões cuidadosos pode ajudar, mas você pode impor padrões cuidadosos usando qualquer linguagem, até mesmo assembler.Cada suposição sobre cada valor precisa de um código que teste a suposição.Por exemplo, sempre teste o divisor para zero antes de dividir.
Quanto mais você confiar nos componentes reutilizáveis, mais fácil será a tarefa, mas os componentes reutilizáveis raramente são certificados para uso crítico e não passarão por processos regulatórios de segurança.Você deve usar um pequeno kernel do sistema operacional e, em seguida, construir pequenos módulos que são testados em unidade com entrada aleatória.Uma linguagem como Eiffel pode ajudar, mas não existe solução mágica.
Qualquer produto de software pode passar no processo de certificação DO-178b usando qualquer ferramenta, mas a questão é quão difícil seria.Se o compilador não for certificado, talvez seja necessário demonstrar que seu código é rastreável no nível do assembly.Portanto, é útil que seu compilador seja certificado.Usamos C em nossos projetos, mas tivemos que verificar no nível do assembly e usar um padrão de código que incluía desligar o otimizador, uso limitado de pilha, uso limitado de interrupções, bibliotecas transparentes certificáveis, etc.ADA não é pó mágico, mas faz com que o plano PSAC pareça mais viável.
À medida que os aplicativos ficam maiores, o código assembly se torna uma escolha menos viável.O processador ARM apenas convida C++, mas se você perguntar a empresas como Kiel que sua ferramenta é certificada, eles retornarão com um "hein?" E não se esqueça que as ferramentas de verificação também precisam ser certificadas.Tente verificar um programa de teste LabView.
Um novo padrão crítico de segurança para Java está atualmente em desenvolvimento - JSR 302:Tecnologia Java crítica para segurança.
O Java crítico para segurança (SCJ) é baseado em um subconjunto de RTSJ.O objetivo é ter uma estrutura adequada para o desenvolvimento e análise de programas críticos de segurança para certificação crítica de segurança (DO-178B, Nível A e outras normas críticas de segurança).
SCJ, por exemplo, remove o heap, que ainda está presente no RTSJ, também define 3 níveis de conformidade aos quais tanto a aplicação quanto a implementação de VM podem estar em conformidade, os níveis de conformidade são definidos para facilitar a certificação de aplicações de diversas complexidades.
Recursos:
Não sei que idioma usaria, mas sei que idioma não usaria:
NOTA SOBRE SUPORTE JAVA.O PRODUTO DE SOFTWARE PODE CONTER SUPORTE PARA PROGRAMAS ESCRITOS EM JAVA.A TECNOLOGIA JAVA NÃO É TOLERANTE A FALHAS E NÃO É PROJETADA, FABRICADA OU DESTINADA A USO OU REVENDA COMO EQUIPAMENTO DE CONTROLE ON-LINE EM AMBIENTES PERIGOSOS QUE EXIGEM DESEMPENHO À PROVA DE FALHA, COMO NA OPERAÇÃO DE INSTALAÇÕES NUCLEARES, NAVEGAÇÃO DE AERONAVES OU SISTEMAS DE COMUNICAÇÃO, AÉREA CONTROLE DE TRÁFEGO, MÁQUINAS DE SUPORTE DIRETO À VIDA OU SISTEMAS DE ARMAS, NOS QUAIS A FALHA DA TECNOLOGIA JAVA PODE LEVAR DIRETAMENTE À MORTE, LESÕES PESSOAIS OU GRAVES DANOS FÍSICOS OU AMBIENTAIS.
HAL/S é usado para o ônibus espacial.
