Výsledky vyhledávání - "José B. Almeida"

Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages

Autor: Marcus Vinícius Midena Ramos, Ruy J. G. B. de Queiroz, José B. Almeida, Nelma Moreira

Publikováno v: LSFA
Repositório Científico de Acesso Aberto de Portugal
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP

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

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6c32fafd787cd6ffd810c5e3e1a52923
https://doi.org/10.1016/j.entcs.2019.07.010

Zobrazit plný text záznamu

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification

Autor: Tiago Oliveira, José B. Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte

Publikováno v: International Conference on Cryptology in India
International Conference on Cryptology in India, Dec 2020, Bangalore, India
Progress in Cryptology – INDOCRYPT 2020 ISBN: 9783030652760
INDOCRYPT
Indocrypt 2020
Indocrypt 2020, Dec 2020, Bangalore, India

We 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

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b5e9c13a88e31c7ec8bc720a4f72fd1e
https://hal.univ-lorraine.fr/hal-02983256

Zobrazit plný text záznamu

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations

Autor: Tiago Oliveira, Adrien Koutsos, José B. Almeida, Pierre-Yves Strub, Vincent Laporte, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire

Publikováno v: SP 2020-41st IEEE Symposium on Security and Privacy
SP 2020-41st IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.965-982, ⟨10.1109/SP40000.2020.00028⟩
IEEE Symposium on Security and Privacy

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 handwritten assembly. We illu

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b6f1cc4c35cb2796677a765c91ed1177
https://hal.univ-lorraine.fr/hal-02974993

Zobrazit plný text záznamu

A formal treatment of the role of verified compilers in secure computation

Autor: Gilles Barthe, José B. Almeida, Hugo Pacheco, Vitor Pereira, Bernardo Portela, Manuel Barbosa

Publikováno v: Journal of Logical and Algebraic Methods in Programming. 125:100736

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 accessi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::ba343c485cea4ff6fc7d52e9e7b37dfd
https://doi.org/10.1016/j.jlamp.2021.100736

Zobrazit plný text záznamu

Teaching how to program using automated assessment and functional glossy games (experience report)

Autor: Nuno Macedo, Hugo Pacheco, José B. Almeida, José Proença, Alcino Cunha

Publikováno v: Proceedings of the ACM on Programming Languages. 2:1-17

Our department has long been an advocate of the functional-first school of programming and has been teaching Haskell as a first language in introductory programming course units for 20 years. Although the functional style is largely beneficial, it ne

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::305782dae11726a82073600949f11733
https://doi.org/10.1145/3236777

Zobrazit plný text záznamu

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3

Autor: José B. Almeida, Alley Stoughton, Benjamin Grégoire, Pierre-Yves Strub, Gilles Barthe, Manuel Barbosa, François Dupressoir, Cécile Baritel-Ruet, Vincent Laporte, Tiago Oliveira

Publikováno v: CCS 2019-26th ACM Conference on Computer and Communications Security
CCS 2019-26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.1607-1622, ⟨10.1145/3319535.3363211⟩
CCS
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
Bacelar Almeida, J, Barbosa, M, Baritel-Ruet, C, Barthe, G, Dupressoir, F, Grégoire, B, Laporte, V, Oliveira, T, Strub, P-Y & Stoughton, A 2019, Machine-Checked Proofs for Cryptographic Standards : Indifferentiability of Sponge and secure high-assurance implementations of SHA-3 . in CCS'19 : Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security . Association for Computing Machinery (ACM), pp. 1607-1622, ACM CCS 2019, London, United Kingdom, 11/11/19 . https://doi.org/10.1145/3319535.3363211

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 resistanc

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::81ad6142ce1106a8c1d25f32a2c29be8
https://hal.archives-ouvertes.fr/hal-02404581/document

Zobrazit plný text záznamu

A machine-checked proof of security for AWS key management service

Autor: Vitor Pereira, José B. Almeida, Benjamin Grégoire, Pierre-Yves Strub, Serdar Tasiran, Ernie Cohen, Manuel Barbosa, Gilles Barthe, Bernardo Portela, Matthew J. Campagna

Publikováno v: CCS
ACM CCS 2019-26th ACM Conference on Computer and Communications Security
ACM CCS 2019-26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.63-78, ⟨10.1145/3319535.3354228⟩

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;

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2118f3eb8993c52131e01c3f034a1d8a
https://hdl.handle.net/1822/66487

Zobrazit plný text záznamu

Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks

Autor: Vitor Pereira, Gilles Barthe, José B. Almeida, Bernardo Portela, Manuel Barbosa, Hugo Pacheco

Publikováno v: CSF

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 imper

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::2ed31386db007f55260263455eadf22d
https://doi.org/10.1109/csf.2018.00017

Zobrazit plný text záznamu

Jasmin

Autor: José B. Almeida, Gilles Barthe, Benedikt Schmidt, Pierre-Yves Strub, Benjamin Grégoire, Vincent Laporte, Hugo Pacheco, Tiago Oliveira, Arthur Blot, Manuel Barbosa

Publikováno v: CCS
CCS 2017-Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security
CCS 2017-Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-17

International audience; 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

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f9b7c572cf658af9f643580f055b996f
https://doi.org/10.1145/3133956.3134078

Zobrazit plný text záznamu

Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC

Autor: José B. Almeida, François Dupressoir, Manuel Barbosa, Gilles Barthe

Publikováno v: Fast Software Encryption ISBN: 9783662529928
FSE

We provide further evidence that implementing software countermeasures against timing attacks is a non-trivial task and requires domain-specific software development processes: we report an implementation bug in the s2n library, recently released by

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::20f403fb4b658fd2198dd9a709f964eb
https://doi.org/10.1007/978-3-662-52993-5_9

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání