Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/4737
Full metadata record
DC FieldValueLanguage
dc.contributor.authorJosé Bacelar Almeidaen
dc.contributor.authorManuel Barbosaen
dc.contributor.authorJorge Sousa Pintoen
dc.contributor.authorVieira,Ben
dc.date.accessioned2017-12-22T10:02:25Z-
dc.date.available2017-12-22T10:02:25Z-
dc.date.issued2013en
dc.identifier.urihttp://repositorio.inesctec.pt/handle/123456789/4737-
dc.identifier.urihttp://dx.doi.org/10.1016/j.scico.2011.10.008en
dc.description.abstractFormal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper, we extend previous results supporting the practicality of self-composition proofs of non-interference and generalizations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We formalize these policies and propose a formal verification approach based on self-composition, extending the range of security policies that could previously be handled using this technique. We demonstrate our results by addressing compliance with the NaCl security policies in real-world cryptographic code, highlighting the potential for automation of our techniques.en
dc.languageengen
dc.relation5595en
dc.relation5598en
dc.relation5604en
dc.rightsinfo:eu-repo/semantics/openAccessen
dc.titleFormal verification of side-channel countermeasures using self-compositionen
dc.typearticleen
dc.typePublicationen
Appears in Collections:HASLab - Other Publications

Files in This Item:
File Description SizeFormat 
P-004-ZVC.pdf467.2 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.