arXiv subjects

Matteo Maffei

Publications and source records attributed to Matteo Maffei.

At least 19 recordsLinked to original sources

arXiv2026

LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean

Computer-aided formal verification is a widely used approach for the symbolic analysis of cryptographic protocols. However, many modern protocols rely on features that remain challenging for existing techniques. In particular, reasoning about state, time-dependent behavior, inductively defined data structures, unbounded executions, and conditional secrecy requires a level of expressiveness that is difficult to reconcile with effective automation. As a result, protocol verification has largely followed two disjoint paths: fully automated methods with limited expressiveness, or interactive proofs in general-purpose theorem provers that offer flexibility but only limited, non-specialized automation. We present an orthogonal approach that bridges this gap by combining compositional type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols. Guided by the language-and-automation co-design (LAC) principle, our approach delivers protocol-specific automation while retaining high expressiveness. We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*, and combining protocol-specific automation with interactive proofs. Our framework supports, in a unified setting, a broad class of functional and security requirements, including secrecy and authentication for stateful protocols, as well as recursive conditional secrecy for protocols using XOR. We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels on top of this blockchain model, verifying punishment mechanisms and properties that depend on chain liveness.

cs.CR↗

arXiv2026

Differential Zonotopes for Verifying Global Robustness of DNNs

The robustness of deep neural networks (DNNs) is critical in security-sensitive applications, where small input perturbations should not alter model predictions. This property is commonly formalized as local or global robustness: the former considers perturbations around a single input, while the latter -- strictly stronger -- quantifies over all input pairs. While local robustness can be expressed as a safety property, global robustness is a 2-safety property, making it substantially more challenging to verify. We present a novel static analysis technique for verifying the global robustness of DNNs. Our approach is based on differential halo zonotopes, a new abstract domain that extends zonotopes to jointly propagate pairs of perturbed inputs in lock-step while tightly bounding their divergence. In addition, we introduce a symmetric variant of confidence-based global robustness that disregards perturbations leading to differing but low-confidence predictions. This relaxation yields a practically meaningful notion of robustness that applies to a broader class of networks. We implement our approach in a new tool, called TwoSafe, and evaluate it on standard DNN verification benchmarks, including widely deployed models. Our results show that TwoSafe significantly outperforms the state of the art in both precision and scalability, enabling the verification of networks an order of magnitude larger than those handled by prior techniques.

cs.CR↗

arXiv2026

Ark: Offchain Transaction Batching in Bitcoin

Bitcoin is the cryptocurrency with the largest market capitalisation, but its widespread adoption is fundamentally limited by the scalability constraints of its consensus algorithm, which requires every transaction to be confirmed onchain. To address this, several Layer-2 scalability solutions have been proposed to move payments offchain -- most notably, the Lightning Network. However, their deployment remains hindered by cumbersome setup requirements: users must lock funds onchain to participate and engage in complex auxiliary protocols (e.g., for channel rebalancing, top-ups, and routing). Other solutions, like payment pools, sidechains and rollups, cannot be implemented in a non-custodial way on Bitcoin due to its limited scripting capabilities, or require all protocol participants to update the offchain state. In this work, we present Ark, the first Bitcoin-compatible commit-chain. Ark enables offchain transactions of virtual UTXOs (VTXOs), through an untrusted operator who aggregates them into succinct onchain commitments. A distinctive feature of Ark is its ease of deployment: users can receive offchain payments without locking any funds beforehand and Ark state updates can be performed only requiring the users involved in that update. We formally define the Ark protocol and prove its security. During this process, we identified two attacks affecting the testnet implementation, which we responsibly disclosed and proposed fixes for, which have been now integrated into the mainnet implementation. Our experimental evaluation demonstrates that Ark can commit onchain to batches of arbitrarily many VTXOs with a constant-sized footprint of approximately 200 vB. Cooperative exits add one output per user, while unilateral exits require $\mathcal{O}(\log n)$ transactions of roughly 150 vB per VTXO for a batch of $n$ VTXOs.

cs.DC↗

arXiv2025

Calyx: Privacy-Preserving Multi-Token Optimistic-Rollup Protocol

