Blockchain Papers

Follow blockchain research across journals, conferences, and preprint repositories.

1,684 papersLast indexed Aug 31, 2026
Search papers

Paper index

1,684 results · page 41 of 71

Clear filters
Nov 18, 2021·Applied Sciences
112 cites
Educational Blockchain: A Secure Degree Attestation and Verification Traceability Architecture for Higher Education Commission

Abdullah Ayub Khan, Asif Ali Laghari, Aftab Ahmed Shaikh, Sami Bourouis · 6 authors

Degree attestation verification and traceability are complex one-to-one processes between the Higher Education Commission (HEC) and universities. The procedure shifted to the digitalized manner, but still, on a certain note, manual authentication is required. In the initial process, the university verified the degree and stamp seal first. Then, a physical channel of degree submission to the receiving ends is activated. After that, the degree is attested while properly examining and analyzing the tamper records related to degree credentials through e-communication with the university for verification and validation. This issue poses a serious challenge to educational information integrity and privacy. Potentially, blockchain technology could become a standardized platform to perform tasks including issuing, verifying, auditing, and tracing immutable records, which would enable the HEC, universities, and Federal Education Ministry (FEM) to quickly and easily get attested and investigate the forge proof versions of certificates. Besides, decentralized distributed data blocks in chronological order provide high security between distributed ledgers, consensus engine, digital signature, smart contracts, permissioned application, and private network node transactions that guarantee degree record validation and traceability. This paper presents an architecture (HEDU-Ledger) and detail design of blockchain-enabled hyperledger fabric applications implementation for degree attestation verification and traceable direct channel design between HEC and universities. The hyperledger fabric endorses attestation records first, and then validates (committer) the degree and maintains the secure chain of tracing between stakeholder peer nodes. Furthermore, this HEDU-Ledger architecture avoids language and administrative barriers. It also provides robustness in terms of security and privacy of records and maintains integrity with secure preservation as compared to that of the other state-of-the-art methods.

Open access
Blockchain Technology Applications and Security
Security and Verification in Computing
Cloud Data Security Solutions
Original source
Nov 12, 2021·Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
8 cites
Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy · 7 authors

MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH.

Open access
Cryptography and Data Security
Cryptographic Implementations and Security
Security and Verification in Computing
Original source
Nov 12, 2021·Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
25 cites
Constant-Overhead Zero-Knowledge for RAM Programs

Nicholas Franzese, Jonathan Katz, Steve Lu, Rafail Ostrovsky · 6 authors

We show a constant-overhead interactive zero-knowledge (ZK) proof system for RAM programs, that is, a ZK proof in which the communication complexity as well as the running times of the prover and verifier scale linearly in the size of the memory N and the running time T of the underlying RAM program. Besides yielding an asymptotic improvement of prior work, our implementation gives concrete performance improvements for RAM-based ZK proofs. In particular, our implementation supports ZK proofs of private read/write accesses to 64~MB of memory (224 32-bit words) using only 34~bytes of communication per access, a more than 80x improvement compared to the recent BubbleRAM protocol. We also design a lightweight RISC CPU that can efficiently emulate the MIPS-I instruction set, and for which our ZK proof communicates only ~320 bytes per cycle, more than 10x less than the BubbleRAM CPU. In a 100 Mbps network, we can perform zero-knowledge executions of our CPU (with 64~MB of main memory and 4~MB of program memory) at a clock rate of 6.6 KHz.

Cryptography and Data Security
Distributed systems and fault tolerance
Security and Verification in Computing
Original source
Nov 12, 2021·Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
20 cites
Zero Knowledge Static Program Analysis

Zhiyong Fang, David Darais, Joseph P. Near, Yupeng Zhang

