Subversion Repositories HelenOS-doc

\institute{Department of Software Engineering\\

\institute{Department of Distributed and Dependable Systems\\

        \email{martin.decky@dsrg.mff.cuni.cz}}

        \email{martin.decky@d3s.mff.cuni.cz}}

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

        of almost any other software system. This paper points out several key design choices which

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

        should make the formal verification of an operating system easier and presents a work-in-progress

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

        and initial experiences with formal verification of HelenOS, a state-of-the-art microkernel-based

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

        operating system, which, however, was not designed specifically with formal verification in mind,

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

        as this is mostly prohibitive due to time and budget constrains.

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

        formalisms and techniques to successfully cover various aspects of the operating system.

        operating system is the emerging property of the combination.

        A reliable and dependable operating system is the emerging property of the combination,

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

        Operating systems (OSes for short) have a somewhat special position among all software.

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

        OSes are usually designed to run on bare hardware. This means that they do not require

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

        any special assumptions on the environment except the assumptions on the properties and

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

        behavior of hardware. In many cases it is perfectly valid to consider the hardware

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

        as \emph{idealized hardware} (zero mathematical probability of failure, perfect compiance

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

        with the specifications, etc.). This means that it is solely the OS that defines the

        and basic mathematical principles by this term.

        environment for other software.

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

        OSes represent the lowest software layer and provide services to essentially all other

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

        software. Considering the principle of recursion, the properties of an OS form the

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

        assumptions for the upper layers of software. Thus the dependability of end-user and

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

        enterprise software systems is always limited by the dependability of the OS.

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

        Finally, OSes are non-trivial software on their own. The way they are generally designed

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

        and programmed (spanning both the kernel and user mode, manipulating execution contexts

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

        and concurrency, handling critical hardware-related operations) represent significant

        the shortcomings of the physical world.

        and interesting challenges for software analysis.

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

        These are probably the most important reasons that led to several research initiatives

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

        in the recent years which target the creation of a formally verified OSes from scratch

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

        (e.g. \cite{seL4}). Methods of formal description and verification provide fundamentally

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

        better guarantees of desirable properties than non-exhaustive engineering methods such

        \end{itemize}

        as testing.

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

        However, 98~\%\footnote{98~\% of client computers connected to the Internet as of January

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

        2010~\cite{marketshare}.} of the market share of general-purpose OSes is taken

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

        by Windows, Mac~OS~X and Linux. These systems were clearly not designed with formal

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

        verification in mind from the very beginning. The situation on the embedded, real-time

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

        and special-purpose OSes market is probably different, but it is unlikely that the

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

        segmentation of the desktop and server OSes market is going to change very rapidly

        very rapidly in the near future.

        in the near future.

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

        The architecture of these major desktop and server OSes is monolithic, which makes

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

        any attempts to do formal verification on them extremely challenging due to the large

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

        state space. Fortunatelly we can observe that aspects of several novel approaches from

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

        the OS research from the late 1980s and early 1990s (microkernel design, user space

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

        file system and device drivers, etc.) are slowly emerging in these originally purely

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

        monolithic implementations.

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

        In this paper we show how specific design choices can markedly improve the feasibility

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

        of verification of an OS, even if the particular OS was not designed

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

        specifically with formal verification in mind. These design choices can be gradually

        principles.

        general-purpose OSes.

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

        \noindent\textbf{Structure of the Paper.} In Section \ref{design} we introduce

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

        the design choices and our case study in more detail. In Section \ref{analysis} we

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

        discuss our approach of the combination of methods and tools. In Section \ref{evaluation}

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

        we present a preliminary evaluation of our efforts and propose the imminent next steps

        we present the conclusion of the paper.

        to take. Finally, in Section \ref{conclusion} we present the conclusion of the paper.

    \section{Context}

    \section{Operating Systems Design}

        \label{context}

        \label{design}

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

        Two very common schemes of OS 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

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

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

        a preference to put numerous aspects of the core OS functionality into the kernel, while microkernel

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

        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

        The features which are missing from the kernel in the microkernel design are implemented

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

        in user space, usually by means of libraries, servers (e.g. processes/tasks) and/or software components.

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

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

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

            as Solaris kernel developers and many are freelance IT professionals).

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

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

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

            modified to run on various embedded boards) and does not implement real-time features.

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

            Many development projects such as task snapshoting and migration, support for MMU-less

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

            platforms and performance monitoring are currently underway.

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

            HelenOS can be briefly described as microkernel multiserver design. However, the actual design

            actually more elaborate:

            guiding principles of the HelenOS are more elaborate:

            \begin{itemize}

            \begin{description}

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

                \item[Microkernel principle] Every functionality of the OS that does not

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

                \item[Full-fledged principle] Features which need to be placed in kernel should

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

                      be implemented by full-fledged algorithms and data structures. In contrast

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

                      to several other microkernel OSes, where the authors have deliberately chosen

                \item \emph{(Multiserver principle)} Subsystems in user space should be decomposed with the smallest

                \item[Multiserver principle] Subsystems in user space should be decomposed with the smallest

                \item \emph{(Split of mechanism and policy)} The kernel should only provide low-level mechanisms,

                \item[Split of mechanism and policy] The kernel should only provide low-level mechanisms,

                \item \emph{(Encapsulation principle)} The communication between the tasks/components should be

                \item[Encapsulation principle] The communication between the tasks/components should be

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

                \item[Portability principle] The design and implementation should always maintain a high

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

                      libraries and tasks implementing device drivers should be clearly separated from the

                      or at least by internal compile-time APIs).

                      generic code (either by component decomposition or at least by internal compile-time APIs).

            \end{itemize}

            \end{description}

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

            In Section \ref{analysis} we argue that several of these design principles significantly improve

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

            the feasibility of formal verification of the entire system. On the other hand, other design principles

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

            induce new interesting challenges for formal description and verification.

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

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

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

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

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

            The design of the ubiquitous HelenOS IPC mechanism and the associated threading model present

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

            the possibility to significantly reduce the size of the state space which needs to be explored

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

            constrains in many formalisms. The IPC is inherently asynchronous with constant message buffers

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

            mandatory pairing of requests and replies, binding establishment and abolishment handshakes,

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

            memory sharing and fast message forwarding.

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

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

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

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

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

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

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

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

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

            messages and provide synchronization, special fibril-aware synchronization primitives

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

            in advance with formal verification in mind (some of the design principles might be beneficial,

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

            but others might be disadvantageous), but the design of HelenOS is also non-trivial and not obsolete.

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

            A large majority of OSes 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

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

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

            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.

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

            properties do not allow to make many general assumptions about the code.

            properties that do not allow to make many general assumptions about the code.

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

            The reasons for frequent use of C in the user space of many established OSes (and HelenOS) is

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

            probably much more questionable. In the case of HelenOS, except for the core libraries and tasks

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

            (such as device drivers), C might be easily replaced by any high-level and perhaps even

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

            non-imperative programming language. The reasons for using C in this context are mostly historical.

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

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

        Our approach will be mostly bottom-to-top, or, in other words, from the lower levels of abstraction

        Our approach will be mostly bottom-up, or, in other words, from the lower levels of abstraction

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

        are tackled. A structured overview of the formalisms, methods and tools can be seen on

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

        taxonomy. We have simply chosen the names to be intuitivelly descriptive.