Enhancing Blockchain System Security, Smart Contract Verification, and Blockchain Scalability: A Multi-Dimensional Approach

Blockchain enables decentralized trust, transparent data integrity, and programmable smart contracts, but its adoption is limited by security threats and low transaction throughput. This thesis addresses these challenges through integrated contributions that strengthen user security and improve blockchain scalability. The first challenge examined is the rise of cryptojacking malware, where attackers covertly exploit user devices to mine cryptocurrencies. Existing defenses struggle against evasive behaviors due to reliance on observable signatures or heuristics. To address this, the thesis introduces CryptojackingTrap, an evasion-resilient detection framework that leverages low-level memory traces and network activity to identify mining operations. This approach achieves robust detection even against sophisticated evasion strategies such as code obfuscation, encrypted command-and-control channels, and reduced hash-rate mining, improving detection accuracy by an order of magnitude. The second challenge involves smart contract security, where immutability amplifies the impact of vulnerabilities. This thesis enhances VeriSolid, a formal methods tool for correct-by-design smart contract development. By addressing verification limitations and introducing new property templates, the improved VeriSolid significantly expands the range of contract behaviors that can be verified. Its coverage—the proportion of software requirement specifications that can be formally represented—was increased from 45.6\% to 90.5\% over a dataset of 555 specifications, enabling verification of a far wider set of property specifications. The third focus addresses the scalability bottleneck in the Ethereum blockchain, where sequential transaction execution prevents validators from fully exploiting multi-core infrastructure. Following a systematic review of blockchain concurrency and a comprehensive taxonomy, this thesis proposes two key contributions: a static analysis framework for detecting transaction conflicts and Conthereum, a novel scheduler that safely enables intra-block parallelism. By combining conflict detection with a high-performance, conflict-aware scheduling algorithm, Conthereum avoids costly re-execution and achieves near-linear throughput gains on standard 8-core machines. Although scalability diverges from linear with higher core counts and more frequent conflicts, Conthereum still substantially outperforms sequential execution and existing concurrent solutions across diverse conditions. Collectively, these contributions advance cryptojacking detection, formal verification of smart contracts, and scalable transaction execution, paving the way for more secure, efficient, and widely adopted blockchain systems.