Static program analysis tools can automatically prove many useful properties of programs. However, using static analysis to prove to a third party that a program satisfies a property requires revealing the program's source code. We introduce the concept of zero-knowledge static analysis, in which the prover constructs a zero-knowledge proof about the outcome of the static analysis without revealing the program. We present novel zero-knowledge proof schemes for intra- and inter-procedural abstract interpretation. Our schemes are significantly more efficient than the naive translation of the corresponding static analysis algorithms using existing schemes. We evaluate our approach empirically on real and synthetic programs; with a pairing-based zero knowledge proof scheme as the backend, we are able to prove the control flow analysis on a 2,000-line program in 1,738s. The proof is only 128 bytes and the verification time is 1.4ms. With a transparent zero knowledge proof scheme based on discrete-log, we generate the proof for the tainting analysis on a 12,800-line program in 406 seconds, the proof size is 282 kilobytes, and the verification time is 66 seconds.

Open access
Security and Verification in Computing
Adversarial Robustness in Machine Learning
Advanced Malware Detection Techniques
Original source
Nov 3, 2021·2021 Sixth International Conference on Informatics and Computing (ICIC)
44 cites
Management of Access Control for Decentralized Online Educations using Blockchain Technology

Lista Meria, Qurotul Aini, Nuke Puji Lestari Santoso, Untung Raharja · 5 authors

The rapid development of information technology opens up opportunities for the development of better services in the field of education. With internet services, the information that students have is not limited by space, place, time and distance. Created a network that does not have a service provider acting as a central authority and users have access to control information that avoids the presence of third parties. An alternative solution to today’s centralized networked learning systems uses the efficient and distributed Decentralized Online Educations (DOE). This platform uses blockchain technology as an educational data storage system that is used to solve academic privacy issues in a decentralized system. This study, created a manageable and auditable access control framework for Decentralized Online Education (DOE) using blockchain technology to discuss the definition of privacy policy.

Blockchain Technology in Education and Learning
Security and Verification in Computing
Blockchain Technology Applications and Security
Original source
Nov 1, 2021·2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)
178 cites
SMARTIAN: Enhancing Smart Contract Fuzzing with Static and Dynamic Data-Flow Analyses

Jaeseung Choi, Doyeon Kim, Soomin Kim, Gustavo Grieco · 6 authors

Unlike traditional software, smart contracts have the unique organization in which a sequence of transactions shares persistent states. Unfortunately, such a characteristic makes it difficult for existing fuzzers to find out critical transaction sequences. To tackle this challenge, we employ both static and dynamic analyses for fuzzing smart contracts. First, we statically analyze smart contract bytecodes to predict which transaction sequences will lead to effective testing, and figure out if there is a certain constraint that each transaction should satisfy. Such information is then passed to the fuzzing phase and used to construct an initial seed corpus. During a fuzzing campaign, we perform a lightweight dynamic data-flow analysis to collect data-flow-based feedback to effectively guide fuzzing. We implement our ideas on a practical open-source fuzzer, named SMARTIAN. SMARTIAN can discover bugs in real-world smart contracts without the need for the source code. Our experimental results show that SMARTIAN is more effective than existing state-of-the-art tools in finding known CVEs from real-world contracts. SMARTIAN also outperforms other tools in terms of code coverage.

2 source records
Advanced Malware Detection Techniques
Software Testing and Debugging Techniques
Security and Verification in Computing
Original source
Oct 29, 2021·2021 International Conference on Smart Generation Computing, Communication and Networking (SMART GENCON)
3 cites
A Template for Alternative Proof of Work for Cryptocurrencies

Sajedul Talukder, Riley Vaughn

Many popular cryptocurrencies, such as Bitcoin, form consensus through a method known as Proof of Work. Problematically, current implementations of Proof of Work require immense amounts of energy consumption, where a majority of this energy is spent solely on securing consensus. Our focus is not to directly decrease energy consumption, but to allow for more useful and pragmatic computation to come from Proof of Work, such that energy is saved by not running these computational tasks separately. In this paper, we create a template for Proof of Work protocols, such that if followed, can guarantee similar security assurances as to the Proof of Work present in Bitcoin. Secondarily, we also develop “useful” prototypes based on this template.

