POK

architectures

2008-08-02T23:07:09+02:00

At this time, we only support the x86 architecture. However, we plan to port our kernel on other architectures. Visit our project page for further information.

architecturevalidation

2009-05-04T14:51:40+02:00

POK configuration code can be automatically generated using AADL models. AADL models describe the overall architecture of a distributed system, including thread requirements, partitioning mechanisms and distribution specificities. Before generate configuration/deployment or application code, a validation step can be issued on architecture models.

basicusage

2008-10-28T19:27:12+02:00

Build your first partitioned system using POK You can experience POK with the examples provided in the examples directory. Download the POK distribution, uncompress it and go to sources. Issue make configure to configure your system and check that all required software is installed. Then, go to the examples/partitions-threads directory and issue make clean all install run. You should have a QEMU emulator that executes your partitioned system.

bugreport

2008-10-28T19:18:03+02:00

To report bugs, please send an email to the the following mailing-list: pok-devel well-known at sign listes.enst.fr. Please provide information as more as possible in your mail, especially he following things: * The compiler you use (version, build, ...) * The emulator you use to run POK. * Instructions that cause problems.

contact

2009-08-12T16:33:28+02:00

* For information about development of POK, you can send an email to the developer mailing-list. * For information about the use of POK, you can send an email to the POK community mailing-list. * For other request, please send a mail to delange at enst dot fr.

debug

2009-07-15T16:51:38+02:00

You can plug gdb with QEMU. For that, invoke QEMU like that : qemu -fda floppy.img -boot a -S -s -p 1234 Then, start gdb with gdb kernel-binary.elf and then, connect gdb to the VM with target remote :1234 Then, resume the VM.

demoarincmiddlewarequeueing

2009-08-19T17:27:49+02:00

In this demonstration, we automatically implement an ARINC653 system by an Model-Based development process. In particular we: * Model the system using the TOPCASED modeling framework. We define the architecture using the Architecture Analysis and Design Language * Validate the architecture using Ocarina/Real * Automatically generate the code from the AADL models using Ocarina * Compiles the generated code against POK * Simulate the system using an emulator like QEMU.

demoarincthreads

2009-08-19T17:22:41+02:00

design

2008-07-04T01:56:37+02:00

POK is a kernel designed to provide space and time isolation. It was designed to be small and highly tunable and fits with embedded/real-time requirements. The kernel provides the following services : * Space isolation. Partitions have a dedicated address space to store its code and data. Data sended/received in the distributed system are protected using a partitioned middleware. * Time isolation. Partitions have a time budget to execute their tasks (or threads). Each partition schedules i…

examples

2009-11-26T17:09:00+02:00

This page gives some examples and case studies we made during our experiments with POK. These examples are available in POK releases, in the examples directory. They illustrate the partitioning concept of POK and how we enforce safety and security during system execution.

faq

2009-10-22T19:36:25+02:00

POK is a partitioned operating system. It provides separation functionnalities to isolate different software components. With this separation, different software components can be collocated on the same machine ensuring safety and security enforcement:

features

2009-12-21T16:31:12+02:00

POK tries to be compliant with many standards of real-time embedded systems. At this time, we support the following standards: * ARINC653, an avionics standard for safety-critical systems. POK supports time and space partitioning to isolate different partitions. * MILS, an approach to build real-time embedded systems. Our MILS implementation relies on strong isolation of devices and partitioning services.

home

2009-12-21T16:32:58+02:00

POK is a real-time embedded operating system for safety-critical systems (avionics, aerospace and so on). It provides several functionalities and complies with many industrial standards, such as ARINC653 or POSIX. POK was designed to be used in safety-critical systems as well as in public systems.

installation

2009-09-16T17:58:57+02:00

Requirements * A version of GCC that can create ELF binaries * GNU binutils that manipulates ELF binaries * Perl with the modules XML::LibXML and XML::XPath::XMLParser * Mtools to manipulate MS-DOS style disks (optional) * QEMU * Make

integratedexample

2009-12-21T17:04:21+02:00

[Integrated avionics case-study] To demonstrate that we can use POK for real avionics architecture, we use an AADL model made by the Software Engineering Institute and converts it to make it working with Ocarina and POK. You can find the original model on this page.

introduceverifications

2008-10-24T21:33:40+02:00

You can automatically check some properties or requirements of your system using our POK tools. In fact, you can build your system using the AADL language. This language provides facilities to model the architecture of your system with its properties and its requirements. We can analyze your models and detect security breakage or safety issues.

introduction

