arXiv subjects

Igor Konnov

Publications and source records attributed to Igor Konnov.

18 recordsLinked to original sources

arXiv2025

ChonkyBFT: Consensus Protocol of ZKsync

We present ChonkyBFT, a partially-synchronous Byzantine fault-tolerant (BFT) consensus protocol used in the ZKsync system. The proposed protocol is a hybrid protocol inspired by FAB Paxos, Fast-HotStuff, and HotStuff-2. It is a committee-based protocol with only one round of voting, single slot finality, quadratic communication, and n >= 5f + 1 fault tolerance. This design enables its effective application within the context of the ZKsync rollup, achieving its most critical goals: simplicity, low transaction latency, and reduced system complexity. The target audience for this paper is the ZKsync community and others worldwide who seek assurance in the safety and security of the ZKsync protocols. The described consensus protocol has been implemented, analyzed, and tested using formal methods.

cs.DC↗

arXiv2025

Technical Report: Exploring Automatic Model-Checking of the Ethereum specification

We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique challenges it poses for formal verification. Our primary tools are TLA+ for specification and the Apalache model checker for verification. Our formalization builds on the executable Python specification of 3SF. To begin, we manually translate this specification into TLA+, revealing significant combinatorial complexity in the definition of Accountable Safety. To address these challenges, we introduce several layers of manual abstraction: (1) replacing recursion with folds, (2) substituting abstract graphs with integers, and (3) decomposing chain configurations. To cross-validate our results, we develop alternative encodings in SMT (CVC5) and Alloy. Despite the inherent complexity, our results demonstrate that exhaustive verification of Accountable Safety is feasible for small instances - supporting up to 7 checkpoints and 24 validator votes. Moreover, no violations of Accountable Safety are observed, even in slightly larger configurations. Beyond these findings, our study highlights the importance of manual abstraction and domain expertise in enhancing model-checking efficiency and showcases the flexibility of TLA+ for managing intricate specifications.

cs.LO↗

arXiv2023

A case study on parametric verification of failure detectors

Partial synchrony is a model of computation in many distributed algorithms and modern blockchains. These algorithms are typically parameterized in the number of participants, and their correctness requires the existence of bounds on message delays and on the relative speed of processes after reaching Global Stabilization Time. These characteristics make partially synchronous algorithms parameterized in the number of processes, and parametric in time bounds, which render automated verification of partially synchronous algorithms challenging. In this paper, we present a case study on formal verification of both safety and liveness of the Chandra and Toueg failure detector that is based on partial synchrony. To this end, we first introduce and formalize the class of symmetric point-to-point algorithms that contains the failure detector. Second, we show that these symmetric point-to-point algorithms have a cutoff, and the cutoff results hold in three models of computation: synchrony, asynchrony, and partial synchrony. As a result, one can verify them by model checking small instances, but the verification problem stays parametric in time. Next, we specify the failure detector and the partial synchrony assumptions in three frameworks: TLA+, IVy, and counter automata. Importantly, we tune our modeling to use the strength of each method: (1) We are using counters to encode message buffers with counter automata, (2) we are using first-order relations to encode message buffers in IVy, and (3) we are using both approaches in TLA+. By running the tools for TLA+ and counter automata, we demonstrate safety for fixed time bounds. By running IVy, we prove safety for arbitrary time bounds. Moreover, we show how to verify liveness of the failure detector by reducing the verification problem to safety verification. Thus, both properties are verified by developing inductive invariants with IVy.

cs.LO↗

arXiv2023

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker

Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems in distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain algorithms such as, e.g., Tendermint consensus. In this article, we give an overview of techniques for automated verification of threshold-guarded fault-tolerant distributed algorithms, implemented in the Byzantine Model Checker (ByMC). These threshold-guarded algorithms have the following features: (1) up to $t$ of processes may crash or behave Byzantine; (2) the correct processes count messages and make progress when they receive sufficiently many messages, e.g., at least $t+1$; (3) the number $n$ of processes in the system is a parameter, as well as the number $t$ of faults; and (4) the parameters are restricted by a resilience condition, e.g., $n > 3t$. Traditionally, these algorithms were implemented in distributed systems with up to ten participating processes. Nowadays, they are implemented in distributed systems that involve hundreds or thousands of processes. To make sure that these algorithms are still correct for that scale, it is imperative to verify them for all possible values of the parameters.

cs.DC↗

arXiv2022

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS

Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their complementary strengths and weaknesses, we suggest a workflow that supports different types of analysis and that can be adapted to the desired degree of confidence.

cs.LO↗

arXiv2022

Holistic Verification of Blockchain Consensus

Blockchain has recently attracted the attention of the industry due, in part, to its ability to automate asset transfers. It requires distributed participants to reach a consensus on a block despite the presence of malicious (a.k.a. Byzantine) participants. Malicious participants exploit regularly weaknesses of these blockchain consensus algorithms, with sometimes devastating consequences. In fact, these weaknesses are quite common and are well illustrated by the flaws in the hand-written proofs of existing blockchain consensus protocols [63]. Paradoxically, until now, no blockchain consensus has been holistically verified using model checking. In this paper, we remedy this paradox by model checking for the first time a blockchain consensus used in industry. We propose a holistic approach to verify the consensus algorithm of the Red Belly Blockchain [20], for any number $n$ of processes and any number $f<n/3$ of Byzantine processes. We decompose directly the algorithm pseudocode in two parts -- an inner broadcast algorithm and an outer decision algorithm -- each modelled as a threshold automaton [36], and we formalize their expected properties in linear-time temporal logic. We then automatically check the inner broadcasting algorithm, under a carefully identified fairness assumption. For the verification of the outer algorithm, we simplify the model of the inner algorithm by relying on its checked properties. Doing so, we formally verify not only the safety properties of the Red Belly Blockchain consensus but also its liveness in about 70 seconds.

cs.CR↗

arXiv2022

Primal-Dual Method for Optimization Problems with Changing Constraints

We propose a modified primal-dual method for general convex optimization problems with changing constraints. We obtain properties of Lagrangian saddle points for these problems which enable us to establish convergence of the proposed method. We describe specializations of the proposed approach to multi-agent optimization problems under changing communication topology and to feasibility problems.

math.OC↗

arXiv2020

A Tendermint Light Client

In Tendermint blockchains, the proof-of-stake mechanism and the underlying consensus algorithm entail a dynamic fault model that implies that the active validators (nodes that sign blocks) may change over time, and a quorum of these validators is assumed to be correct only for a limited period of time (called trusting period). The changes of the validator set are under control of the blockchain application, and are committed in every block. In order to check what is the state of the blockchain application at some height h, one needs to know the validator set at that height so that one can verify the corresponding digital signatures and hashes. A naive way of determining the validator set for height h requires one to: (i) download all blocks before h, (ii) verify blocks by checking digital signatures and hashes and (iii) execute the corresponding transactions so the changes in the validator sets are reproduced. This can potentially be very slow and computationally and data intensive. In this paper we formalize the dynamic fault model imposed by Tendermint, and describe a light client protocol that allows to check the state of the blockchain application that, in realistic settings, reduces significantly the amount of data needed to be downloaded, and the number of required computationally expensive signature verification operations. In addition to mathematical proofs, we have formalized the light client protocol in TLA+, and checked safety and liveness with the APALACHE model checker.

cs.DC↗

arXiv2020

Decentralized Multi-Agent Optimization Based on a Penalty Method

We propose a decentralized penalty method for general convex constrained multi-agent optimization problems. Each auxiliary penalized problem is solved approximately with a special parallel descent splitting method. The method can be implemented in a computational network where each agent sends information only to the nearest neighbours. Convergence of the method is established under rather weak assumptions. We also describe a specialization of the proposed approach to the feasibility problem.

math.OC↗

arXiv2020

Variational Inequality Type Formulations of General Market Equilibrium Problems with Local Information

We suggest a new approach to creation of general market equilibrium models involving economic agents with local and partial knowledge about the system and under different restrictions. The market equilibrium problem is then formulated as a quasi-variational inequality that enables us to establish existence results for the model in different settings. We also describe dynamic processes, which fall into information exchange schemes of the proposed market model. In particular, we propose an iterative solution method for quasi-variational inequalities, which is based on evaluations of the proper market information only in a neighborhood of the current market state without knowledge of the whole feasible set and prove its convergence.

math.OC↗

arXiv2019

A Non-Monotone Conjugate Subgradient Type Method for Minimization of Convex Functions

We suggest a conjugate subgradient type method without any line-search for minimization of convex non differentiable functions. Unlike the custom methods of this class, it does not require monotone decrease of the goal function and reduces the implementation cost of each iteration essentially. At the same time, its step-size procedure takes into account behavior of the method along the iteration points. Preliminary results of computational experiments confirm efficiency of the proposed modification.

math.OC↗

arXiv2018

A Simple Adaptive Step-size Choice for Iterative Optimization Methods

We suggest a simple adaptive step-size procedure, which does not require any line-search, for a general class of nonlinear optimization methods and prove convergence of a general method under mild assumptions. In particular, the goal function may be non-smooth and non-convex. Unlike the descent line-search methods, it does not require monotone decrease of the goal function values along the iteration points and reduces the implementation cost of each iteration essentially. The key element of this procedure consists in inserting a majorant step-size sequence such that the next element is taken only if the current iterate does not give a sufficient descent. Its applications yield in particular a new gradient projection method for smooth constrained optimization problems and a new projection type method for minimization of the gap function of a general variational inequality. Preliminary results of computational experiments confirm efficiency of the proposed modification.

