Skip to main content

TS

Sequoll: A framework for model checking binaries

Authors

Bernard Blackham and Gernot Heiser

NICTA

UNSW

Abstract

Multi-criticality real-time systems require protected-mode operating systems with bounded interrupt latencies and guaranteed isolation between components. A tight WCET analysis of such systems requires trustworthy information about loop bounds and infeasible paths.

We propose sequoll, a framework for employing model checking of binary code to determine loop counts and infeasible paths, as well as validating manual infeasible path annotations which are often error-prone. We show that sequoll automatically determines the majority of loop counts in the Mälardalen WCET benchmarks. We also show that sequoll computes loop bounds and validates several infeasible path annotations used to reduce the computed WCET bound of seL4, a high-assurance protected microkernel for multi-criticality systems.

BibTeX Entry

  @inproceedings{Blackham_Heiser_13,
    isbn             = {978-1-4799-0184-5},
    author           = {Blackham, Bernard and Heiser, Gernot},
    year             = {2013},
    month            = {apr},
    slides           = {http://ts.data61.csiro.au/publications/nicta_slides/6405.pdf},
    editor           = {{Eduardo Tovar}},
    keywords         = {verification, trustworthy systems},
    title            = {Sequoll: a framework for model checking binaries},
    booktitle        = {IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)},
    pages            = {97-106},
    address          = {Philadelphia, USA}
  }

Download