Tutorial Speaker : Prof. Suraj Kothari, Iowa State University, USA

Title : Software Model Checking (SMC) - an essential technology for cybersecurity

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