Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Publicações

Publicações por Manuel Barbosa

2009

Verifying Cryptographic Software Correctness with Respect to Reference Implementations

Autores
Almeida, JB; Barbosa, M; Pinto, JS; Vieira, B;

Publicação
FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS

Abstract
This 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 conditions automatically. To this end, the difficult results in the verification process (to be proved interactively) are isolated as a set of lemmas. The fundamental notion of natural invariant is used to link the specification level and the interactive proof construction process.

2009

Deductive Verification of Cryptographic Software

Autores
Barbosa, M; Almeida, JB; Pinto, JS; Vieira, B;

Publicação
First NASA Formal Methods Symposium - NFM 2009, Moffett Field, California, USA, April 6-8, 2009.

Abstract

2010

A Deductive Verification Platform for Cryptographic Software

Autores
Barbosa, M; Pinto, JS; Filliâtre, JC; Vieira, B;

Publicação
ECEASST

Abstract

2023

Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium

Autores
Barbosa, M; Barthe, G; Doczkal, C; Don, J; Fehr, S; Grégoire, B; Huang, YH; Hülsing, A; Lee, Y; Wu, X;

Publicação
IACR Cryptol. ePrint Arch.

Abstract

2023

Execution Time Program Verification with Tight Bounds

Autores
Silva, AC; Barbosa, M; Florido, M;

Publicação
PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES, PADL 2023

Abstract
This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time reasoning, and less pessimistic execution time estimation using amortized analysis. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. Finally, we define a verification conditions (VC) generator that generates the goals needed to prove program correctness, cost, and termination. Those goals are then sent to the Easycrypt toolset for validation. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs. Our case studies are motivated by real-time and cryptographic software.

2021

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability

Autores
Barbosa, M; Barthe, G; Grégoire, B; Koutsos, A; Strub, PY;

Publicação
IACR Cryptol. ePrint Arch.

Abstract

  • 15
  • 20