Follow blockchain research across journals, conferences, and preprint repositories.
28 results · page 1 of 2
Jing Yee Tan, Yuanzhang Zhao, Wai-Ki Ching
No abstract is available for this record.
Usman Zafar
Abstract The SIS‑10 framework establishes a typed, invariant preserving safety calculus for cyber physical systems. It unifies temporal semantics, schedulability, semantic preservation, ML admissibility, cryptographic verification, and risk bounded control into a single mathematically coherent architecture. All domains and operators are fully explicit, enabling formal reasoning over system trajectories and safety envelopes. The temporal layer defines an ordered metric structure with drift aware bounded causality, interval set operators, and jitter robust event semantics. The QoS layer enforces schedulability and feasible actuation, ensuring that all control actions remain within admissible timing and load bounds. Semantic compression provides a safety preserving homomorphism that guarantees invariants survive dimensionality reduction. Multi‑modal fusion introduces cross sensor falsifiability, enabling fault detection through probabilistic disagreement. The ML layer is input validated and logic embedded, ensuring that all model outputs entail the SIS‑10 invariant set. The cryptographic layer supplies zero knowledge execution trace proofs, allowing runtime verification of transition correctness without revealing internal state. Predictive shutdown optimization is constrained by a formally defined safety envelope, ensuring that operational objectives never violate admissible safety bounds. Cyber physical risk evolves through a bounded monotone propagation model with explicit mitigation operators, while the Safety Twin provides deterministic and stochastic discrete time system dynamics. The inductive proof layer establishes global invariant preservation for all admissible executions, and the event→action mapping connects the formal calculus to real SIS triggers. SIS‑10 therefore constitutes a unified, verifiable, and implementation ready safety architecture, suitable for runtime assurance, cyber‑physical certification, and next generation functional safety systems. Further enhancements include graphical formalization, parameterized system tuning, implementation DSLs, and automated verification scripts, none of which alter the core mathematical model..
Amin Karami, Mogos Anday Gebremedhin
No abstract is available for this record.
Vimal Teja Manne
Address verification and spend limit checks in card and instant payment systems expose cardholder ZIP codes and velocity histories to gateways and intermediaries, which increases the privacy impact of breaches. At the same time, issuers rely on these checks to control fraud within strict two to three hundred millisecond authorization budgets. This paper presents ZK-AVS, a design that replaces plaintext AVS and spend limit evaluation with zero knowledge proofs produced on the customer device and verified at the payment gateway. The issuer stores commitments to the cardholder ZIP and per window spend counters, and the device proves that its ZIP matches the committed value and that the proposed transaction keeps cumulative spend within the configured limit, without revealing the underlying values. We instantiate a synthetic workload of fifty thousand transactions and show that AVS mismatch and limit pressure carry useful fraud signal that can be exposed as proof outcomes. The design is structured to fit within sub three hundred millisecond budgets on commodity devices, while removing direct exposure of address and spend history data at the gateway and keeping changes largely at endpoints.
Mehdi Beriane, Muhammed Ali Bingöl
No abstract is available for this record.
Oleksandr Kuznetsov, Anton Yezhov, Alexandr Kuznetsov, Valentyn Chernushevych · 5 authors
No abstract is available for this record.
Andrea Esposito, Francesco Rossi, Marco Bernardo, Francesco Fabris · 5 authors
Algorand is a scalable and secure permissionless blockchain that achieves proof-of-stake consensus via cryptographic self-sortition and binary Byzantine agreement. In this paper we present a process algebraic model of the Algorand consensus protocol with the aim of enabling formal verification. Our model captures the behavior of participants in terms of the structured alternation of consensus steps toward a committee-based agreement. We validate the correctness of the protocol in the absence of adversaries and then extend our model to assess the influence of coordinated malicious nodes that can force the commit of an empty block instead of the proposed one. The adversarial scenario is analyzed through an equivalence-checking-based noninterference framework that we have implemented in the CADP verification toolkit. In addition to highlighting both the robustness and the limitations of the Algorand protocol under adversarial assumptions, this work illustrates the added value of using formal methods for the analysis of consensus algorithms within blockchains.
Yuliia Horbenko
Web Assembly (Wasm) and blockchain technology offer a viable solution for reliable and high-performance front-end systems. Wasm provides high execution speeds by incorporating code from high-level languages to improvise on performance limitations. Its sand-boxed execution model enhances security by extenuating memory-related weaknesses. Similarly, blockchain reinforces security with decentralized, tamper-resistant data structures and smart contracts. Conventional blockchain frameworks often suffer from computational overhead, but Wasm-based execution platforms like Polkadot and EOS optimize resource utilization and improve interoperability. This integration facilitates high-speed, reliable interactions in decentralized applications (dApps). Potential benefits include fast and secure off-chain computations, hence reducing blockchain congestion in front-end frameworks. However, challenges remain in securing Wasm execution in decentralized environments and optimizing blockchain and Wasm interoperability. A promising direction is to exploit Just-In-Time (JIT), Ahead-of-Time (AOT) compilation schemes along with zero-knowledge proofs to further enhance performance and security characteristics. By coupling Wasm’s efficiency with blockchain’s security, scalable and decentralized front-end systems are evolving to meet challenging web demand scenarios.
Beth Probert, Ruaridh Clark, Erik Blasch, Malcolm Macdonald
As the density of objects in Low Earth Orbit continues to increase, greater levels of coordination among satellites are needed to ensure the continued operation and sustainability of the space environment. Existing centralised space governance frameworks suffer from delays, ambiguity, and vulnerability to manipulation, introducing further complexity and risk into satellite operations, and hindering the development of new space-based services. This review examines the feasibility of leveraging Distributed Ledger Technologies to facilitate secure, decentralised, and autonomous coordination among satellites, conceptualised as an extension of Internet of Things networks. By examining analogous applications in swarms of Uncrewed Aerial Systems, and the Internet of Things, key system requirements for decentralised satellite coordination are defined. It is found that traditional Blockchain systems using Proof of Work-based consensus mechanisms are impractical for use in space-based systems, whilst Directed Acyclic Graph architectures, Sharded Blockchain architectures, and non-deterministic Proof of Stake consensus mechanisms are the most suitable. Critical gaps preventing the implementation of Distributed Ledger Technologies in the space environment are identified. These include wider regulatory considerations, and technical obstacles relating to the storage of transactional data and reaching consensus in time-varying, asynchronous networks.
Nuno Neto, Rolando Martins, Luís Veiga
Over the last few decades, a large body of research was carried out covering Byzantine Fault Tolerance (BFT) systems. This research has brought forward new techniques, including but not limited, for ordering operations (Abraham et al., 2018; Buchman, 2016; Guo et al., 2020; Bessani et al., 2014; Duan et al., 2018) and state transfer (Bessani et al., 2013; Distler, 2021 , Eischer et al., 2019 ), on networks that suffer from byzantine faults. More recently, the ongoing research on distributed ledgers re-ignited the interest on BFT, due to its high throughput when compared to other alternatives of byzantine consensus ( Vukolić, 2016 ). In this paper we present three contributions covering several aspects, including modular and extensible framework design and implementation, system optimization through development of better networking alternatives, a greater use of parallelism, several ordering protocol improvements and extensive comparative assessment of previous state-of-the-art approaches. First, we introduce Atlas, an open-source modular BFT framework that aims to support the research and development of highly efficient BFT protocols, by decoupling traditionally entangled sub-protocols, e.g., consensus primitive from the execution (Bessani et al., 2014), and deferment of log management to replicated services from state transfer. Atlas allows to further provide modules that can be re-used across different BFT approaches, such as deterministic and probabilistic/randomized models. Second, we present FeBFT, a new BFT implementation developed upon Atlas that combines pre-existing proven ideas from PBFTs, namely its 3-phase consensus and view-change protocol. This base approach is then extended with novel optimizations of the protocol, namely, multi-leader proposals (Stathakopoulou et al., 2019), multi-instance consensus execution (Stathakopoulou et al., 2022; Behl et al., 2015), and configurable batching solution that allow us to reduce the latency while improving throughput at the same time. Third, we offer a comprehensive evaluation amongst our work and other state-of-the-art BFT-SMR implementations, namely, Atlas ( Anon, 2024a ) with FeBFT (Official febft repository 2024), BFT-SMaRt (Bessani et al., 2014) and Themis (Rüsch et al., 2019). With these contributions, we aim to lay the ground work to: (i) improve reusability and hence productivity in BFT(-SMR) development; (ii) increase system safety, performance, scalability and reduce recovery time with the optimizations proposed; (iii) draw insights on the bottlenecks preventing order-of-magnitude improvements in BFT processing from a system’s perspective; and lastly, (iv) improve reproducibility between different BFT (sub-)protocols by allowing for true apples-to-apples comparisons. • Atlas, an open-source, modular BFT framework designed to support the efficient development of BFT protocols by separating traditionally intertwined sub-protocols and allowing for reusable modules across different BFT approaches. • FeBFT, introduces a novel BFT implementation leveraging the Atlas framework, which boosts protocol efficiency via multi-leader proposals and multi-instance consensus execution. It incorporates a batching solution designed to scale with network throughput, prioritizing this over network latency while maintaining the configurability to be tuned for low latency if needed. • Focusing on the essential need for reproducibility in scientific evaluation, Atlas provides a critical framework for accurate comparisons between different protocols. By offering a modular and reusable architecture, it significantly reduces the workload for system researchers in developing and testing implementations. This approach ensures a true apple-to-apple comparison, enabling a more precise and reliable assessment of protocol performance and efficacy. • And lastly, a comprehensive evaluation comparison with two well-known BFT-SMR (deterministic) implementations, namely, BTF-SMaRt and Themis, against FeBFT, our PBFT implementation that uses Atlas.
Ana Kovačević, Nenad Gligorić
The increasing connectivity and complexity of automotive systems require enhanced mechanisms for firmware updates to ensure security and integrity. Traditional methods are insufficient for modern vehicles that require seamless over-the-air (OTA) updates. Current OTA mechanisms often lack robust security measures, leaving vehicles vulnerable to attacks. This paper proposes an innovative approach based on the use of decentralized identifiers (DIDs) and distributed ledger technology (DLT) for secure OTA firmware updates of on-vehicle software. By utilizing DIDs for unique vehicle identification, as well as verifiable credentials (VCs) and verifiable presentations (VPs) for secure information exchange and verification, the solution ensures the integrity and authenticity of software updates. It also allows for the revocation of specific updates, if necessary, thereby improving overall security. The security analysis applied the STRIDE methodology, which enabled the identification of potential threats, including spoofing, tampering, and privilege escalation. The results showed that our solution effectively mitigates these threats, while a performance evaluation indicated low latency during operations.
Naseeruddin Lodge, Nahush Tambe, Fareena Saqib
The rapid advancement of technology, alongside state-of-the-art techniques is at an all-time high. However, this unprecedented growth of technological prowess also brings forth potential threats, as oftentimes the security encompassing these technologies is imperfect. Particularly within the automobile industry, the recent strides in technology have brought about increased complexity. A notable flaw lies in the CAN-FD protocol, which lacks robust security measures, making it vulnerable to data theft, injection, replay, and flood data attacks. With the rising complexity of in-vehicular networks and the widespread adoption of CAN-FD, the imperative to safeguard the protocol has never been more crucial. This paper aims to provide a comprehensive review of the existing in-vehicle communication protocol, CAN-FD. It explores existing security approaches designed to fortify CAN-FD, demonstrating multiple multi-layer solutions that leverage modern techniques including Physical Unclonable Function (PUF), Elliptical Curve Cryptography (ECC), Ethereum Blockchain, and Smart contracts. The paper highlights existing multi-layer security measures that offer minimal overhead, optimal performance, and robust security. Moreover, it identifies areas where these security measures fall short and discusses ongoing research along with suggestions for implementing software and hardware-level modifications. These proposed changes aim to streamline complexity, reduce overhead while ensuring forward compatibility. In essence, the methods outlined in this study are poised to excel in real-world applications, offering robust protection for the evolving landscape of in-vehicular communication systems.
Edvardas Dlugauskas, Karolis Petrauskas
The IOTA Extended UTXO (IOTA EUTXO) model extends the UTXO blockchain to include features like smart contracts and non-fungible tokens. In this work, we show that the IOTA EUTXO model maintains the base correctness properties of the UTXO model while extending it with extra functionality. We achieve this by specifying and verifying the essential concepts of the base UTXO model and the extensions proposed by IOTA using the Isabelle proof assistant. The specification is designed to be modular and extensible, meaning it can be used as a foundation for further research of the UTXO and IOTA EUTXO models.
Cezara Drăgoi, Srinidhi Nagendra, Mandayam Srivas
No abstract is available for this record.
Zhigang Xu, Duoyue Liao, Xinhua Dong, Hongmu Han · 6 authors
Hyperledger Fabric, which satisfies decentralization and security, is one of the most popular blockchain distributed ledger technologies, but in high-throughput, high-concurrency distributed scenarios, concurrency conflicts can cause transactions to fail, resulting in significant network bandwidth and resource waste. In this paper, we deeply analyze the operation flow of Fabric’s underlying transactions, and propose a solution to concurrent transaction conflicts in Fabric based on distributed locks and message queues. Redis is used to implement the locking mechanism of concurrent keys, and the ChaincodeEvent event listener is used to detect the transactions and realize the unlocking operation; on this basis, the message asynchronous retry mechanism, i.e., use the message queue RabbitMQ to re-consume the conflicting transactions to solve the concurrent transaction conflicts encountered against Fabric at present. Experiments show that the proposed approach can significantly improve the concurrency capability of the system, including transaction success rate and effective transaction throughput, under different levels of transaction conflicts; it does not affect the performance of the system in the absence of transaction conflicts.
Nickolas Carter, Duane Davis, Cynthia E. Irvine, Peter Pommer
Autonomous multi-vehicle systems are becoming increasingly relevant in military operations and have demonstrated potential applicability in civilian environments as well. A problem emerges, however, when logging data within these systems. In particular, potential loss of individual vehicles and inherently lossy and noisy communications environments can result in the loss of important mission data. This paper describes a novel distributed ledger protocol that can be used to ensure that the data in such a system survives and documents verification of the behavioral correctness of this protocol using informal verification methods and tools provided by the Monterey Phoenix project.
Peter Pommer
Autonomous vehicle systems, including multi-vehicle systems, are becoming increasingly relevant in military operations. A problem emerges, however, when logging data within these systems. In particular, loss of individual vehicles and inherently lossy and noisy communications environments can result in the loss of important mission data. This thesis presents a novel distributed ledger protocol that can be used to ensure that the data in such a system survives. To test the efficacy of the protocol, we implemented it as a Robot Operating System (ROS) node on the Advanced Robotic Systems Engineering Laboratory (ARSENL) aerial swarm system. Results are presented for implementation tests in the ARSENL software-in-the-loop simulation environment and during live-flight field experiments conducted at Camp Roberts, CA.
Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni · 5 authors
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.
Cosimo Laneve, Adele Veschetti
We study Nakamoto’s Bitcoin protocol that implements a distributed ledger on peer-to-peer asynchronous networks. In particular, we define a principled formal model of key participants - the miners - as stochastic processes and describe the whole system as a parallel composition of miners. We therefore compute the probability that ledgers turn into a state with more severe inconsistencies, e.g. with longer forks, under the assumptions that messages are not lost and nodes are not hostile. We also study how the presence of hostile nodes mining blocks in wrong positions impacts on the consistency of the ledgers. Our theoretical results agree with the simulations performed on a probabilistic model checker that we extended with dynamic datatypes in order to have a faithful description of miners' behaviour.
Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian · 6 authors
No abstract is available for this record.
Anna Klimenko, Irina Safronenkova
Abstract In the current paper the issues of the workload relocation in the fog- and edge-computing environments are in-question. The workload relocation problem is closely connected to the scheduling problems, yet, outside the cloud there is almost unlimited number of nodes to place the computational tasks. So the search space for the optimization problem grows, and the time of the workload relocation degrades. We emphasize the techniques to limit the set of candidate nodes for the tasks distribution. In the paper two approaches are proposed and considered in terms of time consumption. The simple models are developed with the following simulation. Also the distributed-ledger-based modifications of the techniques are proposed and examined.
Christian Berger, Birgit Penzenstadler, Olaf Drögehorn
Innovation in the world of today is mainly driven by software. Companies need to continuously rejuvenate their product portfolios with new features to stay ahead of their competitors. For example, recent trends explore the application of blockchains to domains other than finance. This paper analyzes the state-of-the-art for safety-critical systems as found in modern vehicles like self-driving cars, smart energy systems, and home automation focusing on specific challenges where key ideas behind blockchains might be applicable. Next, potential benefits unlocked by applying such ideas are presented and discussed for the respective usage scenario. Finally, a research agenda is outlined to summarize remaining challenges for successfully applying blockchains to safety-critical cyber-physical systems.
Sanjit A. Seshia, Shiyan Hu, Wenchao Li, Qi Zhu
A cyber-physical system (CPS) is an integration of computation with physical processes whose behavior is defined by both computational and physical parts of the system. In this paper, we present a view of the challenges and opportunities for design automation of CPS. We identify a combination of characteristics that define the challenges unique to the design automation of CPS. We then present selected promising advances in depth, focusing on four foundational directions: combining model-based and data-driven design methods; design for human-in-the-loop systems; component-based design with contracts, and design for security and privacy. These directions are illustrated with examples from two application domains: smart energy systems and next-generation automotive systems.
M. Teresa Higuera‐Toledano, Uwe Brinkschulte, Achim Rettberg
The increasing complexity of contemporary embedded computing systems requires the use of self-management in order to handle unforeseen changes in both hardware and application environments (i.e., hardware/software defects, resource changes, and non-continual feature usage). Moreover, often these systems are distributed, running on processor architectures with multiple cores, which may require self-organization to ensure efficiency and reliability. Real-time properties are another key issue in many complex systems. Adaptive and self-organized properties extent the area of operations and improves the efficiency of the system resources at the cost to introduce additional complexity, overhead, and resource requirements. Consequently, real-time adaptive systems must be careful analyzed, designed, and built taken into account the right tradeoffs between flexibility and complexity, while accomplishing time-constrains. The combination of the flexibility and uncertain behavior of self-organizing systems with time-predictability is a grand challenge. Therefore, substantial research has been done in the last years to address the so-called Self-X features (e.g., self-configuration, self-optimization, self-adaptation, self-healing, and self-protection). This fact has as resutl that self-organizing computing systems become an established research nowadays as they promise to handle the increasing complexity resulting from highly distributed systems and ubiquitous applications. In addition, real-time properties are required in many areas (such as cyber physical systems) self-organizing computing systems are dealing with. Combining the flexible and and uncertain behavior of self-organizing systems with time-predictability necessary for real-time systems is a grand challenge. The Workshop on Self-Organizing Real-Time Systems (SORT) is specifically dedicated to research on adaptive real-time systems. SORT started 2014 as a workshop attached at International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC). The purpose of this workshop is to provide an open forum to discuss new and ongoing research that is centered on the idea of adaptability in real-time systems. The target audience includes researchers from academia, tool vendors, system suppliers, and users in industry who are interested in the all aspects of the topics mentioned below. This special issue of Concurrency and Computation: Practice and Experience contains four invited papers from the SORT 2014 workshop that has been expanded and carefully peer reviewed. The first paper, titled An Artificial DNA for Self-Descripting and Self-Building Embedded Real-Time Systems 1, Uwe Brinkschulte proposes an approach to use an artificial DNA-based approach for embedded real-time and distributed systems. This kind of systems is growing more and more complex because of the increasing chip integration density, larger number of chips in distributed applications and demanding application fields (e.g., in cars and in households). Bio-inspired techniques like self-organization are a key feature to handle this complexity. Because many embedded systems can be composed from a limited number of basic elements, the structure and parameters of such systems can be stored in a compact way representing an artificial DNA deposited in each computation node. This leads to a self-describing system. Based on the DNA, the self-organization mechanisms can build the system autonomously providing a selfbuilding system. System repair and optimization at runtime are also possible, leading to higher robustness, dependability, and flexibility. Autonomous adaptation in self-adapting embedded real-time systems introduces novel risks as it may lead to unforeseen system behavior. An anomaly detection framework integrated in a real-time operating system can ease the identification of such suspicious novel behavior and, thereby, offers the potential to enhance the reliability of the considered self-x system. However, anomaly detection is based on knowledge about normal behavior. When dealing with self-reconfiguring applications, normal behavior changes. Hence, knowledge base requires adaptation or even reconstruction at runtime. The stringent restrictions of real-time systems considering runtime and memory consumption make this task to a really challenging problem. In next paper, Two-Level Extensions of an Artifical Hormone System 2, Mathias Pacher describes a decentralized software which is able to allocate tasks in a system of heterogeneous processing elements. Tasks are allocated according to their suitability for the heterogeneous processing elements, the current processing element and task relationships. This software provides properties like self-configuration, self-optimization, and self-healing in the context of task allocation. In addition, it is able to guarantee real-time bounds for such self-X-properties. However, using self-organization principles introduces increased system complexity such as control of system parameters for self-organization and additional communication effort, which have been addressed by using a hierarchic structure. This solution uses a machine learning approach presenting an Observer-/Controller architecture. The user has to provide a simple set of initial rules and the Observer-/Controller is able to generate new rules if needed. This paper also presents a hierarchical structure to save communication bandwidth, which consists of several different clusters of processing elements where each cluster has its own communication infrastructure (e.g., a bus system). In the paper titled Online behavior classification for anomaly detection in self-x real-time systems 3, Katharina Stahl presents an online construction of application behavior knowledge that does not rely on training phase. The applications' behavior is defined by the application's system call invocations. For the knowledge base, they use Suffix Trees to represent application behavior patterns and associated information in a compact manner. The online algorithm provided by Suffix Trees is a basis to construct the knowledge base with low computational effort. Anomaly detection and classification is integrated into the online construction method. New behavioral patterns do not unconditionally update the behavior knowledge base. They are evaluated in a context-related manner inspired by Danger Theory, a special discipline of Artificial Immune Systems. For highly safety-critical applications, rigorous offline verification should be complemented by online verification. One promising technique is Online Model Checking (OMC). As OMC is a run- time-provided service, it seems to be natural providing it by an operating system service like any other service offered by the OS. In the paper titled Efficient Integration of Online Model Checking into a Small-Footprint Real-time Operating System 4 the authors study the feasibility of integrating OMC as an RTOS service. In order to ease understanding the approach, the paper discusses various integration methods in which OMC runs concurrently to the application task to be online model checked. The OMC may become: (i) an integral part of the RTOS, (ii) a separate task running on the same host as the RTOS, or (iii) a remote host as a kind of service-oriented architecture.