Encontrados 32 documentos, a visualizar página 1 de 4
Formally verifying Kyber. Episode IV: implementation correctness
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Grégoire, Benjamin; Laporte, Vincent; Léchenet, Jean-Christophe; Oliveira, Tiago; Pacheco, HugoIn this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present hi...
A formal treatment of the role of verified compilers in secure computation
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Pacheco, Hugo; Pereira, Vitor; Portela, BernardoSecure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed.We review the role of these compilers and provide a...
Verified password generation from password composition policies
Grilo, Miguel; Campos, João; Ferreira, João F.; Almeida, José Bacelar; Mendes, AlexandraPassword managers (PMs) are important tools that enable the use of stronger passwords, freeing users from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust PMs. In this paper, we focus on a feature that most PMs offer that might impact the user’s trust, which is the process of generating a random password. We present three of the most commonly used algorit...
Machine-checked ZKP for NP relations: formally verified security proofs and imp...
Almeida, José Bacelar; Barbosa, Manuel; Correia, Manuel L.; Eldefrawy, Karim; Graham-Lengrand, Stéphane; Pacheco, Hugo; Pereira, VitorMPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protoco...
Certified compilation for cryptography: Extended x86 instructions and constant-...
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Laporte, Vincent; Oliveira, TiagoWe present a new tool for the generation and verification of high-assurance high-speed machine-level cryptography implementations: a certified C compiler supporting instruction extensions to the x86. We demonstrate the practical applicability of our tool by incorporating it into supercop: a toolkit for measuring the performance of cryptographic software, which includes over 2000 different implementations. We sh...
The last mile: High-Assurance and High-Speed cryptographic implementations
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Gregoire, Benjamin; Koutsos, Adrien; Laporte, Vincent; Oliveira, Tiago; Strub, Pierre-YvesWe develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as handwritten assembly. We illustrate our approach using ChaCha20Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outpe...
Some applications of the formalization of the pumping lemma for context-free la...
Ramos, Marcus V. M.; Almeida, José Bacelar; Moreira, Nelma; de Queiroz, Ruy J. G. B.Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma for Context-Free Languages states a property that is valid for all context-free languages, which makes it a tool for showing the existence of non-context-free languages. This paper presents a formalization, extending the previously formalized Lemma, of the fact that seve...
A machine-checked proof of security for AWS key management service
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Campagna, Matthew; Cohen, Ernie; Gregoire, Benjamin; Pereira, Vitor; Portela, BernardoWe 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 ...
Machine-checked proofs for cryptographic standards indifferentiability of SPONG...
Almeida, José Bacelar; Baritel-Ruet, Cecile; Barbosa, Manuel; Barthe, Gilles; Dupressoir, Francois; Gregoire, Benjamin; Laporte, VincentWe present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable secur...
hnforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Pacheco, Hugo; Pereira, Vitor; Portela, BernardoWe give a language-based security treatment of domain-specific languages and compilers for secure multi-party computation, a cryptographic paradigm that. enables collaborative computation over encrypted data. Computations are specified in a core imperative language, as if they were intended to be executed by a trusted-third party, and formally verified against. an information-flow policy modelling (an upper bou...