Chao Ni, Cong Tian, Kaiwen Yang, David Lo · 6 authors
Smart contract, a special software code running on and resided in the blockchain, enlarges the general application of blockchain and exchanges assets without dependence of external parties. With blockchain’s characteristic of immutability, they cannot be modified once deployed. Thus, the contract and the records are persisted on the blockchain forever, including failed transactions that are caused by runtime errors and result in the waste of computation, storage, and fees. In this paper, we refer to smart contracts which will cause runtime errors as crash-inducing smart contracts. However, automatic identification of crash-inducing smart contracts is limited investigated in the literature. The existing approaches to identify crash-inducing smart contracts are either limited in finding vulnerability (e.g., pattern-based static analysis) or very expensive (e.g., program analysis), which is insufficient for Ethereum.To reduce runtime errors on Ethereum, we propose an efficient, generalizable, and machine learning-based crash-inducing smart contract detector, CRASHSCDET, to automatically identify crash-inducing smart contracts. To investigate the effectiveness of CRASHSCDET, we firstly propose 34 static source code metrics from four dimensions (i.e., complexity metrics, count metrics, object-oriented metrics, and Solidity-specific metrics) to characterize smart contracts. Then, we collect a large-scale dataset of verified smart contracts (i.e., 54,739) and label these smart contracts based on their execution traces on Etherscan. We make a comprehensive comparison with three state-of-the-art approaches and the results show that CRASHSCDET can achieve good performance (i.e., 0.937 of F1-measure and 0.980 of AUC on average) and statistically significantly improve the baselines by 0.5%-60.4% in terms of F1-measure and by 41.2%-44.3% in terms of AUC, which indicates the effectiveness of static source code metrics in identifying crash-inducing smart contracts. We further investigate the importance of different types of metrics and find that metrics in different dimensions have varying abilities to depict the characteristic of smart contracts. Especially, metrics belonging to the "Count" dimension are the most discriminative ones but combining all metrics can achieve better prediction performance.
Smart contracts on the Ethereum blockchain greatly benefit from cutting-edge analysis techniques and pose significant challenges. A primary challenge is the extremely low-level representation of deployed contracts. We present Elipmoc, a decompiler for the next generation of smart contract analyses. Elipmoc is an evolution of Gigahorse, the top research decompiler, dramatically improving over it and over other state-of-the-art tools, by employing several high-precision techniques and making them scalable. Among these techniques are a new kind of context sensitivity (termed “transactional sensitivity”) that provides a more effective static abstraction of distinct dynamic executions; a path-sensitive (yet scalable, through path merging) algorithm for inference of function arguments and returns; and a fully context sensitive private function reconstruction process. As a result, smart contract security analyses and reverse-engineering tools built on top of Elipmoc achieve high scalability, precision and completeness. Elipmoc improves over all notable past decompilers, including its predecessor, Gigahorse, and the state-of-the-art industrial tool, Panoramix, integrated into the primary Ethereum blockchain explorer, Etherscan. Elipmoc produces decompiled contracts with fully resolved operands at a rate of 99.5% (compared to 62.8% for Gigahorse), and achieves much higher completeness in code decompilation than Panoramix—e.g., up to 67% more coverage of external call statements—while being over 5x faster. Elipmoc has been the enabler for recent (independent) discoveries of several exploitable vulnerabilities on popular protocols, over funds in the many millions of dollars.
Distributed ledger systems have become more prominent and successful in recent years, with a focus on blockchains and cryptocurrency. This has led to various misunderstandings about both the technology itself and its capabilities, as in many cases blockchain and cryptocurrency is used synonymously and other applications are often overlooked. Therefore, as a whole, the view of distributed ledger technology beyond blockchains and cryptocurrencies is very limited. Existing vocabularies and ontologies often focus on single aspects of the technology, or in some cases even just on one product. This potentially leads to other types of distributed ledgers and their possible use cases being neglected. In this paper, we present a knowledge graph and an ontology for distributed ledger technologies, which includes security considerations to model aspects such as threats and vulnerabilities, application domains, as well as relevant standards and regulations. Such a knowledge graph improves the overall understanding of distributed ledgers, reveals their strengths, and supports the work of security personnel, i.e. analysts and system architects. We discuss potential uses and follow semantic web best practices to evaluate and publish the ontology and knowledge graph.
Pietro Ferraro, Andreas Penzkofer, Christopher King, Robert Shorten
In this article, we present a feedback approach to the design of an attack mitigation policy for directed acyclic graph (DAG)-based distributed ledgers. We develop a model to analyze the behavior of the ledger under the so-calledTips Inflation Attack, which endangers the liveness of transactions, and we design a control strategy to counteract this attack strategy. The efficacy of this approach is showcased through a theoretical analysis, in the form of two theorems about the stability properties of the ledger with and without the controller, and extensive Monte Carlo simulations of an agent-based model of the distributed ledger.
Transactions involving multiple blockchains are implemented by cross-chain protocols. These protocols are based on smart contracts, programs that run on blockchains, executed by a network of computers. Because smart contracts can automatically transfer ownership of cryptocurrencies, electronic securities, and other valuable assets among untrusting parties, verifying the runtime correctness of smart contracts is a problem of compelling practical interest. Such verification is challenging since smart contract execution is time-sensitive, and the clocks on different blockchains may not be perfectly synchronized. This paper describes a method for runtime monitoring of blockchain executions. First, we propose a generalized runtime verification technique for verifying partially synchronous distributed computations for the metric temporal logic (MTL) by exploiting bounded-skew clock synchronization. Second, we introduce a progression-based formula rewriting scheme for monitoring \MTL specifications which employ SMT solving techniques and report experimental results.
The digital ecosystems have experienced a paradigm shift as there is a growing level of integration of Artificial Intelligence (AI), distributed computing apparatus, and robotic policy enforcement strategies. Governance structures are faced with the difficult task of negotiating the vagaries of privacy laws and decentralized data processing and the use of algorithmic decision-making with the migration of data-intensive applications to web-based environments. The increasing regulatory environment, such as GDPR, CCPA, and industry-specific data protection requirements, have significant forces on the requirement to have strong policy-driven governance infrastructures that entrench privacy and security at every layer of the web application stack. Although cloud platforms and microservice architectures have been developed, modern governance solutions have weaknesses in terms of scalability, being context-aware and dynamically adapting to changes in policy constraints. The research paper presents the AI-Enabled Policy-Driven Web Governance Framework that has been developed on the Full-Stack Java ecosystem which involves spring boot, Jakarta EE, containerized deployment platforms and intelligent agents which are rule-based. The framework incorporates machine learning-related policy interpretation, semantic arguments engines, as well as automated monitoring applications that regulate user interactions, data activities, service coordination, and cross-layer correspondence. AI agents will adapt legal and organizational privacy requirements into dynamic policies that are explicitly and dynamically implemented in real-time at the front-end, API, middleware, and database tiers. These challenges in digital governance that are solved are minimization of data, contextual privacy, verification of compliance, detection of anomalies, and fine-grained access control. The given architecture proposes a Multi-Layer Governance Orchestration Model (MGOM) that divides the governance issues into policy ingestion, AI interpretation, runtime enforcement, auditability, and compliance reporting. The framework also includes three levels of privacy shield with a static code analysis, user behavior analytics (UBA), and encrypted data pipelines. Through an extensive assessment analysis, it is evident that the framework has the ability to be highly precise in automated policy enforcement, decreases the latency of governance and enhances consistency of compliance over the traditional rule-based systems. The findings of the experiments point out that AI-enabled governance engine helps to improve the accuracy of policy compliance by 27.8 percent, minimize privacy invasions by 42.1 percent, and decrease administrative workload by 34.6 percent. A combination of a supervised learning, the natural language processing (NLP) and the symbolic rule mining allow the system to be autonomously adapted to new regulatory conditions without being reconfigured by human operators. Security benchmarks also indicate resiliency to partial attack vectors, such as inference attacks, unauthorized data elevation, and access patterns analysis. The paper will add value to the digital governance field by offering a holistic, scalable, and future-proof implementation that can assist with current web environments of many services including medicine, finance, online commerce, and smarter cities. The framework ensures the creation of a novel model of transparent, compliant, and privacy-conscious digital ecosystems by entrenching AI at the core of policy interpretation and enforcement. The publication contributes to the discussion of intelligent governance systems and offers a reference design to the developers, policymakers, and researchers, who seek to develop trustful and ethically aligned digital spaces
Dan Bogdanov, Joosep Jääger, Peeter Laud, Härmel Nestra · 10 authors
We present ZK-SECREC, a domain-specific language for zero-knowledge (ZK) proofs. We focus on its type system, making the point that this is the most appropriate mechanism for tracking information flows in a statement that is meant to be proved using a zero-knowledge protocol. The appropriateness stems from the necessary distinctions between the two involved parties and between the computations made locally or on top of the protocol. The appropriateness also stems from how the types match with the major steps of typical ZK protocols, including the generation of Common Reference Strings. We compare the type system of ZK-SECREC with those of the previously proposed languages for ZK proofs and privacy-preserving computations, and show how ZK-SECREC handles certain aspects better.
Heidelinde Rameder, Monika di Angelo, Gernot Salzer
Programs on public blockchains often handle valuable assets, making them attractive targets for attack. At the same time, it is challenging to design correct blockchain applications. Checking code for potential vulnerabilities is a viable option to increase trust. Therefore, numerous methods and tools have been proposed with the intention to support developers and analysts in detecting code vulnerabilities. Moreover, publications keep emerging with different focus, scope, and quality, making it difficult to keep up with the field and to identify relevant trends. Thus, regular reviews are essential to keep pace with the varied developments in a structured manner. Regarding blockchain programs, Ethereum is the platform most widely used and best documented. Moreover, applications based on Ethereum are entrusted with billions of USD. Like on similar blockchains, they are subject to numerous attacks and losses due to vulnerabilities that exist at all levels of the ecosystem. Countermeasures are in great demand. In this work, we perform a systematic literature review (SLR) to assess the state of the art regarding automated vulnerability analysis of smart contracts on Ethereum with a focus on classifications of vulnerabilities, detection methods, security analysis tools, and benchmarks for the assessment of tools. Our initial search of the major on-line libraries yields more than 1,300 publications. For the review, we apply a clear strategy and protocol to assure consequent, comprehensive, and reproducible documentation and results. After collecting the initial results, cleaning up references, removing duplicates and applying the inclusion and exclusion criteria, we retain 303 publications that include 214 primary studies, 70 surveys and 19 SLRs. For quality appraisal, we assess their intrinsic quality (derived from the reputation of the publication venue) as well as their contextual quality (determined by rating predefined criteria). For about 200 publications with at least a medium score, we extract the vulnerabilities, methods, and tools addressed, among other data. In a second step, we synthesize and structure the data into a classification of both the smart contract weaknesses and the analysis methods. Furthermore, we give an overview of tools and benchmarks used to evaluate tools. Finally, we provide a detailed discussion.
The blockchain-based smart contract lacks privacy since the contract state and instruction code are exposed to the public. Combining smart-contract execution with Trusted Execution Environments (TEEs) provides an efficient solution, called TEE-assisted smart contracts, for protecting the confidentiality of contract states. However, the combination approaches are varied, and a systematic study is absent. Newly released systems may fail to draw upon the experience learned from existing protocols, such as repeating known design mistakes or applying TEE technology in insecure ways. In this paper, we first investigate and categorize the existing systems into two types: the layer-one solution and layer-two solution. Then, we establish an analysis framework to capture their common lights, covering the desired properties (for contract services), threat models, and security considerations (for underlying systems). Based on our taxonomy, we identify their ideal functionalities and uncover the fundamental flaws and reasons for the challenges in each specification design. We believe that this work would provide a guide for the development of TEE-assisted smart contracts, as well as a framework to evaluate future TEE-assisted confidential contract systems.
Abstract Traditional zero-knowledge protocols have been studied and optimized for the setting where a single prover holds the complete witness and tries to convince a verifier about a predicate on the witness, without revealing any additional information to the verifier. In this work, we study the notion of distributed-prover zero knowledge (DPZK) for arbitrary predicates where the witness is shared among multiple mutually distrusting provers and they want to convince a verifier that their shares together satisfy the predicate. We make the following contributions to the notion of distributed proof generation: (i) we propose a new MPC-style security definition to capture the adversarial settings possible for different collusion models between the provers and the verifier, (ii) we discuss new efficiency parameters for distributed proof generation such as the number of rounds of interaction and the amount of communication among the provers, and (iii) we propose a compiler that realizes distributed proof generation from the zero-knowledge protocols in the Interactive Oracle Proofs (IOP) paradigm. Our compiler can be used to obtain DPZK from arbitrary IOP protocols, but the concrete efficiency overheads are substantial in general. To this end, we contribute (iv) a new zero-knowledge IOP Graphene which can be compiled into an efficient DPZK protocol. The (D + 1)-DPZK protocol D-Graphene, with D provers and one verifier, admits O ( N 1 /c ) proof size with a communication complexity of O (D 2 ·( N 1−2 /c + N s )), where N is the number of gates in the arithmetic circuit representing the predicate and N s is the number of wires that depends on inputs from two or more parties. Significantly, only the distributed proof generation in D-Graphene requires interaction among the provers. D-Graphene compares favourably with the DPZK protocols obtained from the state-of-art zero-knowledge protocols, even those not modelled as IOPs.
We present two attacks targeting the Proof-of-Stake (PoS) Ethereum consensus protocol. The first attack suggests a fundamental conceptual incompatibility between PoS and the Greedy Heaviest-Observed Sub-Tree (GHOST) fork choice paradigm employed by PoS Ethereum. In a nutshell, PoS allows an adversary with a vanishing amount of stake to produce an unlimited number of equivocating blocks. While most equivocating blocks will be orphaned, such orphaned `uncle blocks' still influence fork choice under the GHOST paradigm, bestowing upon the adversary devastating control over the canonical chain. While the Latest Message Driven (LMD) aspect of current PoS Ethereum prevents a straightforward application of this attack, our second attack shows how LMD specifically can be exploited to obtain a new variant of the balancing attack that overcomes a recent protocol addition that was intended to mitigate balancing-type attacks. Thus, in its current form, PoS Ethereum without and with LMD is vulnerable to our first and second attack, respectively.
Developing secure smart contracts remains a challenging task. Existing approaches are either impractical or leave the burden to developers for fixing bugs. In this paper, we propose the first practical smart contract compiler, called HCC, which automatically inserts security hardening checks at the source-code level based on a novel and language-independent code property graph (CPG) notation. The high expressiveness of our developed CPG allows us to mitigate all of the most common smart contract vulnerabilities, namely reentrancy, integer bugs, suicidal smart contracts, improper use of tx.origin, untrusted delegate-calls, and unchecked low-level call bugs. Our large-scale evaluation on 10k real-world contracts and several sets of vulnerable contracts from related work demonstrates that HCC is highly practical, outperforms state-of-the-art contract hardening techniques, and effectively prevents all verified attack transactions without hampering functional correctness.
Elizabeth Nathania Witanto, Yustus Eko Oktian, Sang-Gon Lee
AI has been implemented in many sectors such as security, health, finance, national defense, etc. However, together with AI’s groundbreaking improvement, some people exploit AI to do harmful things. In parallel, there is rapid development in cloud computing technology, introducing a cloud-based AI system. Unfortunately, the vulnerabilities in cloud computing will also affect the security of AI services. We observe that compromising the training data integrity means compromising the results in the AI system itself. From this background, we argue that it is essential to keep the data integrity in AI systems. To achieve our goal, we build a data integrity architecture by following the National Institute of Standards and Technology (NIST) cybersecurity framework guidance. We also utilize blockchain technology and smart contracts as a suitable solution to overcome the integrity issue because of its shared and decentralized ledger. Smart contracts are used to automate policy enforcement, keep track of data integrity, and prevent data forgery. First, we analyze the possible vulnerabilities and attacks in AI and cloud environments. Then we draw out our architecture requirements. The final result is that we present five modules in our proposed architecture that fulfilled NIST framework guidance to ensure continuous data integrity provisioning towards secure AI environments.
The meteoric rise of Decentralized Finance (DeFi) has been accompanied by a plethora of frequent and often financially devastating attacks on its protocols There have been over 70 exploits of DeFi protocols, with the total of lost funds amounting to approximately 1.5bn USD. In this paper, we introduce a new approach to minimizing the frequency and severity of such attacks: dissimilar redundancy for smart contracts. In a nutshell, the idea is to implement a program logic more than once, ideally using different programming languages. Then, for each implementation, the results should match before allowing the state of the blockchain to change. This is inspired by and has clear parallels to the field of avionics, where on account of the safety-critical environment, flight control systems typically feature multiple redundant implementations. We argue that the high financial stakes in DeFi protocols merit a conceptually similar approach, and we provide a novel algorithm for implementing dissimilar redundancy for smart contracts.
David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi · 6 authors
Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs - in different programming languages - communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses. In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit. Pairs of send and receive actions that "belong together" are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance. The design space of dApp programming and other multi-party languages depends on one major choice: a local model versus a global model. In a local model, parties are defined in separate programs and their interactions are encoded via send and receive effects. In a global language, parties are defined within one shared program and interactions are encoded via combined send-and-receive operations with no effects visible to the outside world. The global model is followed by tierless [Christian Queinnec, 2000; Cooper et al., 2007; Choi and Chang, 2019; Fowler et al., 2019; Serrano et al., 2006; Serrano and Prunet, 2016; Radanne et al., 2016; Weisenburger et al., 2018] and choreographic [Kohei Honda et al., 2011; Fabrizio Montesi et al., 2014; Saverio Giallorenzo et al., 2020] languages. However, known approaches to dApp programming follow the local model, thus rely on explicitly specifying the client-contract interaction protocol. Moreover, the contract and clients are implemented in different languages, hence, developers have to master two technology stacks. The dominating approach in industry is Solidity [Mix, 2019] for the contract and JavaScript for clients. Solidity relies on expressing the protocol using assertions in the contract code, which are checked at run time [Solidity documentation - common patterns, 2020]. Failing to insert the correct assertions may give parties illegal access to monetary values to the detriment of others [Nikolić et al., 2018; Luu et al., 2016]. In research, contract languages [Ankush Das et al., 2019; Michael J. Coblenz, 2017; Franklin Schrans et al., 2018; Franklin Schrans et al., 2019; Michael J. Coblenz et al., 2019; Michael J. Coblenz et al., 2019; Reed Oei et al., 2020; Sam Blackshear et al., 2019] have been proposed that rely on advanced type systems such as session types, type states, and linear types. The global model has not been explored for dApp programming. This is unfortunate given the potential to get by with a standard typing discipline and to avoid intricacies and potential mismatches of a two-language stack. Our work fills this gap by proposing Prisma - the first language that features a global programming model for Ethereum dApps. While we focus on the Ethereum blockchain, we believe our techniques to be applicable to other smart contract platforms. Prisma enables interleaving contract and client logic within the same program and adopts a direct style (DS) notation for encoding send-and-receive operations (with our awaitCl language construct) akin to languages with async/await [Gavin M. Bierman et al., 2012; Scala async rfc]. DS addresses shortcomings with the currently dominant encoding of the protocol’s finite state machines (FSM) [Mix, 2019; Michael J. Coblenz, 2017; Franklin Schrans et al., 2018; Franklin Schrans et al., 2019; Michael J. Coblenz et al., 2019; Michael J. Coblenz et al., 2019]. We argue writing FSM style corresponds to a control-flow graph of basic blocks, which is low-level and more suited to be written by a compiler than by a human. With FSM style, the contract is a passive entity whose execution is driven by clients. whereas the DS encoding allows the contract to actively ask clients for input, fitting dApp execution where a dominant contract controls execution and diverts control to other parties when their input is needed. In the following Prisma snippet, the payout function is a function invoked by the contract when it is time to pay money to a client. In Prisma, variables, methods and classes are separated into two namespaces, one for the contract and one for the clients. The payout method is located on the contract via the annotation @co. The body of the method diverts the control to the client using awaitCl(...) { ... }, hence the contained readLine call is executed on the client. Note that no explicit send/receive operations are needed but the communication protocol is expressed through the program control flow. Only after the check client == toBePayed that the correct client replied, the current contact balance balance() is transferred to the client via transfer. @co def payout(toBePayed: Arr[Address]): Unit = { awaitCl(client => client == toBePayed) { readLine("Press enter for payout") } toBePayed.transfer(balance()) } Overall, Prisma relieves the developer from the responsibility of correctly managing distributed, asynchronous program flows and the heterogeneous technology stack. Instead, the burden is put on the compiler, which distributes the program flow by means of selective continuation-passing-style (CPS) translation and defunctionalisation and inserts guards against malicious client interactions. We needed to develop a CPS translation for the code that runs on the Ethereum Virtual Machine (EVM) since the EVM has no built-in support for concurrency primitives which could be used for asynchronous communication. While CPS translations are well-known, we cannot use them out-of-the-box because the control flow is interwoven with distribution in our case. A CPS translation that does not take distribution into account would allow malicious clients to force the contract to deviate from the intended control flow by sending a spoofed continuation. Thus, it was imperative to prove correctness of our distributed CPS translation to ensure control-flow integrity of the contract.
Oliver Stengele, Christina Westermeyer, Hannes Hartenstein
Software can be described, like human users and other objects, through attributes. For this work, we define software attributes as humanly verifiable, falsifiable, or judgeable statements regarding characteristics of said software. Much like attributes in general, software attributes require robust identities for their source but also for their target, meaning a software in general or a binary in particular. As software can be of critical importance, performing an independent review of attribute claims appears beneficial. We posit that decentralized platforms that were developed and refined over the past decade can bridge the gap between existing tools and methods for software review and their open, transparent, and accountable use for the benefit of users. In this work, we explore the feasibility and implications of decentralizing an independent review of software attribute claims. We envision the decentralization of a review process from initialization and execution to the persistent recording of results. We sketch the available design space by decomposing the overall process into a modular design and describe how each component covers overarching objectives. To illustrate practical implications and trade-offs, we present ETHDPR, a proof of concept implementation based on Ethereum and IPFS. Through a quantitative and qualitative evaluation, we show that a decentralized software review is practically feasible. We illustrate the flexibility of the proposed approach using a toy example of a software component in automotive systems. Lastly, we provide a discussion on fundamental limits and open issues of facilitating independent reviews via technological means.
AI collaboration increasingly spans untrusted, heterogeneous nodes from edge devices to multi-clouds raising acute concerns around privacy, integrity, and verifiability of shared models and updates. This paper proposes a secure distributed computing framework that unifies privacy-preserving learning, verifiable coordination, and incentive-aligned governance for decentralized AI model sharing. The architecture composes federated and peer-to-peer training with secure aggregation, differential privacy, and hardware-backed confidential computing to prevent data leakage while mitigating gradient inversion risks. Model provenance, access control, and policy enforcement are anchored via a lightweight, append-only ledger with decentralized identifiers, enabling auditability without central authorities. To counter poisoning, backdoors, and Sybil attacks, the framework integrates robust aggregation, reputation-weighted participation, and update attestation with zero-knowledge proofs for selective disclosure. A resource-aware scheduler adapts to edge variability using gossip-based dissemination, opportunistic bandwidth utilization, and erasure-coded checkpoints to preserve liveness under churn. Interoperability is ensured through portable model artifacts (e.g., ONNX), secure enclaves for cross-framework execution, and privacy budgets tracked as first-class governance assets. We outline threat models, compliance hooks for jurisdictional constraints, and a token-free contribution accounting mechanism that rewards data quality and validation work. Simulated and real-world deployments illustrate improved end-to-end trust, reduced coordination overhead, and resilient performance under adversarial conditions, positioning the framework as a practical substrate for open, secure, and accountable AI collaboration in decentralized environments
The distribution of information through web protocols is today based on the client-server model. Recently, decentralized protocols with greater availability appear as well as blockchain-based attestation methods, allowing for proving the existence of information. In combination, these methods promise a secure, decentralized and long-term storage. However, there exist two major problems: (1) the scalability of blockchains limits their storage capacity and (2) various (de)centralized web protocols are in use and could alleviate this problem, but they do not support blockchain-based attestations. In this paper, we extend an approach for blockchain-based attestation with compatibility for multi-protocol storage. Instead of specific protocols or blockchains, the extended approach aims to contribute novel concepts to the discussion on blockchain scalability. It augments the capabilities of existing protocols for applications such as certification or timestamping of digital artifacts. With the use of decentralized protocols such as IPFS, further availability and inherent resilience properties are gained, allowing for applications such as open research repositories and digital registries. We discuss the architecture of the extended approach, a possible implementation in a smart contract on the Ethereum blockchain with IPFS and Git, and evaluate the time and cost of attestations.
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio
Abstract Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present $$\textsf {GASOL}^{v2}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GASOL</mml:mi> <mml:mrow> <mml:mi>v</mml:mi> <mml:mn>2</mml:mn> </mml:mrow> </mml:msup> </mml:math> , a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also wrt. memory and storage. $$\textsf {GASOL}^{v2}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GASOL</mml:mi> <mml:mrow> <mml:mi>v</mml:mi> <mml:mn>2</mml:mn> </mml:mrow> </mml:msup> </mml:math> can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler , and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas wrt. the previous version of the optimizer without memory handling, and gains of 3.28% in bytes-size over code already optimized by .
Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
We provide three detailed case studies of vulnerabilities in smart contracts, and show how property-based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave's BAT token. The last example is, in fact, new, and was missed in the auditing process. We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and Concordium's rust language. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.