[cap-talk] Pict programming language and the kernel space

[Matej Kosik]

Friends,

Two years ago I have reported about the possibility to tame the
(somewhat extraterrestrial) programming language Pict.

The original version is downloadable here:
http://www.cis.upenn.edu/~bcpierce/papers/pict/Html/Pict.html

My tamed version is downloadable here:
http://altair.fiit.stuba.sk/mediawiki/index.php/Tamed_Pict

I did the taming with the vision of making a simple operating system
kernel with a similar motivations as MS Singularity. The result:
http://altair.fiit.stuba.sk/mediawiki/index.php/Backwater
was partially successful (it is possible to elegantly enforce POLA over
untrusted subsystems) modulo two problems:

Problem 1: Any subsystem was able to perform denial of service by
depleting the available free memory. No corruption happned but the
runtime halted the system. This is not acceptable.

Problem 2: Due to very simplistic scheduler (which is part of the
semantics of the language) any subsystem can arbitrarily degrade
responsiveness of the whole system by forking many processes which can
eat up CPU bandwidth.

These two problems are related to:
- defensive consistency
- defensive correctness
Obviously, what we want is the ability to build defensively correct
software system. This was not possible to do with Tamed Pict and I am
trying to fix this in a new version of the language.

At the moment it *does not* contain "usual" features:
- usual syntactic sugar
  - for functional programming
  - for sequential (procedural) programming
  - for object-oriented programming
- usual basic types (it only contains unit type and capability types)
- usual type constructors:
  - tuples
  - records
  - recursive types
- separate compilation

However, the preliminary new version
http://altair.fiit.stuba.sk/mediawiki/index.php/Kalahari
of the language is rich enough to simulate the whole set of old problems
plus it contains mechanisms that can be used avoid them.

Of course, without expanding it to the full height curent version is not
very useful.

The scheduler was part of the semantics of the old language. It is part
of the semantics also in the new version, although I changed it. It has
disadvantages. E.g. it is only approximate. Its advantage is that it
does not need external clock to enforce scheduling policy. This makes it
possible to refactor driver of the PIT (Programmable Interval Timer)
chip out of TCB which is a good thing. Even though initialization of the
PIT chip takes only 8 assembly instructions, the full explanation spans
several pages. That documentation now need not to be part of TCB
documentation.

I have made some effort to explain basic construct of the language on
the home page by examples. The homepage contains instructions how to
download and build kernels written in this language and boot them in QEMU.

I am now considering to gather some data concerning TCB size and
concrete diagrams of "reliance relationship" of other kernels although I
am not yet sure what will be the result and what kernels I will be able
to investigate. I am considering:
- W7 (Scheme based kernel)
- SPIN (Ada based kernel)
- Minix (they declare relevant goals)
- Singularity

My preliminary information is that TCB size of Singularity is roughly
around 100000 lines of code. If any experts are willing to help with
this, I would be grateful and we can post something to EUROSYS.
(I do not think that my results are that good but I believe
 it is worth trying to evaluate object-capability security paradigm
 in this context).
-- 
Matej Kosik