10 citations · 13 across the 8 of their papers we have counts for
8 papers
Formally Verifying Noir Zero Knowledge Programs with NAVe
Pedro Antonino, Namrata Jain
Zero-Knowledge (ZK) proof systems are cryptographic protocols that can (with overwhelming probability) demonstrate that the pair is in a relation without revealing inf…
Demystification and Near-perfect Estimation of Minimum Gas Limit and Gas Used for Ethereum Smart Contracts
Danilo Rafael de Lima Cabral, Pedro Antonino, Augusto Sampaio
The Ethereum blockchain has a \emph{gas system} that associates operations with a cost in gas units. Two central concepts of this system are the \emph{gas limit} assigned by the is…
Flexible remote attestation of pre-SNP SEV VMs using SGX enclaves
Pedro Antonino, Ante Derek, Wojciech Aleksander Wołoszyn
We propose a protocol that explores a synergy between two TEE implementations: it brings SGX-like remote attestation to SEV VMs. We use the notion of a \emph{trusted guest owner},…
A Pattern-based deadlock-freedom analysis strategy for concurrent systems
Pedro Antonino, Augusto Sampaio, Jim Woodcock
Local analysis has long been recognised as an effective tool to combat the state-space explosion problem. In this work, we propose a method that systematises the use of local analy…
Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts
Pedro Antonino, Juliandson Ferreira, Augusto Sampaio +1
Smart contracts are the building blocks of the "code is law" paradigm: the smart contract's code indisputably describes how its assets are to be managed - once it is created, its c…
Trusted And Confidential Program Analysis
Han Liu, Pedro Antonino, Zhiqiang Yang +2
We develop the concept of Trusted and Confidential Program Analysis (TCPA) which enables program certification to be used where previously there was insufficient trust. Imagine a s…
Guardian: symbolic validation of orderliness in SGX enclaves
Pedro Antonino, Wojciech Aleksander Wołoszyn, A. W. Roscoe
Modern processors can offer hardware primitives that allow a process to run in isolation. These primitives implement a trusted execution environment (TEE) in which a program can ru…
Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity
Pedro Antonino, A. W. Roscoe
The exploitation of smart-contract vulnerabilities can have catastrophic consequences such as the loss of millions of pounds worth of crypto assets. Formal verification can be a us…