Many applications still follow a monolithic design pattern today. Often, their size and complexity precludes thorough verification and increases the likelihood of errors. The lack of isolation allows an errors in an uncritical part of a software to impact other security critical parts.

A well-known solution to this problem are systems comprised of components which only interact through well-defined communication channels. In such systems functionality is split into complex untrusted components and simple trusted components. While untrusted parts realize sophisticated application logic, trusted components are typically small, implement mandatory policies, and enforce security properties. An open question is how to implement such trusted components correctly.

Gneiss is a SPARK library providing a component-based systems abstraction for trusted components. Its main design goals are portability, performance and verifiability. Components built against the library can be compiled for the Genode OS Framework and Linux without modification. Only a minimal runtime such as our ada-runtime is required. To enable high-performance implementations, Gneiss imposes a fully asynchronous programming style where all work is done inside event handlers. All language constructs used in Gneiss can be analyzed by the SPARK proof tools to facilitate formally verified components.

The library is comprised of two parts: a platform independent interface and a platform implementation. The interface consists mostly of specifications that define the API and the SPARK contracts. The platform implementation is required to implement those specs with platform specific mechanisms. This can either be a native Ada platform or a binding to a different language.

Interfaces are implemented as regular or generic packages. Since components built with Gneiss use an asynchronous approach most interfaces trigger callbacks or events. To avoid access procedures that are forbidden in SPARK, event handlers and callbacks are provided as formal generic parameters to interface packages.

Instances of interfaces are called sessions. There are three session types: client, server and dispatcher. The client uses a server session of its own type. The specific implementation of the server is not visible for the client but determined by the platform. The dispatcher is like a special purpose client that does not connect to any server but the platform itself. It is responsible for registering a server implementation on the platform and thereby making it available for clients.

A component is a collection of SPARK packages that contain all its state and implementation. To interact with the system the state needs to hold a system capability and interface instance objects. To announce the component to the system it needs to instantiate a component package with an initialization procedure. This must only be done once per component. An empty component looks as follows:

with Gneiss;
with Gneiss.Component;

package Component is

   procedure Construct (Cap : Gneiss.Capability);
   procedure Destruct;

   package Main is new Gneiss.Component (Construct, Destruct);

end Component;

The procedure Construct is the first procedure of the component that is called (except for elaboration code) and receives a valid system capability. This capability is required to initialize clients or register servers. The procedure Destruct is called when the platform decides to stop the component and allows it to finalize component state. As a convention the components main package is always called Component and it must contain an instance of the generic package Gneiss.Component that is named Main.

The simplest interfaces are used like regular libraries. An example is the Log client that provides standard logging facilities. A hello world with the component described above looks as follows

with Gneiss.Log;
with Gneiss.Log.Client;

package body Component is

   package Log is new Gneiss.Log;
   package Log_Client is new Log.Client;

   Client : Gneiss.Log.Client_Session;

   procedure Construct (Cap : Gneiss.Capability)
   is
   begin
      Log_Client.Initialize (Client, Cap, "channel1");
      if Log.Initialized (Client) then
         Log_Client.Info (Client, "Hello World!");
         Log_Client.Warning (Client, "Hello World!");
         Log_Client.Error (Client, "Hello World!");
         Main.Vacate (Cap, Main.Success);
      else
         Main.Vacate (Cap, Main.Failure);
      end if;
   end Construct;

   procedure Destruct
   is
   begin
      Log_Client.Finalize (Client);
   end Destruct;

end Component;

In Construct the component initializes the log session. Since the initialization can fail it checks again if it succeeded. If this is the case it prints "Hello World!" as an info, warning and error message.

The component then calls Vacate to tell the platform that it has finished its work and can be terminated. Vacate does not immediately kill the component but tell the platform that it can safely be stopped now. The current method will still return normally. There is no guarantee that a subprogram that called Vacate is not called again.

When the platform decides to terminate the component at some point it will call Destruct. This procedure only checks if the Log session has been initialized and finalizes it if this is the case. In more complex scenarios the Destruct procedure can be used to safely shut down hardware devices or write data to disk.

POSIX:

[Hello_World] Info: Hello World!
[Hello_World] Warning: Hello World!
[Hello_World] Error: Hello World!

Genode:

[init -> test-hello_world -> Hello_World] Hello World!
[init -> test-hello_world -> Hello_World] Warning: Hello World!
[init -> test-hello_world -> Hello_World] Error: Hello World!

