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 "5604"
  • Item
  • Item
  • 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
    CODBS: A cascading oblivious search protocol optimized for real-world relational database indexes
    ( 2021) Rogério António Pontes ; Bernardo Luís Portela ; Manuel Barbosa ; Ricardo Pereira Vilaça ; 5604 ; 5635 ; 6246 ; 6060
  • Item
    Decentralized Privacy-Preserving Proximity Tracing
    ( 2020) Binns,R ; Barrat,A ; Fiore,D ; Manuel Barbosa ; Rui Carlos Oliveira ; José Orlando Pereira ; Basin,DA ; Beutel,J ; Jackson,D ; Roeschlin,M ; Leu,P ; Preneel,B ; Smart,NP ; Abidin,A ; Gürses,SF ; Veale,M ; Cremers,C ; Backes,M ; Tippenhauer,NO ; Cattuto,C ; Troncoso,C ; Payer,M ; Hubaux,JP ; Salathé,M ; Larus,JR ; Bugnion,E ; Lueks,W ; Stadler,T ; Pyrgelis,A ; Antonioli,D ; Barman,L ; Chatel,S ; Paterson,KG ; Capkun,S ; 5602 ; 5604 ; 5594
  • Item
    Efficient Function-Hiding Functional Encryption: From Inner-Products to Orthogonality
    ( 2019) Manuel Barbosa ; Catalano,D ; Soleimanian,A ; Warinschi,B ; 5604
    We construct functional encryption (FE) schemes for the orthogonality (OFE) relation where each ciphertext encrypts some vector (Formula Presented) and each decryption key, associated to some vector (Formula Presented), allows to determine if (Formula Presented) is orthogonal to (Formula Presented) or not. Motivated by compelling applications, we aim at schemes which are function hidding, i.e. (Formula Presented) is not leaked. Our main contribution are two such schemes, both rooted in existing constructions of FE for inner products (IPFE), i.e., where decryption keys reveal the inner product of (Formula Presented) and (Formula Presented). The first construction builds upon the very efficient IPFE by Kim et al. (SCN 2018) but just like the original scheme its security holds in the generic group model (GGM). The second scheme builds on recent developments in the construction of efficient IPFE schemes in the standard model and extends the work of Wee (TCC 2017) in leveraging these results for the construction of FE for Boolean functions. Conceptually, both our constructions can be seen as further evidence that shutting down leakage from inner product values to only a single bit for the orthogonality relation can be done with little overhead, not only in the GGM, but also in the standard model. We discuss potential applications of our constructions to secure databases and provide efficiency benchmarks. Our implementation shows that the first scheme is extremely fast and ready to be deployed in practical applications. © 2019, Springer Nature Switzerland AG.
  • 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
    Execution Time Program Verification with Tight Bounds
    ( 2023) Manuel Barbosa ; 5604
    This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time reasoning, and less pessimistic execution time estimation using amortized analysis. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. Finally, we define a verification conditions (VC) generator that generates the goals needed to prove program correctness, cost, and termination. Those goals are then sent to the Easycrypt toolset for validation. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs. Our case studies are motivated by real-time and cryptographic software. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
  • Item
  • 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 Part I: Implementation Correctness
    ( 2023) Hugo Pereira Pacheco ; Manuel Barbosa ; José Bacelar Almeida ; 5647 ; 5604 ; 5598
  • Item
    Kyber terminates
    ( 2023) Manuel Barbosa ; 5604
  • Item
    Labeled Homomorphic Encryption - Scalable and Privacy-Preserving Processing of Outsourced Data
    ( 2017) Manuel Barbosa ; Fiore,D ; Catalano,D ; 5604
    In privacy-preserving processing of outsourced data a Cloud server stores data provided by one or multiple data providers and then is asked to compute several functions over it. We propose an efficient methodology that solves this problem with the guarantee that a honest-but-curious Cloud learns no information about the data and the receiver learns nothing more than the results. Our main contribution is the proposal and efficient instantiation of a new cryptographic primitive called Labeled Homomorphic Encryption (labHE). The fundamental insight underlying this new primitive is that homomorphic computation can be significantly accelerated whenever the program that is being computed over the encrypted data is known to the decrypter and is not secret—previous approaches to homomorphic encryption do not allow for such a trade-off. Our realization and implementation of labHE targets computations that can be described by degree-two multivariate polynomials. As an application, we consider privacy preserving Genetic Association Studies (GAS), which require computing risk estimates from features in the human genome. Our approach allows performing GAS efficiently, non interactively and without compromising neither the privacy of patients nor potential intellectual property of test laboratories. © 2017, Springer International Publishing AG.
  • 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
  • Item
    Secure Multiparty Computation from SGX
    ( 2017) Manuel Barbosa ; Sadeghi,A ; Bernardo Luís Portela ; Brasser,F ; Bahmani,R ; Warinschi,B ; Scerri,G ; 6060 ; 5604
  • Item
    The security of Kyber's FO-transform
    ( 2023) Manuel Barbosa ; 5604