arXiv subjects

Pavle Subotic

Publications and source records attributed to Pavle Subotic.

7 recordsLinked to original sources

arXiv2025

A Fast Ethereum-Compatible Forkless Database

The State Database of a blockchain stores account data and enables authentication. Modern blockchains use fast consensus protocols to avoid forking, improving throughput and finality. However, Ethereum's StateDB was designed for a forking chain that maintains multiple state versions. While newer blockchains adopt Ethereum's standard for DApp compatibility, they do not require multiple state versions, making legacy Ethereum databases inefficient for fast, non-forking blockchains. Moreover, existing StateDB implementations have been built on key-value stores (e.g., LevelDB), which make them less efficient. This paper introduces a novel state database that is a native database implementation and maintains Ethereum compatibility while being specialized for non-forking blockchains. Our database delivers ten times speedups and 99% space reductions for validators, and a threefold decrease in storage requirements for archive nodes.

cs.DB↗

arXiv2025

Efficient Forkless Blockchain Databases

Operating nodes in an L1 blockchain remains costly despite recent advances in blockchain technology. One of the most resource-intensive components of a node is the blockchain database, also known as StateDB, that manages balances, nonce, code, and the persistent storage of accounts/smart contracts. Although the blockchain industry has transitioned from forking to forkless chains due to improved consensus protocols, forkless blockchains still rely on legacy forking databases that are suboptimal for their purposes. In this paper, we propose a forkless blockchain database, showing a 100x improvement in storage and a 10x improvement in throughput compared to the geth-based Fantom Blockchain client.

cs.DB↗

arXiv2025

Provenance Guided Rollback Suggestions

Advances in incremental Datalog evaluation strategies have made Datalog popular among use cases with constantly evolving inputs such as static analysis in continuous integration and deployment pipelines. As a result, new logic programming debugging techniques are needed to support these emerging use cases. This paper introduces an incremental debugging technique for Datalog, which determines the failing changes for a \emph{rollback} in an incremental setup. Our debugging technique leverages a novel incremental provenance method. We have implemented our technique using an incremental version of the Souffl\'{e} Datalog engine and evaluated its effectiveness on the DaCapo Java program benchmarks analyzed by the Doop static analysis library. Compared to state-of-the-art techniques, we can localize faults and suggest rollbacks with an overall speedup of over 26.9$\times$ while providing higher quality results.

cs.LO↗

arXiv2025

Formal Model Guided Conformance Testing for Blockchains

Modern blockchains increasingly consist of multiple clients that implement a single blockchain protocol. If there is a semantic mismatch between the protocol implementations, the blockchain can permanently split and introduce new attack vectors. Current ad-hoc test suites for client implementations are not sufficient to ensure a high degree of protocol conformance. As an alternative, we present a framework that performs protocol conformance testing using a formal model of the protocol and an implementation running inside a deterministic blockchain simulator. Our framework consists of two complementary workflows that use the components as trace generators and checkers. Our insight is that both workflows are needed to detect all types of violations. We have applied and demonstrated the utility of our framework on an industrial strength consensus protocol.

cs.CR↗

arXiv2024

Reusable Formal Verification of DAG-based Consensus Protocols

Blockchains use consensus protocols to reach agreement, e.g., on the ordering of transactions. DAG-based consensus protocols are increasingly adopted by blockchain companies to reduce energy consumption and enhance security. These protocols collaboratively construct a partial order of blocks (DAG construction) and produce a linear sequence of blocks (DAG ordering). Given the strategic significance of blockchains, formal proofs of the correctness of key components such as consensus protocols are essential. This paper presents safety-verified specifications for five DAG-based consensus protocols. Four of these protocols -- DAG-Rider, Cordial Miners, Hashgraph, and Eventual Synchronous BullShark -- are well-established in the literature. The fifth protocol is a minor variation of Aleph, another well-established protocol. Our framework enables proof reuse, reducing proof efforts by almost half. It achieves this by providing various independent, formally verified, specifications of DAG construction and ordering variations, which can be combined to express all five protocols. We employ TLA+ for specifying the protocols and writing their proofs, and the TLAPS proof system to automatically check the proofs. Each TLA+ specification is relatively compact, and TLAPS efficiently verifies hundreds to thousands of obligations within minutes. The significance of our work is two-fold: first, it supports the adoption of DAG-based systems by providing robust safety assurances; second, it illustrates that DAG-based consensus protocols are amenable to practical, reusable, and compositional formal methods.

cs.LO↗

arXiv2019

Provenance for Large-scale Datalog

Logic programming languages such as Datalog have become popular as Domain Specific Languages (DSLs) for solving large-scale, real-world problems, in particular, static program analysis and network analysis. The logic specifications which model analysis problems, process millions of tuples of data and contain hundreds of highly recursive rules. As a result, they are notoriously difficult to debug. While the database community has proposed several data-provenance techniques that address the Declarative Debugging Challenge for Databases, in the cases of analysis problems, these state-of-the-art techniques do not scale. In this paper, we introduce a novel bottom-up Datalog evaluation strategy for debugging: our provenance evaluation strategy relies on a new provenance lattice that includes proof annotations, and a new fixed-point semantics for semi-naive evaluation. A debugging query mechanism allows arbitrary provenance queries, constructing partial proof trees of tuples with minimal height. We integrate our technique into Souffle, a Datalog engine that synthesizes C++ code, and achieve high performance by using specialized parallel data structures. Experiments are conducted with DOOP/DaCapo, producing proof annotations for tens of millions of output tuples. We show that our method has a runtime overhead of 1.27x on average while being more flexible than existing state-of-the-art techniques.

cs.PL↗

arXiv2014

Horn Clauses for Communicating Timed Systems

Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in industrial and academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now industrial-grade model checkers are available only for few timed automata dialects (in particular Uppaal timed automata), exhibit limited scalability for systems with large discrete state space, or cannot handle parametrised systems. We explore the use of Horn constraints and off-the-shelf model checkers for analysis of networks of timed automata. The resulting analysis method is fully symbolic and applicable to systems with large or infinite discrete state space, and can be extended to include various language features, for instance Uppaal-style communication/broadcast channels and BIP-style interactions, and systems with infinite parallelism. Experiments demonstrate the feasibility of the method.

cs.LO↗