Blockchain Technology Applications and Security
Security and Verification in Computing
Physical Unclonable Functions (PUFs) and Hardware Security
Original source
Oct 28, 2021·IEEE Internet of Things Magazine 2021
16 cites
Secure Blockchain Platform for Industrial IoT with Trusted Computing Hardware

Qing Yang, Hao Wang, Xiaoxiao Wu, Taotao Wang · 6 authors

As a disruptive technology that originates from cryptocurrency, blockchain provides a trusted platform to facilitate industrial IoT (IIoT) applications. However, implementing a blockchain platform in IIoT scenarios confronts various security challenges due to the rigorous deployment condition. To this end, we present a novel design of secure blockchain based on trusted computing hardware for IIoT applications. Specifically, we employ the trusted execution environment (TEE) module and a customized security chip to safeguard the blockchain against different attacking vectors. Furthermore, we implement the proposed secure IIoT blockchain on the ARM-based embedded device and build a small-scale IIoT network to evaluate its performance. Our experimental results show that the secure blockchain platform achieves a high throughput (150TPS) with low transaction confirmation delay (below 66ms), demonstrating its feasibility in practical IIoT scenarios. Finally, we outline the open challenges and future research directions.

Open access
2 source records
cs.CR
cs.NI
Blockchain Technology Applications and Security
Original source
Oct 27, 2021·IEEE Transactions on Software Engineering
41 cites
Aroc: An Automatic Repair Framework for On-Chain Smart Contracts

Hai Jin, Zeli Wang, Ming Wen, Weiqi Dai · 6 authors

Ongoing smart contract attack events have seriously impeded the practical application of blockchain. Although lots of researches have been conducted, they mostly focus on off-chain vulnerability detection. However, smart contracts cannot be modified once they have been deployed on-chain, thus existing techniques cannot protect those deployed contracts from being attacked. To mitigate this problem, we propose a general smart contract repairer named Aroc, which can automatically patch vulnerable deployed contracts without changing the contract codes. The core insight of Aroc is to generate patch contracts to abort malicious transactions in advance. Taking the three most serious bug types (i.e., reentrancy, arithmetic bugs, and unchecked low-level checks) as examples, we present how Aroc automatically repairs them on-chain. We conduct abundant evaluations on four kinds of datasets to evaluate the effectiveness and efficiency of Aroc. In particular, Aroc can repair 95.95% of the vulnerable contracts with an average correctness ratio of 93.32%. Meanwhile, Aroc introduces acceptable additional overheads to smart contract users and blockchain miners. When compared with the state-of-the-art techniques, Aroc introduces either fewer execution overheads or contract codes.

Open access
Blockchain Technology Applications and Security
Advanced Malware Detection Techniques
Security and Verification in Computing
Original source
Oct 25, 2021·IEEE Internet of Things Journal
48 cites
Blockchain and SGX-Enabled Edge-Computing-Empowered Secure IoMT Data Analysis

Ying Gao, Hongliang Lin, Yijian Chen, Yangliang Liu

The Internet of Medical Things (IoMT) is an important application of the Internet of Things (IoT) in the health field, including remote health monitoring and remote medical diagnosis. This not only brings convenience to the patient but also reduces the cost of the patient. However, the surge of data brought by mobile health monitoring equipment challenges the traditional centralized data processing model. In particular, medical data are closely related to patient privacy. Therefore, only part of the specific medical data should be provided to the medical institutions in need, rather than all the data, to ensure the confidentiality of the data to the greatest extent. But curious data processing centers can easily lead to data leakage. To tackle these challenges, we use edge computing and blockchain to build a new framework. In particular, the trusted execution environment, namely, software guard extension (SGX) technology, is introduced into edge computing to ensure the confidentiality of the data analysis process. The blockchain authenticates the IoMT devices and cloud service providers that are added to the network and provides an access policy management mechanism for IoMT data. Moreover, a prototype of the proposed framework is implemented using Hyperledger Fabric and Intel SGX, and the analysis of the blockchain and SGX performance are also presented.

