Deductive verification of cryptographic software

• Tipo: Artigo em Revista Científica Internacional
• Data: 2010

Autores

Almeida, JB (Autor) Outra; Barbosa, M (Autor) Outra; Pinto, JS (Autor) Outra; Vieira, B (Autor) Outra

Revista

Título: Innovations in Systems and Software Engineering

Vol. 6

Páginas: 203-218

ISSN: 1614-5046

Editora: Springer Nature

Indexação

Scopus - 4 Citações

Outras Informações

ID Authenticus: P-007-VE8

DOI: 10.1007/s11334-010-0127-y

Abstract (EN): We apply state-of-the art deductive verification tools to check security-relevant properties of cryptographic software, including safety, absence of error propagation, and correctness with respect to reference implementations. We also develop techniques to help us in our task, focusing on methods oriented towards increased levels of automation, in scenarios where there are clear obvious limits to such automation. These techniques allow us to integrate automatic proof tools with an interactive proof assistant, where the latter is used off-line to prove once-and-for-all fundamental lemmas about properties of programs. The techniques developed have independent interest for practical deductive verification in general. © 2010 Springer-Verlag London Limited.

Idioma: Inglês

Tipo (Avaliação Docente): Científica