Since Gneiss is an asynchronous framework it often requires callbacks to be implemented. The Timer interface is a good example and easy to show. It only requires a single callback procedure that is called after a previously specified time. The package spec is the same as in the previous example.

with Gneiss.Log;
with Gneiss.Log.Client;
with Gneiss.Timer;
with Gneiss.Timer.Client;

package body Component is

   Gneiss_Log   : Gneiss.Log.Client_Session;
   Gneiss_Timer : Gneiss.Timer.Client_Session;
   Capability   : Gneiss.Capability;

   procedure Event;

   package Log_Client is new Gneiss_Log.Client;
   package Timer_Client is new Gneiss_Timer.Client (Event);

   procedure Construct (Cap : Gneiss.Capability)
   is
   begin
      Capability := Cap;
      Log_Client.Initialize (Log, Cap, "Timer");
      Timer_Client.Initialize (Timer, Cap);
      if
         Gneiss_Log.Initialized (Log)
         and then Gneiss.Timer.Initialized (Timer)
      then
         Log_Client.Info (Log, "Start!");
         Timer_Client.Set_Timeout (Timer, 60.0);
      else
         Main.Vacate (Cap, Main.Failure);
      end if;
   end Construct;

   procedure Event
   is
   begin
      if
         Gneiss_Log.Initialized (Log)
         and then Gneiss_Timer.Initialized (Timer)
      then
         Log_Client.Info ("60s passed!");
         Main.Vacate (Capability, Main.Success);
      else
         Main.Vacate (Capability, Main.Failure);
      end if;
   end Event;

   procedure Destruct
   is
   begin
      Componolit.Gneiss.Log.Client.Finalize (Log);
      Timer_Client.Finalize (Timer);
   end Destruct;

end Component;

The usage of the log session here is equivalent to the first example. Also the initialization of the timer session is similar. When Set_Timeout is called on the timer a timeout is set on the platform. The platform will then call the Event procedure when this timeout triggers. Since the Event procedure has no arguments and can be used in multiple contexts no preconditions can be set. This requires an initialization check of the timer session.

Some interfaces need more than a simple event callback and require additional interface specific procedures or functions as generic arguments. These more specialized callbacks can provide preconditions that provide certain guarantees about initialized arguments.

Furthermore the capability needs to be copied to be available in the Event for component termination. The capability is a special object that can be copied but not created from scratch. Only construct is called with a valid capability object which then must be kept somewhere to be used in other contexts.

The generic approach to implement a new platform is to create a new directory in platform and provide bodies for all specs in the src directory. Some of those specs have private parts that include Gneiss_Internal packages and rename their types. Those are platform-specific types and their declaration together with the according Gneiss_Internal package spec need to be provided. Platform specific types can be anything, as they're private to all components.

The log client for example consists of two (in this example simplified) specs:

private with Gneiss_Internal.Log;

generic
package Gneiss.Log is

   type Client_Session is limited private;

   function Initialized (C : Client_Session) return Boolean;

private

   type Client_Session is new Gneiss_Internal.Log.Client_Session;

end Gneiss.Log;

generic
package Gneiss.Log.Client is

   procedure Initialize (C     : in out Client_Session;
                         Cap   :        Capability;
                         Label :        String) with
      Pre => not Initialized (C);

   procedure Info (C : in out Client_Session;
                   M :        String) with
      Pre  => Initialized (C),
      Post => Initialized (C);

end Gneiss.Log.Client;

The client session is a limited private type that can neither be assigned nor copied. Its state functions, such as the initialization in this case are provided by the Log package while all modifying procedures are provided by Log.Client. In case of a generic package this allows the use of state functions as function contracts for formal generic parameters.

An exemplary POSIX implementation consists of three parts: the internal type package, a client body and a C implementation. Since the label should be printed as a prefix in front of each message it needs to be saved in the Client_Session type. As it can have any length it only is a record containing a pointer to the actual string object:

with System;

package Gneiss_Internal.Log is

   type Client_Session is limited record
      Label : System.Address := System.Null_Address;
   end record;

end Gneiss_Internal.Log;

As the session type is limited and has no initialization operation it requires a default initializer. The default value should be a state that marks the session as not initialized. Before the package body can be implemented a C implementation must be present. Since the session type is limited Ada will always pass it by reference, so pointers have to be used in the language binding. This roughly represents the subprograms defined in the package spec:

