详情

原文传递 Formal Model of a Multi Core Kernel based System.

题名：	Formal Model of a Multi Core Kernel based System.
作者：	Andronick, J.; Morgan, C.; Klein, G.
关键词：	Automation, Air force, Case studies, Department of defense, Environment, Generators, Scientific research, Autonomous vehicles, Guarantees, Multithreading, Reasoning, Security, Semantics, Verification, Abstracts, Programming languages, Specifications, Formal languages, Operating systems, Language
摘要：	Professor Andronick and her research team sought to address the grand challenge of providing strong, mathematical guarantees for software that runs on multi-core platforms, thus meeting the increasing demand for more computing power even for critical real-world systems. The research team targeted the operating system kernel, which is the core and foundation of any software system.Their approach was to to solve a large part of the scalability problem in foundational concurrency reasoning by exploiting automation inmodern machine-checked theorem proving. In addition, they sought to soundly reduce reasoning about interleaving with a faithful representation of hardware and software mechanisms such as scheduling, priorities, interrupts, and locks; and to continue to exploit kernel design principles for reducing verification effort.The project has achieved all planned goals, including its stretch goals. They have defined a formal model of execution for a multi-core kernel, as well as a low-level formal language to push the guarantees as close as possible to the real implementation. This framework has been applied to a multi-core version of seL4 [Klein et al., 2009], the landmark verified microkernel, whose verification so far is restricted to uniprocessor systems. They have defined a formal high-level model of multi-core seL4 and proved the correctness of its most criticaloperation. They have also developed an initial refinement framework that will allow us to carry the proofs done at the high specification level down to the low implementation level. The project paves the way for proving full functional correctness of multi-core, high performance microkernels
报告类型：	科技报告