Scalable Methods for Security against Distributed Attacks

Investigator: Gul Agha

Classical methods for expressing and checking properties do not allow us to express many relevant global security properties. By developing a probabilistic distributed temporal logic, important global properties of systems can be represented, which will enable us to represent distributed attacks and probabilistic reasoning. We propose to develop the logic and efficient, scalable methods for reasoning through decentralized monitoring and adaptive sampling. This will allow confidence that certain types of global security properties ar not violated in systems such as clouds or clusters.

Hard Problem Addressed


  1. Minas Charalambides, Peter Dinges, and Gul Agha, “Parameterized Concurrent Multi-Party Session Types”, International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems (FOCLASA 2012), Electronic Proceedings in Theoretical Computer Science, volume 91, pages 16-30, 2012. [full text]
  2. Peter Dinges, Minas Charalambides, and Gul Agha “Automated Inference of Atomic Sets for Safe Concurrent Execution”, 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2013), Seattle, WA, June 20 2013. [full text]
  3. YoungMin Kwon and Gul Agha, “Performance Evaluation of Sensor Networks by Statistical Modeling and Euclidean Model Checking”,  ACM Transactions on Sensor Networks, volume 9, issue 4, article number 39, July 2013. [full text]
  4. Samira Tasharofi, Peter Dinges, and Ralph E. Johnson, “Why Do Scala Developers Mix the Actor Model with other Concurrency Models?”, 27th European Conference on Object-Oriented Programming (ECOOP 2013), Montpelier, France, July 1-5, 2013. [full text]
  5. Peter Dinges and Gul Agha, “Targeted Test Input Generation Using Symbolic-Concrete Backward Execution”, Technical Report, University of Illinois at Urbana–Champaign, September 2014. [full text]
  6. Peter Dinges and Gul Agha, “Targeted Test Input Generation using Symbolic-concrete Backward Execution”, 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014), Västerås, Sweden, September 15-19 2014. [full text]
  7. Peter Dinges and Gul Agha, “Solving Complex Path Conditions through Heuristic Search on Induced Polytopes”, 22nd ACM SIGSOFT Symposium on Foundations of Software Engineering, Hong Kong, November 16-21 2014. [full text]


  1. Gul Agha, “Euclidean Model Checking: A Scalable Method for Verifying Quantitative Properties in Probabilistic Systems”, invited talk, 5th International Conference on Algebraic Informatics, Aix-Marseille University Porquerolles Island-Cote d’Azur, France, September 3-6, 2013. [abstract]
  2. Gul Agha, “Actors Programming for the Mobile Cloud,” invited talk, IEEE 13th International Symposium on Parallel and Distributed Computing, Aix-Marseille University Porquerolles Island-Cote d’Azur, France, June 24-27, 2014. [abstract]