Members

• Mohamed Layouni
• Dr. Sofiene Tahar
• Dr. Jozef Hooman

Description

Many of today's distributed applications rely on communication between groups of users. Such applications involve a set of participants that may not fully trust each others. Even if group participants are, a priori, trusted, it is still safe to assume that an external attacker may gain illicit access to the system. Intrusion-tolerance is the application of fault-tolerance to security. Assuming that faults, both benign and Byzantine, are unavoidable, the main goal of Intrusion-tolerance is to preserve an acceptable, though possibly degraded, service of the overall system despite intrusions at some of its sub-parts. In this project, we consider the Intrusion-tolerant Enclaves protocol, a Byzantine fault-tolerant platform for secure group communication developed at SRI. We formally analyse the protocol, with a special focus the processes Byzantine behaviour, using an adaptive combination of techniques including Model Checking, Theorem Proving and Analytical mathematics.

Publications

1. M. Layouni, J. Hooman, and S. Tahar: Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol ; International Journal of Network Security, Vol. 5, No. 3, Science Publications, 2007, pp. 288-298.
2. M. Layouni, J. Hooman, and S. Tahar: Modeling and Verification of Leaders Agreement in the Intrusion-Tolerant Enclaves Using PVS; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'03), Roma, Italy, September 2003, pp145-158. [In: D. Basin and B. Wolff (Eds.), TPHOLs 2003 Emerging Trends Proceedings, Technical Report No. 187, Institut of Informatics, Albert-Ludwigs University, Freiburg, Germany.]
3. M. Layouni, J. Hooman, and S. Tahar: On the Correctness of an Intrusion-Tolerant Group Communication Protocol;. In the Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'03), L'Aquila, Italy, October 2003. Springer-Verlag.
4. M. Layouni, J. Hooman and S. Tahar: Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol; Technical Report, Concordia University, Department of Electrical and Computer Engineering, November 2003. [23 pages]
5. M. Layouni, J. Hooman, and S. Tahar: Modeling and Verification of Leaders Agreement in the Intrusion-Tolerant Enclaves Using PVS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 2003. [13 pages].
6. Mohamed Layouni, "On the Formal Verification of an Intrusion-Tolerant Group Communications Protocol". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, August 2003.