Blockchain Technology Applications and Security
IoT and Edge/Fog Computing
Security and Verification in Computing
Original source
Oct 22, 2021·Lecture notes in computer science
33 cites
Formal Verification of the Ethereum 2.0 Beacon Chain

Franck Cassez, Joanne Fuller, Aditya Asgaonkar

Abstract We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators , their stakes , their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain’s network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact with the code and proofs in Dafny is available at https://github.com/ConsenSys/eth2.0-dafny .

Open access
3 source records
Security and Verification in Computing
Advanced Malware Detection Techniques
Software Engineering Research
Original source
Oct 19, 2021·Lecture notes in computer science
57 cites
Three Attacks on Proof-of-Stake Ethereum

Caspar Schwarz-Schilling, Joachim Neu, Barnabé Monnot, Aditya Asgaonkar · 6 authors

Recently, two attacks were presented against Proof-of-Stake (PoS) Ethereum: one where short-range reorganizations of the underlying consensus chain are used to increase individual validators' profits and delay consensus decisions, and one where adversarial network delay is leveraged to stall consensus decisions indefinitely. We provide refined variants of these attacks, considerably relaxing the requirements on adversarial stake and network timing, and thus rendering the attacks more severe. Combining techniques from both refined attacks, we obtain a third attack which allows an adversary with vanishingly small fraction of stake and no control over network message propagation (assuming instead probabilistic message propagation) to cause even long-range consensus chain reorganizations. Honest-but-rational or ideologically motivated validators could use this attack to increase their profits or stall the protocol, threatening incentive alignment and security of PoS Ethereum. The attack can also lead to destabilization of consensus from congestion in vote processing.

Open access
3 source records
Distributed systems and fault tolerance
Internet Traffic Analysis and Secure E-voting
Security and Verification in Computing
Original source
Oct 18, 2021·arXiv
11 cites
Lessons Learned from Blockchain Applications of Trusted Execution Environments and Implications for Future Research

Rabimba Karanjai, Lei Xu, Lin Chen, Fengwei Zhang · 6 authors

Modern computer systems tend to rely on large trusted computing bases (TCBs) for operations. To address the TCB bloating problem, hardware vendors have developed mechanisms to enable or facilitate the creation of a trusted execution environment (TEE) in which critical software applications can execute securely in an isolated environment. Even under the circumstance that a host OS is compromised by an adversary, key security properties such as confidentiality and integrity of the software inside the TEEs can be guaranteed. The promise of integrity and security has driven developers to adopt it for use cases involving access control, PKS, IoT among other things. Among these applications include blockchain-related use cases. The usage of the TEEs doesn't come without its own implementation challenges and potential pitfalls. In this paper, we examine the assumptions, security models, and operational environments of the proposed TEE use cases of blockchain-based applications. The exercise and analysis help the hardware TEE research community to identify some open challenges and opportunities for research and rethink the design of hardware TEEs in general.

Open access
2 source records
cs.CR
Security and Verification in Computing
Cloud Data Security Solutions
Original source
Oct 15, 2021·Lecture notes in computer science
20 cites
Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer · 6 authors

The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. MVP has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing in a few minutes. Besides the simplicity of smart contracts and the Move language, three transformations are responsible for the practicality of MVP: (1) an alias-free memory model, (2) fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by MVP in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.

Open access
3 source records
Blockchain Technology Applications and Security
Security and Verification in Computing
Cryptography and Data Security
Original source
Oct 15, 2021·Proceedings of the ACM on Programming Languages
17 cites
Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts

Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Κonstantinos Τriantafyllou · 5 authors

