USI - Email

Archive / INF Seminars / INF_2023_10_09_ArieGurfinkel

USI - Email

	Verifying Verified Code

Host: Prof. Natasha Sharygina

Monday

09.10

USI East Campus, Room D0.03

10:00 - 11:00


	Arie Gurfinkel University of Waterloo, Canada

Abstract: Bounded Model Checking (BMC) is an effective and precise static analysis technique that reduces program verification to satisfiability (SAT) solving. However, it is yet to be widely adopted in Industry. This talk describes our research on improving BMC usability through development of a new BMC engine (SeaBMC) in the SeaHorn verification framework for LLVM and through case studies on production code. Specifically, the talk reports on our recent case study using Amazon Web Services aws-c-common library that was previously verified by CBMC. The talk will also present the design and implementation of SeaBMC that precisely models arithmetic, pointer, and memory operations of LLVM. The key design innovation of SeaBMC is to structure verification condition generation around a series of transformations, starting with a custom IR (called SeaIR) that explicitly purifies all memory operations by explicating dependencies between them. This transformation-based approach enables supporting many different styles of verification conditions. To support memory safety checking, we extend our base approach with fat pointers and shadow bits of memory to keep track of metadata, such as the size of a pointed-to object. We show that SeaBMC is capable of providing order of magnitude improvement compared with state-of-the-art.

Biography: Dr. Arie Gurfinkel is a Professor in the Department of Electrical and Computer Engineering at the University of Waterloo. He has published over 110 papers on automated verification. His research is in the areas of Program Analysis, Model Checking, and Automated Reasoning. His research group has led the implementation of award-winning program analysis framework SeaHorn, and award-winning solver for Constrained Horn Clauses, SPACER.