Trecho de BACK TO THE BUILDING BLOCKS: A PATH TOWARD SECURE AND MEASURABLE SOFTWARE - FEBRUARY 2024
Mesmo que os engenheiros construam usando linguagens de programação e chips seguros para a memória, é necessário considerar as vulnerabilidades que persistirão mesmo depois de os fabricantes de tecnologia tomarem medidas para eliminar as classes mais prevalentes. Dada a complexidade do código, o teste é uma etapa necessária, mas insuficiente no processo de desenvolvimento para reduzir completamente as vulnerabilidades em grande escala. Se a correção é definida como a capacidade de um software atender a um requisito específico de segurança, então é possível demonstrar a correção usando técnicas matemáticas chamadas métodos formais. Essas técnicas, frequentemente usadas para comprovar uma variedade de resultados de software, também podem ser aplicadas em um contexto de cibersegurança e são viáveis mesmo em ambientes complexos como o espaço. Embora os métodos formais sejam estudados há décadas, sua implementação ainda é limitada; inovações adicionais em abordagens para tornar os métodos formais amplamente acessíveis são vitais para acelerar a adoção generalizada. Fazer isso permite que os métodos formais atuem como mais uma ferramenta poderosa para dar aos desenvolvedores de software uma maior garantia de que classes inteiras de vulnerabilidades, mesmo além de falhas de segurança na memória, estão ausentes.
Embora existam vários tipos de métodos formais que abrangem uma variedade de técnicas e estágios no processo de desenvolvimento de software, este relatório destaca alguns exemplos específicos. A análise estática eficaz examina o software em busca de propriedades específicas sem executar o código. Este método é eficaz porque pode ser utilizado em várias representações de software, incluindo o código-fonte, arquitetura, requisitos e executáveis. Os verificadores de modelo podem responder a perguntas sobre várias propriedades de nível superior. Esses algoritmos podem ser usados durante a produção; no entanto, eles são limitados em seu uso em grande escala devido à sua complexidade computacional. O teste baseado em assertivas é uma declaração formal de propriedades incorporadas no código que podem ser usadas para verificar o código durante o teste ou produção. Essas provas geradas permitem a detecção de falhas muito mais cedo e mais próximo do código errôneo, em vez de rastrear a partir de falhas visíveis externamente nos sistemas.
Existem duas maneiras pelas quais os engenheiros de software podem usar essas técnicas em software e hardware. Primeiro, os métodos formais podem ser incorporados diretamente na cadeia de ferramentas do desenvolvedor. À medida que o programador constrói, testa e implanta o software, o compilador pode automatizar essas provas matemáticas e verificar se uma condição de segurança é atendida. Além disso, o desenvolvedor pode usar componentes centrais formalmente verificados em sua cadeia de fornecimento de software. Ao escolher bibliotecas de software comprovadamente seguras, os desenvolvedores podem garantir que os componentes que estão usando têm menos probabilidade de conter vulnerabilidades.
Os métodos formais podem ser incorporados ao longo do processo de desenvolvimento para reduzir a prevalência de várias categorias de vulnerabilidades. Algumas tecnologias emergentes também são adequadas para essa técnica. À medida que surgem perguntas sobre a segurança ou confiabilidade de um novo produto de software, os métodos formais podem acelerar a adoção no mercado de maneiras que os métodos tradicionais de teste de software não conseguem. Eles permitem comprovar a presença de um requisito afirmativo, em vez de testar a ausência de uma condição negativa.
Embora hardware seguro para a memória e métodos formais possam ser abordagens complementares excelentes para mitigar vulnerabilidades não descobertas, uma das ações mais impactantes que os fabricantes de software e hardware podem tomar é adotar linguagens de programação seguras para a memória. Elas oferecem uma maneira de eliminar, não apenas mitigar, classes inteiras de bugs. Esta é uma oportunidade notável para a comunidade técnica melhorar a cibersegurança de todo o ecossistema digital.
Formal Methods Even if engineers build with memory safe programming languages and memory safe chips, one must think about the vulnerabilities that will persist even after technology manufacturers take steps to eliminate the most prevalent classes. Given the complexities of code, testing is a necessary but insufficient step in the development process to fully reduce vulnerabilities at scale. If correctness is defined as the ability of a piece of software to meet a specific security requirement, then it is possible to demonstrate correctness using mathematical techniques called formal methods. These techniques, often used to prove a range of software outcomes, can also be used in a cybersecurity context and are viable even in complex environments like space. While formal methods have been studied for decades, their deployment remains limited; further innovation in approaches to make formal methods widely accessible is vital to accelerate broad adoption. Doing so enables formal methods to serve as another powerful tool to give software developers greater assurance that entire classes of vulnerabilities, even beyond memory safety bugs, are absent. While there are several types of formal methods that span a range of techniques and stages in the software development process, this report highlights a few specific examples. Sound static analysis examines the software for specific properties without executing the code.xxi This method is effective because it can be used across many representations of software, including the source code, architecture, requirements, and executables. Model checkers can answer questions about a number of higher-level properties.xxii These algorithms can be used during production; however, they are limited in their scaled use due to their computational complexity. Assertion-based testing is a formal statement of properties carried in the code that may be used to cross-check the code during testing or production.xxiii These generated proofs allow for faults to be detected much earlier and closer to the erroneous code, rather than tracing back from externally visible systems failures. There are two ways software engineers can use these techniques across software and hardware. First, formal methods can be incorporated directly into the developer toolchain. As the programmer builds, tests, and deploys software, the compiler can automate these mathematical proofs and verify that a security condition is met.xxiv Additionally, the developer can use formally verified core components in their software supply chain.xxv By choosing provably secure software libraries, developers can ensure the components they are using are less likely to contain vulnerabilities. Formal methods can be incorporated throughout the development process to reduce the prevalence of multiple categories of vulnerabilities. Some emerging technologies are also well-suited to this technique.xxvi As questions arise about the safety or trustworthiness of a new software product, formal methods can accelerate market adoption in ways that traditional software testing methods cannot. They allow for proving the presence of an affirmative requirement, rather than testing for the absence of a negative condition.xxvii While memory safe hardware and formal methods can be excellent complementary approaches to mitigating undiscovered vulnerabilities, one of the most impactful actions software and hardware manufacturers can take is adopting memory safe programming languages. They offer a way to eliminate, not just mitigate, entire bug classes. This is a remarkable opportunity for the technical community to improve the cybersecurity of the entire digital ecosystem.
Link https://chat.openai.com/share/6bfd820c-d54a-453d-a6e6-a34d50ba740f