HASLab - Indexed Articles in Journals

Permanent URI for this collection

http://localhost:4000/handle/123456789/167

Browse

Browsing HASLab - Indexed Articles in Journals by Author "5604"
  • 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
    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
    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.