Deductive verification of cryptographic software

• Type: Article in International Scientific Journal
• Date: 2010

Authors

Almeida, JB (Author) Other; Barbosa, M (Author) Other; Pinto, JS (Author) Other; Vieira, B (Author) Other

Journal

Title: Innovations in Systems and Software Engineering

Vol. 6

Pages: 203-218

ISSN: 1614-5046

Publisher: Springer Nature

Indexing

Scopus - 4 Citations

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific