4 papers
Execution Time Program Verification With Tight Bounds
Ana Carolina Silva, Manuel Barbosa, Mario Florido
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: ap…
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy +3
MPC-in-the-Head (MitH) is a general framework that allows constructing efficient Zero Knowledge protocols for general NP-relations from secure multiparty computation (MPC) protocol…
Decentralized Privacy-Preserving Proximity Tracing
Carmela Troncoso, Mathias Payer, Jean-Pierre Hubaux +31
This document describes and analyzes a system for secure and privacy-preserving proximity tracing at large scale. This system, referred to as DP3T, provides a technological foundat…
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe +5
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected ag…