Subversion Repositories HelenOS-doc

\documentclass{llncs}

\usepackage{graphicx}

\title{A Road to a Formally Verified General-Purpose Operating System}

\author{Martin D\v{e}ck\'{y}}

\institute{Department of Software Engineering\\

        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@dsrg.mff.cuni.cz}}

\begin{document}

    \maketitle

    \begin{abstract}

        Methods of formal description and verification represent a viable way for achieving

        fundamentally bug-free software. However, in reality only a small subset of the existing operating

        systems were ever formally verified, despite the fact that an operating system is a critical part

        of almost any other software system. This paper summarizes the challenges involved in formal verification

        of operating systems, points out several key design choices which should make the formal verification

        easier and presents a work-in-progress and initial experiences with formal verification of HelenOS,

        a state-of-the-art microkernel-based operating system, which, however, was not designed specifically

        with formal verification in mind, as this is mostly prohibitive due to time and budget constrains.

        The contribution of this paper is the shift of focus from attempts to use a single ``silver-bullet''

        formal verification method which would be able to verify everything to a combination of multiple

        formalisms and techniques to cover various aspects of the verification process. The formally verified

        operating system is the emerging property of the combination.

    \end{abstract}

    \section{Introduction}

        \label{introduction}

        In the context of formal verification of software, it is always important to model the outer

        environment with a proper level of abstraction. Weak assumptions on the environment make the formal

        verification less feasible, because they yield many degrees of freedom which render

        the properties which we want to verify overly complex. But strong assumptions on the environment are likewise

        not without a price: Any practical usability of the verification results depends on the question

        whether we are really able to create a physical environment which satisfies the assumptions.

        There are some assumptions which are universal for any formal verification method. For the sake of

        simplicity let us call them \emph{idealized hardware}. Let us also cover the computational model

        and basic mathematical principles by this term.

        What is \emph{idealized hardware}? We usually assume that the software is executed by a ``perfect'' hardware

        which works exactly according to its specification. Every divergence between the intended and actual

        behavior of software counts as a software bug and never as an issue in some hardware component. We

        implicitly assume that the hardware is perfect in the sense of physical realization and all probabilities

        of accidental mechanical and electrical failures are expected to be zero.

        It is trivial to see that the \emph{idealized hardware} assumptions can never hold in real world.

        Accidental mechanical and electrical failures are inevitable in principle and their probability can

        never be a mathematical zero. Does this mean that any formal verification method is ultimately futile

        since we are unable to ensure validity of the most elementary assumptions? Probably not. We just need

        to be aware about the inherent and fundamental limitations of the formal methods which result from

        the shortcomings of the physical world.

        The more precisely we model the software environment of the software under discussion, the more precisely

        we can calculate or estimate the resulting impact of the imperfections of the physical world on our software

        system. This is the most important motivation for formal reasoning about the correctness of the operating system.

        \medskip

        In more detail, operating systems have a somewhat special position among all software:

        \begin{itemize}

            \item \emph{Operating systems are usually designed to run on bare hardware.} This means that except

                  the \emph{idealized hardware} assumptions we do not have to take any or almost any extra assumptions

                  into account.

            \item \emph{Operating systems create the lowest software layer and provide services to essentially

                  all other software.} Considering the principle of recursion, the properties of the

                  operating systems which we prove or disprove form the assumptions for the upper layers

                  of software. Thus the dependability of end-user and enterprise software systems is limited

                  by the dependability of the operating system.

            \item \emph{Operating systems are non-trivial software on their own.} The way

                  they are generally designed and programmed (spanning both the kernel and user mode,

                  manipulating execution contexts and concurrency, handling critical hardware-related

                  operations) represent significant and interesting challenges for the formal verification

                  methods and tools.

        \end{itemize}

        Even in the informal understanding, the dependability of an operating system greatly determines the perceived

        dependability of the entire software stack. This led to several research initiatives in the recent years

        which target the creation of a formally verified operating systems from scratch~\cite{seL4}.

        However, 98~\%\footnote{98~\% of client computers connected to the Internet as of January 2010~\cite{marketshare}.} of

        the market share of general-purpose operating systems is taken by Windows, Mac~OS~X and Linux.

        These systems were clearly not designed with formal verification in mind from the very beginning.

        The situation on the embedded, real-time and special-purpose operating systems market is probably different,

        but it is unlikely that the situation in the large domain of desktops and servers is going to change

        very rapidly in the near future.

        Therefore we need to face the challenges of applying formal methods on an existing code base in the domain

        of general-purpose operating systems. Fortunately, the software design qualities of the general-purpose

        operating systems gradually improve over time. We can see then novel approaches in the operating systems

        research from the late 1980s and 1990s (microkernel design, user space file system and device drivers, etc.)

        to slowly emerge in the originally monolithic operating systems. We can also see better code quality thanks

        to improved software engineering (code review, proper escalation management, etc.).

        \medskip

        This paper proposes an approach and presents a work-in-progress case study of formal verification

        of an general-purpose research operating system, which was also not created specifically with formal

        verification in mind from the very beginning, but it was designed according to state-of-the-art operating systems

        principles.

        \medskip

        \noindent\textbf{Structure of the Paper.} In Section \ref{context} we introduce the case study in more detail and explain

        why we believe it is relevant. In Section \ref{analysis} we discuss our proposal of the combination of formal methods

        and tools. In Section \ref{evaluation} we present the preliminary evaluation of our efforts and estimate the complexity

        of the imminent next steps we want to take according to our proposal. Finally, in Section \ref{conclusion}

        we present the conclusion of the paper.

    \section{Context}

        \label{context}

        Two very common schemes of operating system design are \emph{monolithic design} and \emph{microkernel design}.

        Without going into much detail of any specific operating system, we can define the monolithic design as

        a preference to put numerous aspects of the core operating system functionality into the kernel,

        while microkernel design is a preference to keep the kernel small, with just a minimal set of features.

        The features which are missing from the kernel in the microkernel design are implemented in user space, usually

        by means of libraries, servers and/or software components.

        \subsection{HelenOS}

            \label{helenos}

            \emph{HelenOS} is a general-purpose research operating system which is being developed at Charles

            University in Prague. The source code is available under the BSD open source license and can be

            freely downloaded from the project web site~\cite{helenos}. The authors of the code base are

            both from the academia and from the open source community (several contributors are employed

            as Solaris kernel developers and many are freelance IT professionals). We consistently strive to support

            the research and also the practical motivations for developing the system.

            HelenOS uses a preemptive priority-feedback scheduler, it supports SMP hardware and it is

            designed to be highly portable. Currently it runs on 7 distinct hardware architectures, including the

            most common IA-32, x86-64 (AMD64), IA-64, SPARC~v9 and PowerPC. It also runs on ARMv7 and MIPS,

            but currently only in simulators and not on physical hardware.

            Although HelenOS is still far from being an everyday replacement for Linux or Windows due to the lack

            of end-user applications (whose development is extremely time-consuming, but unfortunately of

            no scientific value), the essential foundations such as file system support and TCP/IP networking

            are already in place.

            HelenOS does not currently target embedded devices (although the ARMv7 port can be easily modified to

            run on various embedded boards) and does not implement real-time scheduling and synchronization.

            Many development projects such as task snapshoting and migration, generic device driver

            framework, support for MMU-less platforms and performance monitoring are currently underway.

            \medskip

            HelenOS has a microkernel multiserver design, but the guiding principles of the HelenOS design are

            actually more elaborate:

            \begin{itemize}

                \item \emph{(Microkernel principle)} Every functionality of the operating system that does not

                      have to be necessary implemented in the kernel should be implemented in user space. This

                      implies that subsystems such as the file system, device drivers (except those which are

                      essential for the basic kernel functionality), naming and trading services, networking,

                      human interface and similar features should be implemented in user space.

                \item \emph{(Full-fledged principle)} Features which need to be implemented in kernel should

                      be designed with full-fledged algorithms and data structures. In contrast

                      to several other microkernel operating systems, where the authors have deliberately chosen

                      the most simplistic approach (static memory allocation, na\"{\i}ve algorithms, simple data

                      structures), HelenOS microkernel tries to use the most advanced and suitable means available.

                      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 \emph{(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 \emph{(Split of mechanism and policy)} The kernel should only provide low-level mechanisms,

                      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 \emph{(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

                      communication mechanism is HelenOS IPC, which provides reasonable mix of abstraction and

                      performance (RPC-like primitives combined with implicit memory sharing for large data

                      transfers). In case of synchronous user-to-kernel communication the usual syscalls are used.

                      HelenOS IPC is used again for asynchronous kernel-to-user communication.

                \item \emph{(Portability principle)} The design and implementation should always maintain a high

                      level of platform neutrality and portability. Platform-specific code in the kernel, core

                      libraries and tasks implementing low-level functionality (e.g. device drivers) should be

                      clearly separated from the generic code (either by component decomposition, naming and trading,

                      or at least by internal compile-time APIs).

            \end{itemize}

            As these design guiding principles suggest, the size of the HelenOS microkernel is considerably larger

            compared to ``scrupulous'' microkernel implementations. The average footprint of the kernel ranges from

            569~KiB when all logging messages, asserts, symbol resolution and debugging kernel console are compiled

            in, down to 198~KiB for a non-debugging production build. We do not believe that the raw size

            of the microkernel is a relevant quality criterion per se, without taking the actual feature set

            into account.

            \medskip

            The run-time architecture of HelenOS is inherently dynamic. The bindings between the components are

            not created at compile-time, but during the bootstrap process and can be modified to a large degree

            also during normal operation mode of the system (via human interaction and external events). This

            creates particularly interesting challenges for describing the design of the system by many formalisms.

            \medskip

            Yet another set of obstacles for reasoning about the properties of HelenOS lies in the design of

            the ubiquitous HelenOS IPC mechanism and the associated threading model. The IPC is inherently

            asynchronous with constant message buffers in the kernel and dynamic buffers in user space.

            It uses the notions of uni-directional bindings, mandatory pairing of requests and replies,

            binding establishment and abolishment handshakes, memory sharing and fast message forwarding.

            For easier management of the asynchronous messages and the possibility to process multiple

            messages from different peers without the usual kernel threading overhead, the core user space

            library manages the execution flow by so-called \emph{fibrils}. A fibril is a user-space-managed thread with

            cooperative scheduling. A different fibril is scheduled every time the current fibril is

            about to be blocked while sending out IPC requests (because the kernel buffers of the addressee

            are full) or while waiting on an IPC reply. This allows different execution flows within the

            same thread to process multiple requests and replies. To safeguard proper sequencing

            of IPC messages and provide synchronization, special fibril-aware synchronization primitives

            (mutexes, condition variables, etc.) are available.

            Because of the cooperative nature of fibrils, they might cause severe performance under-utilization

            in SMP configurations and system-wide bottlenecks. As multicore processors are more and more

            common nowadays, that would be a substantial design flaw. Therefore the fibrils can be also freely

            (and to some degree even automatically) combined with the usual kernel threads, which provide

            preemptive scheduling and true parallelism on SMP machines. Needless to say, this combination is

            also a grand challenge for the formal reasoning.

            \medskip

            To sum up, the choice of HelenOS as our case study is based on the fact that it was not designed

            in advance with formal verification in mind. This is similar to most general-purpose operating

            systems in common use. At the same time, it does not have an obsolete design and is non-trivial.

        \subsection{The C Programming Language}

            A large majority of operating systems is coded in the C programming language. HelenOS is no exception

            to this. The choice of C in the case of kernel is usually well-motivated -- the language was designed

            specifically for implementing system software~\cite{c}. It is reasonably low-level in the sense that it allows

            to access the memory and other hardware resources with similar effectiveness as from assembler.

            It also requires almost no run-time support and it exports many features of the von Neumann hardware

            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 or 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.

            \medskip

            The reasons for using C in the user space of HelenOS (and other established operating systems) is

            probably much more questionable. Except for the core libraries and services (such as device drivers),

            C might be easily replaced by any high-level and perhaps even non-imperative programming language.

            The reasons for using C in this context is mostly historical.

            However, as we have stated in Section \ref{introduction}, the way general-purpose operating systems

            are implemented changes only slowly and therefore any propositions which require radical modification

            of the existing code base before committing to the formal verification are not realistic.

    \section{Analysis}

        \label{analysis}

        \begin{figure}[t]

            \begin{center}

                \resizebox*{120mm}{!}{\includegraphics{diag}}

                \caption{Overview of the formalisms and tools proposed.}

                \label{fig:diag}

            \end{center}

        \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.

        Our approach will be mostly bottom-to-top, 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

        does not make much sense to continue with the higher levels of abstraction until the issues

        are tackled. A structured overview of the formalisms and tools can be seen on Figure \ref{fig:diag}.

        Please note that the titles of the following sections do not follow any particular established

        taxonomy of verification methods. We have simply chosen the names to be descriptive.

        \subsection{C Language Compiler and Continuous Integration Tool}

            \label{clang}

            The initial levels of abstraction do not go far from the C source code. First, we would certainly like to

            know whether our code base is compliant with the 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 make 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

            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

            by the build system of HelenOS. Thus, the overall number of distinct configurations in which

            HelenOS can be compiled is at least one order of magnitude larger than the plain number

            of supported hardware platforms.

            Various configuration options affect conditional compilation and linking. The programmers

            are used to make sure that the source code compiles and links fine with respect to the

            most common and obvious configurations, but the unforeseen interaction of the less common

            configuration options might cause linking or even compilation errors.

            \medskip

            A straightforward solution is to generate all distinct configurations, starting from the

            open variables and inferring the others. This can be part of the continuous integration

            process which would try to compile and link the sources in all distinct configurations.

            If we want to be really pedantic, we should also make sure that we run all the relevant higher

            level verification methods on all configurations generated by this step. That would certainly

            require to multiply the time required by the verification methods at least by the number

            of the distinct configurations. Constraining the set of configurations to just the most

            representative ones is perhaps a reasonable compromise.

        \subsection{Regression and Unit Tests}

            Although some people would argue whether testing is a formal verification method, we still include

            it into the big picture. Running regression and unit tests which are part of HelenOS code base

            in the continuous integration process is fairly easy. The only complication lies in the technicalities:

            We need to setup an automated network of physical machines and simulators which can run the

            appropriate compilation outputs for the specific platforms. We need to be able to reboot

            them remotely and distribute the boot images to them. And last but not least, we need to be

            able to gather the results from them.

        \subsection{Instrumentation}

            Instrumentation tools for detecting memory leaks, performance bottlenecks and soft-deadlocks

            are also not usually considered to be formal verification tools. They are also rarely utilized

            on regular basis as part of the continuous integration process. But again, it might be helpful

            to just mention them in the context of regression and unit tests.

            If some regression or unit tests fail, they sometimes do not give sufficient information to

            tell immediately what is the root cause of the issue. In that case running the faulting tests

            on manually or automatically instrumented executable code might provide more data and point

            more directly to the actual bug.

        \subsection{Verifying C Language Compiler}

            C language compilers are traditionally not considered to be formal verification tools. Many people

            just say that C compilers are good at generating executable code, but do not care much about the semantics

            of the source code (on the other hand, formal verification tools usually do not generate any executable code

            at all). However, with recent development in the compiler domain, the old paradigms are shifting.

            As the optimization passes and general maturity of the compilers improve over time,

            the compilers try to extract and use more and more semantic information from the source code.

            The C language is quite poor on explicit semantic information, but the verifying compilers

            try to rely on vendor-specific language extensions and on the fact that some semantic information

            can be added to the source code without changing the resulting executable code.

            The checks done by the verifying compilers cannot result in fatal errors in the usual cases (they

            are just warnings). Firstly, the compilers still need to successfully compile a well-formed C source

            code compliant to some older standard (e.g. C89) even when it is not up with the current quality

            expectations. Old legacy source code should still pass the compilation as it did decades ago.

            Secondly, the checks run by the verifying compilers are usually not based on abstract interpretation

            or exhaustive traversal of a model state space. They are mostly realized as abstract syntax tree

            transformations much in the line with the supporting routines of the compilation process (data

            and control flow graph analysis, dead code elimination, register allocation, etc.) and the evaluation

            function is basically the matching of antipatterns of common programming bugs.

            The checks are usually conservative. The verifying compilers identify code constructs which are suspicious,

            which might arise out of programmer's bad intuition and so on, but even these code snippets cannot be

            tagged as definitive bugs (since the programmer can be simply in a position where he/she really wants to

            do something very strange, but nevertheless legitimate). It is upon the programmer

            to examine the root cause of the compiler warning, tell whether it is really a bug or just a false

            positive and fix the issue by either amending some additional semantic information (e.g. adding an

            explicit typecast or a vendor-specific language extension) or rewriting the code.

        \subsection{Static Analyzer}

            Static analyzers try to go deeper than verifying compilers. Besides detecting common antipatterns of

            bugs, they also use techniques such as abstract interpretation to check for more complex properties.

            Most commercial static analyzers come with a predefined set of properties which cannot be easily changed.

            They are coupled with the commonly used semantics of the environment and generate domain-specific models

            of the software based not only on the syntax of the source code, but also based on the assumptions derived

            from the memory access model, allocation and deallocation rules, tracking of references and tracking of

            concurrency locks.

            The biggest advantage of static analyzers is that they can be easily included in the development or

            continuous integration process as an additional automated step, very similar to the verifying compilers.

            No definition of properties is needed and false positives can be relatively easily eliminated by amending

            some explicit additional information to the source code within the boundaries of the programming language.

            The authors of static analyzers claim large quantities of bugs detected or prevented~\cite{billion}, but static

            analyzers are still relatively limited by the kind of bugs they are designed to detect. They

            are usually good at pointing out common issues with security implications (specific types of buffer

            and stack overruns, usage of well-known functions in an unsafe way, clear cases of forgotten

            deallocation of resources and release of locks, etc.). Unfortunately, many static analyzers

            only analyze a single-threaded control flow and are thus unable to detect concurrency issues

            such as deadlocks.

        \subsection{Static Verifier}

            There is one key difference between a static analyzer and a static verifier: Static verifiers

            allow the user to specify one's own properties, in terms of preconditions, postconditions and

            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:

            \begin{itemize}

                \item \emph{Consistency constrains:} These properties define the correct way how data is supposed

                      to be manipulated by some related set of subroutines. Checking for these

                      properties ensures that data structures and internal states will not get corrupt due

                      to bugs in the functions and methods which are designed to manipulate them.

                \item \emph{Interface enforcement:} These properties define the correct semantics by which

                      a set of subroutines should be used by the rest of the code. Checking for these properties

                      ensures that some API is always used by the rest of the code in a specified way

                      and all possible error states are detected and reported.

            \end{itemize}

        \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

            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.

            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

            question whether they are designed properly in theory.

            If the implementation of these algorithms and protocols do not behave correctly, we can be sure

            that the root cause is in the non-compliance between the design and implementation and not a

            fundamental flaw of the design itself.

        \subsection{Behavior Checker}

            All previously mentioned verification methods were targeting internal properties of the operating system

            components. If we are moving to a higher-level abstraction in order to specify correct interaction of the encapsulated

            components in terms of interface compatibility and communication, we can utilize \emph{Behavior Protocols}~\cite{bp}.

            To gain the knowledge about the architecture of the whole operating system in terms of software

            component composition and bindings, we can use \emph{Architecture Description Language}~\cite{adl}.

            This language has the possibility to capture interface types (with method signatures), primitive

            components (in terms of provided and required interfaces), composite components (an architectural

            compositions of primitive components) and the bindings between the respective interfaces of the

            components.

            Unfortunately, the description is usually static, which is not quite suitable for the dynamic

            nature of HelenOS and other operating systems. 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.

            Behavior Protocol checkers can target three main goals:

            \begin{itemize}

                \item \emph{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)

                      or a \emph{bad activity} (a livelock).

                \item \emph{Vertical compliance:} Also called \emph{substituability}. The goal is to check whether

                      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

                      composition of the components.

                \item \emph{Compliance between the specification and the implementation:} Using various means

                      for generating artificial environments for an isolated component the checker is able to

                      partially answer the question whether the implementation of the component is an instantiation

                      of the component specification.

            \end{itemize}

            Horizontal and vertical compliance checking can be done exhaustively. This is a fundamental property

            which allows the reasoning about the dependability of the entire component-based operating system.

            Assuming that the lower-level verification methods (described in Sections \ref{clang} to \ref{modelcheck})

            prove some specific properties of the primitive components, we can be sure that the composition of

            the primitive components into composite components and ultimately into the whole operating system

            does not break these properties.

            The feasibility of many lower-level verification methods from Sections \ref{clang} to \ref{modelcheck}

            depends largely on the size and complexity of the code under verification. If the entire operating

            system is decomposed into primitive components with a reasonable granularity, it is more likely that the

            individual primitive components can be verified against a large number of properties. Thanks to the

            recursive component composition we can then be sure that these properties also hold for the entire system.

            In monolithic operating systems without a clear decomposition we cannot do this inference and we

            need to verify the lower-level properties over a much larger code base (e.g. the whole monolithic kernel).

            \medskip

            The compliance between the behavior specification and the actual behavior of the implementation is, unfortunately,

            the missing link in the chain. This compliance cannot be easily verified in an exhaustive manner. If there is

            a discrepancy between the specified and the actual behavior of the components, we cannot conclude anything about

            the properties holding in the entire system.

            However, there is one way how to improve the situation: \emph{code generation}. If we generate implementation

            from the specification, the compliance between them is axiomatic. If we are able to generate enough

            code from the specification to run into the hand-written ``business code'' where we check for

            the lower-level properties, the conclusions about the component composition are going to hold.

        \subsection{Behavior Description Generator}

            To conclude our path towards higher abstractions we can utilize tools that can

            generate the behavior descriptions from \emph{textual use cases} written in a domain-constrained English.

            These generated artifacts can be then compared (e.g. via vertical compliance checking) with the formal

            specification. Although the comparison might not provide clean-cut results, it can still be

            helpful to confront the more-or-less informal user expectations on the system with the exact formal description.

        \subsection{Summary}

            \label{missing}

            So far, we have proposed a compact combination of formal methods which start at the level of C programming

            language, offer the possibility to check for the presence of various common antipatterns, to check for generic

            algorithm-related properties, consistency constrains, interface enforcements and conclude with a framework

            to make these properties hold even in the case of a large operating system composed from many

            components of compliant behavior.

            We are also able to fill in some of the missing pieces by other software engineering approaches

            such as regression and unit testing and instrumentation.

            \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-functional

            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}

        \label{evaluation}

        This section copies the structure of the previous Section \ref{analysis} and adds HelenOS-specific

        evaluation of the the proposed formalisms and tools. As this is still largely a work-in-progress,

        in many cases just the initial observations can be made.

        \subsection{Verifying C Language Compiler and Continuous Integration Tool}

            The primary C compiler used by HelenOS is \emph{GNU GCC 4.4.3} (all platforms)~\cite{gcc} and \emph{Clang 2.6.0}

            (IA-32)~\cite{clang}. We have taken some effort to support also \emph{ICC} and \emph{Sun Studio} C compilers,

            but the compatibility with these compilers in not guaranteed.

            The whole code base is compiled with the \texttt{-Wall} and \texttt{-Wextra} compilation options. These options turn on

            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, 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{itemize}

                \item \texttt{-Wfloat-equal} Check for exact equality comparison between floating point values. The

                      usage of equal comparator on floats is usually misguided due to the inherent computational errors

                      of floats.

                \item \texttt{-Wcast-align} Check for code which casts pointers to a type with a stricter alignment

                      requirement. On many RISC-based platforms this can cause run-time unaligned access exceptions.

                \item \texttt{-Wconversion} Check for code where the implicit type conversion (e.g. from float to integer,

                      between signed and unsigned integers or between integers with different number of bits) can

                      cause the actual value to change.

            \end{itemize}

            To enhance the semantic information in the source code, we use GCC-specific language extensions to annotate

            some particular kernel and core library routines:

            \begin{itemize}

                \item \texttt{\_\_attribute\_\_((noreturn))} Functions marked in this way never finish from the point of view

                      of the current sequential execution flow. The most common case are the routines which restore previously saved

                      execution context.

                \item \texttt{\_\_attribute\_\_((returns\_twice))} Functions marked in this way may return multiple times from

                      the point of view of the current sequential execution flow. This is the case of routines which save the current

                      execution context (first the function returns as usual, but the function can eventually ``return again''

                      when the context is being restored).

            \end{itemize}

            The use of these extensions has pointed out to several hard-to-debug bugs on the IA-64 platform.

            \medskip

            The automated continuous integration building system is currently work-in-progress. Thus, we do not

            test all possible configurations of HelenOS with each changeset yet. Currently only

            a representative set of 14 configurations (at least one for each supported platform) is tested by hand

            by the developers before committing any non-trivial changeset.

            From occasional tests of other configurations by hand and the frequency of compilation, linkage and

            even run-time problems we conclude that the automated testing of all feasible configurations will

            be very beneficial.

        \subsection{Regression and Unit Tests}

            As already stated in the previous section, the continuous integration building system has not been finished

            yet. Therefore regression and unit tests are executed occasionally by hand, which is time consuming

            and prone to human omissions. An automated approach is definitively going to be very helpful.

        \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.

            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.

            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.

        \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

            (doubly-linked circular lists) and basic locking operations. Currently we are evaluating the initial experiences

            and we are trying to identify the most suitable methodology, but we expect quite promising results.

            As the VCC is based on the Microsoft C++ Compiler, which does not support many GCC extensions, we have been

            faced with the requirement to preprocess the source code to be syntactically accepted by VCC. This turned out

            to be feasible.

        \subsection{Model Checker}

            We are in the process of creating models of kernel wait queues (basic HelenOS kernel synchronization

            primitive) and futexes (basic user space thread synchronization primitive) using \emph{Promela} and

            verify several formal properties (deadlock freedom, fairness) in \emph{Spin}~\cite{spin}. As both the Promela language

            and the Spin model checker are mature and commonly used tools for such purposes, we expect no major problems

            with this approach. Because both synchronization primitives are relatively complex, utilizing a model checker

            should provide a much more trustworthy proof of the required properties than ``paper and pencil''.

        \subsection{Behavior Checker}

            We have created an architecture description in ADL language similar to SOFA ADL~\cite{adl} for the majority of the

            HelenOS components and created the Behavior Protocol specification of these components. The architecture

            is a snapshot of the dynamic architecture just after a successful bootstrap.

            Both the architecture and behavior description is readily available as part of the source code repository

            of HelenOS, including tools which can preprocess the Behavior Protocols according to the architecture description

            and create an output suitable for \emph{bp2promela} checker~\cite{bp}.

            As the resulting complexity of the description is larger than any of the previously published case studies

            on Behavior Protocols (compare to~\cite{cocome}), our current work-in-progress is to optimize and fine-tune the bp2promela

            checker to process the input.

            \medskip

            We have not started to generate code from the architecture description so far because of time constrains. However,

            we believe that this is a very promising way to go.

        \subsection{Behavior Description Generator}

            We have not tackled the issue of behavior description generation yet, although tools such as \emph{Procasor}~\cite{procasor} are readily

            available. We do not consider it our priority at this time.

    \section{Conclusion}

        \label{conclusion}

        In this paper we propose a complex combination of various formal verification methods and tools

        to achieve the verification of an entire general-purpose operating system. The proposed approach generally follows

        a bottom-to-top path, starting with low-level checks using state-of-the-art verifying C language compilers,

        following by static analyzers and static verifiers. In specific contexts regression and unit tests,

        code instrumentation and model checkers for the sake of verification of key algorithms

        are utilized.

        Thanks to the properties of state-of-the-art microkernel multiserver operating

        system design (e.g. software component encapsulation and composition), we demonstrate

        that it should be feasible to successfully verify larger and more complex operating systems than

        in the case of monolithic designs. We use formal component architecture and behavior

        description for the closure. The final goal -- a formally verified operating system -- is the

        emerging property of the combination of the various methods.

        \medskip

        The contribution of this paper is the shift of focus from attempts to use a single ``silver-bullet''

        method for formal verification of an operating system to a combination of multiple methods supported

        by a suitable architecture of the operating system.

        We also argue that the approach should be suitable for the mainstream

        general-purpose operating systems in the near future, because they are gradually

        incorporating more microkernel-based features and fine-grained software components.

        Although the evaluation of the proposed approach on HelenOS is still work-in-progress, the

        preliminary results and estimates are promising.

        \medskip

        \noindent\textbf{Acknowledgments.} The author would like to express his gratitude to all contributors of the HelenOS

        project. Without their vision and dedication the work on this paper would be almost impossible

        This work was partially supported by the Ministry of Education of the Czech Republic

        (grant MSM\-0021620838).

    \begin{thebibliography}{99}

        \bibitem{billion}Bessey A., Block K., Chelf B., Chou A., Fulton B., Hallem S., Henri-Gros C., Kamsky A., McPeak S., Engler D.: \emph{A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World}, Communications of the ACM, Vol. 53 No. 2, pp 66-75, 2010

        \bibitem{bp}Kofron J.: \emph{Checking Software Component Behavior Using Behavior Protocols and Spin}, in proceedings of Applied Computing 2007, Seoul, Korea, pp. 1513-1517, 2007

        \bibitem{gcc}GCC, the GNU Compiler Collection, \texttt{http://gcc.gnu.org/}

        \bibitem{clang}Clang: a C language family frontend for LLVM, \texttt{http://clang.llvm.org/}

        \bibitem{clanganalyzer}Clang Static Analyzer, \texttt{http://clang-analyzer.llvm.org/}

        \bibitem{cocome}Bulej L., Bures T., Coupaye T., Decky M., Jezek P., Parizek P., Plasil F., Poch T., Rivierre N., Sery O., Tuma P.: \emph{CoCoME in Fractal}, chapter in The Common Component Modeling Example: Comparing Software Component Models, Springer-Verlag, LNCS 5153, 2008

        \bibitem{coverity}Coverity, \texttt{http://scan.coverity.com/}

        \bibitem{procasor}Mencl V.: \emph{Deriving Behavior Specifications from Textual Use Cases}, in Proceedings of Workshop on Intelligent Technologies for Software Engineering (WITSE04, Sep 21, 2004, part of ASE 2004), Linz, Austria, pp. 331 - 341, Oesterreichische Computer Gesellschaft, 2004

        \bibitem{framac}Frama-C, \texttt{http://frama-c.cea.fr/}

        \bibitem{c}Lawlis P. K: \emph{Guidelines for Choosing a Computer Language: Support for the Visionary Organization}, Ada Information Clearinghouse, \texttt{http://archive.adaic.com/docs/reports/lawlis/k.htm}, 1998

        \bibitem{helenos}HelenOS Project, \texttt{http://www.helenos.org/}

        \bibitem{adl}Oplustil T.: \emph{Inheritance in Architecture Description Languages}, reviewed section of Proceedings of the Week of Doctoral Students 2003 conference (WDS 2003), Charles University, Prague, Czech Republic, 2003, pp. 124 - 131, 2003

        \bibitem{marketshare}Operating System Market Share, \texttt{http://marketshare.hitslink.com/report\-.aspx?qprid=8\&qptimeframe=M\&qpsp=132}, retrieved on 2010-02-28

        \bibitem{seL4}Klein G., Elphinstone K., Heiser G., Andronick J., Cock D., Derrin P., Elkaduwe D., Engelhardt K., Kolanski R., Norrish M., Sewell T., Tuch H., Winwood S.: \emph{seL4: Formal verification of an OS kernel}, Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, 2009

        \bibitem{spin}Spin, \texttt{http://spinroot.com/}

        \bibitem{stanse}Stanse: Static Analysis Framework for C code, \texttt{http://stanse.fi.muni.cz/}

        \bibitem{valgrind}Valgrind, \texttt{http://valgrind.org/}

        \bibitem{vcc}VCC, \texttt{http://vcc.codeplex.com/}

    \end{thebibliography}

\end{document}