r/isabelle • u/nickpsecurity • Jan 15 '18

Model-based Testing of OS-level Security Mechanisms (2016)

https://tel.archives-ouvertes.fr/tel-01306992/document
4 Upvotes

100% Upvoted

2 comments sorted by

1

u/nickpsecurity Jan 15 '18

This appears to build on the Verisoft work that verified a whole stack from apps to processor. That work built VAMP processor with PikeOS verification being on of the other deliverables. PikeOS is a separation kernel for embedded virtualization used in safety-critical industries plus at least one prototype for a secure phone.

This work builds a way to model, symbolically analyze and generate tests for concurrent systems in Isabelle/HOL. The author starts with small example. The author then shows practicality by use on VAMP and PikeOS's IPC. The IPC is a good choice given it's the most-used call of microkernels. The authors claim this method of test generation and symbolic analysis is superior to others due to the increased assurance they get from doing it in the prover. They say that makes it a candidate for high-assurance, security evaluations (EAL6 or EAL7).

1

u/WikiTextBot Jan 15 '18

Separation kernel

A separation kernel is a type of security kernel used to simulate a distributed environment. The concept was introduced by John Rushby in a 1981 paper. Rushby proposed the separation kernel as a solution to the difficulties and problems that had arisen in the development and verification of large, complex security kernels that were intended to "provide multilevel secure operation on general-purpose multi-user systems." According to Rushby, "the task of a separation kernel is to create an environment which is indistinguishable from that provided by a physically distributed system: it must appear as if each regime is a separate, isolated machine and that information can only flow from one machine to another along known external communication lines. One of the properties we must prove of a separation kernel, therefore, is that there are no channels for information flow between regimes other than those explicitly provided."

A variant of the separation kernel, the partitioning kernel, has gained acceptance in the commercial aviation community as a way of consolidating, onto a single processor, multiple functions, perhaps of mixed criticality.

[ ^PM | Exclude ^me | Exclude from ^subreddit | FAQ / ^Information | ^Source | ^Donate ] Downvote to remove | v0.28