Overcoming Restraint: Composing Verification of Foreign Functions with Cogent

Louis Cheung*, Liam O'Connor, Christine Rizkallah

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Cogent is a restricted functional language designed to reduce
the cost of developing verified systems code. Because of its
sometimes-onerous restrictions, such as the lack of support
for recursion and its strict uniqueness type system, Cogent
provides an escape hatch in the form of a foreign function
interface (FFI) to C code. This poses a problem when verifying
Cogent programs, as imported C components do not
enjoy the same level of static guarantees that Cogent does.
Previous verification of file systems implemented in Cogent
merely assumed that their C components were correct and
that they preserved the invariants of Cogent’s type system.
In this paper, we instead prove such obligations. We demonstrate
how they smoothly compose with existing Cogent
theorems, and result in a correctness theorem of the overall
Cogent-C system. The Cogent FFI constraints ensure that
key invariants of Cogent’s type system are maintained even
when calling C code. We verify reusable higher-order and
polymorphic functions including a generic loop combinator
and array iterators and demonstrate their application to
several examples including binary search and the BilbyFs
file system. We demonstrate the feasibility of verification of
mixed Cogent-C systems, and provide some insight into verification
of software comprised of code in multiple languages
with differing levels of static guarantees.
Original languageEnglish
Title of host publication CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
EditorsAndrei Popescu, Steve Zdancewic
Place of PublicationNew York, NY, USA
PublisherACM Association for Computing Machinery
Pages13-26
Number of pages14
ISBN (Electronic)9781450391825
DOIs
Publication statusPublished - 17 Jan 2022
EventCertified Programs and Proofs 2022 - Philadelphia, United States
Duration: 17 Jan 202218 Jan 2022
https://popl22.sigplan.org/home/CPP-2022#About

Conference

ConferenceCertified Programs and Proofs 2022
Abbreviated titleCPP 2022
Country/TerritoryUnited States
CityPhiladelphia
Period17/01/2218/01/22
Internet address

Keywords

  • compilers
  • verification
  • type-systems
  • language interoperability
  • data-structures

Fingerprint

Dive into the research topics of 'Overcoming Restraint: Composing Verification of Foreign Functions with Cogent'. Together they form a unique fingerprint.

Cite this