Rollup protocols have recently received significant attention as a promising class of Layer 2 (L2) scalability solutions. By utilizing the Layer 1 (L1) blockchain solely as a bulletin board for a summary of the executed transactions and state changes, rollups enable secure off-chain execution while avoiding the complexity of other L2 mechanisms. However, to ensure data availability, current rollup protocols require the plaintext of executed transactions to be published on-chain, resulting in inherent privacy limitations. In this paper, we address this problem by introducing Calyx, the first privacy-preserving multi-token optimistic-Rollup protocol. Calyx guarantees full payment privacy for all L2 transactions, revealing no information about the sender, recipient, transferred amount, or token type. The protocol further supports atomic execution of multiple multi-token transactions and introduces a transaction fee scheme to enable broader application scenarios while ensuring the sustainable operation of the protocol. To enforce correctness, Calyx adopts an efficient one-step fraud-proof mechanism. We analyze the security and privacy guarantees of the protocol and provide an implementation and evaluation. Our results show that executing a single transaction costs approximately $0.06 (0.00002 ETH) and incurs only constant-size on-chain cost in asymptotic terms.

cs.CR↗

arXiv2025

Wanilla: Sound Noninterference Analysis for WebAssembly

WebAssembly (Wasm) is rapidly gaining popularity as a distribution format for software components embedded in various security-critical domains. Unfortunately, despite its prudent design, WebAssembly's primary use case as a compilation target for memory-unsafe languages leaves some possibilities for memory corruption. Independently of that, Wasm is an inherently interesting target for information flow analysis due to its interfacing role. Both the information flows between a Wasm module and its embedding context, as well as the memory integrity within a module, can be described by the hyperproperty noninterference. So far, no sound, fully static noninterference analysis for Wasm has been presented, but sound reachability analyses were. This work presents a novel and general approach to lift reachability analyses to noninterference by tracking taints on values and using value-sensitive, relational reasoning to remove them when appropriate. We implement this approach in Wanilla, the first automatic, sound, and fully static noninterference analysis for WebAssembly, and demonstrate its performance and precision by verifying memory integrity and other noninterference properties with several synthetic and real-world benchmarks.

cs.CR↗

arXiv2025

A Composable Game-Theoretic Framework for Blockchains

Blockchains rely on economic incentives to ensure secure and decentralised operation, making incentive compatibility a core design concern. However, protocols are rarely deployed in isolation. Applications interact with the underlying consensus and network layers, and multiple protocols may run concurrently on the same chain. These interactions give rise to complex incentive dynamics that traditional, isolated analyses often fail to capture. We propose the first compositional game-theoretic framework for blockchain protocols. Our model represents blockchain protocols as interacting games across the application, network, and consensus layers. It enables formal reasoning about incentive compatibility under composition by introducing two key abstractions: the cross-layer game, which models how strategies in one layer influence others, and cross-application composition, which captures how application protocols interact concurrently through shared infrastructure. We illustrate our framework through case studies on Hashed Timelock Contracts (HTLCs), Layer-2 protocols, and Maximal Extractable Value (MEV) showing how compositional analysis reveals new subtle incentive vulnerabilities and supports modular security proofs. Also, by introduction of a novel rational miner model, we derive new conditions for the robustness of timelocks to bribing attacks.

cs.GT↗

arXiv2025

A Security Framework for General Blockchain Layer 2 Protocols

Layer 2 (L2) protocols, payment channels, sidechains, and rollups, are central to blockchain scalability, enabling off-chain execution while preserving on-chain security. Despite growing deployment, existing security models remain protocol-specific and monolithic, hindering compositional reasoning and principled comparison of assumptions and requirements. We present a general security framework for L2 protocols in the IITM-style Universal Composability (iUC) model. At its core is a modular ideal functionality F_layer2 that abstracts mechanism-specific details while capturing the essential structure of L2 systems through composable subroutines for joining, submission, updating, reading, and settlement under adversarial conditions. This yields uniform definitions of safety, liveness, and data availability across a broad class of L2 protocols. We demonstrate generality by instantiating the framework for three representative constructions: the Brick payment channel, the Liquid sidechain, and the Arbitrum Nitro rollup. Each case study yields a protocol-specific ideal functionality derived from F_layer2 and tailored to its assumptions. Our analysis (i) establishes security via simulation-based proofs, (ii) exposes inherent trade-offs among safety, liveness, and data availability, and (iii) derives lower bounds characterizing fundamental limitations of each design class. Finally, we illustrate the framework as a design tool by presenting FRoll, the first optimistic rollup protocol with fast-finality guarantees, together with a security analysis in our model, showing how the framework supports requirement-driven design of L2 protocols.

cs.CR↗

arXiv2024

Verifying Global Two-Safety Properties in Neural Networks with Confidence

We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundness of our static analysis technique. Furthermore, we implement it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification.

cs.LO↗

