Finding Trojan Message Vulnerabilities in Distributed Systems

Trojan messages are messages that seem correct to the re-ceiver but cannot be generated by any correct sender. Such messages constitute major vulnerability points of a dis-tributed system—they constitute ideal targets for a malicious actor and facilitate failure propagation across nodes. We de-scribe Achilles, a tool that searches for Trojan messages in a distributed system. Achilles uses dynamic white-box analysis on the distributed system binaries in order to infer the predicate that defines messages parsed by receiver nodes and generated by sender nodes, respectively, and then com-putes Trojan messages as the difference between the two. We apply Achilles on implementations of real distributed systems: FSP, a file transfer application, and PBFT, a Byzantine-fault-tolerant state machine replication library. Achilles discovered a new bug in FSP and rediscovered a previously known vulnerability in PBFT. In our evaluation we demonstrate that our approach can perform orders of magnitude better than general approaches based on regular fuzzing and symbolic execution