Publications

Farsi M, Barbosa MB.  2000.  CANopen Implementation: Application to Industrial Networks. Computers and Communications Series. AbstractWebsite

Fieldbus technology has long been recognised as the future in industrial control applications. This book is intended for those wishing to embark on implementing CANopen protocols in their products, system integrators and for those planning to do pre-conformance testing of their products before pursuing a certification authority.This book describes the application of CAN, the CANopen protocol and communication technology at the shop floor level.

Barbosa MB, Castro D, Silva P.  2014.  Compiling CAO: From Cryptographic Specifications to C Implementations. Principles of Security and Trust. 8414:240-244. Abstractpost14.pdf

We present a compiler for CAO, an imperative DSL for the cryptographic domain. The tool takes high-level cryptographic algorithm specifications and translates them into C implementations through a series of security-aware transformations and optimizations.
The compiler back-end is highly configurable, allowing the targeting of very disparate platforms in terms of memory requirements and computing power.

Backes M, Barbosa MB, Fiore D, Reischuk RM.  2015.  ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data. 2015 IEEE Symposium on Security and Privacy, {SP} 2015, San Jose, CA, USA, May 17-21, 2015. :271–286. Abstractadsnark.pdf

We study the problem of privacy-preserving proofs on authenticated data, where a party receives data from a trusted source and is requested to prove computations over the data to third parties in a correct and private way, i.e., the third party learns no information on the data but is still assured that the claimed proof is valid. Our work particularly focuses on the challenging requirement that the third party should be able to verify the validity with respect to the specific data authenticated by the source — even without having access to that source. This problem is motivated by various scenarios emerging from several application areas such as wearable computing, smart metering, or general business-to-business interactions. Furthermore, these applications also demand any meaningful solution to satisfy additional properties related to usability and scalability. In this paper, we formalize the above three-party model, discuss concrete application scenarios, and then we design, build, and evaluate ADSNARK, a nearly practical system for proving arbitrary computations over authenticated data in a privacy-preserving manner. ADSNARK improves significantly over state-of-the-art solutions for this model. For instance, compared to corresponding solutions based on Pinocchio (Oakland’13), ADSNARK achieves up to 25× improvement in proof computation time and a 20× reduction in prover storage space.

Barbosa MB, Farshim P.  2014.  The Related- Key Analysis of Feistel Constructions. IACR Cryptology ePrint Archive. 93 Abstractlubyr_crc-ack.pdf

It is well known that the classical three- and four-round Feistel constructions are provably secure under chosen-plaintext and chosen-ciphertext attacks, respectively. However, irrespective of the
number of rounds, no Feistel construction can resist related-key attacks where the keys can be offset by a constant. In this paper we show that, under suitable reuse of round keys, security under related-key attacks can be provably attained. Our modification is substantially simpler and more efficient than alternatives obtained using generic transforms, namely the PRG transform of Bellare and Cash (CRYPTO 2010) and its random-oracle analogue outlined by Lucks (FSE 2004). Additionally we formalize Luck’s transform and show that it does not always work if related keys are derived in an oracle-dependent way, and then prove it sound under appropriate restrictions.

Barbosa MB, Farshim P.  2013.  On the Semantic Security of Functional Encryption Schemes. The 16th International Conference on Practice and Theory in Public Key Cryptography - PKC. :143-161. Abstract474.pdf

Functional encryption (FE) is a powerful cryptographic primitive that generalizes many asymmetric encryption systems proposed in recent years. Syntax and security definitions for FE were proposed by Boneh, Sahai, and Waters (BSW) (TCC 2011) and independently by O’Neill (ePrint 2010/556). In this paper we revisit these definitions, identify several shortcomings in them, and propose a new definitional approach that overcomes these limitations. Our definitions display good compositionality properties and allow us to obtain new feasibility and impossibility results for adaptive token-extraction attack scenarios that shed further light on the potential reach of general FE for practical applications.

Almeida JB, Barbosa MB, Barthe G, Dupressoir F.  2013.  Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. ACM Conference on Computer and Communications Security. :1217-1230. Abstract316.pdf

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 standard- ized in PKCS#1 v2.1. The outcome is a rigorous analysis of the advantage of an adversary to break the security of as- sembly 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.

Alwen J, Barbosa MB, Farshim P, Gennaro R, Gordon D, Tessaro S, Wilson D.  2013.  On the Relationship between Functional Encryption, Obfuscation, and Fully Homomorphic Encryption. 8th International Conference on Instrumental Methods of Analysis-Modern Trends and Applications - IMA. :65-84. Abstractrfe_cir.pdf

We investigate the relationship between Functional Encryption (FE) and Fully Homomorphic Encryption (FHE), demonstrating that, under certain assumptions, a Functional Encryption scheme supporting evaluation on two ciphertexts implies Fully Homomorphic Encryption. We first introduce the notion of Randomized Functional Encryption (RFE), a generalization of Functional Encryption dealing with randomized functionalities of interest in its own right, and show how to construct an RFE from a (standard) semantically secure FE. For this we define the notion of entropically secure FE and use it as an intermediary step in the construction. Finally we show that RFEs constructed in this way can be used to construct FHE schemes thereby establishing a relation between the FHE and FE primitives. We conclude the paper by recasting the construction of RFE schemes in the context of obfuscation.

Barbosa MB, Farshim P.  2012.  Delegatable Homomorphic Encryption with Applications to Secure Outsourcing of Computation. The Cryptographers' Track at the RSA Conference on Topics in Cryptology - CT-RSA. 7178 Abstract2152.pdf

In this work we propose a new cryptographic primitive called Delegatable Homomorphic Encryption (DHE). This allows a Trusted Authority to control/delegate the capability to evaluate circuits over encrypted data to untrusted workers/evaluators by issuing tokens. This primitive can be both seen as a public-key counterpart to Verifiable Computation, where input generation and output verification are performed by different entities, or as a generalisation of Fully Homomorphic Encryption enabling control over computations on encrypted data.

Our primitive comes with a series of extra features as follows: 1) there is a one-time setup procedure for all circuits; 2) senders do not need to be aware of the functions which will be evaluated on the encrypted data, nor do they need to register keys; 3) tokens are independent of senders and receiver; and 4) receivers are able to verify the correctness of computation given short auxiliary information on the input data and the function, independently of the complexity of the computed circuit.

We give a modular construction of such a DHE scheme from three components: Fully Homomorphic Encryption (FHE), Functional Encryption (FE), and a (customised) MAC. As a stepping stone, we first define Verifiable Functional Encryption (VFE), and then show how one can build a secure DHE scheme from a VFE and an FHE scheme. We also show how to build the required VFE from a standard FE together with a MAC scheme. All our results hold in the standard model.Finally, we show how one can build a verifiable computation (VC) scheme generically from a DHE. As a corollary, we get
the first VC scheme which remains verifiable even if the attacker can observe verification results

Brumley B, Barbosa MB, Page D, Vercauteren F.  2012.  Practical realisation and elimination of an ECC-related software bug attack. The Cryptographers' Track at the RSA Conference on Topics in Cryptology - CT-RSA. 7178 Abstractpaper.pdf

We analyse and exploit implementation features in OpenSSL version 0.9.8g which permit an attack against ECDH-based functionality. The attack, although more general, can recover the entire (static) private key from an associated SSL server via 633 adaptive queries when the NIST curve P-256 is used. One can view it as a software-oriented analogue of the bug attack concept due to Biham et al. and, consequently, as the first bug attack to be successfully applied against a real-world system. In addition to the attack and a posteriori countermeasures, we show that formal verification, while rarely used at present, is a viable means of detecting the features which the attack hinges on. Based on the security implications of the attack and the extra justification posed by the possibility of intentionally incorrect implementations in collaborative software development, we conclude that applying and extending the coverage of formal verification to augment existing test strategies for OpenSSL-like software should be deemed a worthwhile, long-term challenge.

Arriaga A, Barbosa MB, Farshim P.  2012.  On the Joint Security of Signature and Encryption Schemes under Randomness Reuse: Efficiency and Security Amplification. 10th International Conference on Applied Cryptography and Network Security - ACNS. :206-223. Abstract382.pdf

We extend the work of Bellare, Boldyreva and Staddon on the systematic analysis of randomness reuse to construct multi-recipient encryption schemes to the case where randomness is reused across different cryptographic primitives. We find that through the additional binding introduced through randomness reuse, one can actually obtain a security amplification with respect to the standard black-box compositions, and achieve a stronger level of security. We introduce stronger notions of security for encryption and signatures, where challenge messages can depend in a restricted way on the random coins used in encryption, and show that two variants of the KEM/DEM paradigm give rise to encryption schemes that meet this enhanced notion of security. We obtain the most efficient signcryption scheme to date that is secure against insider attackers without random oracles.