2009-11-09T19:52:07+02:00

POK is a partitioned operating system focused on safety and security. It relies on a minimalist kernel for real-time embedded systems. The kernel has a microkernel architecture and complies with many industrial standards (like ARINC653). It provides time and space partitioning to run different applications that have different levels of safety or security.

legal

2009-08-12T15:08:45+02:00

POK was designed by a large team and was based on teaching activities. The project is managed by Julien Delange and involves many people from different school and companies. You can have the list of all the people involved in the project in the documentation.

libpok

2008-08-02T22:50:48+02:00

Libpok is a runtime dedicated for each partition. It has a set of functionnalities to use kernel legacy services (thread creation, extra-partition communications and so on). For each partition, we can tune and modify the services of the libpok. It reduces the memory overhead for each partition.

links

2009-07-17T11:47:04+02:00

Embedded kernel * RTEMS * eCos * L4 community and the implementation of L4 : Fiasco and Pistachio. Many papers on security/safety-related microkernel could be retrieved on these websites. * , a hypervisor for embedded and real-time systems

lists

2008-08-02T22:54:58+02:00

We have two mailing-list to get feedback from our users and communicate between developers. These lists are kindly hosted by the ENST. General For any question about pok, please send an email on the list pok-general. The address of the list is the following : pok -famous at sign- listes dot enst dot fr

milsexample

2009-12-21T16:49:53+02:00

[MILS case study architecture] This case study defines a distributed architecture with two nodes: * One node executes three partition, each of them has a different security level * One node executes two partitions, one has topsecret and secret security level and the other has the unclassified security level.

modelsrules

2008-10-24T21:39:50+02:00

To be defined Security and safety layer To be defined

modules

2008-11-20T04:04:38+02:00

You can also visit our next improvements on pok on this page. Status of POK kernel * Space isolation : done * Time isolation : done * Scheduling policies inside partition : 10% * Exception handler : 20% * Extra-partition communication : 70%

news

2010-03-18T17:09:40+02:00

* 03/18/2010: We are currently improving the code coverage of pok and libpok. Generated examples would be covered up to 80%. Thanks to the couverture project and the xcov tool. * 12/20/2009: The ARINC653 layer is now available for Ada, thanks to Laurent Lec ! * 12/19/2009: A port on LEON3 is currently in progress and would be working soon. Thanks to Fabien Chouteau ! * 12/10/2009: POK snapshots are back ! You can download them on . Last POK snapshot is avai…

oldhome

2009-05-01T15:31:16+02:00

POK is a partitioned AADL runtime compliant with partitioned standards and initiatives such as ARINC653 or MILS. It provides strong isolation services to separate partition in term in space and time. It has a fine-grained configuration and each resource or functionnality can be tuned. Moreover, it could be used and configured by hand or code generation from AADL models. This website give details about the project and its use.

people

2008-11-20T04:00:28+02:00

Main developers * Julien Delange (design, libpok, most of core services of the kernel, POK tools) Contributors * Julian Pidancet (space isolation) * Pierre-Olivier Haye (space isolation) * Camille Meulien (space isolation) * François Goudal (initial base of code)

pokconfiguration

2008-08-02T22:51:52+02:00

The whole project is divided into two pieces of software : kernel and libpok. The kernel is the legacy kernel that handles partition and ensures space and time isolation. On the other hand, libpok is the runtime used by each partition. The configuration of the kernel and libpok can be achieved with two methods :

pokdocumentation

2010-03-26T22:34:43+02:00

