A formal approach to intrusion detection

点击翻译按钮获取中文摘要

Cyber criminality is a flourishing industry. A recent report by Statistics Canada shows that Canadian businesses spent 14 G$ on cyber security in 2017, and 41 % of large business were impacted by a cyber security incident.  Intrusion detection systems are responsible for identifying cyber intrusions in an organisation. They monitor network traffic and host systems activity to detect malicious and abnormal behaviour.  The long-term objective of this research program is to develop a formally grounded intrusion detection approach. The idea is to explore how formal methods can help in efficiently building efficient IDS.  A first subgoal of this proposal is to design an appropriate set of notations to specify abstract intrusion detection rules.  A second subgoal is to define rules that can transform online detection rules into offline detection rules and vice-versa.  A third subgoal is to define algorithms to generate efficient intrusion detection monitor from specifications expressed in the notations proposed in the first subgoal.  A fourth subgoal is to define an approach to validate intrusion detection rules.  Our approach will be based on algebraic state-transition diagrams, an algebra that allows for the composition of state machines using process algebra operators.  This proposal lays a solid scientific foundation for the development of industrial strength tools that could efficiently protect the Canadian IT infrastructure, whose role is now essential for the proper functioning of modern society.