Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by José Bacelar Almeida

2013

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F;

Publication
IACR Cryptology ePrint Archive

Abstract

2017

A Fast and Verified Software Stack for Secure Function Evaluation

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; Pereira, V;

Publication
CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY

Abstract
We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i.a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.

2014

Verified Implementations for Secure and Verifiable Computation

Authors
Almeida, JB; Barbosa, M; Barthe, G; Davy, G; Dupressoir, F; Grégoire, B; Strub, PY;

Publication
IACR Cryptology ePrint Archive

Abstract

2016

Verifying Constant-Time Implementations

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Emmi, M;

Publication
PROCEEDINGS OF THE 25TH USENIX SECURITY SYMPOSIUM

Abstract
The constant-time programming discipline is an effective countermeasure against timing attacks, which can lead to complete breaks of otherwise secure systems. However, adhering to constant-time programming is hard on its own, and extremely hard under additional efficiency and legacy constraints. This makes automated verification of constant-time code an essential component for building secure software. We propose a novel approach for verifying constant-time security of real-world code. Our approach is able to validate implementations that locally and intentionally violate the constant-time policy, when such violations are benign and leak no more information than the public outputs of the computation. Such implementations, which are used in cryptographic libraries to obtain important speedups or to comply with legacy APIs, would be declared insecure by all prior solutions. We implement our approach in a publicly available, cross-platform, and fully automated prototype, ct-verif, that leverages the SMACK and Boogie tools and verifies optimized LLVM implementations. We present verification results obtained over a wide range of constant-time components from the NaCl, OpenSSL, FourQ and other off-the-shelf libraries. The diversity and scale of our examples, as well as the fact that we deal with top-level APIs rather than being limited to low-level leaf functions, distinguishes ct-verif from prior tools. Our approach is based on a simple reduction of constant-time security of a program P to safety of a product program Q that simulates two executions of P. We formalize and verify the reduction for a core high-level language using the Coq proof assistant.

2013

Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F;

Publication
Proceedings of the ACM Conference on Computer and Communications Security

Abstract
We present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementations. The front-end of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of C-like programs extended with idealised probabilistic operations in the style of code-based security proofs. The framework also incorporates an extension of the CompCert certified compiler to support trusted libraries providing complex arithmetic calculations or instantiating idealized components such as sampling operations. This certified compiler allows us to carry to executable code the security guarantees established at the high-level, and is also instrumented to detect when compilation may interfere with side-channel countermeasures deployed in source code. We demonstrate the applicability of the framework by applying it to the RSA-OAEP encryption scheme, as standardized in PKCS#1 v2.1. The outcome is a rigorous analysis of the advantage of an adversary to break the security of assembly implementations of the algorithms specified by the standard. The example also provides two contributions of independent interest: it bridges the gap between computer-assisted security proofs and real-world cryptographic implementations as described by standards such as PKCS,and demonstrates the use of the CompCert certified compiler in the context of cryptographic software development. © 2013 ACM.

2015

Formalization of context-free language theory

Authors
Ramos, MarcusV.M.; Queiroz, RuyJ.G.B.de; Moreira, Nelma; Almeida, JoseCarlosBacelar;

Publication
CoRR

Abstract

  • 2
  • 8