Validating common criteria documentation using Alloy

Abstract

Cryptographic software is typically associated with critical components of systems that require additional efforts in order to improve their level of assurance. Therefore, the certification of cryptographic software is necessary to ensure that it meets the desired guarantees. This certification must follow standards such as Common Criteria (CC) to ensure that the evaluation was conducted in a rigorous way. CC is an internationally recognized standard that allows for security software certification with the focus on producing evidence of the software development. This evidence usually takes the form of a series of documents that can cost the organizations that intend to achieve software certifications time and money. This master thesis focuses on the analysis of the whole CC process of certification. Specifically, all the documentation produced as evidence for the evaluation. Research is conducted to understand the process of certification, the documentation produced, the Protection Profile and the Security Target, both of which deserved special attention, and lastly techniques that could improve the development of documentation and its validation. Typically, formal methods are enforced in certification procedures in order to obtain strong correctness guarantees for the highest levels of assurance. In the presented work we show that formal methods can also be used to increase the rigor of the certification process at the documentation analysis level. We use the Alloy specification language to model the fundamental concepts of a security certification according to the CC, and then show how these models can be used to validate the consistency of Protection Profile and Security Target documentation. During this work we have been involved in a cryptographic certification process in a software package for digital certification, project CESeCore2. We look at the documentation for CESeCore to develop our models and to validate said documentation. For this project we have also written a document that describes all the process of the CESeCore certification. Finally, we have developed a prototype of what could be a tool to aid in the creation of an ion document for the CC certification. This prototype uses the Alloy models as bases and allows us to load documents produced for CESeCore certification, modify these documents, analyze them and validate the models. This could be an interesting tool for the industry involved in CC certifications.

O software criptográfico é frequentemente associado a componentes críticos de sistemas que requerem esforços adicionais para melhorar o seu nível de segurança. A certificação de software criptográfico é necessária para garantir que este vai de encontro às garantias de segurança desejadas. Esta certificação tem que seguir standards tais como Common Criteria (CC) para assegurar que a avaliação foi feita de uma forma rigorosa. CC é um standard internacionalmente reconhecido que permite a certificação de software de segurança com relevo para a produção de provas do correcto desenvolvimento do software. Estas provas geralmente tomam a forma de uma série de documentos que podem custar tempo e dinheiro às organizações que pretendem conseguir certificações de software. Esta tese de mestrado trata da análise de todo o processo de certificação CC. Em específico, trata da documentação produzida como prova para uma avaliação. Pesquisa foi efectuada para compreender o processo de certificação, a documentação produzida, o Protection Profile e o Security Target, que mereceram especial atenção e, por último, técnicas que possam melhorar o desenvolvimento de documentação e a sua validação. Geralmente os métodos formais são utilizados em procedimentos de certificação para obter fortes garantias de correcção para os níveis de segurança mais elevados. No trabalho aqui apresentado mostramos que os métodos formais também podem ser usados para aumentar o rigor do processo de certificação ao nível da análise documental. Usamos a linguagem de especificação Alloy para modelar os conceitos fundamentais de uma certificação de segurança de acordo com CC, e subsequentemente para mostrar como estes modelos podem ser usados para validar a consistência da documentação do Protection Profile e do Security Target. Durante este trabalho estivemos envolvidos no projecto de certificação de um core criptográfico num pacote de software para certificação digital, o projecto CESeCore1. Olhamos para a documentação do CESeCore para desenvolver os nossos modelos e para validar a dita documentação. Para este projecto escrevemos ainda um documento que descreve todo o processo de certificação do CESeCore. Finalmente, desenvolvemos um protótipo daquilo que pode vir a ser uma ferramenta para ajudar na criação de documentos para a certificação CC. Este protótipo usa os modelos Alloy como bases e permite-nos carregar documentos produzidos pela certificação CC, modificá-los, analisá-los e validá-los. Esta pode vir a ser uma ferramenta interessante para a indústria envolvida em certificação CC.