We present a static analysis approach that combines concrete values and symbolic expressions. This symbolic value-flow (“symvalic”) analysis models program behavior with high precision, e.g., full path sensitivity. To achieve deep modeling of program semantics, the analysis relies on a symbiotic relationship between a traditional static analysis fixpoint computation and a symbolic solver: the solver does not merely receive a complex “path condition” to solve, but is instead invoked repeatedly (often tens or hundreds of thousands of times), in close cooperation with the flow computation of the analysis. The result of the symvalic analysis architecture is a static modeling of program behavior that is much more complete than symbolic execution, much more precise than conventional static analysis, and domain-agnostic: no special-purpose definition of anti-patterns is necessary in order to compute violations of safety conditions with high precision. We apply the analysis to the domain of Ethereum smart contracts. This domain represents a fundamental challenge for program analysis approaches: despite numerous publications, research work has not been effective at uncovering vulnerabilities of high real-world value. In systematic comparison of symvalic analysis with past tools, we find significantly increased completeness (shown as 83-96% statement coverage and more true error reports) combined with much higher precision, as measured by rate of true positive reports. In terms of real-world impact, since the beginning of 2021, the analysis has resulted in the discovery and disclosure of several critical vulnerabilities, over funds in the many millions of dollars. Six separate bug bounties totaling over $350K have been awarded for these disclosures.

Open access
2 source records
Advanced Malware Detection Techniques
Security and Verification in Computing
Software Engineering Research
Original source
Oct 14, 2021·arXiv (Cornell University)
1 cites
zk-Fabric, a Polylithic Syntax Zero Knowledge Joint Proof System

Sheng Yih Sun, Tong Wen

In this paper, we create a single-use and full syntax zero-knowledge proof system, a.k.a zk-Fabric. Comparing with zk-SNARKS and another variant zero-knowledge proofing system, zkBOO and it's variant zkBOO++. We present multiple new approaches on how to use partitioned garbled circuits to achieve a joint zero-knowledge proof system, with the benefits of less overhead and full syntax verification. zk-Fabric based on partitioned garbled circuits has the advantage of being versatile and single-use, meaning it can be applied to arbitrary circuits with more comprehensive statements, and it can achieve the non-interactivity among all participants. One of the protocols proposed within is used for creating a new kind of partitioned garbled circuits to match the comprehensive Boolean logical expression with multiple variables, we use the term "polythitic syntax" to refer to the context-based multiple variables in a comprehensive statement. We also designed a joint zero knowledge proof protocol that uses partitioned garbled circuits

Open access
2 source records
Cryptography and Data Security
Security and Verification in Computing
Formal Methods in Verification
Original source
Oct 1, 2021·Proceedings of the ACM on Programming Languages
29 cites
SolType: Refinement Types for Arithmetic Overflow in Solidity

Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Işıl Dillig · 5 authors

