Some users are experiencing upload errors at the moment. If you receive a "UWSpace is down for maintenance" error, please email jordan.hale@uwaterloo.ca as soon as possible. We are very sorry for the inconvenience.

Show simple item record

dc.contributor.authorPriya, Siddharth
dc.date.accessioned2021-09-14 14:24:35 (GMT)
dc.date.available2021-09-14 14:24:35 (GMT)
dc.date.issued2021-09-14
dc.date.submitted2021-09-10
dc.identifier.urihttp://hdl.handle.net/10012/17381
dc.description.abstractAbstract: Bounded Model Checking(BMC) is an effective and precise static analysis technique that reduces program verification to satisfiability (SAT) solving. However, with a few exceptions, BMC is not actively used in software industry, especially, when compared to dynamic analysis techniques such as fuzzing, or light-weight formal static analysis. This thesis describes our experience of applying BMC to industrial code using a novel BMC tool SEABMC. We present three contributions: First, a case study of (re)verifying the aws-c-common library from AWS using SEABMC and KLEE. This study explores the methodology from the perspective of three research questions: (a) can proof artifacts be used across verification tools; (b) are there bugs in verified code; and (c) can specifications be improved. To study these questions, we port the verification tasks for aws-c-common library to SEAHORN and KLEE. We show the benefits of using compiler semantics and cross-checking specifications with different verification techniques, and call for standardizing proof library extensions to increase specification reuse. Second, a description of SEABMC - a novel BMC engine for SEAHORN. We start with a custom IR (called SEA-IR) that explicitly purifies all memory operations by explicating dependencies between them. We then run program transformations and allow for generating 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. To evaluate SEABMC, we use the aws-c-common library from AWS as a benchmark and compare with CBMC, SMACK, and KLEE. We show that SEABMC is capable of providing an order of magnitude improvement compared with state-of-the-art. Third, a case study of extending SEABMC to work with Rust - a young systems programming language. We ask three research questions: (a) can SEABMC be used to verify Rust programs easily; (b) can the specification style of aws-c-common be applied successfully to Rust programs; and (c) can verification become more efficient when using higher level language information. We answer these questions by verifying aspects of the Rust standard library using SEAURCHIN, an extension of SEABMC for Rust.en
dc.language.isoenen
dc.publisherUniversity of Waterlooen
dc.subjectsoftware verificationen
dc.subjectbounded model checkingen
dc.subjectformal verificationen
dc.subjectbmcen
dc.subjectrusten
dc.subjectCen
dc.subjectsmten
dc.titleBounded Model Checking of Industrial Codeen
dc.typeMaster Thesisen
dc.pendingfalse
uws-etd.degree.departmentElectrical and Computer Engineeringen
uws-etd.degree.disciplineElectrical and Computer Engineeringen
uws-etd.degree.grantorUniversity of Waterlooen
uws-etd.degreeMaster of Applied Scienceen
uws-etd.embargo.terms0en
uws.contributor.advisorGurfinkel, Arie
uws.contributor.affiliation1Faculty of Engineeringen
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.typeOfResourceTexten
uws.peerReviewStatusUnrevieweden
uws.scholarLevelGraduateen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record


UWSpace

University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages