4,9 → 4,9 |
\title{A Road to a Formally Verified General-Purpose Operating System} |
\author{Martin D\v{e}ck\'{y}} |
\institute{Department of Distributed and Dependable Systems\\ |
Faculty of Mathematics and Physics, Charles University\\ |
Malostransk\'{e} n\'{a}m\v{e}st\'{i} 25, Prague 1, 118~00, Czech Republic\\ |
\email{martin.decky@d3s.mff.cuni.cz}} |
Faculty of Mathematics and Physics, Charles University\\ |
Malostransk\'{e} n\'{a}m\v{e}st\'{i} 25, Prague 1, 118~00, Czech Republic\\ |
\email{martin.decky@d3s.mff.cuni.cz}} |
|
\begin{document} |
\maketitle |
132,7 → 132,7 |
|
\medskip |
|
HelenOS can be briefly described as microkernel multiserver design. However, the actual design |
HelenOS can be briefly described as microkernel multiserver OS. However, the actual design |
guiding principles of the HelenOS are more elaborate: |
|
\begin{description} |
151,8 → 151,8 |
\item[Multiserver principle] Subsystems in user space should be decomposed with the smallest |
reasonable granularity. Each unit of decomposition should be encapsulated in a separate task. |
The tasks represent software components with isolated address spaces. From the design point of |
view the kernel can be seen as a separate component, too. |
\item[Split of mechanism and policy] The kernel should only provide low-level mechanisms, |
view the kernel can be seen as a separate software component, too. |
\item[Split of mechanism and policy] The kernel should only provide low-level me\-chanisms, |
while the high-level policies which are built upon these mechanisms should be defined in |
user space. This also implies that the policies should be easily replaceable while keeping |
the low-level mechanisms intact. |
227,9 → 227,9 |
However, what is the biggest advantage of C in terms of run-time performance is also the biggest weakness |
for formal reasoning. The permissive memory access model of C, the lack of any reference safety |
enforcement, the weak type system and generally little semantic information in the code -- all these |
properties that do not allow to make many general assumptions about the code. |
properties do not allow to make many general assumptions about the code. |
|
Programming languages which target controlled environments such as Java or C\(\sharp\) are |
Programming languages which target controlled environments such as Java and C\(\sharp\) are |
generally easier for formal reasoning because they provide a well-known set of primitives |
and language constructs for object ownership, threading and synchronization. Many non-imperative |
programming languages can be even considered to be a form of ``executable specification'' and thus |
273,10 → 273,10 |
of the term. However, even methods which are based on semi-formal reasoning and non-exhaustive |
testing provide some limited guarantees in their specific context. A valued property |
of the formal methods is to preserve these limited guarantees even on the higher levels |
of abstraction, thus complementing the formal guarantees where the formal methods do not provide |
any feasible verification so far. This increases the coverage of the set of all hypothetical |
interesting properties of the system (although it is probably impossible to formally define |
this set). |
of abstraction, thus allowing the semi-formal methods to complement the big picture |
where the formal methods do not provide any feasible verification so far. This increases |
the coverage of the set of all hypothetical interesting properties of the system (although |
it is probably impossible to formally define this entire set). |
|
\medskip |
|
292,7 → 292,7 |
these decisions can be made by any plain C compiler. However, with the current implementation |
of HelenOS even this is not quite trivial. |
|
Besides the requirement to support 7 hardware platforms, the system's compile-time configuration |
Besides the requirement to support 7 hardware platforms, the system's com\-pile-time configuration |
can be also affected by approximately 65 configuration options, most of which are booleans, |
the rest are enumerated types. |
|
433,7 → 433,7 |
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. |
state space. |
|
Nevertheless, model checkers on their own can still serve a good job verifying abstract |
properties of key algorithms without dealing with the technical details of the implementation. |
474,13 → 474,13 |
compatible. All required interfaces need to be bound to provided interfaces and |
the communication between the components cannot lead to \emph{no activity} (a deadlock), |
\emph{bad activity} (a livelock) or other communication and synchronization errors. |
\item[Vertical compliance] Also called \emph{substituability}. The goal is to check whether |
\item[Vertical compliance] Also called \emph{substituability}. The goal is to check whe\-ther |
it is possible to replace a set of primitive components that are nested inside a composite |
component by the composite component itself. In other words, this compliance can answer the |
questions whether the architecture description of the system is sound with respect to the hierarchical |
question whether the architecture description of the system is sound with respect to the hierarchical |
composition of the components. |
\item[Compliance between the specification and the implementation] Using various means |
for generating artificial environments for an isolated component the checker is able to |
\item[Specification and implementation compliance] Using various means |
of generating artificial environments for an isolated component a checker is able to |
partially answer the question whether the implementation of the component is an instantiation |
of the component specification. |
\end{description} |
491,7 → 491,7 |
\end{description} |
|
Unfortunately, most of the behavior and architecture formalisms are static, which is not quite suitable |
for the dynamic of most OSes. This limitation can be circumvented by considering a relevant |
for the dynamic nature of most OSes. This limitation can be circumvented by considering a relevant |
snapshot of the dynamic run-time architecture. This snapshot fixed in time is equivalent to |
a statically defined architecture. |
|
557,7 → 557,7 |
|
We have spoken only about the functional properties. In general, we cannot apply the same formalisms |
and methods on extra-functional properties (e.g. timing properties, performance properties, etc.). |
And although it probably does make a good sense to reason about component composition for the extra-functional |
And although it probably does make a good sense to reason about component composition for the extra-functi\-onal |
properties, the exact relation might be different compared to the functional properties. |
|
The extra-functional properties need to be tackled by our future work. |
584,7 → 584,7 |
of unchecked overflows), the usage of uninitialized variables, the presence of unused local variables, |
NULL-pointer dereferencing (determined by conservative local control flow analysis), functions |
with non-void return typed that do not return any value and so on. We treat all compilation warnings |
as fatal errors, thus the code base must pass without any warnings. |
as fatal errors (\texttt{-Werror}), thus the code base must pass without any warnings. |
|
We also turn on several more specific and strict checks. These checks helped to discover several |
latent bugs in the source code: |
636,9 → 636,6 |
by the need to support MMU-less architectures in the future. But this framework might be also very helpful |
in detecting memory and generic resource leaks. We have not tried \emph{Valgrind}~\cite{valgrind} or any similar |
existing tool because of the estimated complexity to adopt it for the usage in HelenOS. |
|
HelenOS was also scanned by \emph{Coverity}~\cite{coverity} in 2006 when no errors were detected. However, since |
that time the code base has not been analyzed by Coverity. |
|
\subsection{Static Analyzer} |
The integration of various static analyzers into the HelenOS continuous integration process is underway. |
649,6 → 646,9 |
The open framework of Clang seems to be very promising for implementing domain-specific checks (and at |
the same time it is also a very promising compiler framework). Our mid-term goal is to incorporate some of the features |
of Stanse and VCC (see Section \ref{staticverifier2}) into Clang Analyzer. |
|
HelenOS was also scanned by \emph{Coverity}~\cite{coverity} in 2006 when no errors were detected. However, since |
that time the code base has not been analyzed by Coverity. |
|
\subsection{Static Verifier} |
\label{staticverifier2} |