Suraj C. Kothari
Richardson Chair Professor
Iowa State University
This event is part of the CyLab Distinguished Seminar Series.
What does software verifiability have to do with an 18th-century Swiss mathematician? Come to hear the story that starts with Leonhard Euler, progresses to a patent worth hundreds of millions, and ends with software verifiability for safety and security.
Deriving precise enough relevant architectural knowledge and applying that knowledge are critical for accurate and efficient software verifiability. Our approach has two key components: (1) a mathematical foundation for describing architecture; (2) an accompanying platform to build sophisticated tools.
The mathematical foundation in our framework differs from the so-called formal methods for program verification. De Millo, Lipton, and Perlis point out in their 1979 landmark paper the difference between mathematics and the formal methods. Proving in mathematics works by elevating concepts to high-level abstractions that enable human comprehension, whereas formal methods work by lowering concepts to low-level representations that facilitate machine proofs. A mathematical approach of human-comprehensible high-level abstractions is important for high-assurance, without it we are left to a blind trust in machine proofs.
We will present a verification study of the Linux kernel using our approach and compare results with the formal verification of the Linux kernel using the BLAST model checker.
Suraj Kothari is the Richardson Chair Professor at Iowa State University. He founded EnSoft in 2002. EnSoft’s software analysis and verification products are used worldwide in more than 350 companies including all major aerospace and automobile companies. He has been a PI on DARPA APAC and STAC cybersecurity projects. He has served as a Distinguished ACM Lecturer. He led the effort to the software engineering undergraduate degree program at Iowa State University. He has been awarded the Iowa State Board of Regents Professor Award for excellence in research, teaching, and service.