Encontrados 10 documentos, a visualizar página 1 de 1
Formal verification of side-channel countermeasures using self-composition
Almeida, José Bacelar; Barbosa, Manuel; Pinto, Jorge Sousa; Vieira, BárbaraFormal 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 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-com...
A certifying compiler for zero-knowledge proofs of knowledge based on sigma-pro...
Almeida, José Bacelar; Bangerter, Endre; Barbosa, Manuel Bernardo; Krenn, Stephan; Sadeghi, Ahmad-Reza; Schneider, ThomasZero-knowledge proofs of knowledge (ZK-PoK) are important building blocks for numerous cryptographic applications. Although ZK-PoK have a high potential impact, their real world deployment is typically hindered by their significant complexity compared to other (non-interactive) crypto primitives. Moreover, their design and implementation are time-consuming and error-prone. We contribute to overcoming these chal...
Formal verification of side channel countermeasures using self-composition
Almeida, José Bacelar; Barbosa, Manuel Bernardo; Pinto, Jorge Sousa; Vieira, BárbaraFormal 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 optimisations 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-comp...
Partial derivative automata formalized in Coq
Almeida, José Bacelar; Moreira, Nelma; Pereira, David; Sousa, Simão Melo deIn this paper we present a computer assisted proof of the correctness of a partial derivative automata construction from a regular expression within the Coq proof assistant. This proof is part of a for- malization of Kleene algebra and regular languages in Coq towards their usage in program certification.
Deductive verification of cryptographic software
Almeida, José Bacelar; Barbosa, Manuel Bernardo; Pinto, Jorge Sousa; Vieira, BárbaraWe apply state-of-the art deductive verification tools to check security-relevant properties of cryptographic software, including safety, absence of error propagation, and correctness with respect to reference implementations. We also develop techniques to help us in our task, focusing on methods oriented towards increased levels of automation, in scenarios where there are clear obvious limits to such automatio...
Verifying cryptographic software correctness with respect to reference implemen...
Almeida, José Bacelar; Barbosa, Manuel Bernardo; Pinto, Jorge Sousa; Vieira, BárbaraThis paper presents techniques developed to check program equivalences in the context of cryptographic software development, where specifications are typically reference implementations. The techniques allow for the integration of interactive proof techniques (required given the difficulty and generality of the results sought) in a verification infrastructure that is capable of discharging many verification con...
A tool for programming with interaction nets
Almeida, José Bacelar; Pinto, Jorge Sousa; Vilaça, MiguelProceedings of the Eighth International Workshop on Rule Based Programming (RULE 2007) ; 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 inter...
Token-passing nets for functional languages
Almeida, José Bacelar; Pinto, Jorge Sousa; Vilaça, MiguelProceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007) ; 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 sys...
A local graph-rewriting system for deciding equality in sum-product theories
Almeida, José Bacelar; Pinto, Jorge Sousa; Vilaça, MiguelProceedings of the Third International Workshop on Term Graph Rewriting (TERMGRAPH 2006) ; 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 coproduct...
A local graph-rewriting system for deciding equality in sum-product theories : ...
Pinto, Jorge Sousa; Almeida, José Bacelar; Vilaça, MiguelIn this paper we give a graph-based decision procedure for a calculus with sum and product types. Al- though 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...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||