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.
Amal Abdulbaqi Maryoosh, Ahmed Abd Ali Abdulkadhim, Muntaha AbdulzahraHatem
Block chain is a technology for securely storing data in a manner that makes system changes or hacks impossible or difficult. Numerous organizations have adopted this technology, which utilizes a peer-to-peer distributed network. Using a decentralized peer-to-peer network to operate. A block chain is a collection of linked computer systems that operate as a distributed ledger of transactions. Every new transaction that happens on the block chain is copied to each participant's ledger, and each block on the chain is made up of numerous transactions. This paper aims to explain block chain technology, including its uses and difficulties.
Orestis Alpos, Christian Cachin, Simon Holmgaard Kamp, Jesper Buus Nielsen
We present simple and practical protocols for generating randomness as used by asynchronous total-order broadcast. The protocols are secure in a proof-of-stake setting with dynamically changing stake. They can be plugged into existing protocols for asynchronous total-order broadcast and will turn these into asynchronous total-order broadcast with dynamic stake. Our contribution relies on two important techniques. The paper "Random Oracles in Constantinople: Practical Asynchronous Byzantine Agreement using Cryptography" [Cachin, Kursawe, and Shoup, PODC 2000] has influenced the design of practical total-order broadcast through its use of threshold cryptography. However, it needs a setup protocol to be efficient. In a proof-of-stake setting with dynamic stake this setup would have to be continually recomputed, making the protocol impractical. The work "Asynchronous Byzantine Agreement with Subquadratic Communication" [Blum, Katz, Liu-Zhang, and Loss, TCC 2020] showed how to use an initial setup for broadcast to asymptotically efficiently generate sub-sequent setups. The protocol, however, resorted to fully homomorphic encryption and was therefore not practically efficient. We adopt their approach to the proof-of-stake setting with dynamic stake, apply it to the Constantinople paper, and remove the need for fully homomorphic encryption. This results in simple and practical proof-of-stake protocols.
Shikaku is a pencil puzzle consisting of a rectangular grid, with some cells containing a number. The player has to partition the grid into rectangles such that each rectangle contains exactly one number equal to the area of that rectangle. In this paper, we propose two physical zero-knowledge proof protocols for Shikaku using a deck of playing cards, which allow a prover to physically show that he/she knows a solution of the puzzle without revealing it. Most importantly, in our second protocol we develop a general technique to physically verify a rectangle-shaped area with a certain size in a rectangular grid, which can be used to verify other problems with similar constraints.
Despite a considerable progress in verification of random and control logic, advances in formal verification of arithmetic designs have been lagging. This can be attributed mostly to the difficulty of efficient modeling of arithmetic circuits and data paths without resorting to computationally expensive Boolean methods, such as Binary Decision Diagrams (BDDs) and Boolean Satisfiability (SAT) that require ``bit blasting'', i.e., flattening the design to a bit-level netlist. Similarly, approaches that rely on computer algebra and Satisfiability Modulo Theories (SMT) methods are either too abstract to handle the bit-level complexity of arithmetic designs or require solving computationally expensive decision or satisfiability problems. On the other hand, theorem provers, popular solvers used in industry, require a significant human interaction and intimate knowledge of the design to guide the proof process. The work proposed in this thesis aims at overcoming the limitations of verifying arithmetic circuits, especially at the post-synthesis, implementation phase. It addresses the verification problem at an algebraic level, treating an arithmetic circuit and its specification as an algebraic system. Specifically, verification approach employed in this work is based on the algebraic rewriting method. In this method, the circuit is modeled in the algebraic domain, where both the circuit specification and its gate-level implementation are represented as polynomials. This work formally analyzes the algebraic approach and compares it with the established computer algebra methods based on Grobner basis reduction. It shows that algebraic rewriting is more effective than the Grobner basis reduction from the computational point of view. This thesis addresses two classes of arithmetic circuits that could not directly benefit from this type of functional verification, since performing algebraic rewriting of such circuits encounters a serious memory issue. The circuits that fall in the first category are approximate arithmetic circuits, such as truncated integer multipliers. Different truncation schemes are considered, including bit deletion, bit truncation, and rounding. The proposed verification method is based on reconstructing the truncated multiplier to a complete, exact multiplier; it is then followed by algebraic rewriting to prove that it indeed implements multiplication over the required range of bits. The reconstruction of the multiplier helps avoid the memory overload issue as it creates a "clean" multiplier with a well defined specification polynomial. The other class of circuits that suffer from memory overload during algebraic rewriting are circuits subjected to some arithmetic constraints. An example of such circuits is a divider, where the divisor value cannot be zero. The other example can be found in the basic blocks of the constant divider, where the value of carry into each block must be less than the divisor value. In general, such constraints will be modeled using the concept of vanishing monomials. A case-splitting method is proposed along with the modified algebraic rewriting to resolve the memory issue. The proposed verification method not only can prove that the circuit performs a correct function under the desired (valid) conditions, but also will test all the undesired (invalid) cases. This work also addresses logic debugging of combinational arithmetic circuits over field F<sub>2<sup>k</sup></sub> , including Galois field multipliers. Galois Field (GF) arithmetic has numerous applications in digital communication, cryptography and security engineering, and formal verification of such circuits is of prime importance. In addition to functional verification of GF multipliers, this work proposes a novel and effective method for identifying and correcting bugs in such circuits, commonly referred to as debugging. In this work we propose a novel approach to debugging of GF arithmetic circuits based on forward rewriting, which enables functional verification and debugging at the same time. This technique can handle multiple bugs, does not suffer from the polynomial size explosion encountered by other methods, and allows one to identify and automatically correct bugs in GF circuits. The techniques and algorithms proposed in this dissertation have been implemented in several computer programs, some stand-alone, and some integrated with a popular synthesis and verification tool, ABC. The experimental results for verification and debugging are compared with the state-of-the-art SAT, SMT, and other computer algebraic solvers.
The Android platform is undoubtedly the most popular platform for smartphones, with thousands of new applications becoming available daily and billions of app installations each year. Ethereum is the most popular smart contract platform, with thousands of applications on the blockchain serving as trading platforms and providing other functionalities. Due to these platforms’ popularity, security issues in their applications may reach a catastrophic scale with ease. Several prominent automated techniques help to reveal security problems in applications at the early stages of expansion. One such technique is static analysis. This thesis focuses on the design of static analysis techniques for Android apps and smart contracts distributed in the form of low-level code (bytecode).After installation, an Android app may get access to a set of sensitive information sources (e.g., location data). Unfortunately, exposure of such information to third parties has led in the past to several cases of privacy breach, and continues to be a serious threat. In this thesis, we tackle information flow propagation in the bytecode of Android applications by sound Horn-clause based abstraction techniques. This work will be the first to use Horn-clause based techniques in the context of security analysis. Moreover, we prove that our approach is sound, that is, our approach provides guarantees for its results. As a consequence, it can be used to show the absence of explicit data leaks in an app. Furthermore, Horn-clause based abstraction techniques are not limited to information propagation tasks, that is, our techniques can be used to show any kind of program property expressed as a reachability property. In addition, our Horn-clause based techniques scale to large codebases, benefit from the advancements in Satisfiability Modulo Theory solving, and allow for favorable performance with respect to the state-of-the-art. We instantiate the principles that were obtained while developing the analysis techniques for Android applications in the context of Ethereum smart contracts distributed in the form of Ethereum Virtual Machine (EVM) bytecode. Smart contracts are programs mainly used to perform financial operations (e.g., auctions) on cryptocurrency blockchains (e.g., Ethereum). Recent attacks demonstrate that certain vulnerabilities in smart contracts might cause severe money loss and an overall decrease of trust in the technology. Therefore, security analysis of EVM bytecode is in the focus of the research community. This thesis presents two results which establish the foundations for sound security analysis of EVM bytecode. First, the semantics of EVM bytecode is mechanized for the first time and tested against the official Ethereum test suite. This result facilitates both the design of analysis techniques and establishing their correctness properties. Second, this thesis provides the first sound Control Flow Graph reconstruction solution for EVM bytecode, that is, our analysis guarantees that reachable parts of the code are never pruned. This guarantee is required by a number of security properties for smart contracts. We also develop a tool implementing our analysis and successfully evaluate it on a big collection of real-world contracts.
This paper introduces the PoSH Consensus protocol, a novel work-in-progress construction for achieving Sybil-resistant Nakamoto-style probabilistic consensus on the contents of a cryptocurrency ledger in a permissionless decentralized network where parties stake their hardware’s computational power towards participation in leader election. PoSH aims to establish an openly mintable cryptocurrency that eliminates the requirement for block rewards and disincentivizes mining pools.
Zhongqi Cheng, Tim Schmidt, Guantao Liu, Rainer Doomer
The rapidly growing design complexity has become a big obstacle and dramatically increased the time required for SystemC simulation. In this case study, we exploit different levels of parallelism, including thread- and data-level parallelism, to accelerate the simulation of a Bitcoin miner model in SystemC. Our experiments are performed on two multi-core processors and one many-core Intel(g) Xeon PhiTMCoprocessor. Our results show that with the combination of data- and thread-level parallelism, the peak simulation speed improves by over 11x on a 4-core host, 50x on a 16-core host, and 510x on a 60-core host, respectively. The results confirm the efficiency of combining thread- and datalevel parallelism for higher SystemC simulation speed, and can serve as a benchmark for future optimization of system level design, modeling, and simulation.
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.
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.
This work reports on the experience arising from the master internship contract-based design tailored to safety issues for cyber-physical systems (CPS). The main educational goal is to confront the student with realistic mixed-critical smart CPS systems, using the railway domain and autonomous trains as a case study. The results show that, for this class of systems, education should transition from a 2D to a 3D modeling design space, which is much better suited to visualizing the evolution and the underlying properties of the system. We use contract-based design to properly deal with the integration and composition of heterogeneous components, where safety aspects require special attention. The main scientific and technical results concern the implementation of contract-based design in a 3D tool. Finally, we discuss the teaching methodology underlying the internship and the competences required to address the design of a (critical) CPS by the new generation of students.
One of the most fundamental goals in cryptography is to design protocols that remain secure when adversarial participants can engage in arbitrary malicious behavior. In 1986, Goldreich, Micali, and Wigderson presented a powerful paradigm for designing such protocols: their approach reduced the task of designing secure protocols to designing protocols that only guarantee security against &ldquo;honest-but-curious&rdquo; participants. By making use of zero-knowledge proofs, the GMW paradigm enforces honest behavior without compromising secrecy. Over the past two decades, this approach has been the dominant paradigm for cryptographic protocol design.
Modern computing platforms strive to support mobile code without putting system security at stake. These platforms can be viewed as open systems, as the mobile code adds new components to the running system. Establishing that such platforms function correctly can be divided into two steps. First, it is shown that the system functions correctly regardless of the mobile components that join it, provided that they satisfy certain assumptions. These assumptions can, for instance, restrict the behavior of the component to ensure that the security policy of the platform is not violated. Second, the mobile component is checked to satisfy its assumptions, before it is allowed to join the system. This thesis presents algorithmic verification techniques to support this methodology. In the first two parts, we present techniques for the verification of open systems relative to the given component assumptions. In the third part, a technique for the quick certification of mobile code is presented for the case where a particular type of program rewriting is used as a means of enforcing the component assumptions.In the first part of this study, we present a framework for the verification of open systems based on explicit state space representation. We propose Extended Modal Transition Systems (EMTS) as a suitable structure for representing the state space of open systems when assumptions on components are written in the modal μ-calculus. EMTSs are based on the Modal Transition Systems (MTS) of Larsen and provide a formalism for graphical specification and facilitate a thorough understanding of the system by visualization. In interactive verification, this state space representation enables proof reuse and aids the user guiding the verification process. We present a construction of state space representations from process algebraic open system descriptions based on a maximal model construction for the modal μ-calculus. The construction is sound and complete for systems with a single unknown component and sound for those without dynamic process reation. We also suggest a tableau-based proof system for establishing temporal properties of open systems represented as EMTS. The proof system is sound in general and complete for prime formulae.The problem of open system correctness also arises in compositional verification, where the problem of showing a global property of a system is reduced to showing local properties of components. In the second part, we extend an existing compositional verification framework for Java bytecode programs. The framework employs control flow graphs with procedures to model component implementations and open systems for the purpose of checking control-flow properties. We generalize these models to capture exceptional and multi-threaded behavior. The resulting control flow graphs are specifically tailored to support the compositional verification principle; however, they are sufficiently intuitive and standard to be useful on their own. We describe how the models can be extracted from program code and give preliminary experimental results for our implementation of the extraction of control flow graphs with exceptions. We also discuss further tool support and practical applications of the method.In the third part of the thesis, we develop a technique for the certification of safe mobile code, by adapting the proof-carrying code scheme of Necula to the case of security policies expressed as security automata. In particular, we describe how proofs of policy compliance can be automatically generated for programs that include a monitor for the desired policy. A monitor is an entity that observes the execution of a program and terminates the program if a violation to the property is about to occur. One way to implement such a monitor is by rewriting the program to make it self-monitoring. Given a property, we characterize self-monitoring of Java bytecode programs for this property by an annotation scheme with annotations in the style of Floyd-Hoare logics. The annotations generated by this scheme can be extended in a straightforward way to form a correctness proof in the sense of axiomatic semantics of programs. The proof generated in this manner essentially establishes that the program satisfies the property because it contains a monitor for it. The annotations that comprise the proofs are simple and efficiently checkable, thus facilitate certification of mobile code on devices with restricted computing power such as mobile phones.