34,7 → 34,7 |
OSes are usually designed to run on bare hardware. This means that they do not require |
any special assumptions on the environment except the assumptions on the properties and |
behavior of hardware. In many cases it is perfectly valid to consider the hardware |
as \emph{idealized hardware} (zero mathematical probability of failure, perfect compiance |
as \emph{idealized hardware} (zero mathematical probability of failure, perfect compliance |
with the specifications, etc.). This means that it is solely the OS that defines the |
environment for other software. |
|
66,7 → 66,7 |
|
The architecture of these major desktop and server OSes is monolithic, which makes |
any attempts to do formal verification on them extremely challenging due to the large |
state space. Fortunatelly we can observe that aspects of several novel approaches from |
state space. Fortunately we can observe that aspects of several novel approaches from |
the OS research from the late 1980s and early 1990s (microkernel design, user space |
file system and device drivers, etc.) are slowly emerging in these originally purely |
monolithic implementations. |
80,7 → 80,7 |
general-purpose OSes. |
|
Our approach is not based on using a single ``silver-bullet'' formalism, methodology or |
tool, but on combining various enginering, semi-formal and formal approaches. |
tool, but on combining various engineering, semi-formal and formal approaches. |
While the lesser formal approaches give lesser guarantees, they can complement |
the formal approaches on their boundaries and increase the coverage of the set of |
all hypothetical interesting properties of the system. |
259,8 → 259,7 |
\end{figure} |
|
In this section, we analyze the properties we would like to check in a general-purpose |
operating system. Each set of properties usually requires a specific verification method, |
tool or toolchain. |
OS. Each set of properties usually requires a specific verification method, tool or toolchain. |
|
Our approach will be mostly bottom-up, or, in other words, from the lower levels of abstraction |
to the higher levels of abstraction. If the verification fails on a lower level, it usually |
282,7 → 281,7 |
\medskip |
|
Please note that the titles of the following sections do not follow any particular established |
taxonomy. We have simply chosen the names to be intuitivelly descriptive. |
taxonomy. We have simply chosen the names to be intuitively descriptive. |
|
\subsection{C Language Compiler and Continuous Integration Tool} |
\label{clang} |
414,8 → 413,7 |
invariants in the code. Many static verifiers also target true multithreaded usage patterns |
and have the capability to check proper locking order, hand-over-hand locking and even liveliness. |
|
In the context of an operating system kernel and core libraries two kinds of properties are |
common: |
In the context of an OS kernel and core libraries two kinds of properties are common: |
|
\begin{description} |
\item[Consistency constrains] These properties define the correct way how data is supposed |
431,8 → 429,8 |
\subsection{Model Checker} |
\label{modelcheck} |
On the first sight it does not seem to be reasonable to consider general model checkers as |
relevant independent tools for formal verification of an existing operating system. While many |
different tools use model checkers as their backends, verifying a complete model of the entire |
relevant independent tools for formal verification of an existing OS. While many different |
tools use model checkers as their backends, verifying a complete model of the entire |
system created by hand seems to be infeasible both in the sense of time required for the model |
creation and resources required by the checker to finish the exhaustive traversal of the model's |
address space. |
463,7 → 461,7 |
|
It is extremely important to define the right role of the behavior and architecture description. |
A flawed approach would be to reverse-engineer this description from the source code (either manually |
or via some sophisticated tool) and then verify the compliance between the desciption and |
or via some sophisticated tool) and then verify the compliance between the description and |
the implementation. However, different directions can give more interesting results: |
|
\begin{description} |
501,7 → 499,7 |
|
The key features of software systems with respect to behavior and architecture checkers are the granularity |
of the individual primitive components, the level of isolation and complexity of the communication mechanism |
between them. Large monolithic OSes created in sematic-poor C present a severe challenge because the |
between them. Large monolithic OSes created in semantic-poor C present a severe challenge because the |
isolation of the individual components is vague and the communication between them is basically unlimited |
(function calls, shared resources, etc.). |
|