Modeling and security analysis of a commercial real-time operating system kernel

Abstract

This chapter summarizes the modeling and formal analysis effort that led to an EAL6+ certification for a commercial real-time operating system kernel. We begin by describing the INTEGRITY-178B kernel, as well as the approach taken for the Common Criteria evaluation effort. We present a generalization of the GWV theorem, formulated in order to capture the meaning of separation in a dynamic system. We detail how the INTEGRITY-178B kernel was modeled, including System State, Behavior, and Information Flow. We discuss the proof architecture used to demonstrate correspondence and conclude with a description of the informal analysis of the hardware abstraction layer. © 2010 Springer Science+Business Media, LLC.