As smart contracts gain adoption in financial transactions, it becomes increasingly important to ensure that they are free of bugs and security vulnerabilities. Of particular relevance in this context are arithmetic overflow bugs, as integers are often used to represent financial assets like account balances. Motivated by this observation, this paper presents SolType, a refinement type system for Solidity that can be used to prevent arithmetic over- and under-flows in smart contracts. SolType allows developers to add refinement type annotations and uses them to prove that arithmetic operations do not lead to over- and under-flows. SolType incorporates a rich vocabulary of refinement terms that allow expressing relationships between integer values and aggregate properties of complex data structures. Furthermore, our implementation, called Solid, incorporates a type inference engine and can automatically infer useful type annotations, including non-trivial contract invariants. To evaluate the usefulness of our type system, we use Solid to prove arithmetic safety of a total of 120 smart contracts. When used in its fully automated mode (i.e., using Solid's type inference capabilities), Solid is able to eliminate 86.3% of redundant runtime checks used to guard against overflows. We also compare Solid against a state-of-the-art arithmetic safety verifier called VeriSmart and show that Solid has a significantly lower false positive rate, while being significantly faster in terms of verification time.

Open access
2 source records
cs.PL
Security and Verification in Computing
Advanced Malware Detection Techniques
Original source
Oct 1, 2021·Publikationsdatenbank der Fraunhofer-Gesellschaft (Fraunhofer-Gesellschaft)
1 cites
Privacy-Preserving Remote Attestation Protocol

Dominik Roy George

Binary Attestation (BA) ist ein Sicherheitsmechanismus, der schon lange zur Sicherstellung der Integrität der auszuführenden Software auf einem Computerssystem verwendet wird. Dies wird durch die Anwendung der Konzepte von Trusted Computing Technologie erreicht. Die Konzepte der Trusted Computing Technologie sind: Trusted Platform Module (TPM), measured/trusted boot und Linux Integrity Measurement Architecture (IMA). Damit die Vertrauenswürdigkeit des Betriebszustandes des Systems überprüft werden kann, wird eine Logdatei erstellt. Diese enthält den Dateinamen und die Hash-Summe der Softwarekomponenten, welche an das TPM gebunden wird. Zu einem späteren Zeitpunkt kann eine entfernte Partei (Verifier) die Evidenz verifizieren, um zu sehen, ob der Betriebszustand des Systems vertrauenswürdig ist. Dies wird als Remote Attestation (RA) bezeichnet.Auf den Systemen im Bereich der Cyber-physische Systeme (z. B.: Energie Netze und Kernkraftwerke) und im Bereich der Verkehrsmittel (z. B.: Züge und Automobil Fahrzeuge) laufen mehrere Anwendungen von verschiedenen Herstellern. Bei bisherigen Ansätzen der BA, werden alle Einträge der Logdatei von allen laufenden Anwendungen aller Hersteller während der RA an die entfernte Partei preisgegeben. Daher gewährleistet die Binary Remote Attestation keine Privatheit. Diese Masterarbeit adressiert die genannte Schwäche von der Binary Remote Attestation indem es eine Privacy-Preserving Remote Attestation Ansatz erstellt. Im Kern der Arbeitsteht die Konzeptionierung eines Ansatzes, welches den Trusted Computing Sektor mit Privacy-Enhancing Technologie verknüpft. Der Ansatz bewahrt die Privatheit, indem alle Logeinträge verschleiert werden. Dabei werden dem Verifier nur die jeweilig zugehörigen Einträge offengelegt. Dadurch kann der Attester dem Verifier durch die Anwendung des Schnorr Non-Interactive Zero-Knowledge Proofs über eine elliptische Kurve (Schnorr-Signatur) beweisen, dass es sich bei den ausgeblendeten Einträgen um die tatsächlich laufende Anwendung auf dem System des Attesters handelt, ohne die anderen Einträge preiszugeben. Dieser Ansatz wird in dieser Arbeit als Proof-of-Concept umgesetzt. Die Leistung und die Privatheit des Proof-of-Concepts wurden in dieser Arbeit analysiert. Hierdruch wird gezeigt, dass die Privatheit gegenüber der entfernten Partei gewährleistet wird, während die Integrität und Authentizität des Betriebszustands des Systems vom Attester sichergestellt wird. Die Gewährleistung der Privatheit geht allerdings mit einem Anstieg der benötigten Ressourcen einher.

Open access
Network Security and Intrusion Detection
IoT and Edge/Fog Computing
Security and Verification in Computing
Original source
Oct 1, 2021·2021 IEEE 30th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE)
8 cites
A Solidity-to-CPN Approach Towards Formal Verification of Smart Contracts

Ikram Garfatta, Kaïs Klai, Mohamed Graïet, Walid Gaaloul

While Blockchains can open intriguing opportunities of research in many application contexts, they come with the risk of bringing new unconventional problems. In fact, because of the monetary value they hold, Blockchains have been subject to many attacks. Smart contracts, which are at the core of second-generation Blockchains, have been proven to be the origin of such attacks due to the exploitable vulnerabilities their code may hold. It is therefore an essential requirement to prove the correctness of the smart contracts to be deployed on a Blockchain to ensure its protection. The existing approaches have been focusing on targeting generic vulnerabilities like reentrancy, without offering the possibility to check temporal-based contract-specific properties. In this paper, we aim to address smart contracts verification while supporting such properties. We propose and implement a transformation of Solidity smart contracts into Coloured Petri nets and investigate the capability of existing model checking tools to check specific temporal properties of the formally modeled contract.

