Sequoll: A framework for model checking binaries
Sequoll: A framework for model checking binaries
复制标题
DOI：
10.1109/rtas.2013.6531083
复制
发表时间：
2013-04
期刊：
影响因子：
--
通讯作者：
Bernard Blackham;Gernot Heiser
中科院分区：
文献类型：
--
作者：
Bernard Blackham;Gernot Heiser
多临界实时系统需要具有有限中断延迟和组件间保证隔离的保护模式操作系统。对这类系统进行严格的WCET分析需要关于循环边界和不可行的路径的可靠信息。我们提出了sequoll，一个使用二进制代码的模型检查来确定循环计数和不可行路径的框架，以及验证经常容易出错的手动不可行路径注释。我们展示了sequoll在Malardalen WCET基准测试中自动确定许多循环计数。我们还展示了sequoll计算循环边界并验证了几个不可行的路径注释，这些注释用于减少seL4（用于多临界系统的高保证保护微内核）计算的WCET边界。
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 many of the loop counts in the Malardalen 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.