Marisol García‐Valls, Alejandro M. Chirivella-Ciruelos
The lack of sufficient guarantee about the authenticity of running smart contracts is a major entry barrier to blockchain networks. By authenticity,we refer to the smart contract ownership or provenance; this implies perfect matching between a published source-code and the corresponding running version of a given smart contract. Block verifiers are services that check the provenance authenticity of the logic contained in blockchain networks. Nevertheless, as a block verifier is an external verification service, it consumes time to use it; and the derived overhead may not comply with temporal requirements of time-sensitive domains like cyber-physical systems. Such systems require that the temporal cost of using external services is assessed prior to the final system deployment. To the best of our knowledge, there are no previous contributions on the determination of the temporal cost of the smart-contract provenance verification process. This paper presents the design and implementation of a middleware that assesses the temporal overhead of accessing the verification services; the middleware is hosted in the global ledger and runs the verification services over large sets of smart contracts. Our contribution is validated by providing an implementation on a real blockchain network, employing actual smart contract verifier logic, and analysing the temporal behavior of the overall system operations to comply with the time-sensitive requirements of cyber-physical systems.
The unstoppably increasing number of the Internet of Things (IoT), autonomous agents, and massive distributed web ecosystems have made data acquisition a complicated, risk-prone, and a very sensitive process. Regulation Web data collection is a fixed pipeline that is strictly regulated by established rules and legal limits, and reactive policy audits to operate in traditional forms of governance. Nevertheless, the contemporary digital ecosystem requires a decentralized system of governance that could identify unpredictable streams of data, the shifting web framework, loosely distributed computing individuals, and shifting conditions of regulation. This paper will present Governance-of-Things (GoT), an emerging conceptual and architectural design that will address these issues and show how to smoothly integrate ethical intelligence, regulatory and laws compliance, semantic awareness, and integrity assurance within autonomous systems of web data acquisition. GoT suggests a view where governance follows a first-class computation i.e. embedded, adaptive, intelligent and context-aware. In contrast to traditional approaches of governing IoT, GoT regards any acquisition agent as ethics-regulated, compliance-aware, and self-regulating. Agents do not simply pull information, they negotiate access rights, authenticate provenance, reason about risk, and implement multi-jurisdictional policies all by themselves. The framework combines dynamic enforcement of policies, federated governance, semantic classification pipelines, AI-enhanced agent frameworks built on Java and distributed analytics to create an ecosystem, producing an automated acquisition that is compatible with responsible, transparent, and audit-friendly behaviours. Fairness, legality, transparency, explainability and accountability are the principles of ethical autonomy which are expounded in the paper. GoT has the aspect of federated ethical rule orchestration where the governance layers among organizations in various stakeholders share without necessarily providing the raw information. The system incorporates automation using structural integrity that guarantees cryptographic validation and review trails that are not tampered with. The given adaptive monitoring model promotes the constant policy updating, data flows redirection and the detection of threats. Furthermore, GoT involves semantic intelligence so that data classification, contextual labeling, entity recognition, and domain mapping take place before storing or processing data- therein avoiding compliance violation at its early phases. GoT architecturally has a multi-layer stack that is organized and includes Perception Layer, Autonomous Agent Layer, Governance Core, Distributed Analytics Layer, and Compliance Ledger Layer. The primitives of computational governance are embedded in each layer, making it highly modular and allowing run-time updates of rules and cooperating across agents. Java frameworks boosted with AI facilitate interoperability with legacy enterprise systems and with current base systems. Using experimental simulation, it was found that GoT enhances compliance accuracy, governance throughput, policy adaptation latency and decision explainability on varying scenarios of acquisitions. This article is in the pre-2021 academic style, has extensive literature review, methodological description, architectural schematics, theoretical framework, and profound results discussion. It ends by establishing GoT as an innovative paradigm which is able to influence the future of web data governance, autonomous systems, and distributed analytics
Rafael Belchior, Dimo Dimov, Zahary Karadjov, Jonas Pfannschmidt · 6 authors
The field of blockchain interoperability plays a pivotal role in blockchain adoption. Despite these advances, a notorious problem persists: the high number and success rate of attacks on blockchain bridges. We propose Harmonia, a framework for building robust, secure, efficient, and decentralized cross-chain applications. A main component of Harmonia is DendrETH, a decentralized and efficient zero-knowledge proof-based light client. DendrETH mitigates security problems by lowering the attack surface by relying on the properties of zero-knowledge proofs. The DendrETH instance of this paper is an improvement of Ethereum’s light client sync protocol that fixes critical security flaws. This light client protocol is implemented as a smart contract, allowing blockchains to read the state of the source blockchain in a trust-minimized way. Harmonia and DendrETH support several cross-chain use cases, such as secure cross-blockchain bridges (asset transfers) and smart contract migrations (data transfers), without a trusted operator. We implemented Harmonia in 9K lines of code. Our implementation is compatible with the Ethereum Virtual Machine (EVM) based chains and some non-EVM chains. Our experimental evaluation shows that Harmonia can generate light client updates with reasonable latency, costs (a dozen to a few thousand US dollars per year), and minimal storage requirements (around 4.5 MB per year). We also carried out experiments to evaluate the security of DendrETH. We provide an open-source implementation and reproducible environment for researchers and practitioners to replicate our results.
This paper extends the previous paper [6] by implementing two blockchain simulators of Solidity-style smart contracts – a simple and a complex one, using the interactive theorem prover Agda. In the previous article [6], we built a simple and complex abstract model of Solidity-style smart contracts in Agda. These models had many features, such as calling different smart contracts, supporting the ability to call different smart contracts, and providing simple and complex instructions. Because of the use of coalgebras for representing smart contracts they supported loops and conditionals, using the support of those features for coalgebraic programs in Agda. The complex model supported gas costs and pure functions, similar to the Solidity language.
Kai Ma, Jintao Huang, Ningyu He, Zhuo Wang · 5 authors
Non-fungible tokens (NFTs) drive the prosperity of the Web3 ecosystem. By November 2023, the total market value of NFT projects reached approximately 16 billion USD. Accompanying the success of NFTs are various security issues, i.e., attacks and scams are prevalent in the ecosystem. While NFTs have attracted significant attentions from both industry and academia, there is a lack of understanding of kinds of NFT security issues. The discovery, in-depth analysis, and systematic categorization of these security issues are of significant importance for the prosperous development of the NFT ecosystem. To fill the gap, we performed a systematic literature review related to NFT security, and we have identified 142 incidents from 213 security reports and 18 academic papers until October 1st, 2023. Through manual analysis of the compiled security incidents, we have classified them into 12 major categories. Then we explored potential solutions and mitigation strategies. Drawing from these analyses, we established the first NFT security reference frame. Except, we extracted the characteristics of NFT security issues, i.e., the prevalence, severity, and intractability. We have indicated the gap between industry and academy for NFT security, and provide further research directions for the community. This paper, as the first SoK of NFT security, has systematically explored the security issues within the NFT ecosystem, shedding light on their root causes, real-world attacks, and potential ways to address them. Our findings will contribute to the future research of NFT security.
If tokenized assets are to be a reality in the future decentralized Web3 then transaction keys need to be distributed and under the control of the asset-owners. This requires a careful design of wallet systems based on trusted hardware. A core feature needed for wallet systems is the attestation of the state of the transaction keys in the wallet without disclosure of the keys. This feature is relevant for relying parties such as insurance providers who need to perform risk assessment based on the security quality of the environment inside the wallet system that is protecting the transaction keys. In the longer term, all key-bearing devices that participate in a decentralized tokenized asset network will need to be hardened using trusted hardware, with attestation capabilities for detecting and countering cyberattacks.
Michael Eckel, Dominik Roy George, Björn Grohmann, Christoph Krauß
Trusted Platform Modules (TPMs) are used for remote attestation to ensure the authenticity and integrity of software running on a computer system. However, measuring software executed as containers or virtual machines can be challenging as it is measured concurrently, resulting in a jumbled measurement log that is difficult to disentangle. Moreover, disclosing the entire measurement log in traditional binary remote attestation raises privacy and intellectual property concerns. To address these issues, we propose a remote attestation method with constrained disclosure, allowing for selective disclosure of entries in the measurement log using a non-interactive zero-knowledge (NIZK) proof with Schnorr signatures. Our approach is evaluated for security and privacy and proven to be correct, sound, and satisfies the properties of a NIZK proof. Formal verification of our solution with ProVerif also supports our claims. Furthermore, the performance evaluation of our proof-of-concept implementation shows that our contribution is feasible, and the overhead introduced is negligible.
Kunsong Zhao, Zihao Li, Jianfeng Li, He Ye · 6 authors
Smart contracts play an increasingly important role in Ethereum platform. It provides various functions implementing numerous services, whose bytecode runs on Ethereum Virtual Machine. To use services by invoking corresponding functions, the callers need to know the function signatures. Moreover, such signatures provide crucial information for many downstream applications, e.g., identifying smart contracts, fuzzing, detecting vulnerabilities, etc. However, it is challenging to infer function signatures from the bytecode due to a lack of type information. Existing work solving this problem depended heavily on limited databases or hard-coded heuristic patterns. However, these approaches are hard to be adapted to semantic differences in distinct languages and various compiler versions when developing smart contracts. In this paper, we propose a novel framework DeepInfer that first leverages deep learning techniques to automatically infer function signatures and returns. The novelties of DeepInfer are: 1) DeepInfer lifts the bytecode into the Intermediate Representation (IR) to preserve code semantics; 2) DeepInfer extracts the type-related knowledge (e.g., critical data flows, constant values, and control flow graphs) from the IR to recover function signatures and returns. We conduct experiments on Solidity and Vyper smart contracts and the results show that DeepInfer performs faster and more accurate than existing tools, while being immune to changes in different languages and various compiler versions.
Sharon Rose H, Razeenath Aafiya A, Kamachi Swetha R, G. R. Ramya
The system focuses on proposing a robust authentication framework based on these Secure Remote Password (SRP) protocol to enhance the security of data exchange in Peer-to- Peer (P2P) cloud environments. The Advanced Encryption Standard (AES) algorithm provides encryption and the SRP protocol leverages cryptographic primitives to establish mutual authentication between cloud servers and users, ensures that data, remains protected against any vulnerabilities. The system encompasses various stages, including user registration, key establishment, and secure data transmission. After user registration, the SRP protocol employs a zero-knowledge proof mechanism to maintain the security of data available on cloud servers, mitigating the risks associated with password leaks and unauthorized access. Furthermore, the protocol facilitates secure key exchange to establish a confidential communication channel between peers, enabling encrypted data transmission. The system integrates SRP protocol and AES encryption, fortifying data security in P2P cloud environments through robust authentication, ensuring a comprehensive defence against potential vulnerabilities.
The novel contribution of this research is decentralised IOTA-based concepts of digital trust for securing remote driving in an urban environment. The conceptual solutions are studied and described, and respective experimental solutions are developed relying on digital identities, public key cryptography with a decentralised approach using decentralised identifiers (DIDs) and verifiable credentials (VCs), and an IOTA-based distributed ledger. The provided digital trust solutions were validated by executing them according to the remote driving scenario but with a simulated vehicle and simulated remote driving system. The hybrid simulation mainly focused on the validation of functional, causal temporal correctness, feasibility, and capabilities of the provided solutions. The evaluations indicate that the concepts of digital trust fulfil the purpose and contribute towards making remote driving more trustable. A supervisory stakeholder was used as a verifier, requiring a set of example verifiable credentials from the vehicle and the remote driver, and accepting them to the security control channel. The separation of control and data planes from each other was found to be a good solution because the delays caused by required security control can be limited to the initiation of the remote driving session without causing additional delays in the actual real-time remote driving control data flow. The application of the IOTA Tangle as the verifiable data registry was found to be sufficient for security control purposes. During the evaluations, the need for further studies related to scalability, application of wallets, dynamic trust situations, time-sensitive behaviour, and autonomous operations, as well as smart contract(s) between multiple stakeholders, were detected. As the next step of this research, the provided digital trust solutions will be integrated with a vehicle, remote driving system and traffic infrastructure for evaluation of the performance, reliability, scalability, and flexibility in real-world experiments of remote driving of an electric bus in an urban environment.
The privacy concern in smart contract applications continues to grow, leading to the proposal of various schemes aimed at developing comprehensive and universally applicable privacy-preserving smart contract (PPSC) schemes. However, the existing research in this area is fragmented and lacks a comprehensive system overview. This paper aims to bridge the existing research gap on PPSC schemes by systematizing previous studies in this field. The primary focus is on two categories: PPSC schemes based on cryptographic tools like zero-knowledge proofs, as well as schemes based on trusted execution environments. In doing so, we aim to provide a condensed summary of the different approaches taken in constructing PPSC schemes. Additionally, we also offer a comparative analysis of these approaches, highlighting the similarities and differences between them. Furthermore, we shed light on the challenges that developers face when designing and implementing PPSC schemes. Finally, we delve into potential future directions for improving and advancing these schemes, discussing possible avenues for further research and development.
Haojia Sun, K. Ranjith Singh, Jan-Paul Ramos-Dávila, Jonathan Aldrich · 5 authors
Blockchains facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities, particularly when interacting with external contracts, leading to substantial monetary losses. Traditional verification techniques fall short in providing comprehensive security assurances, especially against re-entrancy attacks, due to the unavailable implementations of external contracts. This paper introduces an incremental approach: gradual verification. We combine static and dynamic verification techniques to enhance security, guarantee soundness and flexibility, and optimize resource usage in smart contract interactions. By implementing a prototype for gradually verifying Algorand smart contracts via the pyTEAL language, we demonstrate the effectiveness of our approach, contributing to the safe and efficient execution of smart contracts.
Blockchains add transactions to a distributed shared ledger by arriving at consensus on sets of transactions contained in blocks. This provides a total ordering on a set of global transactions. However, total ordering is not enough to satisfy application semantics under the Byzantine fault model. This is due to the fact that malicious miners and clients can collaborate to add their own transactions ahead of correct clients' transactions in order to gain application level and financial advantages. These attacks fall under the umbrella of front-running attacks. Therefore, total ordering is not strong enough to preserve application semantics. In this paper, we propose causality preserving total order as a solution to this problem. The resulting Blockchains will be stronger than traditional consensus based blockchains and will provide enhanced security ensuring correct application semantics in a Byzantine setting.
Yibin Yang, David Heath, Carmit Hazay, Vladimir Kolesnikov · 5 authors
Vector Oblivious Linear Evaluation (VOLE) supports fast and scalable interactive Zero-Knowledge (ZK) proofs. Despite recent improvements to VOLE-based ZK, compiling proof statements to a control-flow oblivious form (e.g., a circuit) continues to lead to expensive proofs. One useful setting where this inefficiency stands out is when the statement is a disjunction of clauses \mathcalL _1 łor \cdots łor \mathcalL _B. Typically, ZK requires paying the price to handle all B branches. Prior works have shown how to avoid this price in communication, but not in computation.
Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu · 6 authors
Despite the notable advances in the development of high-assurance, verified implementations of cryptographic protocols, such implementations typically face significant performance overheads, particularly due to the penalties induced by formal verification and automated extraction of executable code. In this paper, we address some core performance challenges facing computer-aided cryptography by presenting a formal treatment for accelerating such verified implementations based on multiple generic optimizations covering parallelism and memory access. We illustrate our techniques for addressing such performance bottlenecks using the Line-Point Zero-Knowledge (LPZK) protocol as a case study. Our starting point is a new verified implementation of LPZK that we formalize and synthesize using EasyCrypt; our first implementation is developed to reduce the proof effort and without considering the performance of the extracted executable code. We then show how such (automatically) extracted code can be optimized in three different ways to obtain a 3000x speedup and thus matching the performance of the manual implementation of LPZK of lpzkv2.[13] We obtain such performance gains by first modifying the algorithmic specifications, then by adopting a provably secure parallel execution model, and finally by optimizing the memory access structures. All optimizations are first formally verified inside EasyCrypt, and then executable code is automatically synthesized from each step of the formalization. For each optimization, we analyze performance gains resulting from it and also address challenges facing the computer-aided security proofs thereof, and challenges facing automated synthesis of executable code with such an optimization.
Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg · 8 authors
A zero-knowledge proof (ZKP) is a powerful cryptographic primitive used in many decentralized or privacy-focused applications. However, the high overhead of ZKPs can restrict their practical applicability. We design a programming language, Ou, aimed at easing the programmer's burden when writing efficient ZKPs, and a compiler framework, Lian, that automates the analysis and distribution of statements to a computing cluster. Ou uses programming language semantics, formal methods, and combinatorial optimization to automatically partition an Ou program into efficiently sized chunks for parallel ZK-proving and/or verification. We contribute: (1) A front-end language where users can write proof statements as imperative programs in a familiar syntax; (2) A compiler architecture and implementation that automatically analyzes the program and compiles it into an optimized IR that can be lifted to a variety of ZKP constructions; and (3) A cutting algorithm, based on Pseudo-Boolean optimization and Integer Linear Programming, that reorders instructions and then partitions the program into efficiently sized chunks for parallel evaluation and efficient state reconciliation.
Zero-knowledge circuits are sets of equality constraints over arithmetic expressions interpreted in a prime field; they are used to encode computations in cryptographic zero-knowledge proofs. We make the following contributions to the problem of ensuring that a circuit correctly encodes a computation: a formal framework for circuit correctness; an ACL2 library for prime fields; an ACL2 model of the existing R1CS (Rank-1 Constraint Systems) formalism to represent circuits, along with ACL2 and Axe tools to verify circuits of this form; a novel PFCS (Prime Field Constraint Systems) formalism to represent hierarchically structured circuits, along with an ACL2 model of it and ACL2 tools to verify circuits of this form in a compositional and scalable way; verification of circuits, ranging from simple to complex; and discovery of bugs and optimizations in existing zero-knowledge systems.
Open access
2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
Nerla Jean-Louis, Yunqi Li, Yan Ji, Harjasleen Malvai · 7 authors
TEE-based smart contracts are an emerging blockchain architecture, offering fully programmable privacy with better performance than alternatives like secure multiparty computation. They can also support compatibility with existing smart contract languages, such that existing (plaintext) applications can be readily ported, picking up privacy enhancements automatically. While previous analysis of TEE-based smart contracts have focused on failures of TEE itself, we asked whether other aspects might be understudied. We focused on state consistency, a concern area highlighted by Li et al., as well as new concerns including access pattern leakage and software upgrade mechanisms. We carried out a code review of a cohort of four TEE-based smart contract platforms. These include Secret Network, the first to market with in-use applications, as well as Oasis, Phala, and Obscuro, which have at least released public test networks. The first and most broadly applicable result is that access pattern leakage occurs when handling persistent contract storage. On Secret Network, its fine-grained access pattern is catastrophic for the transaction privacy of SNIP-20 tokens. If ERC-20 tokens were naively ported to Oasis they would be similarly vulnerable; the others in the cohort leak coarse-grained information at approximately the page level (4 kilobytes). Improving and characterizing this will require adopting techniques from ORAMs or encrypted databases. Second, the importance of state consistency has been underappreciated, in part because exploiting such vulnerabilities is thought to be impractical. We show they are fully practical by building a proof-of-concept tool that breaks all advertised privacy properties of SNIP-20 tokens, able to query the balance of individual accounts and the token amount of each transfer. We additionally demonstrate MEV attacks against the Sienna Swap application. As a final consequence of lacking state consistency, the developers have inadvertently introduced a decryption backdoor through their software upgrade process. We have helped the Secret developers mitigate this through a coordinated vulnerability disclosure, after which their state consistency should be roughly on par with the rest.
Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, S. Hitarth
Modern programmable blockchains have built-in support for smart contracts, i.e. programs that are stored on the blockchain and whose state is subject to consensus. After a smart contract is deployed on the blockchain, anyone on the network can interact with it and call its functions by creating transactions. The blockchain protocol is then used to reach a consensus about the order of the transactions and, as a direct corollary, the state of every smart contract. Reaching such consensus necessarily requires every node on the network to execute all function calls. Thus, an attacker can perform DoS by creating expensive transactions and function calls that use considerable or even possibly infinite time and space. To avoid this, following Ethereum, virtually all programmable blockchains have introduced the concept of “gas”. A fixed hard-coded gas cost is assigned to every atomic operation and the user who calls a function has to pay for its total gas usage. This technique ensures that the protocol is not vulnerable to DoS attacks, but it has also had significant unintended consequences. Out-of-gas errors, i.e. when a user misunderestimates the gas usage of their function call and does not allocate enough gas, are a major source of security vulnerabilities in Ethereum. We focus on the well-studied problem of automatically finding upper-bounds on the gas usage of a smart contract. This is a classical problem in the blockchain community and has also been extensively studied by researchers in programming languages and verification. In this work, we provide a novel approach using theorems from polyhedral geometry and real algebraic geometry, namely Farkas’ Lemma, Handelman’s Theorem, and Putinar’s Positivstellensatz, to automatically synthesize linear and polynomial parametric bounds for the gas usage of smart contracts. Our approach is the first to provide completeness guarantees for the synthesis of such parametric upper-bounds. Moreover, our theoretical results are independent of the underlying consensus protocol and can be applied to smart contracts written in any language and run on any blockchain. As a proof of concept, we also provide a tool, called “Asparagus” that implements our algorithms for Ethereum contracts written in Solidity. Finally, we provide extensive experimental results over 24,188 real-world smart contracts that are currently deployed on the Ethereum blockchain. We compare Asparagus against GASTAP, which is the only previous tool that could provide parametric bounds, and show that our method significantly outperforms it, both in terms of applicability and the tightness of the resulting bounds. More specifically, our approach can handle 80.56% of the functions (126,269 out of 156,735) in comparison with GASTAP’s 58.62%. Additionally, even on the benchmarks where both approaches successfully synthesize a bound, our bound is tighter in 97.85% of the cases.
In this paper, we design, implement, and (partially-) evaluate a lightweight bridge (as a type of middleware) to connect the Bitcoin and Ethereum networks that were heterogeneously uncontactable before. Inspired by the recently introduced Bitcoin Request Comment (BRC-20) standard, we leverage the flexibility of Bitcoin inscriptions by embedding editable operations within each satoshi and mapping them to programmable Ethereum smart contracts. A user can initialize his/her requests from the Bitcoin network, subsequently triggering corresponding actions on the Ethereum network. We validate the lightweight nature of our solution and its ability to facilitate secure and seamless interactions between two heterogeneous ecosystems.
Open access
3 source records
Blockchain Technology Applications and Security
Physical Unclonable Functions (PUFs) and Hardware Security
Metin Lamby, Valentin Zieglmeier, Christian Ziegler
Smart contract access control mechanisms can introduce centralization into supposedly decentralized ecosystems. In our view, such centralization is an overlooked risk of smart contracts that underlies well-known smart contract security incidents. Critically, mitigating the known vulnerability of missing permission verification by implementing authorization patterns can in turn introduce centralization. To delineate the issue, we define centralization risk and describe smart contract source code patterns for Ethereum and Algorand that can introduce it to smart contracts. We explain under which circumstances the centralization can be exploited. Finally, we discuss implications of centralization risk for different smart contract stakeholders.
This article conducts an extensive examination of the persisting challenges related to smart contract attacks within blockchain networks, with a particular focus on the reentrancy attack. It emphasizes the inherent vulnerabilities embedded in the programming languages commonly employed for smart contract development, particularly within Ethereum Virtual Machine (EVM)-based blockchains. While the concrete example used primarily employs the Solidity programming language, the insights garnered from this study are readily generalizable to a wide array of blockchain architectures. Significantly, this article extends beyond the mere identification of vulnerabilities and ventures into the realm of proactive security measures. It explores the adaptation and adoption of dataflow programming paradigms, employing Domain-Specific Languages (DSLs) to enforce security by design in the context of smart contract development. This forward-looking approach aims to bolster the foundational principles of blockchain security, offering a promising research direction for mitigating the risks associated with smart contract vulnerabilities. The objective of this article is to cater to a diverse audience, ranging from individuals with limited computer science and programming expertise to seasoned experts in the field. It provides a comprehensive and accessible resource for fostering a deeper understanding of the intricate dynamics between blockchain technology and the imperative need for secure smart contract development practices.