Mind the gap: A verification framework for low-level C

Simon Winwood; Gerwin Klein; Thomas Sewell; June Andronick; David Cock; Michael Norrish

doi:10.1007/978-3-642-03359-9_34

Mind the gap: A verification framework for low-level C

Simon Winwood^*, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

33 Citations (Scopus)

Abstract

This paper presents the formal Isabelle/HOL framework we use to prove refinement between an executable, monadic specification and the C implementation of the seL4 microkernel. We describe the refinement framework itself, the automated tactics it supports, and the connection to our previous C verification framework. We also report on our experience in applying the framework to seL4. The characteristics of this microkernel verification are the size of the target (8,700 lines of C code), the treatment of low-level programming constructs, the focus on high performance, and the large subset of the C programming language addressed, which includes pointer arithmetic and type-unsafe code.

Original language	English
Title of host publication	Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings
Pages	500-515
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-03359-9_34
Publication status	Published - 2009
Event	22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009 - Munich, Germany Duration: 17 Aug 2009 → 20 Aug 2009

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5674 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009
Country/Territory	Germany
City	Munich
Period	17/08/09 → 20/08/09

Access to Document

10.1007/978-3-642-03359-9_34

Cite this

Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., & Norrish, M. (2009). Mind the gap: A verification framework for low-level C. In Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings (pp. 500-515). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5674 LNCS). https://doi.org/10.1007/978-3-642-03359-9_34

@inproceedings{3b8d3fbc9b4f4886961e6b19d64e7b15,

title = "Mind the gap: A verification framework for low-level C",

abstract = "This paper presents the formal Isabelle/HOL framework we use to prove refinement between an executable, monadic specification and the C implementation of the seL4 microkernel. We describe the refinement framework itself, the automated tactics it supports, and the connection to our previous C verification framework. We also report on our experience in applying the framework to seL4. The characteristics of this microkernel verification are the size of the target (8,700 lines of C code), the treatment of low-level programming constructs, the focus on high performance, and the large subset of the C programming language addressed, which includes pointer arithmetic and type-unsafe code.",

author = "Simon Winwood and Gerwin Klein and Thomas Sewell and June Andronick and David Cock and Michael Norrish",

year = "2009",

doi = "10.1007/978-3-642-03359-9_34",

language = "English",

isbn = "364203358X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "500--515",

booktitle = "Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings",

note = "22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009 ; Conference date: 17-08-2009 Through 20-08-2009",

}

Winwood, S, Klein, G, Sewell, T, Andronick, J, Cock, D & Norrish, M 2009, Mind the gap: A verification framework for low-level C. in Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5674 LNCS, pp. 500-515, 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009, Munich, Germany, 17/08/09. https://doi.org/10.1007/978-3-642-03359-9_34

Mind the gap: A verification framework for low-level C. / Winwood, Simon; Klein, Gerwin; Sewell, Thomas et al.
Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings. 2009. p. 500-515 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5674 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Mind the gap

T2 - 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009

AU - Winwood, Simon

AU - Klein, Gerwin

AU - Sewell, Thomas

AU - Andronick, June

AU - Cock, David

AU - Norrish, Michael

PY - 2009

Y1 - 2009

N2 - This paper presents the formal Isabelle/HOL framework we use to prove refinement between an executable, monadic specification and the C implementation of the seL4 microkernel. We describe the refinement framework itself, the automated tactics it supports, and the connection to our previous C verification framework. We also report on our experience in applying the framework to seL4. The characteristics of this microkernel verification are the size of the target (8,700 lines of C code), the treatment of low-level programming constructs, the focus on high performance, and the large subset of the C programming language addressed, which includes pointer arithmetic and type-unsafe code.

AB - This paper presents the formal Isabelle/HOL framework we use to prove refinement between an executable, monadic specification and the C implementation of the seL4 microkernel. We describe the refinement framework itself, the automated tactics it supports, and the connection to our previous C verification framework. We also report on our experience in applying the framework to seL4. The characteristics of this microkernel verification are the size of the target (8,700 lines of C code), the treatment of low-level programming constructs, the focus on high performance, and the large subset of the C programming language addressed, which includes pointer arithmetic and type-unsafe code.

UR - http://www.scopus.com/inward/record.url?scp=70350303809&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-03359-9_34

DO - 10.1007/978-3-642-03359-9_34

M3 - Conference contribution

SN - 364203358X

SN - 9783642033582

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 500

EP - 515

BT - Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings

Y2 - 17 August 2009 through 20 August 2009

ER -

Winwood S, Klein G, Sewell T, Andronick J, Cock D, Norrish M. Mind the gap: A verification framework for low-level C. In Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings. 2009. p. 500-515. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-03359-9_34

Mind the gap: A verification framework for low-level C

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this