Title: Exploiting the SAT/SMT Revolution for Automated Software Verification

Speaker: Lucas Cordeiro    (bio) (bio)

Lucas Cordeiro is a Reader in the Department of Computer Science at the University of Manchester (UoM), where he leads the Systems and Software Security (S3) Research Group. Dr. Cordeiro is the Arm Centre of Excellence Director at UoM; he also leads the Trusted Digital Systems cluster at the Centre for Digital Trust and Society. He is also affiliated with the Formal Methods Group at UoM. Dr. Cordeiro has implemented various tools used to verify safety and security properties in significant industrial programs written in Java, C/C++, and CUDA. Among those are ESBMC, an SMT-based model checker for C/C++/Qt and CUDA, and JBMC, a SAT-based model checker for Java bytecode. In the last ten years, he also won 28 awards from international software verification and testing competitions held as part of ETAPS at TACAS 2012-2021 and FASE 2020-2021. Dr. Cordeiro's industrial research collaborators include Samsung, Nokia, Motorola, TP Vision, Intel, and ARM. His tools have been applied to find real security vulnerabilities in large-scale software systems. He has a proven track record of securing research funding from Samsung, Nokia Institute of Technology, Motorola, CAPES, CNPq, FAPEAM, British Council, EPSRC, and Royal Society. He leads one large EPSRC project concerning verifiable and explainable secure AI. He is Co-I on three others about software security and automated reasoning, with a portfolio of approximately 5.4m GBP.

When: Tuesday, 02 November 2021 at 1900 hrs (IST)    

Abstract:
In the last three decades, Boolean Satisfiability (SAT) solvers, used as the backend of various verification engines, experienced a dramatic performance revolution. SAT solvers can now check formulas that contain millions of propositional variables. In Satisfiability Modulo Theories (SMT) solvers, predicates from various theories are not encoded using propositional variables as in SAT but remain in the problem formulation. Thus, SMT solvers can be used as backends for solving the generated verification conditions to cope with increasing software complexity. This talk will overview automated software verification techniques that rely on sophisticated SMT solvers built over efficient SAT solvers. I will discuss challenges, problems, and recent advances to ensure safety and security in embedded systems. I will describe novel algorithms that exploit explicit-state and symbolic model checking for verifying single- and multi-threaded software using SMT solvers. These algorithms were the first to verify multi-threaded C/Posix software based on shared-memory synchronization and communication symbolically. These algorithms are implemented in software verification tools, now considered state-of-the-art in the software testing and verification community, receiving 28 medals at SV-COMP and Test-COMP. This achievement enabled industrial research collaborations with Intel and Nokia. Software engineers applied these tools to find real security vulnerabilities in large-scale software systems (e.g., memory safety in firmware for Intel and arithmetic overflow in telecommunication software for Nokia, neither of which had been found before). Both were fixed after being confirmed business-critical.