math.OC↗

arXiv2018

Simplified Versions of the Conditional Gradient Method

We suggest simple modifications of the conditional gradient method for smooth optimization problems, which maintain the basic convergence properties, but reduce the implementation cost of each iteration essentially. Namely, we propose the step-size procedure without any line-search, and inexact solution of the direction finding subproblem. Preliminary results of computational tests confirm efficiency of the proposed modifications.

math.OC↗

arXiv2017

Application of Market Models to Network Equilibrium Problems

We present a general two-side market model with divisible commodities and price functions of participants. A general existence result on unbounded sets is obtained from its variational inequality re-formulation. We describe an extension of the network flow equilibrium problem with elastic demands and a new equilibrium type model for resource allocation problems in wireless communication networks, which appear to be particular cases of the general market model. This enables us to obtain new existence results for these models as some adjustments of that for the market model. Under certain additional conditions the general market model can be reduced to a decomposable optimization problem where the goal function is the sum of two functions and one of them is convex separable, whereas the feasible set is the corresponding Cartesian product. We discuss some versions of the partial linearization method, which can be applied to these network equilibrium problems.

math.OC↗

arXiv2017

Gradient Methods with Regularization for Constrained Optimization Problems and Their Complexity Estimates

We suggest simple implementable modifications of conditional gradient and gradient projection methods for smooth convex optimization problems in Hilbert spaces. Usually, the custom methods attain only weak convergence. We prove strong convergence of the new versions and establish their complexity estimates, which appear similar to the convergence rate of the weakly convergent versions.

math.OC↗

arXiv2016

A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms

Distributed algorithms have many mission-critical applications ranging from embedded systems and replicated databases to cloud computing. Due to asynchronous communication, process faults, or network failures, these algorithms are difficult to design and verify. Many algorithms achieve fault tolerance by using threshold guards that, for instance, ensure that a process waits until it has received an acknowledgment from a majority of its peers. Consequently, domain-specific languages for fault-tolerant distributed systems offer language support for threshold guards. We introduce an automated method for model checking of safety and liveness of threshold-guarded distributed algorithms in systems where the number of processes and the fraction of faulty processes are parameters. Our method is based on a short counterexample property: if a distributed algorithm violates a temporal specification (in a fragment of LTL), then there is a counterexample whose length is bounded and independent of the parameters. We prove this property by (i) characterizing executions depending on the structure of the temporal formula, and (ii) using commutativity of transitions to accelerate and shorten executions. We extended the ByMC toolset (Byzantine Model Checker) with our technique, and verified liveness and safety of 10 prominent fault-tolerant distributed algorithms, most of which were out of reach for existing techniques.

cs.LO↗

arXiv2013

Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms

We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the assumed maximum number of Byzantine faulty processes. At the center of our technique is a parametric interval abstraction (PIA) where the interval boundaries are arithmetic expressions over parameters. Using PIA for both data abstraction and a new form of counter abstraction, we reduce the parameterized problem to finite-state model checking. We demonstrate the practical feasibility of our method by verifying several variants of the well-known distributed algorithm by Srikanth and Toueg. Our semi-decision procedures are complemented and motivated by an undecidability proof for FTDA verification which holds even in the absence of interprocess communication. To the best of our knowledge, this is the first paper to achieve parameterized automated verification of Byzantine FTDA.

cs.LO↗

arXiv2012

Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms

Fault-tolerant distributed algorithms are central for building reliable spatially distributed systems. Unfortunately, the lack of a canonical precise framework for fault-tolerant algorithms is an obstacle for both verification and deployment. In this paper, we introduce a new domain-specific framework to capture the behavior of fault-tolerant distributed algorithms in an adequate and precise way. At the center of our framework is a parameterized system model where control flow automata are used for process specification. To account for the specific features and properties of fault-tolerant distributed algorithms for message-passing systems, our control flow automata are extended to model threshold guards as well as the inherent non-determinism stemming from asynchronous communication, interleavings of steps, and faulty processes. We demonstrate the adequacy of our framework in a representative case study where we formalize a family of well-known fault-tolerant broadcasting algorithms under a variety of failure assumptions. Our case study is supported by model checking experiments with safety and liveness specifications for a fixed number of processes. In the experiments, we systematically varied the assumptions on both the resilience condition and the failure model. In all cases, our experiments coincided with the theoretical results predicted in the distributed algorithms literature. This is giving clear evidence for the adequacy of our model. In a companion paper, we are addressing the new model checking techniques necessary for parametric verification of the distributed algorithms captured in our framework.

cs.FL↗