Blockchain Technology Applications and Security
Security and Verification in Computing
Cryptography and Data Security
Original source
Oct 1, 2021·2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)
129 cites
Peculiar: Smart Contract Vulnerability Detection Based on Crucial Data Flow Graph and Pre-training Techniques

Hongjun Wu, Zhuo Zhang, Shangwen Wang, Lei Yan · 8 authors

Smart contracts with natural economic attributes have been widely and rapidly developed in various fields. However, the bugs and vulnerabilities in smart contracts have brought huge economic losses, which has strengthened people's attention to the security issues of smart contracts. The immutability of smart contracts makes people more willing to conduct security checks before deploying smart contracts. Nonetheless, existing smart contract vulnerability detection techniques are far away from enough: static analysis approaches rely heavily on manually crafted heuristics which is difficult to reuse across different types of vulnerabilities while deep learning based approaches also have unique limitations. In this study, we propose a novel approach, Peculiar, which uses Pre-training technique for detection of smart contract vulnerabilities based on crucial data flow graph. Compared against the traditional data flow graph which is already utilized in existing approach, crucial data flow graph is less complex and does not bring an unnecessarily deep hierarchy, which makes the model easy to focus on the critical features. Moreover, we also involve pre-training technique in our model due to the dramatic improvements it has achieved on a variety of NLP tasks. Our empirical results show that Peculiar can achieve 91.80 % precision and 92.40 % recall in detecting reentrancy vulnerability, one of the most severe and common smart contract vulnerabilities, on 40,932 smart contract files, which is significantly better than the state-of-the-art methods (e.g., Smartcheck achieves 79.37% precision and 70.50% recall). Meanwhile, another experiment shows that Peculiar is more discerning to reentrancy vulnerability than existing approaches. The ablation experiment reveals that both crucial data flow graph and pre-trained model contribute significantly to the performances of Peculiar.

2 source records
Advanced Malware Detection Techniques
Adversarial Robustness in Machine Learning
Security and Verification in Computing
Original source
Sep 27, 2021·2021 3rd Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS)
0 cites
Coupling Smart Contracts: A Comparative Case Study

Sebastian Friebe, Oliver Stengele, Hannes Hartenstein, Martina Zitterbart

When software systems become more complex, it can be advantageous to partition their code into multiple, separate components. In this work, we examine how multiple smart contracts can be coupled to work together. When coupling smart contracts, different design approaches are possible with their own advantages and disadvantages. As an example, we couple two smart contract applications on the Ethereum blockchain: Palinodia and DecentID. Palinodia can be used to ensure the integrity of downloaded executable binaries by checking their hashes against the hashes stored in the blockchain. To make sure that not everyone can modify the data stored on the blockchain, an identity management system is required. This task is fulfilled by DecentID, which provides decentralized identities stored as smart contracts on the blockchain. We evaluate approaches of coupling these two applications and discuss their benefits and drawbacks for this use case.

Open access
Blockchain Technology Applications and Security
Distributed systems and fault tolerance
Security and Verification in Computing
Original source
Sep 27, 2021·2021 3rd Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS)
34 cites
Smart Contracts Refinement for Gas Optimization

Keerthi Nelaturu, Sidi Mohamed Beillahi, Fan Long, Andreas Veneris

