Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/31023
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Almeida, José Bacelar | por |
dc.contributor.author | Barbosa, Manuel | por |
dc.contributor.author | Filliâtre, Jean-Christophe | por |
dc.contributor.author | Pinto, Jorge Sousa | por |
dc.contributor.author | Vieira, Bárbara Isabel Sousa | por |
dc.date.accessioned | 2014-11-19T16:27:40Z | - |
dc.date.available | 2014-11-19T16:27:40Z | - |
dc.date.issued | 2014 | - |
dc.identifier.citation | Almeida, J. B., Barbosa, M., Filliâtre, J. C., Pinto, J. S., & Vieira, B. (2014). CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Science of Computer Programming, 91(PART B), 216-233. | por |
dc.identifier.issn | 0167-6423 | - |
dc.identifier.uri | https://hdl.handle.net/1822/31023 | - |
dc.description.abstract | 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. | por |
dc.description.sponsorship | This work was supported by Project Best Case, co-financed by the North Portugal Regional Operational Programme (ON.2 – O Novo Norte), under the National Strategic Reference Framework (NSRF), through the European Regional Development Fund (ERDF). | por |
dc.language.iso | eng | por |
dc.publisher | Elsevier 1 | por |
dc.rights | openAccess | - |
dc.subject | Formal verification | por |
dc.subject | Program verification | por |
dc.subject | Cryptographic software | por |
dc.subject | Deductive verification | por |
dc.title | CAOVerif: an open-source deductive verification platform for cryptographic software implementations | por |
dc.type | article | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | The original publication is available at www.sciencedirect.com | por |
sdum.publicationstatus | published | por |
oaire.citationStartPage | 216 | por |
oaire.citationEndPage | 233 | por |
oaire.citationIssue | PART B | por |
oaire.citationTitle | Science of Computer Programming | por |
oaire.citationVolume | 91 | por |
dc.identifier.doi | 10.1016/j.scico.2012.09.019 | por |
dc.subject.fos | Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática | por |
dc.subject.fos | Ciências Naturais::Ciências da Computação e da Informação | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Science of Computer Programming | por |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
opencertjournal_ack.pdf | Documento Principal | 285,04 kB | Adobe PDF | Ver/Abrir |