The complexity of the Ethereum smart contracts makes it challenging to avoid security flaws. This problem led to many code analysis tools, which detect potential flaws and report them textually. However, the lack of context and visual information in these reports hinders the stakeholders' under-standing of the detailed information. Visualization can assist a developer in grasping such context, but current state-of-the-art visualization tools provide only fixed and limited visualization types. To this end, we present Contract Viz, based on the versatile platform Eclipse Trace Compass (TC), which supports various views and analyses in parallel. Our contribution enables TC to visualize Ethereum transaction traces using flame charts and gas consumption plots. This reveals information on account activities and provides insights into the correct or possibly flawed behaviors. GitHub repo-https://github.com/AisXiaolinlContractViz You Tube video-https://aisxiaolin.github.io/VideoDemo/

Modern microservice architectures pose challenges in understanding and managing the complex workflows within these decentralized services. In particular, it is difficult to identify anomalous behavior that could indicate a bug or attack. We use traces of microservice application activity (requests and responses) to infer a model of the application’s normal behavior. Our approach mines Petri nets to formally represent concurrent operations and their temporal dependencies with a targeted delay injection approach that accurately and efficiently learns these dependencies. The models produced are both explainable and easy to inspect, which offers more transparency and control. Our evaluation shows that injecting delays during model training allows us to achieve perfect model and log fitness (Move-Model and Move-Log fitness of 1) with just 29 traces. In contrast, a straightforward approach requires over 10,000 traces to achieve similar accuracy. Our models successfully identify anomalies in various experiments, such as traces with one missing or multiple missing activities, and reordered sequences to simulate issues in real-world scenarios. Our approach outperforms the state-of-the-art method, demonstrating higher accuracy.

Smart contracts are computer programs running on blockchains to implement Decentralized Applications. The absence of contract specifications hinders routine tasks, such as contract understanding and testing. In this work, we propose a specification mining approach to infer contract specifications from past transaction histories. Our approach derives high-level behavioral automata of function invocations, accompanied by program invariants statistically inferred from the transaction histories. We implemented our approach as tool SMCON and evaluated it on eleven well-studied Azure benchmark smart contracts and six popular real-world DApp smart contracts. The experiments show that SMCON mines reasonably accurate specifications that can be used to enhance symbolic analysis of smart contracts achieving higher code coverage and up to 56 % speedup, and facilitate DApp developers in maintaining high-quality documentation and test suites.

Computation over sensitive data requires that the computation function is secure and trusted. Existing approaches either do not enforce formal verification, require the user to verify the proof, or lack secure attestation guarantees. In addition, neither addresses the issue of having users once again inspect the application after upgrading the code running in the enclave. We propose an approach that uses a formal specification to guarantee that the behavior of the computation function conforms to the desired functionality. By combining automated verification with attestation on a trusted execution environment, we ensure that only conformant applications are executed. At the same time, we allow updates of the computation function without changing the attestation response, as long as the formal specification still holds. We implement and evaluate the system on several functions; our results show an average overhead of only 50 %. Finally, we demonstrate the validity of the system using a real-world application, Dafny-EVM.

Smart home devices collect and transmit user data to smart home Trigger Action Platforms (TAPs) for processing and executing automation rules. However, this data can also be used to infer user activities or other sensitive information. In this paper, we propose PTAP, a privacy-preserving approach based on adversarial example attacks. PTAP injects targeted perturbations into time-series sensor data, effectively confounding potentially malicious TAP classifiers. Our approach significantly reduces the chance of user activity recognition for a malicious TAP while preserving the essential information for automation rule execution, thus safeguarding TAP utility. We evaluated PTAP using a real-world smart-home dataset and examined its effectiveness in preserving utility through the execution of various IoT applications. Our results demonstrate that PTAP effectively preserves user privacy (reducing the accuracy of a malicious classifier 91 to 6 percent) while maintaining automation rule integrity, providing a practical and effective solution to protect user privacy in smart-home environments.

Decentralized Finance (DeFi) systems leverage blockchain oracles to access off/on-chain data as a service. Therefore, maintaining the integrity of oracle data is essential. However, the integrity of these oracles data can be compromised through different attacks, and the effectiveness of these attacks varies depending on the specific stage of the oracle’s lifecycle. This work presents a comprehensive analysis of this lifecycle, identifying potential attack types and examining the efficacy of existing defense mechanisms. We propose a generalized model encompassing data creation, submission, consensus, election, and deprecation stages. We evaluate our model against seven recent high-profile DeFi exploits totaling $ 187 million. We have also studied bond systems as a preventive measure against at least a subset of oracle exploits. Our findings suggest that while bond systems increase the cost of attacks, thereby fortifying oracle data integrity against adversarial manipulations, they also require careful calibration to avoid hindering honest participation.

Logical flaws in smart contracts are often exploited, leading to significant financial losses. Our tool, HighGuard, detects transactions that violate business logic specifications of smart contracts. HighGuard employs dynamic condition response (DCR) graph models as formal specifications to verify contract execution against these models. It is capable of operating in a cross-chain environment for detecting business logic flaws across different blockchain platforms. We demonstrate HighGuard's effectiveness in identifying deviations from specified behaviors in smart contracts without requiring code instrumentation or incurring additional gas costs. By using precise specifications in the monitor, HighGuard achieves detection without false positives. Our evaluation, involving 54 exploits, confirms HighGuard's effectiveness in detecting business logic vulnerabilities. Our open-source implementation of HighGuard and a screencast of its usage are available at: https://github.com/mojtaba-eshghie/HighGuard https://www.youtube.com/watch?v=sZYVV-slDaY

Industrial embedded systems often require special-ized hardware. However, software engineers have access to such domain-specific hardware only at the continuous integration (CI) stage and have to use simulated hardware otherwise. This results in a higher proportion of compilation errors at the CI stage than in other types of systems, warranting a deeper study. To this end, we create a CI diagnostics solution called 'Shadow Job' that analyzes our industrial CI system. We collected over 40000 builds from 4 projects from the product source code and categorized the compilation errors into 14 error types, showing that the five most common ones comprise 89 % of all compilation errors. Additionally, we analyze the resolution time, size, and distance for each error type, to see if different types of compilation errors are easier to localize or repair than others. Our results show that the resolution time, size, and distance are independent of each other. Our research also provides insights into the human effort required to fix the most common industrial compilation errors. We also identify the most promising directions for future research on fault localization.

We give an account of JPF’s current architecture as it has evolved over the last 20 years. Key changes include a modular, extensible design, and Java 11 support. Java 11 brought with it fundamental changes in the language and its runtime, in particular, a new modular library system, different compilation of string expressions to bootstrap methods, and changes in many internal interfaces that allow access to the loaded code and the virtual machine state. These changes required numerous adaptations in JPF to ensure a successful compilation and correct behavior under Java 11.

Many smart contracts are prone to exploits, which has given rise to analysis tools that try to detect and fix vulnerabilities. Such analysis tools are often trained and evaluated on limited data sets, which has the following drawbacks: 1. The ground truth is often based on the verdict of related tools rather than an actual verification result; 2. Data sets focus on low-level vulnerabilities like reentrancy and overflow; 3. Data sets lack concrete exploit examples. To address these shortconUngs, we introduce XruiGEN, which uses a model-based oracle specification of the business logic of the smart contracts to synthesize valid exploits using LLMs. Our experiments, involving 104 synthesized vulnerability-exploit pairs, demonstrated a 57% success rate in exploiting targeted aspects of the contract. They achieved exploit efficiency with an average of only 3.5 transactions per exploit, highlighting the effectiveness of our methodology.