Some smart contracts violate decentralization principles by defining privileged accounts that manage other users' assets without permission, introducing centralized risks that have caused financial losses. Existing methods, however, face challenges in accurately detecting diverse centralized risks due to their dependence on predefined behavior patterns. In this paper, we propose JANUS, an automated analyzer for Solidity smart contracts that detects financial centralized risks independently of their specific behaviors. JANUS identifies differences between states reached by privileged and ordinary accounts, and analyzes whether these differences are finance-related. Focusing on the impact of risks rather than behaviors, JANUS achieves improved accuracy compared to existing tools and can uncover centralized risks with unknown patterns. To evaluate JANUS's performance, we compare it with other tools using a dataset of 540 contracts. Our evaluation demonstrates that JANUS outperforms representative tools in terms of detection accuracy for financial centralized risks. Additionally, we evaluate JANUS on a real-world dataset of 33,151 contracts, successfully identifying two types of risks that other tools fail to detect. We also prove that the state traversal method and variable summaries, which are used in JANUS to reduce the number of states to be compared, do not introduce false alarms or omissions in detection.

WebAssembly (WASM) has emerged as a crucial technology in smart contract development for several blockchain platforms. Unfortunately, since their introduction, WASM smart contracts have been subject to several security incidents caused by contract vulnerabilities, resulting in substantial economic losses. However, existing tools for detecting WASM contract vulnerabilities have accuracy limitations, one of the main reasons being the coarse-grained emulation of the on-chain data APIs. In this article, we introduce WACANA, an analyzer for WASM contracts that accurately detects vulnerabilities through fine-grained emulation of on-chain data APIs. WACANA precisely simulates both the structure of on-chain data tables and their corresponding API functions, and integrates concrete and symbolic execution within a coverage-guided loop to balance accuracy and efficiency. Evaluations on a vulnerability dataset of 2,012 contracts show WACANA outperforming state-of-the-art tools in accuracy. Further validation on 5,602 real-world contracts confirms WACANA’s practical effectiveness.

Deep learning has emerged as a promising technology for achieving Android malware detection. To further unleash its detection potentials, software visualization can be integrated for analyzing the details of app behaviors clearly. However, facing increasingly sophisticated malware, existing visualization-based methods, analyzing from one or randomly-selected few views, can only detect limited attack types. We propose and implement LensDroid, a novel technique that detects Android malware by visualizing app behaviors from multiple complementary views. Our goal is to harness the power of combining deep learning and software visualization to automatically capture and aggregate high-level features that are not inherently linked, thereby revealing hidden maliciousness of Android app behaviors. To thoroughly comprehend the details of apps, we visualize app behaviors from three related but distinct views of behavioral sensitivities, operational contexts and supported environments. We then extract high-order semantics based on the views accordingly. To exploit semantic complementarity of the views, we design a deep neural network based model for fusing the visualized features from local to global based on their contributions to downstream tasks. A comprehensive comparison with six baseline techniques is performed on datasets of more than 51K apps in three real-world typical scenarios, including overall threats, app evolution and zero-day malware. The experimental results show that the overall effectiveness of LensDroid is better than the baseline techniques. We also validate the complementarity of the views and demonstrate that the multi-view fusion in LensDroid enhances Android malware detection.

Current formal approaches have been successfully used to find design flaws in many security protocols. However, it is still challenging to automatically analyze protocols due to their large or infinite state spaces. In this paper, we propose SmartVerif, a novel and general framework that pushes the limit of automation capability of Tamarin, a state-of-the-art protocol verifier. The primary technical contribution is thedynamicstrategy inside SmartVerif, which can be used to smartly search proof trees. Different from the existing static strategies, our dynamic strategy can automatically optimize itself according to the security protocols without any human intervention. We implement the strategy by modifying Tamarin and introducing a reinforcement learning algorithm to avoid non-terminating paths in the proof tree. Besides, to improve SmartVerif, we add multiple extracted information for training the reinforcement learning network and design a submodule of Non-termination Estimation to collect training data precisely and rapidly. Experimental results show that SmartVerif can automatically verify all security protocols studied in this paper. The case study validates the efficiency of our dynamic strategy. The experimental results also demonstrate the effectiveness of our extracted information, and the accuracy of the submodule of Non-termination Estimation.