Smart contracts facilitate the execution of programmable code on a blockchain. The cost for executing smart contract code is metered using gas - the exact amount of which is based on the computational complexity of the underlying smart contract. Hence, it is imperative to optimize smart contract code to reduce gas consumption and, in some instances, to even avoid malicious attacks. In this paper, we propose an approach to optimize the gas consumption of smart contracts, specifically loop control structures. We present a prototype implementation of our approach using off-the-shelf tools for Solidity smart contracts. We experimentally evaluate our technique using 72 Solidity smart contracts. Our evaluation demonstrates the average gas cost savings per transaction to be around 23,943 gas units, or an equivalent 21% decrease in gas costs. Although the approach causes a slight increase in deployment costs due to the additional internal functions, this is only 16,710 gas units on the average, or a 5% of the total deployment cost. As this overhead remains quite reasonable when compared to the gas cost savings for each transaction, it also confirms the efficacy, practicality and effectiveness of the proposed methodology.

Blockchain Technology Applications and Security
Security and Verification in Computing
Advanced Malware Detection Techniques
Original source
Sep 23, 2021·arXiv (Cornell University)
3 cites
Security Review of Ethereum Beacon Clients

Jean-Philippe Aumasson, Denis Kolegov, Ε. Σταθοπούλου

The beacon chain is the backbone of the Ethereum's evolution towards a proof-of-stake-based scalable network. Beacon clients are the applications implementing the services required to operate the beacon chain, namely validators, beacon nodes, and slashers. Security defects in beacon clients could lead to loss of funds, consensus rules violation, network congestion, and other inconveniences. We reported more than 35 issues to the beacon client developers, including various security improvements, specification inconsistencies, missing security checks, exposure to known vulnerabilities. None of our findings appears to be high-severity. We covered the four main beacon clients, namely Lighthouse (Rust), Nimbus (Nim), Prysm (Go), and Teku (Java). We looked for bugs in the logic and implementation of the new security-critical components (BLS signatures, slashing, networking protocols, and API) over a 3-month project that followed a preliminary analysis of BLS signatures code. We focused on Lighthouse and Prysm, the most popular clients, and thus the highest-value targets. Furthermore, we identify protocol-level issues, including replay attacks and incomplete forward secrecy. In addition, we reviewed the network fingerprints of beacon clients, discussing the information obtainable from passive and active searches, and we analyzed the supply chain risk related to third-party dependencies, providing indicators and recommendations to reduce the risk of backdoors and unpatchable vulnerabilities. Our results suggest that despite intense scrutiny by security auditors and independent researchers, the complexity and constant evolution of a platform like Ethereum requires regular expert review and thorough SSDLC practices.

Open access
2 source records
Cryptography and Data Security
Cloud Data Security Solutions
Security and Verification in Computing
Original source
Sep 21, 2021·Security and Communication Networks
14 cites
SESCon: Secure Ethereum Smart Contracts by Vulnerable Patterns’ Detection

Amir Ali, Zain Ul Abideen, Kalim Ullah

Ethereum smart contracts have been gaining popularity toward the automation of so many domains, i.e., FinTech, IoT, and supply chain, which are based on blockchain technology. The most critical domain, e.g., FinTech, has been targeted by so many successful attacks due to its financial worth of billions of dollars. In all attacks, the vulnerability in the source code of smart contracts is being exploited and causes the steal of millions of dollars. To find the vulnerability in the source code of smart contracts written in Solidity language, a state-of-the-art work provides a lot of solutions based on dynamic or static analysis. However, these tools have shown a lot of false positives/negatives against the smart contracts having complex logic. Furthermore, the output of these tools is not reported in a standard way with their actual vulnerability names as per standards defined by the Ethereum community. To solve these problems, we have introduced a static analysis tool, SESCon (secure Ethereum smart contract), applying the taint analysis techniques with XPath queries. Our tool outperforms other analyzers and detected up to 90% of the known vulnerability patterns. SESCon also reports the detected vulnerabilities with their titles, descriptions, and remediations as per defined standards by the Ethereum community. SESCon will serve as a foundation for the standardization of vulnerability detection.

Open access
Blockchain Technology Applications and Security
Security and Verification in Computing
Advanced Malware Detection Techniques
Original source