The School of Computer Science at the University of Windsor is pleased to present…  

Colloquium Presentation by Dr. Saeed Nejati 

Toward Verification of Unchecked Codes in Checked C 

Date: Friday, November 11, 2022

Time: 11:00 am – 12:00 pm

Location: Erie Hall, Room 3123

Reminders: Two-part attendance is mandatory; arrive 5-10 minutes before the event starts – LATECOMERS WILL NOT BE ADMITTED once the door has been closed and the presentation has begun. If the door is closed, please be respectful of the presenter by NOT knocking on the door for admittance.

Abstract:

Checked C is an extension of C programming language that adds bounds checking to address some of the memory safety challenges of C. One feature of Checked C is its incremental adoption, meaning that it allows for a mix of unchecked and checked C code. However, we cannot claim any security guarantees for a mixed code. In this work, we will explore software verification of unchecked pieces of code using the information at the edge of going from checked to unchecked to provide an end-to-end memory safety guarantee.

Keywords: Checked C, Software Verification, Compilers

Biography: 

Saeed Nejati is an applied scientist at Amazon. He is working on using formal reasoning methods to tackle security-related problems in AWS. Saeed got his Ph.D. from the University of Waterloo on enhancing Boolean SAT solvers to work better on cryptanalysis problems. His research interests are automated reasoning, hardware/software security, and high-performance computing.