arXiv2023

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model

Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models yield rigorous guarantees but support at present only interactive proofs and/or restricted classes of protocols. A promising approach is given by the computationally complete symbolic attacker (CCSA), formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic analysis. The BC Logic is supported by a recently developed interactive theorem prover, Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert knowledge. We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. We overcome the burden of interactive proving in higher-order (HO) logic and automatically establish soundness of cryptographic protocols using only FO reasoning. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness. On the practical side, CryptoVampire integrates dedicated proof techniques using FO saturation algorithms and heuristics, which enable leveraging the state-of-the-art Vampire FO theorem prover as the underlying proving engine. Our experimental results show CryptoVampire's effectiveness of as a standalone verifier and in terms of automation support for Squirrel.

cs.CR↗

arXiv2022

WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms

The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the interplay between new and existing Web platform components. To tackle this problem, we developed WebSpec, the first formal security framework for the analysis of browser security mechanisms, which enables both the automatic discovery of logical flaws and the development of machine-checked security proofs. WebSpec, in particular, includes a comprehensive semantic model of the browser in the Coq proof assistant, a formalization in this model of ten Web security invariants, and a toolchain turning the Coq model and the Web invariants into SMT-lib formulas to enable model checking with the Z3 theorem prover. If a violation is found, the toolchain automatically generates executable tests corresponding to the discovered attack trace, which is validated across major browsers. We showcase the effectiveness of WebSpec by discovering two new logical flaws caused by the interaction of different browser mechanisms and by identifying three previously discovered logical flaws in the current Web platform, as well as five in old versions. Finally, we show how WebSpec can aid the verification of our proposed changes to amend the reported inconsistencies affecting the current Web platform.

cs.CR↗

arXiv2021

Adoption and Actual Privacy of Decentralized CoinJoin Implementations in Bitcoin

We present a first measurement study on the adoption and actual privacy of two popular decentralized CoinJoin implementations, Wasabi and Samourai, in the broader Bitcoin ecosystem. By applying highly accurate (> 99%) algorithms we can effectively detect 30,251 Wasabi and 223,597 Samourai transactions within the block range 530,500 to 725,348 (2018-07-05 to 2022-02-28). We also found a steady adoption of these services with a total value of mixed coins of ca. 4.74 B USD and average monthly mixing amounts of ca. 172.93 M USD) for Wasabi and ca. 41.72 M USD for Samourai. Furthermore, we could trace ca. 322 M USD directly received by cryptoasset exchanges and ca. 1.16 B USD indirectly received via two hops. Our analysis further shows that the traceability of addresses during the pre-mixing and post-mixing narrows down the anonymity set provided by these coin mixing services. It also shows that the selection of addresses for the CoinJoin transaction can harm anonymity. Overall, this is the first paper to provide a comprehensive picture of the adoption and privacy of distributed CoinJoin transactions. Understanding this picture is particularly interesting in the light of ongoing regulatory efforts that will, on the one hand, affect compliance measures implemented in cryptocurrency exchanges and, on the other hand, the privacy of end-users.

cs.CR↗

arXiv2021

Towards a Game-Theoretic Security Analysis of Off-Chain Protocols

Off-chain protocols constitute one of the most promising approaches to solve the inherent scalability issue of blockchain technologies. The core idea is to let parties transact on-chain only once to establish a channel between them, leveraging later on the resulting channel paths to perform arbitrarily many peer-to-peer transactions off-chain. While significant progress has been made in terms of proof techniques for off-chain protocols, existing approaches do not capture the game-theoretic incentives at the core of their design, which led to overlooking significant attack vectors like the Wormhole attack in the past. In this work we take a first step towards a principled game-theoretic security analysis of off-chain protocols by introducing the first game-theoretic model that is expressive enough to reason about their security. We advocate the use of Extensive Form Games (EFGs) and introduce two instances of EFGs to capture security properties of the closing and the routing of the Lightning Network. Specifically, we model the closing protocol, which relies on punishment mechanisms to disincentivize parties to upload old channel states on-chain. Moreover, we model the routing protocol, thereby formally characterizing the Wormhole attack, a vulnerability that undermines the fee-based incentive mechanism underlying the Lightning Network.

cs.CR↗

arXiv2021

The Good, the Bad and the Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts

Ethereum smart contracts are distributed programs running on top of the Ethereum blockchain. Since program flaws can cause significant monetary losses and can hardly be fixed due to the immutable nature of the blockchain, there is a strong need of automated analysis tools which provide formal security guarantees. Designing such analyzers, however, proved to be challenging and error-prone. We review the existing approaches to automated, sound, static analysis of Ethereum smart contracts and highlight prevalent issues in the state of the art. Finally, we overview eThor, a recent static analysis tool that we developed following a principled design and implementation approach based on rigorous semantic foundations to overcome the problems of past works.

cs.CR↗

arXiv2020

Can I Take Your Subdomain? Exploring Related-Domain Attacks in the Modern Web

Related-domain attackers control a sibling domain of their target web application, e.g., as the result of a subdomain takeover. Despite their additional power over traditional web attackers, related-domain attackers received only limited attention by the research community. In this paper we define and quantify for the first time the threats that related-domain attackers pose to web application security. In particular, we first clarify the capabilities that related-domain attackers can acquire through different attack vectors, showing that different instances of the related-domain attacker concept are worth attention. We then study how these capabilities can be abused to compromise web application security by focusing on different angles, including: cookies, CSP, CORS, postMessage and domain relaxation. By building on this framework, we report on a large-scale security measurement on the top 50k domains from the Tranco list that led to the discovery of vulnerabilities in 887 sites, where we quantified the threats posed by related-domain attackers to popular web applications.

cs.CR↗

arXiv2020

Optimizing Virtual Payment Channel Establishment in the Face of On-Path Adversaries

Payment channel networks (PCNs) are among the most promising solutions to the scalability issues in permissionless blockchains, by allowing parties to pay each other off-chain through a path of payment channels (PCs). However, routing transactions comes at a cost which is proportional to the number of intermediaries, since each charges a fee for the routing service. Furthermore, analogous to other networks, malicious intermediaries in the payment path can lead to security and privacy threats. Virtual channels (VCs), i.e., bridges over PC paths, mitigate the above PCN issues, as an intermediary participates only once to set up the VC and is then excluded from every future VC transaction. However, similar to PCs, creating a VC has a cost that must be paid out of the bridged PCs' balance. Currently, we are missing guidelines to where and how many VCs to set up. Ideally, VCs should minimize transaction costs while mitigating security and privacy threats from on-path adversaries. In this work, we address for the first time the VC setup problem, formalizing it as an optimization problem. We present an integer linear program (ILP) to compute the globally optimal VC setup strategy in terms of transaction costs, security, and privacy. We then accompany the computationally heavy ILP with a fast local greedy algorithm. Our model and algorithms can be used with any on-path adversary, given that its strategy can be expressed as a set of corrupted nodes that is estimated by the honest nodes. We conduct an evaluation of the greedy algorithm over a snapshot of the Lightning Network (LN), the largest Bitcoin-based PCN. Our results confirm on real-world data that our greedy strategy minimizes costs while protecting against security and privacy threats of on-path adversaries. These findings may serve the LN community as guidelines for the deployment of VCs.

cs.CR↗

arXiv2020

Cross-Layer Deanonymization Methods in the Lightning Protocol

Bitcoin (BTC) pseudonyms (layer 1) can effectively be deanonymized using heuristic clustering techniques. However, while performing transactions off-chain (layer 2) in the Lightning Network (LN) seems to enhance privacy, a systematic analysis of the anonymity and privacy leakages due to the interaction between the two layers is missing. We present clustering heuristics that group BTC addresses, based on their interaction with the LN, as well as LN nodes, based on shared naming and hosting information. We also present linking heuristics that link 45.97% of all LN nodes to 29.61% BTC addresses interacting with the LN. These links allow us to attribute information (e.g., aliases, IP addresses) to 21.19% of the BTC addresses contributing to their deanonymization. Further, these deanonymization results suggest that the security and privacy of LN payments are weaker than commonly believed, with LN users being at the mercy of as few as five actors that control 36 nodes and over 33% of the total capacity. Overall, this is the first paper to present a method for linking LN nodes with BTC addresses across layers and to discuss privacy and security implications.

cs.CR↗

arXiv2020

eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts

Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences and, even worse, they can be hardly fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging for a variety of reasons, such as the specific transaction-oriented programming mechanisms, which feature a subtle semantics, and the fact that the blockchain data which the contract under analysis interacts with, including the code of callers and callees, are not statically known. In this work, we present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode and an experimental large-scale evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 95% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%.

cs.PL↗

arXiv2020

Language-Based Web Session Integrity

Session management is a fundamental component of web applications: despite the apparent simplicity, correctly implementing web sessions is extremely tricky, as witnessed by the large number of existing attacks. This motivated the design of formal methods to rigorously reason about web session security which, however, are not supported at present by suitable automated verification techniques. In this paper we introduce the first security type system that enforces session security on a core model of web applications, focusing in particular on server-side code. We showcase the expressiveness of our type system by analyzing the session management logic of HotCRP, Moodle, and phpMyAdmin, unveiling novel security flaws that have been acknowledged by software developers.

cs.CR↗