Type Systems for Systems Types

dc.contributor.advisor Keller, Gabriele en_US
dc.contributor.advisor Rizkallah, Christine en_US
dc.contributor.advisor Heiser, Gernot en_US O'Connor, Liam en_US 2022-03-23T11:19:31Z 2022-03-23T11:19:31Z 2019 en_US
dc.description.abstract This thesis presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating systems components, designed around a new programming language, Cogent. This language is total, polymorphic, higher-order, and purely functional, including features such as algebraic data types and type inference. Crucially, Cogent is equipped with a uniqueness type system, which eliminates the need for a trusted runtime or garbage collector, and allows us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. We prove that the functional semantics is a valid abstraction of the imperative semantics for all well-typed programs. Cogent is designed to easily interoperate with existing C code, to enable Cogent software to interact with existing C systems, and also to provide an escape hatch of sorts, for when the restrictions of Cogent's type system are too onerous. This interoperability extends to Cogent's verification framework, which composes with existing C verification frameworks to enable whole systems to be verified. Cogent's verification framework is based on certifying compilation: For a well-typed Cogent program, the compiler produces C code, a high-level representation of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL. To evaluate the effectiveness of this framework, two realistic file systems were implemented as a case study, and key operations for one file system were formally verified on top of Cogent specifications. These studies demonstrate that verification effort is drastically reduced for proving higher-level properties of file system implementations, by reasoning about the generated formal specification from Cogent, rather than low-level C code. en_US
dc.language English
dc.language.iso EN en_US
dc.publisher UNSW, Sydney en_US
dc.rights CC BY-NC-ND 3.0 en_US
dc.rights.uri en_US
dc.subject.other Uniqueness Types en_US
dc.subject.other Cogent en_US
dc.subject.other Refinement en_US
dc.subject.other Isabelle/HOL en_US
dc.subject.other Formal Verification en_US
dc.subject.other File Systems en_US
dc.title Type Systems for Systems Types en_US
dc.type Thesis en_US
dcterms.accessRights open access
dcterms.rightsHolder O'Connor, Liam
dspace.entity.type Publication en_US
unsw.relation.faculty Engineering
unsw.relation.originalPublicationAffiliation O'Connor, Liam, Computer Science & Engineering, Faculty of Engineering, UNSW en_US
unsw.relation.originalPublicationAffiliation Keller, Gabriele, Utrecht University, The Netherlands en_US
unsw.relation.originalPublicationAffiliation Rizkallah, Christine, Computer Science & Engineering, Faculty of Engineering, UNSW en_US
unsw.relation.originalPublicationAffiliation Heiser, Gernot, Computer Science & Engineering, Faculty of Engineering, UNSW en_US School of Computer Science and Engineering *
unsw.thesis.degreetype PhD Doctorate en_US
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
public version.pdf
1.26 MB
Resource type