Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/50511
Título: | Verifying constant-time implementations |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Barthe, Gilles Jacques Denis Dupressoir, François Emmi, Michael |
Palavras-chave: | implementation security constant-time policy |
Data: | 10-Ago-2016 |
Editora: | Advanced Computing Systems Association (USENIX) |
Resumo(s): | The constant-time programming discipline is an effective countermeasure against timing attacks, which can lead to complete breaks of otherwise secure systems. However, adhering to constant-time programming is hard on its own, and extremely hard under additional efficiency and legacy constraints. This makes automated verification of constant-time code an essential component for building secure software. We propose a novel approach for verifying constant- time security of real-world code. Our approach is able to validate implementations that locally and intentionally violate the constant-time policy, when such violations are benign and leak no more information than the pub- lic outputs of the computation. Such implementations, which are used in cryptographic libraries to obtain impor- tant speedups or to comply with legacy APIs, would be declared insecure by all prior solutions. We implement our approach in a publicly available, cross-platform, and fully automated prototype, ct-verif, that leverages the SMACK and Boogie tools and verifies optimized LLVM implementations. We present verifica- tion results obtained over a wide range of constant-time components from the NaCl, OpenSSL, FourQ and other off-the-shelf libraries. The diversity and scale of our ex- amples, as well as the fact that we deal with top-level APIs rather than being limited to low-level leaf functions, distinguishes ct-verif from prior tools. Our approach is based on a simple reduction of constant-time security of a program P to safety of a prod- uct program Q that simulates two executions of P. We formalize and verify the reduction for a core high-level language using the Coq proof assistant. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/50511 |
ISBN: | ISBN 978-1-931971-32-4 |
Versão da editora: | The original publication is available at https://www.usenix.org/system/files/conference/usenixsecurity16/sec16_paper_almeida.pdf |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
16Usenix.pdf | 1,3 MB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons