Journal Articles

Almeida JB, Barbosa M, Pacheco H, Pereira V.  2016.  A Tool-Chain for High-Assurance Cryptographic Software. ERCIM News. 2016 Abstract16ercimnews.pdfWebsite

Cryptography is an inherently interdisciplinary area and the development of high-quality cryptographic software is a time-consuming task drawing on skills from mathematics, computer science and electrical engineering, only achievable by highly skilled programmers. The challenge is to map high-level cryptographic specifications phrased using mathematical abstractions into efficient implementations at the level of C or assembly that can be deployed on a target computational platform, whilst adhering to the specification both in terms of correctness and security. The High Assurance Software Laboratory at INESC-TEC maintains a domain-specific toolchain for the specification, implementation and verification of cryptographic software centred on CAO, a cryptography analyses and operations-aware language.

Fontaínhas EG, Andrade F, Almeida JB.  2016.  Do consentimento para a utilização de testemunhos de conexão (cookies). SCIENTIA IVRIDICA. 65(341):173-206. Abstract16scientiaivridica.pdf

O n.º 3 do artigo 5.º da Diretiva da Privacidade Eletrónica ( Directiva 2002/58/CE) estabelece os requisitos para o armazenamento e acesso a informação armazenada no terminal do utilizador ou assinante. Esta norma aplica-se à utilização de testemunhos de conexão (cookies), entendidos na aceção da definição dada pela norma RFC 6265 da Internet Engineering Task Force (IETF).

Na sua versão original, a Diretiva da Privacidade Eletrónica permitia a utilização de redes de comunicações eletrónicas para a armazenagem de informações ou para obter acesso à informação armazenada no equipamento terminal de um assinante ou utilizador, na condição de serem prestadas ao assinante ou utilizador informações claras e completas, nomeadamente sobre as finalidades do processamento e de, cumulativamente, lhe ser garantido o direito de recusar o tratamento (direito de autoexclusão ou direito de opt-out). Em 2009, a Diretiva dos Cidadãos (Diretiva 2009/136/CE) veio dar uma nova redação ao n.º 3 do artigo 5.º da Diretiva da Privacidade Eletrónica e passou a fazer depender a utilização de cookies da prévia obtenção do consentimento da pessoa em causa (direito de opt-in).

O novo requisito de consentimento veio abalar as práticas correntes no que respeita à utilização de cookies e está na base de um aceso debate sustentado pelas dúvidas acerca da sua interpretação e condições de implementação prática.

Procuramos, com este trabalho, contribuir para o esclarecimento dos conceitos de cookies e de consentimento enquanto fundamento legitimante para a sua utilização.

Ramos MVM, Almeida JB, Moreira N, de Queiroz RJGB.  2016.  Formalization of the Pumping Lemma for Context-Free Languages. Journal of Formalized Reasoning. 9(2):53-68. Abstract16jfr.pdfWebsite

Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages.
Pinto JS, Almeida JB, Barbosa MB, Vieira B, Filliâtre JC.  2014.  CAOVerif: An Open- Source Deductive Verification Platform for Cryptographic Software Implementations. Science of Computer Programming. 91:216–233. Abstractopencertjournal_ack.pdf

CAO is a domain-specific imperative language for cryptography, offering a rich mathematical type system and crypto-oriented language constructions. We describe the design and implementation of a deductive verification platform for CAO and demonstrate that the development time of such a complex verification tool could be greatly reduced by building on the Jessie plug-in included in the Frama-C framework. We discuss the interesting challenges raised by the domain-specific characteristics of CAO, and describe how we tackle these problems in our design. 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.
Almeida JB, Barbosa MB, Pinto JS, Vieira B.  2013.  Formal verification of side-channel countermeasures using self-composition. Science Computer Programming. 78(7):796–812. Abstract11scp.pdf

Formal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive low-level optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper we extend previous results supporting the practicality of self-composition proofs of non-interference and generalisations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We propose a formal verification framework to address these policies, extending the range of attacks that could previously be han- dled using self-composition. We demonstrate our techniques by addressing functional correctness and compliance with security policies for a practical use case.
Almeida JB, Pinto JS, Vilaça M.  2008.  Token-passing Nets for Functional Languages. Electronic Notes in Theoretical Computer Science. 204:181-198. Abstract07tnfp.pdf

Token-passing nets were proposed by Sinot as a simple mechanism for encoding evaluation strategies for the λ-calculus in interaction nets. This work extends token-passing nets to cover a typed functional language equipped with structured types and unrestricted recursion. The resulting interaction system is derived systematically from the chosen big-step operational semantics. Along the way, we actually characterize and discuss several design decisions of token-passing nets and extend them in order to achieve simpler interaction net systems with a higher degree of embedded parallelism.
Almeida JB, Pinto JS, Vilaça M.  2008.  A Tool for Programming with Interaction Nets. Electronic Notes in Theoretical Computer Science. 219:83-96. Abstract07tpin.pdf

This paper introduces INblobs, a visual tool developed at Minho for integrated development with Interaction Nets. Most of the existing tools take as input interaction nets and interaction rules represented in a textual format. INblobs is first of all a visual editor that allows users to edit interaction systems (both interaction nets and interaction rules) graphically, and to convert them to textual notation. This can then be used as input to other tools that implement reduction of nets. INblobs also allows the user to reduce nets within the tool, and includes a mechanism that automatically selects the next active pair to be reduced, following one of the given reduction strategies. The paper also describes other features of the tool, such as the creation of rules from pre-defined templates.
Almeida JB, Pinto JS, Vilaça M.  2007.  A Local Graph-rewriting System for Deciding Equality in Sum-product Theories. Electronic Notes in Theoretical Computer Science. 176(1):139-163. Abstract06sum-product.pdf

In this paper we give a graph-based decision procedure for a calculus with sum and product types. Although our motivation comes from the Bird-Meertens approach to reasoning algebraically about functional programs, the language used here can be seen as the internal language of a category with binary products and coproducts. As such, the decision procedure presented has independent interest.
A standard approach based on term rewriting would work modulo a set of equations; the present work proposes a simpler approach, based on graph-rewriting. We show in turn how the system covers reflection equational laws, fusion laws, and cancellation laws.