Go to:
Logótipo
Comuta visibilidade da coluna esquerda
Você está em: Start > Publications > View > CAOVerif: An open-source deductive verification platform for cryptographic software implementations
Publication

Publications

CAOVerif: An open-source deductive verification platform for cryptographic software implementations

Title
CAOVerif: An open-source deductive verification platform for cryptographic software implementations
Type
Article in International Scientific Journal
Year
2014
Authors
Almeida, JB
(Author)
Other
The person does not belong to the institution. The person does not belong to the institution. The person does not belong to the institution. View Authenticus page Without ORCID
Filliatre, JC
(Author)
Other
The person does not belong to the institution. The person does not belong to the institution. The person does not belong to the institution. Without AUTHENTICUS Without ORCID
Pinto, JS
(Author)
Other
The person does not belong to the institution. The person does not belong to the institution. The person does not belong to the institution. View Authenticus page Without ORCID
Vieira, B
(Author)
Other
The person does not belong to the institution. The person does not belong to the institution. The person does not belong to the institution. Without AUTHENTICUS Without ORCID
Journal
Vol. 91
Pages: 216-233
ISSN: 0167-6423
Publisher: Elsevier
Other information
Authenticus ID: P-008-Y45
Abstract (EN): CAO is a domain-specific imperative language for cryptography, offering a rich mathematical type system and crypto-oriented language constructions. We describe the design and implementation of a deductive verification platform for CAO and demonstrate that the development time of such a complex verification tool could be greatly reduced by building on the Jessie plug-in included in the Frama-C framework. We discuss the interesting challenges raised by the domain-specific characteristics of CAO, and describe how we tackle these problems in our design. We base our presentation on real-world examples of CAO code, extracted from the open-source code of the NaCl cryptographic library, and illustrate how various cryptography-relevant security properties can be verified.
Language: English
Type (Professor's evaluation): Scientific
No. of pages: 18
Documents
We could not find any documents associated to the publication.
Related Publications

Of the same journal

Typed connector families and their semantics (2017)
Article in International Scientific Journal
Proença, J; Clarke, D
The CAOS framework for Scala: Computer-aided design of SOS (2025)
Article in International Scientific Journal
Proença, J; Edixhoven, L
Ranking programming languages by energy efficiency (2021)
Article in International Scientific Journal
Rui Pereira; Marco Couto; Francisco Ribeiro; Rui Rua; Jácome Cunha; João Paulo Fernandes; João Saraiva
Multiple intermediate structure deforestation by shortcut fusion (2016)
Article in International Scientific Journal
Pardo, A; Joao Paulo Fernandes; Saraiva, J

See all (16)

Recommend this page Top
Copyright 1996-2025 © Faculdade de Direito da Universidade do Porto  I Terms and Conditions  I Acessibility  I Index A-Z
Page created on: 2025-07-26 at 09:10:30 | Privacy Policy | Personal Data Protection Policy | Whistleblowing