Abstract

During the last decade, machine learning algorithms have massively integrated the defense arsenal made available to security professionals. And intrusion detection is a perfect illustration of this. In this branch of digital security, there are two main detection approaches: misuse detection (MD) and anomaly-detection (AD). In misuse detection, abnormal system behavior is defined first, and then any other behavioris defined as normal. The definition of abnormal system states is achieved using malware signatures and attacks patterns. MD stands against the anomaly detection approach which defines the normal system behavior and considers any other behavior as abnormal. While MD is reputed to be simple and efficient as known attacks are easy to add, its main disadvantage lies in its inability to detect unknown attacks (I.e., zero-day attacks). With respect to this, anomaly-detection provides a serious alternative. This approach generally relies on the use of Machine Learning (ML) techniques to learn the system normal behavior and detects any deviation that is considered as an attack.

Although the results and performance of machine learning are constantly improving, it is still relatively simple to deliberately mislead the trained model, by means of what is commonly called Adversarial Machine Learning Attacks. The increase in adverse attacks raises the debate about "who will really benefit from machine learning in the future? Attackers or security professionals? In an attempt to resolve this issue, several researchers have explored attacks targeting machine learning algorithms in order to influence the models produced or the predictions generated by them. This research topic started gaining the security community attraction in the mid of 2010’s whenSzegedy's team managed to fool the classification model based on deep neural networks by generating adversarial examples that resulted in arbitrary or specific incorrect outputs. Since then, assessing the reliability, the robustness and the trust that security professional might put on this approach started to become a major challenge for academics, companies and even governmental agencies.

In this tutorial, we will provide an overlapping view of cybersecurity and Artificial Intelligence. We will provide hands-on examples on how Cybersecurity is benefiting from the advanced in Machine Learning discipline and why this later needs to gain robustness to be fully trusted by security professionals.

Biography of tutorial speaker

Reda Yaich is a senior researcher and Cybersecurity Team Leader at IRT SystemX. Reda holds a Phd in Computer Science from the ENS Mines of Saint-Etienne with a focus on Trust Management using Artificial Intelligence technologies. He served as lecturer and/or research assistant in several universities (e.g. University of Saint-Etienne, University of Lyon) and engineering schools (ENS Mines Saint-Etienne, Telecom Bretagne, IMT Atlantique, ENSIBS, Telecom SudParis). Reda has several publications in journals and conferences related to Decentralised Access Control, Authorisation and Digital Trust Management. He has also participated in numerous national and European projects.

Abstract

Software is everywhere from billions of IoT devices to huge displays in Tesla cars. Without being able to verify safety and security properties of software, we have a disaster waiting to happen. Fundamentally, the safety and cyber security problems stem from the complexities inherent in the cyber-physical systems software. The objective of the tutorial is to expose the attendees to software model checking (SMC) as a state-of-the-art technology for verifying critical software.
In traditional SMC, there is an unreasonable focus on logic and theorem proving. In other areas, engineers rarely prove theorems; instead, they use mathematics to derive important properties of their artifacts. They also use mathematics to describe their artifacts in a way that makes mathematical analysis possible. The difference is important and it is the key to practicality. Instead of logic and theorem proving, we will present SMC as powerful mathematical abstractions of software that enable verification of large software with millions of lines of code.
We have crystalized our SMC research into material that is fit for engaging bright undergraduate students. The tutorial will be valuable to anyone who is interested in getting the gist of how software model checking works using innovative abstractions of software.

Technical issues that the tutorial will address

• The difference: software model checking vs. testing
• A succinct view of software architecture and program behaviors
• Accuracy and scalability issues for software model checking

Tutorial outline

1. Bring out the fundamental structural and behavioral attributes of software that make it susceptible cyber security exploits. (30 minutes)
2. Introduce the notion of software model checker and how it works as a powerful tool to reason about and verify software for a wide class security and safety vulnerabilities (45 minutes)
3. An overview of the state-of-the-art for software model checking (30 minutes)
4. Demonstrations of software model checking with real-world examples (30 minutes)
5. A concluding summary of main points and food for thought (30 minutes)

Biography of tutorial speaker

Suraj Kothari is the Richardson Chair Professor of Electrical and Computer Engineering (ECE) at Iowa State University (ISU). He has pioneered research on machine-enabled reasoning to solve complex problems of software productivity, security and safety. He served as a Principal Investigator (PI) for the US Defense Advanced Research Project Agency (DARPA) Automated Program Analysis for Cybersecurity (APAC) program, and a Co-PI for the DARPA Software Enabled Control (SEC) program. Currently he is a PI for the DARPA Space/Time Analysis for Cybersecurity (STAC) program. Dr. Kothari founded EnSoft (http://www.ensoftcorp.com) in 2002. EnSoft’s products are used worldwide by 350 companies including all major aerospace and automobile companies. He was awarded in 2008 the Prometheus Award for Innovation in Teaching for the software engineering courses he developed. He was awarded in 2012 the Iowa State Board of Regents Professor Award for excellence in research, teaching, and service. He has served as a Distinguished ACM Lecturer. URL: https://www.ece.iastate.edu/kcsl/

Experience of the speaker on the topic of the tutorial

The speaker is an expert in the field. He has been the Principal Investigator for two multi-million dollar projects DARPA cyber security projects awarded to his institution in the last eight years. He has founded a successful company that develops software analysis and verification tools for safety-critical control systems software. He has given talks on the subject at many companies and universities. Here is link to his recent talk, on April 29, 2019, in the Distinguished Seminar Series at the CyLab: Security and Privacy Institute at Carnegie Mellon University: https://www.cylab.cmu.edu/events/2019/04/29_kothari.html