A Framework for the Automatic Formal Verification of Refinement from Cogent to C
Our language Cogent simplifies verification of systems software using a certifying compiler, which produces a proof that the generated C code is a refinement of the original Cogent program. Despite the fact that Cogent itself contains a number of refineme
- PDF / 919,772 Bytes
- 18 Pages / 439.37 x 666.142 pts Page_size
- 76 Downloads / 187 Views
Data61 (formerly NICTA), Sydney, Australia 2 UNSW, Sydney, Australia [email protected]
Abstract. Our language Cogent simplifies verification of systems software using a certifying compiler, which produces a proof that the generated C code is a refinement of the original Cogent program. Despite the fact that Cogent itself contains a number of refinement layers, the semantic gap between even the lowest level of Cogent semantics and the generated C code remains large. In this paper we close this gap with an automated refinement framework which validates the compiler’s code generation phase. This framework makes use of existing C verification tools and introduces a new technique to relate the type systems of Cogent and C.
1
Introduction
In previous work, we designed a new language called Cogent [9] for easing the verification of certain classes of systems code such as file systems. Cogent is a linearly-typed, pure, polymorphic, functional language with a certifying compiler. We used it in separate work to write two Linux filesystems, ext2 and BilbyFs, and achieved performance comparable to their native C implementations [2]. From a Cogent program the Cogent compiler produces three artefacts: C code, a shallow embedding of the Cogent program in Isabelle/HOL [8], and an Isabelle/HOL proof relating the two. The compiler certificate is a series of NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program. This material is based on research sponsored by Air Force Research Laboratory and the Defense Advanced Research Projects Agency (DARPA) under agreement number FA8750-12-9-0179. The U.S. Government is authorised to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of Air Force Research Laboratory, the Defense Advanced Research Projects Agency or the U.S. Government. c Springer International Publishing Switzerland 2016 J.C. Blanchette and S. Merz (Eds.): ITP 2016, LNCS 9807, pp. 323–340, 2016. DOI: 10.1007/978-3-319-43144-4 20
324
C. Rizkallah et al.
Fig. 1. An overview of the verification chain and our refinement framework.
language-level proofs and per-program translation validation phases that are combined into one top-level theorem in Isabelle/HOL. The most involved phase, and the phase we discuss in this paper, is the translation validation phase relating Cogent’s imperative semantics to the generated C. We present a refinement framework that enables the full automation of this phase of Cogent’s certifying compilation. This framework has several components that relate Cogent values, states, types, and statements to their C counterparts. We put significant proof engineering work into enabling the framework to bridge the gap between the Cogent store and th
Data Loading...
