ترغب بنشر مسار تعليمي؟ اضغط هنا

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode

95   0   0.0 ( 0 )
 نشر من قبل Pablo Gordillo
 تاريخ النشر 2018
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English




اسأل ChatGPT حول البحث

Analyzing Ethereum bytecode, rather than the source code from which it was generated, is a necessity when: (1) the source code is not available (e.g., the blockchain only stores the bytecode), (2) the information to be gathered in the analysis is only visible at the level of bytecode (e.g., gas consumption is specified at the level of EVM instructions), (3) the analysis results may be affected by optimizations performed by the compiler (thus the analysis should be done ideally after compilation). This paper presents EthIR, a framework for analyzing Ethereum bytecode, which relies on (an extension of) OYENTE, a tool that generates CFGs; EthIR produces from the CFGs, a rule-based representation (RBR) of the bytecode that enables the application of (existing) high-level analyses to infer properties of EVM code.

قيم البحث

اقرأ أيضاً

BISM (Bytecode-Level Instrumentation for Software Monitoring) is a lightweight bytecode instrumentation tool that features an expressive high-level control-flow-aware instrumentation language. The language follows the aspect-oriented programming para digm by adopting the joinpoint model, advice inlining, and separate instrumentation mechanisms. BISM provides joinpoints ranging from bytecode instruction to method execution, access to comprehensive static and dynamic context information, and instrumentation methods. BISM runs in two instrumentation modes: build-time and load-time. We demonstrate BISM effectiveness using two experiments: a security scenario and a general runtime verification case. The results show that BISM instrumentation incurs low runtime and memory overheads.
We present an efficient and expressive tool for the instrumentation of Java programs at the bytecode-level. BISM (Bytecode-Level Instrumentation for Software Monitoring) is a light-weight Java bytecode instrumentation tool that features an expressive high-level control-flow-aware instrumentation language. The language is inspired by the aspect-oriented programming paradigm in modularizing instrumentation into separate transformers, that encapsulate joinpoint selection and advice inlining. BISM allows capturing joinpoints ranging from bytecode instructions to methods execution and provides comprehensive static and dynamic context information. It runs in two instrumentation modes: build-time and load-time. BISM also provides a mechanism to compose transformers and automatically detect their collision in the base program. Transformers in a composition can control the visibility of their advice and other instructions from the base program. We show several example applications for BISM and demonstrate its effectiveness using three experiments: a security scenario, a financial transaction system, and a general runtime verification case. The results show that BISM instrumentation incurs low runtime and memory overheads.
We introduce a fully automated static analysis that takes a sequential Java bytecode program P as input and attempts to prove that there exists an infinite execution of P. The technique consists in compiling P into a constraint logic program P_CLP an d in proving non-termination of P_CLP; when P consists of instructions that are exactly compiled into constraints, the non-termination of P_CLP entails that of P. Our approach can handle method calls; to the best of our knowledge, it is the first static approach for Java bytecode able to prove the existence of infinite recursions. We have implemented our technique inside the Julia analyser. We have compared the results of Julia on a set of 113 programs with those provided by AProVE and Invel, the only freely usable non-termination analysers comparable to ours that we are aware of. Only Julia could detect non-termination due to infinite recursion.
The High Altitude Water Cherenkov (HAWC) Observatory continuously observes gamma-rays between 100 GeV to 100 TeV in an instantaneous field of view of about 2 steradians above the array. The large amount of raw data, the importance of small number sta tistics, the large dynamic range of gamma-ray signals in time (1 - $10^8$ sec) and angular extent (0.1 - 100 degrees), and the growing need to directly compare results from different observatories pose some special challenges for the analysis of HAWC data. To address these needs, we have designed and implemented a modular analysis framework based on the method of maximum likelihood. The framework facilitates the calculation of a binned Poisson Log-likelihood value for a given physics model (i.e., source model), data set, and detector response. The parameters of the physics model (sky position, spectrum, angular extent, etc.) can be optimized through a likelihood maximization routine to obtain a best match to the data. In a similar way, the parameters of the detector response (absolute pointing, angular resolution, etc.) can be optimized using a well-known source such as the Crab Nebula. The framework was designed concurrently with the Multi-Mission Maximum Likelihood (3ML) architecture, and allows for the definition of a general collection of sources with individually varying spectral and spatial morphologies. Compatibility with the 3ML architecture allows to easily perform powerful joint fits with other observatories. In this contribution, we overview the design and capabilities of the HAWC analysis framework, stressing the overarching design points that have applicability to other astronomical and cosmic-ray observatories.
We present a High-Level Python-based Hardware Description Language (ARGG-HDL), It uses Python as its source language and converts it to standard VHDL. Compared to other approaches of building converters from a high-level programming language into a h ardware description language, this new approach aims to maintain an object-oriented paradigm throughout the entire process. Instead of removing all the high-level features from Python to make it into an HDL, this approach goes the opposite way. It tries to show how certain features from a high-level language can be implemented in an HDL, providing the corresponding benefits of high-level programming for the user.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا