Franklin Schrans, Daniel Hails, Alexander Harkness, Sophia Drossopoulou · 5 authors
The Ethereum blockchain platform supports the execution of decentralised applications or smart contracts. These typically hold and transfer digital currency to other parties on the platform; however, they have been subject to numerous attacks due to the unintentional introduction of bugs. Over a billion dollars worth of currency has been stolen since its release in July 2015. As smart contracts cannot be updated after deployment, it is imperative that the programming language supports the development of robust contracts. We propose Flint, a new statically-typed programming language specifically designed for writing robust smart contracts. Flint's features enforce the writing of safe and predictable code. To encourage good practices, we introduce protection blocks. Protection blocks restrict who can run code and when (using typestate) it can be executed. To prevent vulnerabilities relating to the unintentional loss of currency, Flint Asset traits provide safe atomic operations, ensuring the state of contracts is always consistent. Writes to state are restricted, simplifying reasoning about smart contracts.
This paper describes a new but state-of-the-art approach to provide authenticity in mqtt sessions using the means of zero-knowledge-proofs. This approach completely voids session hijacking for the mqtt protocol and provides authenticity without the need for any network-security nor channel-security nor broker-based predefined ACLs. The presented approach does not require the broker to keep any secrets for session handling, what so ever. Moreover, it allows the clientID, which represents the identification for a session, to be publicly known. The presented approach allows completely anonymous but authentic sessions, hence the broker does not need any a priori knowledge of the client-party. As it is especially targeted for applications within the world of IoT, the presented approach is tuned to require only the minimum in extra power in terms of energy and space. The approach does not introduce any new concept, but simply fusions a state-of-the-art cryptographic zero knowledge proof of identity with the existing MQTT-5 specification. Thus no protocol extension is required in order to provide the targeted security properties. The described approach is completely agnostic to the application layer at the client side and is only required during mqtt-session establishment.
Number of internet connected devices is increasing as IoT is getting more prevalent. Volume of data collected by IoT sensors is very high and requires considerable resources for data processing like analytics. Edge processing enables getting the sensor data processed closer to the source. It's not always possible and/or economical to set up a resource intense infrastructure at the edge. This paper proposes use of blockchain based decentralized application to enable IoT edge processing. With this setup, it is possible for a resource owner to join the ecosystem and to lend the compute resources as needed. IoT devices can offload some of the edge computation to the resource owner nodes as and when required. This paper explains architectural components and overall solution for implementation. Based on the usecase of video analytics at edge, experimental setup is implemented for the IoT edge solution using hyperledger sawtooth blockchain.
Summary We present an overview of hybrid Casper the Friendly Finality Gadget (FFG), a proofâofâstake checkpointing protocol overlaid onto Ethereum's proofâofâwork blockchain. We describe its core functionalities and reward scheme and explore its properties. Our findings indicate that Casper's implemented incentives mechanism ensures liveness, while providing safety guarantees that improve over standard proofâofâwork protocols. On the basis of a minimal impact implementation of the protocol as a smart contract on the blockchain, we discuss additional issues related to parametrization, funding, throughput, and network overhead and detect potential limitations.
Summary The IoT is changing the way we interact with the world. Very soon, almost all of our daily tasks will be made through self intelligent systems embedded in devices scattered all around us. Their mission is to turn our cities, transportation systems, buildings, homes, and bodies in smart environments. These environments will bring us more comfort, improve our performance, increase our profits, and take away timeâconsuming tasks. However, besides its great benefits, the IoT is also a big source of concerns, mainly because a good part of its devices will handle private and confidential information. Recently, cases of successful IoT invasions only worsen this scenario and show us that the today's adopted access control systems need to be replaced by more efficiently and secure ones. To overcome these access control problems, in this work, we present the ControlChain. The ControlChain is an access control authorization architecture that is heavily based on Blockchain technology. We also demonstrate the viability of the ControlChain through the EâControlChain, a proofâofâconcept developed to run over the Ethereum network. Our proposals follows the IoT tendency requirements and are userâtransparent, userâfriendly, fully decentralized, scalable, fault tolerant, and compatible with a wide range of today's access control models already used in the IoT. Finally, we also make a cost and a performance analysis of EâControlChain, using a Raspberry Pi as an IoT device.
This paper reports on the development of a formal symbolic process virtual machine (FSPVM) denoted as FSPVM-E for verifying the reliability and security of Ethereum-based services at the source code level of smart contracts, and a Coq proof assistant is employed for both programming the system and for proving its correctness. The current version of FSPVM-E adopts execution-verification isomorphism, which is an application extension of Curry-Howard isomorphism, as its fundamental theoretical framework to combine symbolic execution and higher-order logic theorem proving. The four primary components of FSPVM-E include a general, extensible, and reusable formal memory framework, an extensible and universal formal intermediate programming language denoted as Lolisa, which is a large subset of the Solidity programming language using generalized algebraic datatypes, the corresponding formally verified interpreter of Lolisa, denoted as FEther, and assistant tools and libraries. The self-correctness of all components is certified in Coq. Currently, FSPVM-E supports the ERC20 token standard, and can automatically and symbolically execute Ethereum-based smart contracts, scan their standard vulnerabilities, and verify their reliability and security properties with Hoare-style logic in Coq. To the best of authors' knowledge, the present work represents the first hybrid formal verification system implemented in Coq for Ethereum smart contracts that is applied at the Solidity source code level.
In the last year we have seen a great deal of both academic and practical
interest in the topic of vulnerabilities in smart contracts, particularly those
developed for the Ethereum blockchain. In this paper we survey the 21,270
vulnerable contracts reported by six recent academic projects. Contrary to what
might have been believed given the reported number of vulnerable contracts,
there has been precious little in terms of actual exploitation when it comes to
these vulnerabilities. We find that at most 504 out of 21,270 contracts have
been subjected to exploits. This corresponds to at most 9,066 ETH (~1.8 million
USD), or only 0.29% of the 3 million ETH (600 million USD) claimed in some of
the papers. While we are certainly not implying that smart contract
vulnerability research is without merit, our results suggest that the potential
impact of vulnerable code had been greatly exaggerated.
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning · 5 authors
Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventing the duplication or deletion of a contract's assets. This article presents the design and type-theoretic foundation of Nomos, a programming language for digital contracts that addresses these challenges. To express and enforce protocols, Nomos is based on shared binary session types. To control resource usage, Nomos employs automatic amortized resource analysis. To prevent the duplication or deletion of assets, Nomos uses a linear type system. A monad integrates the effectful session-typed language with a general-purpose functional language. Nomos' prototype implementation features linear-time type checking and efficient type reconstruction that includes automatic inference of resource bounds via off-the-shelf linear optimization. The effectiveness of the language is evaluated with case studies about implementing common smart contracts such as auctions, elections, and currencies. Nomos is completely formalized, including the type system, a cost semantics, and a transactional semantics to instantiate Nomos contracts on a blockchain. The type soundness proof ensures that protocols are followed at run-time and that types establish sound upper bounds on the resource consumption, ruling out re-entrancy and out-of-gas vulnerabilities.
In the pharmaceutical industry, process validation tasks are based on the raw data and its derived analytical results generated from the process. Process validation failure affects both patient safety and the economic success of the manufacturing company. Hence, data integrity is highly critical in this area. Regulatory agencies, such as the Food and Drug Administration (FDA), reacted to past data integrity breaches by publishing new guidelines on data integrity for the correct handling of data in the pharmaceutical context. In this contribution, we want to show how data integrity can be improved on a technological level, removing the need for trusted third parties and centralized systems for this task. Therefore, we implemented an approach that uses existing tools, currently mostly used by software developers, and combined them with a new smart contract built on top of the Ethereum blockchain. In a case study, we test how data manipulation or backdating of results can be easily detected and how regulatory agencies can audit the complete data flow from the regulatory report back to the original raw data. The results of this contribution outline a possible road map for the development of production-ready tools, such as versioned database systems that natively interoperate with distributed ledgers. This will improve the trustworthiness of pharmaceutical manufacturing data by both protecting the intellectual property of the industrial company and improving the safety of the patients. <i>LAY ABSTRACT:</i> In the pharmaceutical industry, economically driven manufacturing companies are regulated and controlled by regulatory agencies. The pharmaceutical manufacturing companies need to produce large amounts of process and analytical data to show that their products are safe for patients. As the decisions of the regulatory agencies rely on this data, manufacturing companies need to prove how their generated data can be protected from technical breaches or data manipulation. As of today, the available technical solutions to provide data integrity are not working well enough. Regulatory agencies have published multiple documents highlighting the current data integrity issues. In this contribution, we show how blockchain, a technology that multiple cryptocurrencies like Bitcoin rely on, can help to improve the integrity of manufacturing data and data science analysis procedures. Therefore, we combined a smart contract on the Ethereum blockchain with tools currently mostly used by software developers. The presented workflow shows how data integrity can be guaranteed on a technological level without the need for trusted third parties.
Attacks on transactions of Ethereum could be dangerous because they could lead to a big loss of money. There are many tools detecting vulnerabilities in smart contracts trying to avoid potential attacks. However, we found that there are still many missed vulnerabilities in contracts. Motivated by this, we propose a methodology to reinforce EVM to stop dangerous transactions in real time even when the smart contract contains vulnerabilities. Basically, the methodology consists of three steps: monitoring strategy definition, opcode-structure maintenance and EVM instrumentation. Monitoring strategy definition refers to the specific rule to test whether there is a dangerous operation during transaction execution. Opcode-structure maintenance is to maintain a structure to store the rule related opcodes and analyze it before an operation execution. EVM instrumentation inserts the monitoring strategy, interrupting mechanism and the opcode-structure operations in EVM source code. For evaluation, we implement EVM*on js-evm, a widely-used EVM platform written in javascript. We collect 10 contracts online with known bugs and use each contract to execute a dangerous transaction, all of them have been interrupted by our reinforced EVM*, while the original EVM permits all attack transactions. For the time overhead, the reinforced EVM*is slower than the original one by 20-30%, which is tolerable for the financial critical applications.
We propose a framework for threshold cryptosystems under a permissionless-economic model in which the participants are rational profit-maximizing entities. To date, threshold cryptosystems have been considered under permissioned settings with a limited adversary. Our framework relies on an escrow service that slashes and redistributes deposits to incentivize participants to adhere desired behaviors. Today, more than ever, sophisticated escrow services can be implemented over public blockchains like Ethereum, without additional trust assumptions. The key threat to rational threshold cryptosystems is collusion---by cooperating `illegally', a subset of participants can reveal the cryptosystem's secret, which, in turn is translated to unfair profit. Our countermeasure to collusion is framing. If the escrow is notified of collusion, it rewards the framer and slashes the deposits of all other participants. We show that colluding parties find themselves in the prisoner's dilemma, where the dominant strategy is framing.
Jae Min Kim, JaeâWon Lee, Kyungsoo Lee, Junho Huh
Blockchain which enables decentralization of data based on various consensus mechanisms is considered the leading technology of the next generation. Numerous applications are being proposed to benefit from its immunity against modification and manipulation. However, not many appears as a successful business up to now, except for crypto currencies. High operation cost which is essential for the conventional consensus, is acting as an obstacle to the wide adoption of blockchain applications. In this paper, we introduce a novel blockchain platform based on PoP (Proof of Phone), which lowers the operating cost by imposing high entry cost. We conduct theoretical analysis to show that our proposed platform reduces total cost by up to 98.2% compared to that of conventional blockchain. Our new platform will turn various blockchain applications from theory to practice.
The paper presents a BlockChain based distributed framework to manage Antimalware database efficiently. With increased efficiency in computation and network connectivity, systems are delivering better performances day by day. However, the opportunities of initiating malicious activities through malwares are being increased as well. In this work, we propose a distributed framework of Antimalware database management using customized BlockChain that enhances system security by initiating distributed malware prevention program. Due to distributed in nature, BlockChain can ensure better data management without involving any third party.
Blockchain frameworks enable the immutable storage of data. A still open practical question is the so called "oracle" problem, i.e. the way how real world data is actually transferred into and out of a blockchain while preserving its integrity. We present a case study that demonstrates how to use an existing industrial strength secure element for cryptographic software protection (Wibu CmDongle / the "dongle") to function as such a hardware-based oracle for the Hyperledger blockchain framework. Our scenario is that of a dentist having leased a 3D printer. This printer is initially supplied with an amount of x printing units. With each print action the local unit counter on the attached dongle is decreased and in parallel a unit counter is maintained in the Hyperledger-based blockchain. Once a threshold is met, the printer will stop working (by means of the cryptographically protected invocation of the local print method). The blockchain is configured in such a way that chaincode is executed to increase the units again automatically (and essentially trigger any payment processes). Once this has happened, the new unit counter value will be passed from the blockchain to the local dongle and thus allow for further execution of print jobs.
Trusted Execution Environments (TEEs), such as Intel SGX enclaves, use hardware to ensure the confidentiality and integrity of operations on sensitive data. While the technology is available on many processors, the complexity of its programming model and its performance overhead have limited adoption. TEEs provide a new and valuable hardware functionality that has no obvious analogue in programming languages, which means that developers must manually partition their application into trusted and untrusted components. This paper describes an approach that fully integrates trusted execution into a language. We extend the Go language to allow a programmer to execute a goroutine within an enclave, to use low-overhead channels to communicate between the trusted and untrusted environments, and to rely on a compiler to automatically extract the secure code and data. Our prototype compiler and runtime, GOTEE, is a backward-compatible fork of the Go compiler. The evaluation shows that our compiler-driven code and data partitioning efficiently executes both microbenchmarks and applications. On the former, GOTEE achieves a 5.2Ăthroughput and a 2.3Ă latency improvement over the Intel SGX SDK. Our case studies, a Go ssh server, the Go tls package, and a secured keystore inspired by the go-ethereum project, demonstrate that minor source-code modifications suffice to provide confidentiality and integrity guarantees with only moderate performance overheads.
Open access
Security and Verification in Computing
Advanced Malware Detection Techniques
Physical Unclonable Functions (PUFs) and Hardware Security
Eder J. Scheid, Manuel Keller, Muriel Figueredo Franco, Burkhard Stiller
Current projects applying blockchain technology to enhance the trust of NFV environments do not consider the VNF repository. However, the blockchainâs properties can enhance trust by allowing to verify a VNF packageâs integrity without relying (a) on a Trusted Third Party (TTP) for remote attestation or (b) a secure database. This paper presents BUNKER , a Blockchain-based trUsted VNF packagE Repository, intended to be integrated with traditional database-based package verification environments, acting as a trusted repository containing VNF package information. Moreover, BUNKER allows users to acquire VNFs without the need of a TTP using an Ethereum Smart Contract (SC). The SC automatically transfers license fees to the vendor once a VNF is acquired, and sends the VNF packageâs link to the buyer before verifying its integrity.
We give the first construction of three-round non-malleable commitments from the almost minimal assumption of injective one-way functions. Combined with the lower bound of Pass (TCC 2013), our result is almost the best possible w.r.t. standard polynomial-time hardness assumptions (at least w.r.t. black-box reductions). Our results rely on a novel technique which we call 'bidirectional Goldreich-Levin extraction'. Along the way, we also obtain the first rewind secure delayed-input witness indistinguishable (WI) proofs from only injective one-way functions. We also obtain the first construction of an epsilon-extractable commitment scheme from injective one-way functions. We believe both of these to be of independent interest. In particular, as a direct corollary of our rewind secure WI construction, we are able to obtain a construction of 3-round promise zero-knowledge from only injective one-way functions.