Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/4735
Full metadata record
DC FieldValueLanguage
dc.contributor.authorJosé Bacelar Almeidaen
dc.contributor.authorManuel Barbosaen
dc.contributor.authorBarthe,Gen
dc.contributor.authorDupressoir,Fen
dc.date.accessioned2017-12-22T10:02:20Z-
dc.date.available2017-12-22T10:02:20Z-
dc.date.issued2013en
dc.identifier.urihttp://repositorio.inesctec.pt/handle/123456789/4735-
dc.identifier.urihttp://dx.doi.org/10.1145/2508859.2516652en
dc.description.abstractWe present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementations. The front-end of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of C-like programs extended with idealised probabilistic operations in the style of code-based security proofs. The framework also incorporates an extension of the CompCert certified compiler to support trusted libraries providing complex arithmetic calculations or instantiating idealized components such as sampling operations. This certified compiler allows us to carry to executable code the security guarantees established at the high-level, and is also instrumented to detect when compilation may interfere with side-channel countermeasures deployed in source code. We demonstrate the applicability of the framework by applying it to the RSA-OAEP encryption scheme, as standardized in PKCS#1 v2.1. The outcome is a rigorous analysis of the advantage of an adversary to break the security of assembly implementations of the algorithms specified by the standard. The example also provides two contributions of independent interest: it bridges the gap between computer-assisted security proofs and real-world cryptographic implementations as described by standards such as PKCS,and demonstrates the use of the CompCert certified compiler in the context of cryptographic software development. © 2013 ACM.en
dc.languageengen
dc.relation5604en
dc.relation5598en
dc.rightsinfo:eu-repo/semantics/openAccessen
dc.titleCertified computer-aided cryptography: Efficient provably secure machine code from high-level implementationsen
dc.typeconferenceObjecten
dc.typePublicationen
Appears in Collections:HASLab - Other Publications

Files in This Item:
File Description SizeFormat 
P-008-J03.pdf471.72 kBAdobe PDFView/Open


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