#include <string.h>
#include <stdlib.h>
#include <stdio.h>

typedef struct session
{
    char *label;
} session_t;

void initialize(session_t *session, char *label)
{
    session->label = malloc(strlen(label) + 1);
    if(session->label){
        memcpy(session->label, label, strlen(label) + 1);
    }
}

void info(session_t *session, char *msg)
{
    fputs("[", stderr);
    fputs(session->label, stderr);
    fputs("] ", stderr);
    fputs(msg, stderr);
    fputs("\n", stderr);
}

The struct session is equal to the Ada record. A pointer in C is what a System.Address is in Ada. Also by using in out as passing mode or having a limited type Ada will use pointers so session_t will always be passed as a pointer. Procedures in Ada have no return type so they all are void functions in C.

with System;

package body Gneiss.Log.Client is

   procedure Initialize (C     : in out Client_Session;
                         Cap   :        Capability;
                         Label :        String)
   is
      procedure C_Initialize (C_Client : in out Client_Session;
                              C_Label  :        System.Address) with
         Import,
         Convention => C,
         External_Name => "initialize";
      C_String : String := Label & Character'Val (0);
   begin
      C_Initialize (C, C_String'Address);
   end Initialize;

   procedure Info (C : in out Client_Session;
                   M :        String)
   is
      procedure C_Info (C_Client  : in out Client_Session;
                        C_Message :        System.Address) with
         Import,
         Convention => C,
         External_Name => "info";
      C_Msg : String := M & Character'Val (0);
   begin
      C_Info (C, C_Msg'Address);
   end Info;

end Gneiss.Log.Client;

In the package body the C functions are imported. The Client_Session can be in out as it is passed as a pointer and might be modified by C. The message string is more complicated. While C expects a pointer with a null terminated string, Ada uses an array of characters and passes meta data about the length of the string. To convert an Ada string to a C string it is put on the stack and a NULL character is appended as a terminator. Then the address of the first string element is passed to C.

The last part is the package body for Log which only needs to implement Initialized. Since this functions properties are likely required in the proof context it should not be implemented in C. Also since its contract is fixed it needs to be a expression function to get into the proof context:

with System;

package body Gneiss.Log is

   use type System.Address;

   function Initialized (C : Client_Session) return Boolean is
      (C.Label /= System.Null_Address);

end Gneiss.Log;

The initialization checks if Label is a valid address. This ensures that all procedures that have an Initialized precondition can safely use the label. It also makes sure that if malloc fails in C the session will not be initialized.

Gneiss aims to integrate into the existing build systems of the supported platforms. On Genode Gneiss components can be built with the native build system. On Linux we chose a custom approach that fits our use case.

The Cement build system allows designing and building Gneiss systems that run on Linux either in a GNU userspace or as init process. A system consists of a core component that is executed with a configuration. The configuration declares the components and their communication channels. A component is compiled into a shared object that is loaded by the core component and then forks into its own process.

The build configuration is done in XML. The example for a hello world system looks as follows:

<config>
    <component name="log_server" file="libcomponent_linux_log_server.so"/>
    <component name="hello_world" file="libcomponent_hello_world.so">
        <service name="Log" server="log_server"/>
    </component>
</config>

The hello_world component that is implemented by libcomponent_hello_world.so is allowed to communicate via a Log session to the log_server which then prints its outputs to the terminal. To compile this system cement can be called with

$ cd /path/to/gneiss
$ ./cement build -b build test/hello_world/hello_world.xml . test init lib

The arguments after the configuration file are the directory where the Gneiss repository is located and the directories that contain the project files for the components and libraries.

Core is built in build/bin and the components are built in build/lib. To run the system add the components that are shared libraries to the preload path and run core with the build configuration.

$ export LD_LIBRARY_PATH=build/lib
$ ./build/bin/core test/hello_world/hello_world.xml

The resulting output will be:

I: Loading config from test/hello_world/hello_world.xml
I: Started log_server with PID 19294
I: Started hello_world with PID 19295
[hello_world:log_hello_world] Info: Hello World!
[hello_world:log_hello_world] Warning: Hello World!
[hello_world:log_hello_world] Error: Hello World!
[hello_world:log_hello_world] Info: Destructing...
I: Component hello_world exited with status 0