Communicating Concurrent Kleene Algebra and its Use in Designing Secure Distributed Systems
报告题目：Communicating Concurrent Kleene Algebra and its Use in Designing Secure Distributed Systems
报告人：Prof. Ridha Khedri, McMaster University
主持人：朱惠彪 教授
报告时间： 9月6日下午1：30~2：30
报告地点：理科楼B1002
报告摘要：
The existence and usage of covert channels in systems of communicating agents poses a significant threat to the confidentiality of information. It is difficult to fully prevent the possibility of covert channels in a system without limiting the communication between its components or negatively affecting its behaviour. However, by developing an understanding of when a covert channel may exist in a given system and which agents are more prone to covert channels than others, approaches for mitigating covert channels can be developed in such a way that they are able to preserve overall system functionality and the communication between its components and with its environment. In this paper, we propose an approach for mitigating covert channels in systems of communicating agents based on an analysis of the potential for communication amongst system agents. First, we propose a mathematical framework for communication and concurrency called Communicating Concurrent Kleene Algebra (C2KA). We use C2KA to present a formulation of the potential for communication condition for covert channel existence. Then, we show how to use the proposed formulation and its mathematical background to analyse systems of communicating agents in order to devise an approach for modifying the behaviours of agents in a system of communicating agents in order to eliminate the potential for communication, thus eliminating the potential for a covert channel, while still preserving the overall system functionality. Using an illustrative example, we show how to specify a system of communicating agents using the mathematical framework of C2KA and we demonstrate and discuss the proposed mitigation approach.
报告人简介：
Ridha Khedri is a Professor of software engineering at McMaster University. He is the Chair of the department of Computing and Software. He is Adjunct Professor in the School of Computer Engineering and Science, Shanghai University. He obtained his Engineer Diploma in 1987 from the University of Tunis. He received a M.Sc. and a Ph.D. from Laval University, Quebec, Canada, in 1993 and 1998 respectively. In March 1998, he joined the Communications Research Laboratories of McMaster as a post-doctoral researcher under the supervision of Prof. David L. Parnas. He is a licensed professional engineer in the province of Ontario. He is a member of the Association for Computing Machinery and the IEEE Computer Society. He has been co-organizer, program committee member, and referee of more than 30 international workshops and conferences. His research interests include algebraic methods in software engineering, data cleaning, information security, and ontology-based reasoning.
His work on information security tackles covert channels, cryptographic-key distribution schemes, and dynamic cyber defense. With his students and with long term collaboration with Prof. Bernard Moeller, he developed Product Family Algebra (PFA) as a formalism to reason on Software Product Families. He extended the use of PFA to reason on aspects and dynamic cyber defense. His research record includes more than 80 peer-reviewed articles. He supervised more than 20 graduate students.His security trained graduate students are recruited at prestigious places such as the U.S. Department of Homeland Security Cybersecurity Group at Stanford University.