Biblio

Filters: Author is Almeida, José Bacelar  [Clear All Filters]
2020-01-27
Almeida, José Bacelar, Barbosa, Manuel, Barthe, Gilles, Campagna, Matthew, Cohen, Ernie, Grégoire, Benjamin, Pereira, Vitor, Portela, Bernardo, Strub, Pierre-Yves, Tasiran, Serdar.  2019.  A Machine-Checked Proof of Security for AWS Key Management Service. Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. :63–78.

We present a machine-checked proof of security for the domain management protocol of Amazon Web Services' KMS (Key Management Service) a critical security service used throughout AWS and by AWS customers. Domain management is at the core of AWS KMS; it governs the top-level keys that anchor the security of encryption services at AWS. We show that the protocol securely implements an ideal distributed encryption mechanism under standard cryptographic assumptions. The proof is machine-checked in the EasyCrypt proof assistant and is the largest EasyCrypt development to date.

2018-01-10
Almeida, José Bacelar, Barbosa, Manuel, Barthe, Gilles, Dupressoir, François, Grégoire, Benjamin, Laporte, Vincent, Pereira, Vitor.  2017.  A Fast and Verified Software Stack for Secure Function Evaluation. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. :1989–2006.
We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.
Almeida, José Bacelar, Barbosa, Manuel, Barthe, Gilles, Blot, Arthur, Grégoire, Benjamin, Laporte, Vincent, Oliveira, Tiago, Pacheco, Hugo, Schmidt, Benedikt, Strub, Pierre-Yves.  2017.  Jasmin: High-Assurance and High-Speed Cryptography. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. :1807–1823.
Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. Using the supercop framework, we evaluate the Jasmin compiler on representative cryptographic routines and conclude that the code generated by the compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework includes highly automated tools for proving memory safety and constant-time security (for protecting against cache-based timing attacks). We also demonstrate the effectiveness of the verification tools on a large set of cryptographic routines.