CERIAS - Center for Education and Research in Information Assurance and Security

Skip Navigation
Purdue University
Center for Education and Research in Information Assurance and Security

Finding Flaws in Unmodified Distributed Systems

Research Areas: End System Security

Principal Investigator: Charles Killian

Debugging distributed systems is notoriously difficult.  This is in large part due to both the software complexity and accordingly large state space, and because of the inherent asynchrony in networked systems. We have built a model-checker to test unmodified distributed systems built with the Mace programming toolkit.  The modelchecker (MaceMC) uses automated state space exploration combined with long random execution to find and isolate bugs forcing distributed systems to violate liveness properties, which are essentially the properties which developers to specify that a system not only avoids bad states, but eventually accomplishes its goal.

We continue to extend the features and capabilities of the Mace model checker. We are now working on how to use the model checking infrastructure to find performance bugs in unmodified distributed systems, and how to incorporate malicious agents into the testing infrastructure to automatically detect errors and system degradation caused by these malicious agents, and to verify fixes once designed.


Other PIs:

Students: Hyojeong Lee Karthik Nagaraj Salman Pervez Anurag Singh Sunghwan Yoo

Representative Publications

  • Darren Dao, Jeannie Albrecht, Charles Killian, and Amin Vahdat, “Live Debugging of Distributed Systems", International Conference on Compiler Construction, York, UK, March, 2009.

  • Dejan Kostic, Alex C. Snoeren, Amin Vahdat, Ryan Braud, Charles Killian, Jeannie Albrecht, James W. Anderson, Adolfo Rodriguez, and Erik Vandekieft ,"High Bandwidth Data Dissemination for Large-scale Distributed Systems",ACM Transactions on Computer Systems, 2008

Keywords: debug, errors, infrastructure, security