WebSVN – HelenOS-doc – Diff – /papers/isarcs10/isarcs10.tex



\usepackage{graphicx}
 
\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}}
 
\begin{document}
    \maketitle
   
    \begin{abstract}

            Many development projects such as task snapshoting and migration, support for MMU-less
            platforms and performance monitoring are currently underway.
           
            \medskip
           
            HelenOS can be briefly described as microkernel multiserver OS. However, the actual design
            guiding principles of the HelenOS are more elaborate:
           
            \begin{description}
                \item[Microkernel principle] Every functionality of the OS that does not
                      have to be necessary implemented in the kernel should be implemented in user space. This

                      It contains features such as AVL and B+ trees, hashing tables, SLAB memory allocator, multiple
                      in-kernel synchronization primitives, fine-grained locking and so on.
                \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 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.
                \item[Encapsulation principle] The communication between the tasks/components should be
                      implemented only via a set of well-defined interfaces. In the user-to-user case the preferred

            architecture to the programmer in a very straightforward, but still relatively portable way.
           
            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 do not allow to make many general assumptions about the code.
           
            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
            very suitable for formal reasoning. In C, almost everything is left to the programmer who
            is free to set the rules.

       
        Some of the proposed methods cannot be called ``formal methods'' in the rigorous understanding
        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 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
       
        Please note that the titles of the following sections do not follow any particular established
        taxonomy. We have simply chosen the names to be intuitively descriptive.

            programming language specification and passes only the basic semantic checks (proper number
            and types of arguments passed to functions, etc.). It is perhaps not very surprising that
            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 com\-pile-time configuration
            can be also affected by approximately 65 configuration options, most of which are booleans,
            the rest are enumerated types.
           
            These configuration options are bound by logical propositions in conjunctive or disjunctive
            normal forms and while some options are freely configurable, the value of others gets inferred

            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 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
            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.
            Various properties of synchronization algorithms, data structures and communication protocols
            can be verified in the most generic conditions by model checkers, answering the

                        \item[Horizontal compliance] Also called \emph{compatibility}. The goal is to check
                             whether the specifications of components that are bound together are semantically
                             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 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
                             question whether the architecture description of the system is sound with respect to the hierarchical
                             composition of the components.
                        \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}
                \item[Description as abstraction] Generating the behavior and architecture description from the
                      source code by means of abstract interpretation can serve the purpose of verifying various
                      properties of the implementation such as invariants, preconditions and postconditions.
                      This is similar to static verification, but on the level of component interfaces.
            \end{description}
           
            Unfortunately, most of the behavior and architecture formalisms are static, which is not quite suitable
            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.
           
            \medskip
           

           
            \medskip
           
            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-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.
       
    \section{Evaluation}

            most of the verification checks of the compilers. The compilers trip on common bug antipatterns such
            as implicit typecasting of pointer types, comparison of signed and unsigned integer values (danger
            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 (\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:
           
            \begin{description}

        \subsection{Instrumentation}
            We are in the process of implementing our own code instrumentation framework which is motivated mainly
            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.
 
 
 
       
        \subsection{Static Analyzer}
            The integration of various static analyzers into the HelenOS continuous integration process is underway.
            For the initial evaluation we have used \emph{Stanse}~\cite{stanse} and \emph{Clang Analyzer}~\cite{clanganalyzer}.
            Both of them showed to be moderately helpful to point out instances of unreachable dead code, use of language
            constructs which have ambiguous semantics in C and one case of possible NULL-pointer dereference.
           
            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}
            We have started to extend the source code of HelenOS kernel with annotations understood
            by \emph{Frama-C}~\cite{framac} and \emph{VCC}~\cite{vcc}. Initially we have targeted simple kernel data structures
Subversion Repositories HelenOS-doc

(root)/papers/isarcs10/isarcs10.tex – Rev 183 → 184
