Salience-Queue Occupation Theory (SQOT) is a protocol-relative mathematical framework for analyzing when finite-budget operational processes lose effective control over their priority queues under persistent or adversarial salience sources. The manuscript formalizes salience occupation using observable histories, budget ledgers, diagnostic reserves, queue morphisms, finite certificate grammars, checkable ledgers, typed risk composition, self-auditing kernels, and route-sound checker semantics. The theory is designed for artificial, distributed, or post-biological operational systems, but it does not rely on subjective psychology or normative claims about what a process should attend to. Instead, it studies finite, auditable conditions under which a process can preserve diagnostic capacity, response or no-action availability, rollback or quarantine options, semantic-egress safety, mechanism-compatible incentives, and bounded verification cost. The results include finite checker semantics soundness, checked non-circular sovereignty certificates, typed risk composition, adaptive succinct-session soundness, egress abstraction refinement, and payoff-reflected mechanism robustness. SQOT explicitly limits its claims to declared validity domains and does not assert absolute physical, cryptographic, economic, or base-reality guarantees.
Abstract The traditional Byzantine quorum-system model assumes a pre-existing, global agreement on the set of quorums (typically defined as the sets consisting of more than two-thirds of the participants). This assumption is problematic in permissionless systems, which strive to allow anyone to join or leave the system dynamically. While proof-of-stake permissionless systems like Ethereum require newly joining participants to register into the system, other permissionless systems like the Ripple Ledger or the Stellar network allow participants to join the system without synchronization by forgoing agreement on the set of quorums. This results in what we call a heterogeneous quorum system, where each participant has its own, personal set of quorums. An important question is to determine under what condition is it possible to solve synchronization problems like reliable broadcast or consensus in a heterogeneous quorum system. In this work, we show that the traditional quorum intersection and quorum availability conditions are not sufficient in heterogeneous quorum systems. Moreover, we propose quorum subsumption, a new condition which, together with quorum availability and quorum intersection, is sufficient to allow solving reliable broadcast and consensus. Finally, we propose protocols for reliable broadcast and consensus in heterogeneous quorum systems that satisfy quorum subsumption. In particular, we present a practical consensus protocol called Satrapy which in contrast to abstract consensus protocols uses finite state and messages.
Blockchain Technology has presented a tamperproof and secure structure that supports the modern digital environment. Among the many consensus blockchain systems, the Proof of Stake (PoS) has emerged as an extensively used protocol due to its lower energy consumption and high security. However, the staking mechanism and creation of the validator process are the main parts of the PoS network, and any flaw in these processes can cause financial loss and breach the system's security. Therefore, we use formal verification methods for the verification and validation of the staking mechanism. In this study, we presented a formal model of staking processes in a PoS-based system, emphasizing the verification of accurate signer, stake allocation, creation of a validator with an NFT minted, and update timeline. The CSP\# language is used to specify these processes, and Linear Temporal Logics (LTL) are used to define the properties against these specifications. To verify that the system satisfies the critical properties, like verification of an authentic signer, secure stake registration, and deadlock-free validator creation using the Process Analysis Toolkit (PAT) model checker, and ensure the system's liveness and safety. Our results describe the importance of formal verification in enhancing the Polygon Blockchain's integrity by ensuring the staking mechanism in the stake manager contract is secure and reliable.
Sidechains offer partial solutions to Ethereum’s scalability challenges; however, they introduce trade-offs related to security and implementation complexity. These limitations have been further addressed by Layer-2 solutions known as rollups, which combine off-chain computation with on-chain verification, preserving both security and decentralization on the Ethereum platform. This paper proposes a Stochastic Petri Net model to evaluate the feasibility of ZK-Rollups by analyzing their impact on throughput and latency. The results indicate that increased adoption of Layer-2 transactions can enhance system throughput by up to 20%. Conversely, latency may rise by more than 100% when larger batches are used, revealing a fundamental performance trade-off.
Federated cyber–physical systems (CPSs) present unique security challenges due to their distributed nature and the need for secure communication between components from different administrative domains. Distributed ledger technology (DLT) offers a promising approach to implementing a resilient authentication and authorization mechanism and an immutable record of CPS identities and transactions in federated environments. However, using Distributed Ledger (DL) within a CPS raises some important questions regarding scalability, throughput, latency, and potential bottlenecks, which require effective modeling of DL performance. This paper proposes a novel approach to modeling distributed ledgers using Colored Timed Petri Nets (CPNs). We focus on the performance modeling of Hyperledger Fabric (HLF), a permissioned distributed ledger technology which provides a backbone for a Lightweight Authentication and Authorization Framework for Federated IoT (LAAFFI), a novel framework for secure communication between CPS devices. We implement our model using CPN Tools, a widely adopted CPN modeling software that provides advanced simulation, analysis, and performance monitoring features. Our model offers a robust framework for studying distributed ledger systems’ synchronization, throughput, and response time. It supports flexibility in modeling transaction validation and consensus algorithms, which provides an opportunity for adapting the model to future changes in HLF and modeling other DLs. We successfully validate our CPN model by comparing simulation results with experimental measurements obtained from a LAAFFI prototype.
Muhammad Ikram Mohd Rashid, Imran Rasool, Nazir Ahmad Zafar, Hamra Afzaal
The Ethereum 2.0 Beacon chain is a big step toward improving the security, scalability, and decentralization. It is based on the Proof of Stake (PoS) consensus protocol that maintains the validator status, attestation details, and many more. The term validator is introduced in the PoS consensus protocol and its work is to propose blocks and vote for them by becoming a committee member to add those blocks to the blockchain. We address the problem related to validator’s voluntary exit to vanish its active status and do its formal verification using the SPIN Model checker. There does not exist much research in this area as it was introduced recently in 2020. Further, this is the first work on formal verification of the beacon chain using the SPIN model checker. In this work, we formally specify the validator exit process of the Ethereum 2.0 Beacon Chain using the formal specification language, i.e., Process or Protocol Meta Language (PROMELA). We create a program graph for this process through the SPIN Model checker and describe safety and liveness properties using Linear temporal logic (LTL) in the form of a formula. The formal verification is performed to ensure correctness by giving the program graph and LTL formulas as input to the SPIN model checker whether the properties are satisfied with the program graph
Dmitry A. Zaitsev, Tatiana R. Shmeleva, Zeyu Zhou, Ding Liu
The reliability of consensus protocols establishes the basis for cryptocurrency cybersecurity. Formal and simulation techniques are appreciated for the verification of proof-of-work agreement protocols, because the formal techniques development process frequently requires a series of assumptions, leading to somewhat unrealistic models. A conventional colored Petri net model, presented by the authors in a previous study, allowed us to refine the Keller and Böhme consensus protocol by applying the simulation technique. In this study, we developed a reenterable colored Petri net model representing a general construct for model-driven development and refinement of consensus protocols and the corresponding software. A considerable benefit of a reenterable model is the invariance of its structure with respect to the net topology, number of attached nodes, and parameters of their software and hardware, which are represented as the marking of dedicated places. Switching of topology tags associated with dynamic objects represents the basic principle of reenterable model functioning. It is shown that, having the same characteristics, in bounds of admissible error of some 2-3%, the reenterable model results in 6 times speed-up of the simulation process and a drastic decrease in time for model editing, especially when the number of nodes exceeds a hundred. Thus, a reenterable model is a valuable complement to possible formal models that allows us to obtain express-evaluations of characteristics in a rather short time and with an acceptable level of adequacy.
The Blockchain 2.0 era integrated with smart contract along with its platforms and applications have experienced explosive growth in recent years. However, many smart contracts deployed in practice are prone to errors and cannot be modified due to the immutability of the blockchain. In light of this, it is vital to ensure the security of correctness of smart contracts before deployment. This paper proposes a formal modeling method based on Timed Colored Petri net (TCPN) to anlyze smart contracts with time constrains. We apply this formalism to a concrete voting contract system. Its functional requirements are formalized by the improved computing timing logic ASK-CTL with ML (Meta Language). Simulation and experiment show that the security and reliability of the voting contract can be effectively guaranteed.
The formal description and verification of networks of cooperative and interacting agents is made difficult by the interplay of several different behavioral patterns, models of communication, scalability issues. In this paper, we will explore the functionalities and the expressiveness of a general-purpose process algebraic framework for the specification and model checking based analysis of collective and cooperative systems. The proposed syntactic and semantic schemes are general enough to be adapted with small modifications to heterogeneous application domains, like, e.g., crowdsourcing systems, trustworthy networks, and distributed ledger technologies.
Smart contracts are programs that are stored on a blockchain ledger with code immutable after deployment. Thus, verifying the correct behavior of smart contracts before deployment is vital. This paper demonstrates how a security vulnerability verification in a casino smart contract can be transformed to non-blocking verification. To this end, the contract is first modeled as interacting extended finite state machines (EFSM), with one EFSM for each function. Modeling the security vulnerability as a condition in the EFSM system, non-blocking verification reveals the system to be blocking. Investigating the counterexample produced by the verification shows that a transfer that is refused by its receiver may block the casino so that all remaining funds are forever locked into the contract, thus revealing a severe vulnerability. It is then demonstrated how the same technique can show the absence of this vulnerability, by verifying that the EFSM model of an improved casino contract is indeed non-blocking.
The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially permit modular, scalable verification approaches that mimic their modular design. We address this need for verification of distributed agreement-based systems through our novel modeling and verification framework, QuickSilver, that is not only modular, but also fully automated. The key enabling feature of QuickSilver is our encoding of abstractions of verified agreement protocols that facilitates modular, decidable, and scalable automated verification. We demonstrate the potential of QuickSilver by modeling and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more.
Attribute-based cryptography becomes one of the hot topics in cryptography, since it can provide fine-grained access control and good privacy. Σ-protocol is a 3-move public-coin honest verifier zero-knowledge proof protocol, and has important applications in many fields of cryptography. Firstly, combining the concept of attribute-based cryptography with the zero-knowledge proof, a notion of attribute-based Σ-protocol is introduced with its formal security model. Secondly, based on the standard Σ-protocol, the trapdoor samplable relation and the smooth secret sharing, a general construction of decentralized attribute-based Σ-protocol and corresponding scheme are proposed with the proofs of its securities. Finally, as the applications of decentralized attribute-based Σ-protocol, general constructions of decentralized attribute-based signature and decentralized attribute-based two-tier signature are presented by Fiat-Shamir transformation, respectively. Some concrete schemes are also presented. Performance analysis shows that the proposed attribute-based two-tier signature scheme has obvious advantages in both sizes and computation costs compared with existing schemes.
In the process of Accounting Information System (AIS), the business transactions are generated by heterogeneous distributed applications. The business transactions result in T-accounts set up in the General Ledger System (GLS). The requirement changes maybe affect the screen scraping procedure of the business transactions interfaces, and also result in the issues of GLS process, system and control. In this paper, we propose a framework and alternative way to verify the business transaction interfaces of GLS in the early stage using the model checking technique. The GLS abstraction model are modeled using Colored Petri Net (CPN). Next, we verify the obtained CPN model using CPN tools to validate the GLS interfaces.
The growing use of computers in modern control systems has led to the develop- ment of complex dynamic systems known as hybrid systems, which integrates both discrete and continuous systems. Given that hybrid systems are systems that operates in real time allowing for changes in continuous state over time periods, and discrete state changes across zero time, their modelling, analysis and verification becomes very difficult. The formal verifications of such systems based on specifications that can guar- antee their behaviour is very important especially as it pertains to safety critical applications. Accordingly, addressing such verifications issues are important and is the focus of this thesis. In this thesis, in order to actualise the specification and verification of hybrid systems, Interval Temporal Logic(ITL) was adopted as the underlying formalism given its inherent characteristics of providing methods that are flexible for both propositional and first-order reasoning regarding periods found in hardware and software system’s descriptions. Given that an interval specifies the behaviour of a system, specifications of such systems are therefore represented as a set of intervals that can be used to gain an understanding of the possible behaviour of the system in terms of its composition whether in sequential or parallel form. ITL is a powerful tool that can handle both forms of composition given that it offers very strong and extensive proof and specifi- cation techniques to decipher essential system properties including safety, liveliness and time projections.However, a limitation of ITL is that the intervals within its framework are considered to be a sequence of discrete states. Against this back- drop, the current research provides an extension to ITL with the view to deal with verification and other related issues that centres around hybrid systems. The novelty within this new proposition is new logic termed SPLINE Interval Temporal Logic (SPITL) in which not only a discrete behaviour can be expressed, but also a continuous behaviour can be represented in the form of a spline i.e. the interval is considered to be a sequence of continuous phases instead of a sequence of discrete states. The syntax and semantics of the newly developed SPITL are provided in this thesis and the new extension of the interval temporal logic using a hybrid system as a case study. The overall framework adopted for the overall struc- ture of SPITL is based on three fundamental steps namely the formal specification of hybrid systems is expressed in SPLINE Interval Temporal Logic, followed by the executable subset of ITL, called Tempura, which is used to develop and test a hybrid system specification that is written in SPITL and finally a runtime verification tool for ITL called AnaTempura which is linked with Matlab in order to use them as an integrated tool for the verification of hybrid systems specification. Overall, the current work contributes to the growing body of knowledge in hybrid systems based on the following three major milestones namely: i. the proposition of a new logic termed SPITL; ii. executable subset, Tempura, integrated with SPITL specification for hybrid systems; and iii. the development of a tool termed Ana Tempura which is integrated with Matlab to ensure accurate runtime verification of results.
Energy management systems/supervisory control and data acquisition (EMS/SCADA) systems are usually geographically distributed and have operational organizations. They are changing in accordance with the various and varying environments, and they should be flexible enough to adapt to those changes quickly. The paper proposes a new architecture called SCOPE (System Configuration of Power Control System) to realize flexible and reliable EMS/SCADA systems. SCOPE makes application programs independent of the operational organization and system configuration of the EMS/SCADA system, i.e., application programs are not influenced by changes in them. These properties make EMS/SCADA systems flexible and reliable, and also the development of EMS/SCADA systems becomes efficient and economical. Through developing and evaluating a SCOPE prototype system, it has been confirmed that the flexibility and maintainability of EMS/SCADA systems based on the SCOPE architecture has been improved.