Modeling and Security Analysis of a Commercial Real-Time Operating System Kernel

Autor:	Raymond J. Richards
Rok vydání:	2010
Předmět:	Security analysis Theoretical computer science Common Criteria Computer science Generalization Kernel (statistics) Real-time computing Certification Information flow (information theory) State (computer science) Real-time operating system
Zdroj:	Design and Verification of Microprocessor Systems for High-Assurance Applications ISBN: 9781441915382 Design and Verification of Microprocessor Systems for High-Assurance Applications
DOI:	10.1007/978-1-4419-1539-9_10
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::706cb0680f3f9c10340f70ccc6b16a38 https://doi.org/10.1007/978-1-4419-1539-9_10 Zobrazit plný text záznamu