HASLab

Permanent URI for this community

http://localhost:4000/handle/123456789/30
This service produces reliable software systems in contexts where correctness, responsiveness, robustness and security are essential. It develops integrated research in three lines: formal methods for software development, reliable distributed systems and information security.

Browse

Browsing HASLab by Author "5598"
  • Item
    Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification
    ( 2020) Barthe,G ; Tiago Filipe Oliveira ; Laporte,V ; José Bacelar Almeida ; Manuel Barbosa ; 5598 ; 5604 ; 6207
  • Item
    Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations
    ( 2013) Manuel Barbosa ; José Bacelar Almeida ; Barthe,G ; Dupressoir,F ; 5604 ; 5598
  • Item
    Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
    ( 2018) Hugo Pereira Pacheco ; Bernardo Luís Portela ; Vítor Parreira Pereira ; José Bacelar Almeida ; Manuel Barbosa ; Barthe,G ; 5647 ; 5604 ; 5598 ; 6374 ; 6060
    We 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 bound to) their leakage. This allows non-experts to assess the impact of performance-driven authorized disclosure of intermediate values. Specifications are then compiled to multi-party protocols. We formalize protocol security using (distributed) probabilistic information-flow and prove security-preserving compilation: Protocols only leak what is allowed by the source policy. The proof exploits a natural but previously missing correspondence between simulation-based cryptographic proofs and (composable) probabilistic non-interference. Finally, we extend our framework to justify leakage cancelling, a domain-specific optimization that allows to first write an efficient specification that fails to meet the allowed leakage upper-bound, and then apply a probabilistic pre-processing that brings leakage to the acceptable range. © 2018 IEEE.
  • Item
    A formal treatment of the role of verified compilers in secure computation
    ( 2022) José Bacelar Almeida ; Manuel Barbosa ; Barthe,G ; Hugo Pereira Pacheco ; Pereira,V ; Bernardo Luís Portela ; 6060 ; 5647 ; 5604 ; 5598
    Secure 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 formal treatment of the core steps that they perform to bridge the abstraction gap between high-level ideal specifications and efficient SMC protocols. Our abstract framework bridges this secure compilation problem across two dimensions: 1) language-based source- to target-level semantic and efficiency gaps, and 2) cryptographic ideal- to real-world security gaps. We link the former to the setting of certified compilation, paving the way to leverage long-run efforts such as CompCert in future SMC compilers. Security is framed in the standard cryptographic sense. Our results are supported by a machine-checked formalisation carried out in EasyCrypt. © 2021 Elsevier Inc.
  • Item
    Formally verifying Kyber Episode IV: Implementation correctness
    ( 2023) José Bacelar Almeida ; Hugo Pereira Pacheco ; 5598 ; 5647
    In 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 high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.
  • Item
  • Item
    Formally verifying Kyber Part I: Implementation Correctness
    ( 2023) Hugo Pereira Pacheco ; Manuel Barbosa ; José Bacelar Almeida ; 5647 ; 5604 ; 5598
  • Item
    The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
    ( 2020) Barthe,G ; Manuel Barbosa ; José Bacelar Almeida ; Strub,PY ; Tiago Filipe Oliveira ; Laporte,V ; Koutsos,A ; Grégoire,B ; 5604 ; 5598 ; 6207
    We 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 hand-written assembly. We illustrate our approach using ChaCha20-Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code.We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking.We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt. © 2020 IEEE.
  • Item
    A Machine-Checked Proof of Security for AWS Key Management Service
    ( 2019) José Bacelar Almeida ; Tasiran,S ; Strub,PY ; Portela,B ; Pereira,V ; Gregoire,B ; Cohen,E ; Campagna,M ; Barthe,G ; Manuel Barbosa ; 5604 ; 5598
    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.
  • Item
    Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3
    ( 2019) José Bacelar Almeida ; Strub,PY ; Stoughton,A ; Tiago Filipe Oliveira ; Laporte,V ; Gregoire,B ; Dupressoir,F ; Barthe,G ; Manuel Barbosa ; Baritel Ruet,C ; 6207 ; 5598 ; 5604
    We 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 security, and side-channel protection) for a non-trivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.
  • Item
    Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages
    ( 2019) José Bacelar Almeida ; Ramos,MVM ; Moreira,N ; de Queiroz,RJGB ; 5598
    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 several well-known languages are not context-free. Moreover, we build on those results to construct a formal proof of the well-known property that context-free languages are not closed under intersection. All the formalization has been mechanized in the Coq proof assistant.
  • Item
    Verified Password Generation from Password Composition Policies
    ( 2022) Grilo,M ; Campos,J ; Ferreira,JF ; José Bacelar Almeida ; Alexandra Sofia Mendes ; 5598 ; 7344