arXiv subjects

Jinku Li

Publications and source records attributed to Jinku Li.

5 recordsLinked to original sources

arXiv2025

What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection

The application layer of Bluetooth Low Energy (BLE) is a growing source of security vulnerabilities, as developers often neglect to implement critical protections such as encryption, authentication, and freshness. While formal verification offers a principled way to check these properties, the manual effort of constructing formal models makes it impractical for large-scale analysis. This paper introduces a key insight: BLE application security analysis can be reframed as a semantic translation problem, i.e., from real-world code to formal models. We leverage large language models (LLMs) not to directly detect vulnerabilities, but to serve as translators that convert BLE-specific code into process models verifiable by tools like ProVerif. We implement this idea in VerifiaBLE, a system that combines static analysis, prompt-guided LLM translation, and symbolic verification to check three core security features: encryption, randomness, and authentication. Applied to 1,050 Android BLE apps, VerifiaBLE uncovers systemic weaknesses: only 10.2\% of apps implement all three protections, while 53.9\% omit them entirely. Our work demonstrates that using LLMs as structured translators can lower the barrier to formal methods, unlocking scalable verification across security-critical domains.

cs.CR↗

arXiv2025

Trustworthy Reasoning: Evaluating and Enhancing Factual Accuracy in LLM Intermediate Thought Processes

We present a novel framework addressing a critical vulnerability in Large Language Models (LLMs): the prevalence of factual inaccuracies within intermediate reasoning steps despite correct final answers. This phenomenon poses substantial risks in high-stakes domains including healthcare, legal analysis, and scientific research, where erroneous yet confidently presented reasoning can mislead users into dangerous decisions. Our framework integrates three core components: (1) a specialized fact-checking classifier trained on counterfactually augmented data to detect subtle factual inconsistencies within reasoning chains; (2) an enhanced Group Relative Policy Optimization (GRPO) reinforcement learning approach that balances factuality, coherence, and structural correctness through multi-dimensional rewards; and (3) a mechanistic interpretability method examining how factuality improvements manifest in model activations during reasoning processes. Extensive evaluation across multi state-of-the-art models reveals concerning patterns: even leading models like Claude-3.7 and GPT-o1 demonstrate reasoning factual accuracy of only 81.93% and 82.57% respectively. Our approach significantly enhances factual robustness (up to 49.90% improvement) while maintaining or improving performance on challenging benchmarks including Math-500, AIME-2024, and GPQA. Furthermore, our neural activation-level analysis provides actionable insights into how factual enhancements reshape reasoning trajectories within model architectures, establishing foundations for future training methodologies that explicitly target factual robustness through activation-guided optimization.

cs.CL↗

arXiv2022

DeUEDroid: Detecting Underground Economy Apps Based on UTG Similarity

In recent years, the underground economy is proliferating in the mobile system. These underground economy apps (UEware) make profits from providing non-compliant services, especially in sensitive areas such as gambling, pornography, and loans. Unlike traditional malware, most of them (over 80%) do not have malicious payloads. Due to their unique characteristics, existing detection approaches cannot effectively and efficiently mitigate this emerging threat. To address this problem, we propose a novel approach to effectively and efficiently detect UEware by considering their UI transition graphs (UTGs). Based on the proposed approach, we design and implement a system named DeUEDroid to perform the detection. To evaluate DeUEDroid, we collect 25,717 apps and build the first large-scale ground-truth dataset (1,700 apps) of UEware. The evaluation result based on the ground-truth dataset shows that DeUEDroid can cover new UI features and statically construct precise UTG. It achieves 98.22% detection F1-score and 98.97% classification accuracy, significantly outperforming traditional approaches. The evaluation involving 24,017 apps demonstrates the effectiveness and efficiency of UEware detection in real-world scenarios. Furthermore, the result reveals that UEware are prevalent, with 54% of apps in the wild and 11% of apps in app stores being UEware. Our work sheds light on future work in analyzing and detecting UEware.

cs.CR↗

arXiv2021

Lifting The Grey Curtain: A First Look at the Ecosystem of CULPRITWARE

Mobile apps are extensively involved in cyber-crimes. Some apps are malware which compromise users' devices, while some others may lead to privacy leakage. Apart from them, there also exist apps which directly make profit from victims through deceiving, threatening or other criminal actions. We name these apps as CULPRITWARE. They have become emerging threats in recent years. However, the characteristics and the ecosystem of CULPRITWARE remain mysterious. This paper takes the first step towards systematically studying CULPRITWARE and its ecosystem. Specifically, we first characterize CULPRITWARE by categorizing and comparing them with benign apps and malware. The result shows that CULPRITWARE have unique features, e.g., the usage of app generators (25.27%) deviates from that of benign apps (5.08%) and malware (0.43%). Such a discrepancy can be used to distinguish CULPRITWARE from benign apps and malware. Then we understand the structure of the ecosystem by revealing the four participating entities (i.e., developer, agent, operator and reaper) and the workflow. After that, we further reveal the characteristics of the ecosystem by studying the participating entities. Our investigation shows that the majority of CULPRITWARE (at least 52.08%) are propagated through social media rather than the official app markets, and most CULPRITWARE (96%) indirectly rely on the covert fourth-party payment services to transfer the profits. Our findings shed light on the ecosystem, and can facilitate the community and law enforcement authorities to mitigate the threats. We will release the source code of our tools to engage the community.

cs.CR↗

arXiv2019

Towards a First Step to Understand the Cryptocurrency Stealing Attack on Ethereum

We performed the first systematic study of a new attack on Ethereum that steals cryptocurrencies. The attack is due to the unprotected JSON-RPC endpoints existed in Ethereum nodes that could be exploited by attackers to transfer the Ether and ERC20 tokens to attackers-controlled accounts. This study aims to shed light on the attack, including malicious behaviors and profits of attackers. Specifically, we first designed and implemented a honeypot that could capture real attacks in the wild. We then deployed the honeypot and reported results of the collected data in a period of six months. In total, our system captured more than 308 million requests from 1,072 distinct IP addresses. We further grouped attackers into 36 groups with 59 distinct Ethereum accounts. Among them, attackers of 34 groups were stealing the Ether, while other 2 groups were targeting ERC20 tokens. The further behavior analysis showed that attackers were following a three-steps pattern to steal the Ether. Moreover, we observed an interesting type of transaction called zero gas transaction, which has been leveraged by attackers to steal ERC20 tokens. At last, we estimated the overall profits of attackers. To engage the whole community, the dataset of captured attacks is released on https://github.com/zjuicsr/eth-honey.

cs.CR↗