High-Level Separation Logic for Low-Level Code

Add to your list(s) Download to your calendar using vCal

• Nick Benton, MSR Cambridge
• Monday 10 December 2012, 13:00-14:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

(joint work with Jonas Jensen and Andrew Kennedy)

Separation logic is a powerful tool for reasoning about structured, imperative programs that manipulate pointers. However, its application to unstructured, lower-level languages such as assembly language or machine code remains challenging. We describe a separation logic tailored for this purpose that we have applied to x86 machine code programs.

The logic is built from an assertion logic on machine states over which we construct a specification logic that encapsulates uses of frames and step indexing. The traditional notion of Hoare triple is not applicable directly to unstructured machine code, where code and data are mixed together and programs do not in general run to completion, so instead we adopt a continuation-passing style of specification with preconditions alone. Nevertheless, the range of primitives provided by the specification logic, which include a higher-order frame connective, a novel read-only frame connective, and a ‘later’ modality, support the definition of derived forms to support basic-block-style reasoning for common cases, in which standard rules for Hoare triples are derived as lemmas. Furthermore, our encoding of assembly language labels in terms of the more primitive code pointers lets us encapsulate local usage of labels and the definition and rules for assembly-language ‘macros’ such as while loops and conditionals.

We have applied the framework to a model of x86 machine code built entirely within the Coq proof assistant, including tactic support based on computational reflection.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.