There are a set of slides about different topics around POK : system specification, code generation and so on. Does not hesitate to contact us for more information about these documents. * [Introduction to the POK project] * [The ways to specify system requirements (either by AADL or XML files] * [Code Generation patterns used by Ocarina to generate code that targets POK Operating System] * [Validation and Certification tools for POK] * [Overview of the POK Operating System]

pokdownload

2009-09-26T14:35:22+02:00

Before using POK, you MUST read the licence of POK. If you disagree with the licence, you MUST NOT use POK. By downloading and using POK, you are engaged to respect the licence. Public snapshots can be found on http://pok.gunnm.org/snapshots. There is no official release at this time.

pokkernel

2008-08-02T22:47:27+02:00

The kernel is responsible to enforce isolation among partitions. It handles clock interrupts, partitions, threads and communications for extra-partition communications. The kernel is small (about 1000 lines of code for the core services, arch-dependent code not included) so we could envisage to perform verification on fundamental services.

poklicence

2008-11-26T01:54:52+02:00

About the licence The licence chosen is a BSD-style licence. You can grab a template for this licence here. Licence Copyright (c) 2008, POK Team All rights reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

pokprojects

2008-08-02T23:16:54+02:00

Implement thread service in partition At this time, threads are declared to the kernel. However, it is not good for isolation and we think its better to implement them in libpok. However, it introduces many changes : threads scheduling will be performed by the libpok as well as context-switch. However, the kernel will be lighter and more easily verifiable.

poktoolchain

2008-11-17T21:08:38+02:00

POK requires some programs, such as GCC, QEMU or Perl. At this time, it works on UNIX-compliant systems such as Linux, FreeBSD or Mac OS X. Windows is not supported at this time. Required software To use POK, you must have the following software :

poktools

2008-10-28T19:14:27+02:00

The POK tools manipulate AADL models to check security or safety issues and generate/build code according to these models. POK checker The POK checker tool checks AADL models. It looks for security or safety issues in your model. It can be found in $INSTALL_PREFIX/bin/pok-checker.

relatedwork

2008-07-04T01:52:18+02:00

Commercial projects * LynxOS : OS that conforms to the ARINC653 specification * VxWorks : OS that conforms to the ARINC653 specification * PikeOS : OS that deals with the MILS security model OpenSource projects * Ocarina AADL toolsuite * RTEMS : an open source operating system, minimal. The main drawback is that it does not provide any mecanism for space and time isolation. * Topcased * Osate

sourceorga

2008-10-24T21:41:49+02:00

Directory hierarchy * kernel/ : contains the kernel. It provides scheduling and middleware services. It has an Hardware Abstraction Layer to facilitate further port. To ease the development inside the kernel, a little C-library was designed. * libpok/ : runtime system used by each partition. Contain the POSIX and ARINC653-compliant API. * misc/ : misc files, contain makefiles, scripts and so on * tools/ : POK tools * examples/ : tests for PolyORB Kernel. * netdrivers/ : device drive…

support

2009-08-12T16:22:50+02:00

A documentation (a PDF file) is available in each POK snapshot, in the doc/ directory. This file contains all instructions to install required tools to build POK and how to compile it. It also provides instructions to build embedded real-time systems from AADL models.

testingleon3

2010-01-13T16:07:12+02:00

First, download the tsim simulator on the gaisler website. Then, when you configure POK, it should detect if tsim is in your PATH variable. If everything is fine, the make run command target in generated example would invoke tsim with the appropriate arguments.

wiki

2009-12-21T18:25:15+02:00

This is the wiki space of POK. This wiki contains unofficial informations about POK. Public access is allowed and users can add their own relevant information to help the POK community. * Build the toolchain for PPC/Prep * Build the toolchain for SPARC/LEON3 * Testing the LEON3 port * French installation guide

wikiarinc653

2009-05-04T17:04:32+02:00

The part 3 of the ARINC653 standard describes a testsuite to check the compliance of an operating system. We try to make POK compatible with the ARINC653 standard and shows the correctness of the implementation. At this time, the following tests were validated :

wikibuildleontoolchain

2009-12-22T10:50:28+02:00

This has been done on Linux. At this time, the SPARC toolchain does not work on Windows. The target is sparc-elf. So, you have to build binutils and gcc for this target. First, build and install binutils. Then, compile gcc. It has been tested with the following versions :

wikibuildppctoolchain

2009-05-12T18:51:20+02:00

This has been done on Linux and Mac OS X. At this time, the PowerPC toolchain does not work on Windows. The target is powerpc-elf. So, you have to build binutils and gcc for this target. First, build and install binutils. Then, compile gcc. It has been tested with the following versions :

wikicodecoverage

2009-05-13T14:47:12+02:00

Check the code coverage is an important issue. The goal of code coverage consist in verifying that every statement of the code is taken and every condition was tested. By doing that, we ensure that: * No dead code is included in the application * Every statement/decision was tested

wikiformalverification

2009-05-04T11:47:58+02:00

FIXME

wikiinstallationfrench

2009-07-21T17:33:24+02:00

Note : Ce guide d'installation a été réalisé par Wassim Wehbi lors de la réalisation d'un projet concernant POK. Nous le remercions pour ces instructions détaillées. Avant de démarrer avec nos propos, il est judicieux de partager la démarche de mise en place de l’environnement de travail nécessaire pour le bon fonctionnement du noyau. Des compilateurs pour les architectures x86 et powerpc sont nécessaire, et, munis du simulateur QEMU pour x86 nous pourrions mettre au point notre implémentation.…