|
Public viva-voce Notification Date: Thursday, 19 December 2024 Time: 6:30 PM Venue: Seminar Hall Automated testing of distributed protocol implementations Srinidhi Nagendra Chennai Mathematical Institute. 19-12-24 Abstract The growth of modern internet is enabled by large-scale, highly available, and resilient distributed systems. These systems allow data to be replicated globally while ensuring availability under failures. To ensure reliability and availability in the presence of failures, the systems rely on intricate distributed protocols. Yet in practice, bugs in the implementations of these distributed protocols have been the source of many downtimes in popular distributed databases. Ensuring the correctness of the implementations remains a significant challenge due to the large state space. Over the years, many techniques have been developed to ensure the correctness of the implementations ranging from systematic model checking to pure random exploration. However, a developer testing the implementation with current techniques has no control over the exploration. In effect, the techniques are agnostic to the developer’s knowledge of the implementation. Furthermore, very few approaches utilize the formal models of the protocols when testing the implementations. Efforts put into modeling and verifying the correctness of the model are not leveraged to ensure the correctness of the implementation. To address these drawbacks, in this thesis, we propose 3 new approaches to test distributed protocol implementations - Netrix, WaypointRL, and ModelFuzz. The first two techniques - Netrix and WaypointRL are biased exploration approaches that accept developer input. Netrix is a novel unit testing algorithm that allows developers to bias the exploration of an existing testing algorithm. A developer writes low-level filters in a domain-specific language to fix specific events in an execution that are enforced by Netrix. WaypointRL improves on Netrix to accept high-level state predicates as waypoints and uses reinforcement learning to satisfy the predicates. WaypointRL is effective in biasing the exploration while requiring less effort from the developer. Using popular distributed protocol implementations, we show that additional developer input leads to effective biased exploration and improved bug-finding capabilities. The third technique - ModelFuzz - is a new fuzzing algorithm that bridges the gap between the model and the implementation of the protocol. We use model states as coverage to guide input generation that are then executed on the implementation. We show with three industrial benchmarks that existing coverage notions are insufficient for testing distributed systems and that using TLA+ model coverage to test implementations leads to discovering new bugs. Jury: 1.Gennaro PARLATO, Prof, University of Molise, Italy (Reviewer) 2.Stephan MERZ, DR. Université de Lorraine, France (Reviewer) 3.Cezara DRAGOI, CR, Amazon Web Services 4.Praveen M, Associate Prof, Chennai Mathematical Institute, India 5.Burcu OZKAN, Asstistant Prof, Delft University of Technology, Netherlands 6.Tayssir TOUILI, DR, CNRS, France 7.Constantin ENEA, Prof, Ecole Polytechnique, France (Supervisor) 8.Madayam SRIVAS, Prof, Chennai Mathematical Institute, India (Co-Supervisor) Keywords: Formal methods, Distributed Systems, Testing, Reinforcement Learning, Unit testing, Fuzzing. All are invited to attend the viva-voce examination
|