Barbosa MB, Pinto A, Gomes B.  2012.  Generically extending anonymization algorithms to deal with successive queries. 21st ACM International Conference on Information and Knowledge Management - CIKM . :1362-1371. Abstractc46.pdf

This paper addresses the scenario of multi-release anonymization of datasets. We consider dynamic datasets where data can be inserted and deleted, and view this scenario as a case where each release is a small subset of the dataset corresponding, for example, to the results of a query. Compared to multiple releases of the full database, this has the obvious advantage of faster anonymization. We present an algorithm for post-processing anonymized queries that prevents anonymity attacks using multiple released queries. This algorithm can be used with several distinct protection principles and anonymization algorithms, which makes it generic and flexible. We give an experimental evaluation of the algorithm and compare it to $m$-invariance both in terms of efficiency and data quality. To this end, we propose two data quality metrics based on Shannon's entropy, and show that they can be seen as a refinement of existing metrics.

Almeida JB, Barbosa MB, Bangerter E, Barthe G, Krenn S, Béguelin SZ.  2012.  Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. Conference on Computer and Communications Security - CCS. :488-500. Abstract12ccs.pdf

Developers building cryptography into security-sensitive applications face a daunting task. Not only must they understand the security guarantees delivered by the constructions they choose, they must also implement and combine them correctly and efficiently. Cryptographic compilers free developers from having to implement cryptography on their own by turning high-level specifications of security goals into efficient implementations. Yet, trusting such tools is risky as they rely on complex mathematical machinery and claim security properties that are subtle and difficult to verify.
In this paper, we present ZKCrypt, an optimizing cryptographic compiler that achieves an unprecedented level of assurance without sacrificing practicality for a comprehensive class of cryptographic protocols, known as Zero-Knowledge Proofs of Knowledge. The pipeline of ZKCrypt tightly integrates purpose-built verified compilers and verifying compilers producing formal proofs in the CertiCrypt framework. By combining the guarantees delivered by each stage in the pipeline, ZKCrypt provides assurance that the implementation it outputs securely realizes the high-level proof goal given as input. We report on the main characteristics of ZKCrypt, highlight new definitions and concepts at its foundations, and illustrate its applicability through a representative example of an anonymous credential system.

Barbosa MB, Moss A, Page D, Rodrigues N, Silva P.  2011.  Type Checking Cryptography Implementations. Fundamentals of Software Engineering - 4th IPM International Conference, FSEN 2011, Revised Selected Papers. 7141:316-334. Abstractfsen11.pdf

Cryptographic software development is a challenging field: high performance must be achieved, while ensuring correctness and compliance with low-level security policies. CAO is a domain specific language designed to assist development of cryptographic software. An important feature of this language is the design of a novel type system introducing native types such as predefined sized vectors, matrices and bit strings, residue classes modulo an integer, finite fields and finite field extensions, allowing for extensive static validation of source code. We present the formalisation, validation and implementation of this type system.

Barbosa MB, Pinto JS, Filliâtre JC, Vieira B.  2010.  A Deductive Verification Platform for Cryptographic Software. Proceedings of the 4th International Workshop on Foundations and Techniques for Open Source Software Certification - OpenCert. 33 Abstract2010_opencert_10_a.pdf

In this paper we describe a deductive verification platform for the CAO language. CAO is a domain-specific language for cryptography. We show that this language presents interesting challenges for formal verification, not only in the rich mathematical type system that it introduces, but also in the cryptography-oriented language constructions that it offers. We describe how we tackle these problems, and also demonstrate that, by relying on the Jessie plug-in included in the Frama-C framework, the development time of such a complex verification tool could be greatly reduced. We base our presentation on real-world examples of CAO code, extracted from the open-source code of the NaCl cryptographic library, and illustrate how various cryptography-relevant security properties can be verified.

Barbosa MB, Farshim P.  2010.  Strong Knowledge Extractors for Public-Key Encryption Schemes. 15th Australasian Conference on Information Security and Privacy - ACISP. 6168:164-181. Abstractstrongextractorscrc.pdf

Completely non-malleable encryption schemes resist attacks which allow an adversary to tamper with both ciphertexts and public keys. In this paper we introduce two extractor-based properties that allow us to gain insight into the design of such schemes and to go beyond known feasibility results in this area. We formalise strong plaintext awareness and secret key awareness and prove their suitability in realising these goals. Strong plaintext awareness imposes that it is infeasible to construct a ciphertext under any public key without knowing the underlying message. Secret key awareness requires it to be infeasible to produce a new public key without knowing a corresponding secret key.