Concurrent distributed algorithms are crucial for modern applications like cloud computing, IoT, and blockchain, but their verification presents significant challenges. Traditional testing methods often fail to uncover subtle errors related to race conditions and inconsistent states. This paper proposes a novel framework for formally verifying these algorithms using temporal logic, specifically Linear Temporal Logic (LTL). The framework focuses on precisely specifying algorithm behavior through LTL formulas and automatically checking these formulas against simulations of the distributed system. The core contribution lies in the development of an automated tool that translates high-level algorithm descriptions into LTL specifications and executes these specifications within a distributed simulation environment. We demonstrate the effectiveness of this approach by applying it to a simplified consensus algorithm, showcasing the ability to detect potential vulnerabilities that would be missed by conventional testing. The results highlight the potential of formal verification to dramatically improve the reliability and security of concurrent distributed systems.
Abstract Mutation testing is widely used to assess the adequacy of test suite; however, its practical adoption is constrained by the persistent problem of equivalent mutants, i.e., mutants whose observable behavior is indistinguishable from the original program and therefore cannot be killed by any test case. Prior studies report that identifying equivalent mutants often requires substantial manual effort. Meanwhile, fuzzing is increasingly used in real-world systems, especially security-critical software. However, conventional fuzzing oracles typically detect only crash-like failures, thereby missing many behavioral changes introduced by mutants. In this paper, we investigate differential fuzzing as a practical, language-agnostic approach to support mutant classification, focusing on identifying (and confirming) equivalent mutants. We conduct a multi-project study across Bitcoin Core (C++), OpenSSL (C), LND (Go), and Arrow (Python), mutating six real functions with 1,090 valid mutants generated by the universalmutator. We compare unit/functional testing, seed-corpus-only fuzzing, time-bounded fuzzing, and two differential fuzzing configurations (seed-corpus-only and time-bounded). Our results show that conventional fuzzing yields the lowest mutation scores, while time-bounded differential fuzzing (5 minutes per mutant) achieves 98–100\% mutation score in five of six targets, and exposes cases where seed corpora contain valuable test inputs not covered by unit/functional suites. We further analyze runtime variability and observe log-normal behavior in difficult cases, providing practical guidance on stopping criteria (time/execution budgets), as well as evidence that dictionaries and parallel fuzzing can significantly improve effectiveness. Overall, our findings indicate that differential fuzzing is simple to implement and can classify mutants efficiently in practice, while also producing actionable artifacts (seed corpus inputs) to strengthen traditional test suites.
Cyber–physical systems (CPSs) increasingly rely on complex software components whose vulnerabilities may affect both digital services and physical processes. Fuzzing is a practical technique for discovering such vulnerabilities in CPS-facing parsers, protocol handlers, and edge services. Distributed fuzzing improves throughput, but outsourcing fuzzing tasks to multiple untrusted nodes introduces privacy risks: valuable seeds, especially crash-triggering samples, may reveal vulnerability information before affected users are protected. In this paper, we propose PrivFuzz, a privacy-preserving collaborative fuzzing framework. PrivFuzz allows organizations and individuals to collaborate and receive rewards while keeping fuzzing seeds confidential and enabling controlled encrypted seed reuse among untrusted fuzzing nodes. The key idea is to combine trusted execution environments (TEEs) with blockchain-based smart contracts to support confidentiality and fair reward settlement. We give game-based definitions and reduction-style arguments for seed confidentiality, worker soundness, outsourcer atomicity, and duplicate-claim resistance under an attested execution model. We implement a PrivFuzz prototype and evaluate it on four open-source parsing targets. Separately, native AFL++ sanity checks suggest that CPS-facing industrial protocol parsers such as Modbus and OPC UA fall within the same fuzzable target domain. Demonstrating end-to-end PrivFuzz on CPS control programs is left as future work. Using PrivFuzz, we discovered nine bugs and reported them to the developers.