Automated deductive verification of systems software

Pek, Edgar

Permalink

https://hdl.handle.net/2142/88993 Copy

Description

Title

Automated deductive verification of systems software

Author(s)

Pek, Edgar

Issue Date

2015-11-25

Director of Research (if dissertation) or Advisor (if thesis)

Parthasarathy, Madhusudan

Doctoral Committee Chair(s)

Parthasarathy, Madhusudan

Committee Member(s)

• King, Samuel T
• Ball, Thomas
• Rosu, Grigore

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• software verification
• software security
• automated deductive reasoning

Abstract

Software has become an integral part of our everyday lives, and so is our reliance on his correct functioning. Systems software lies at the heart of computer systems, consequently ensuring its reliability and security is of paramount importance. This thesis explores automated deductive verification for increasing reliability and security of systems software. The thesis is comprised of the three main threads. The first thread describes how the state-of-the art deductive verification techniques can help in developing more secure operating system. We have developed a prototype of an Android-based operating system with strong assurance guarantees. Operating systems code heavily relies on mutable data structures. In our experience, reasoning about such pointer-manipulating programs was the hardest aspect of the operating system verification effort because correctness criteria describes intricate combinations of structure (shape), content (data), and separation. Thus, in the second thread, we explore design and development of an automated verification system for assuring correctness of pointer-manipulating programs using an extension of Hoare’s logic for reasoning about programs that access and update heap allocated data-structures. We have developed a verification framework that allows reasoning about C programs using only domain specific code annotations. The same thread contains a novel idea that enables efficient runtime checking of assertions that can express properties of dynamically manipulated linked-list data structures. Finally, we describe the work that paves a new way for reasoning about distributed protocols. We propose certified program models, where an executable language (such as C) is used for modelling – an executable language enables testing, and emerging program verifiers for mainstream executable languages enable certification of such models. As an instance of this approach, concurrent C code is used for modelling and a program verifier for concurrent C (VCC from Microsoft Research) is used for certification of new class of systems software that serves as a backbone for efficient distributed data storage.

Graduation Semester

2015-12

Type of Resource

text

Permalink

http://hdl.handle.net/2142/88993

Copyright and License Information

Copyright 2015 Edgar Pek

Owning Collections