-
Scaling CheckMate for Game-Theoretic Security
Authors:
Sophie Rain,
Lea Salome Brugger,
Anja Petkovic Komel,
Laura Kovacs,
Michael Rawson
Abstract:
We present the CheckMate tool for automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate's input format and its various components, modes…
▽ More
We present the CheckMate tool for automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate's input format and its various components, modes, and output. CheckMate is evaluated on 15 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.
△ Less
Submitted 13 June, 2024; v1 submitted 15 March, 2024;
originally announced March 2024.
-
Towards a Game-Theoretic Security Analysis of Off-Chain Protocols
Authors:
Sophie Rain,
Georgia Avarikioti,
Laura Kovács,
Matteo Maffei
Abstract:
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 p…
▽ More
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.
△ Less
Submitted 24 October, 2022; v1 submitted 15 September, 2021;
originally announced September 2021.
-
Summing Up Smart Transitions
Authors:
Neta Elad,
Sophie Rain,
Neil Immerman,
Laura Kovács,
Mooly Sagiv
Abstract:
Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer…
▽ More
Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer programs that operate over them, e.g., in Solidity. The ability to reason about sums is essential: even the simplest ERC-20 token standard of the Ethereum community provides a way to access the total supply of balances.
Unfortunately, reasoning about code written against this interface is non-trivial: the number of addresses is unbounded, and establishing global invariants like the preservation of the sum of the balances by operations like transfer requires higher-order reasoning. In particular, automated reasoners do not provide ways to specify summations of arbitrary length.
In this paper, we present a generalization of first-order logic which can express the unbounded sum of balances. We prove the decidablity of one of our extensions and the undecidability of a slightly richer one. We introduce first-order encodings to automate reasoning over software transitions with summations. We demonstrate the applicability of our results by using SMT solvers and first-order provers for validating the correctness of common transitions in smart contracts.
△ Less
Submitted 17 May, 2021;
originally announced May 2021.
-
The radio/gamma-ray connection in Active Galactic Nuclei in the era of the Fermi Large Area Telescope
Authors:
M. Ackermann,
M. Ajello,
A. Allafort,
E. Angelakis,
M. Axelsson,
L. Baldini,
J. Ballet,
G. Barbiellini,
D. Bastieri,
R. Bellazzini,
B. Berenji,
R. D. Blandford,
E. D. Bloom,
E. Bonamente,
A. W. Borgland,
A. Bouvier,
J. Bregeon,
A. Brez,
M. Brigida,
P. Bruel,
R. Buehler,
S. Buson,
G. A. Caliandro,
R. A. Cameron,
A. Cannon
, et al. (122 additional authors not shown)
Abstract:
We present a detailed statistical analysis of the correlation between radio and gamma-ray emission of the Active Galactic Nuclei (AGN) detected by Fermi during its first year of operation, with the largest datasets ever used for this purpose. We use both archival interferometric 8.4 GHz data (from the VLA and ATCA, for the full sample of 599 sources) and concurrent single-dish 15 GHz measurements…
▽ More
We present a detailed statistical analysis of the correlation between radio and gamma-ray emission of the Active Galactic Nuclei (AGN) detected by Fermi during its first year of operation, with the largest datasets ever used for this purpose. We use both archival interferometric 8.4 GHz data (from the VLA and ATCA, for the full sample of 599 sources) and concurrent single-dish 15 GHz measurements from the Owens Valley Radio Observatory (OVRO, for a sub sample of 199 objects). Our unprecedentedly large sample permits us to assess with high accuracy the statistical significance of the correlation, using a surrogate-data method designed to simultaneously account for common-distance bias and the effect of a limited dynamical range in the observed quantities. We find that the statistical significance of a positive correlation between the cm radio and the broad band (E>100 MeV) gamma-ray energy flux is very high for the whole AGN sample, with a probability <1e-7 for the correlation appearing by chance. Using the OVRO data, we find that concurrent data improve the significance of the correlation from 1.6e-6 to 9.0e-8. Our large sample size allows us to study the dependence of correlation strength and significance on specific source types and gamma-ray energy band. We find that the correlation is very significant (chance probability <1e-7) for both FSRQs and BL Lacs separately; a dependence of the correlation strength on the considered gamma-ray energy band is also present, but additional data will be necessary to constrain its significance.
△ Less
Submitted 2 August, 2011;
originally announced August 2011.
-
Radio and Gamma-Ray Constraints on the Emission Geometry and Birthplace of PSR J2043+2740
Authors:
A. Noutsos,
A. A. Abdo,
M. Ackermann,
M. Ajello,
J. Ballet,
G. Barbiellini,
M. G. Baring,
D. Bastieri,
K. Bechtol,
R. Bellazzini,
B. Berenji,
E. Bonamente,
A. W. Borgland,
J. Bregeon,
A. Brez,
M. Brigida,
P. Bruel,
R. Buehler,
G. Busetto,
G. A. Caliandro,
R. A. Cameron,
F. Camilo,
P. A. Caraveo,
J. M. Casandjian,
C. Cecchi
, et al. (124 additional authors not shown)
Abstract:
We report on the first year of Fermi gamma-ray observations of pulsed high-energy emission from the old PSR J2043+2740. The study of the gamma-ray efficiency of such old pulsars gives us an insight into the evolution of pulsars' ability to emit in gammma rays as they age. The gamma-ray lightcurve of this pulsar above 0.1 GeV is clearly defined by two sharp peaks, 0.353+/-0.035 periods apart. We ha…
▽ More
We report on the first year of Fermi gamma-ray observations of pulsed high-energy emission from the old PSR J2043+2740. The study of the gamma-ray efficiency of such old pulsars gives us an insight into the evolution of pulsars' ability to emit in gammma rays as they age. The gamma-ray lightcurve of this pulsar above 0.1 GeV is clearly defined by two sharp peaks, 0.353+/-0.035 periods apart. We have combined the gamma-ray profile characteristics of PSR J2043+2740 with the geometrical properties of the pulsar's radio emission, derived from radio polarization data, and constrained the pulsar-beam geometry in the framework of a Two Pole Caustic and an Outer Gap model. The ranges of magnetic inclination and viewing angle were determined to be {alpha,zeta}~{52-57,61-68} for the Two Pole Caustic model, and {alpha,zeta}~{62-73,74-81} and {alpha,zeta}~{72-83,60-75} for the Outer Gap model. Based on this geometry, we assess possible birth locations for this pulsar and derive a likely proper motion, sufficiently high to be measurable with VLBI. At a characteristic age of 1.2 Myr, PSR J2043+2740 is the third oldest of all discovered, non-recycled, gamma-ray pulsars: it is twice as old as the next oldest, PSR J0357+32, and younger only than the recently discovered PSR J1836+5925 and PSR J2055+25, both of which are at least 5 and 10 times less energetic, respectively.
△ Less
Submitted 21 December, 2010;
originally announced December 2010.
