flat assembler
Message board for the users of flat assembler.

Index > OS Construction > original L3 L4 microkernel sources in ASM

Author
Thread Post new topic Reply to topic
Matrix



Joined: 04 Sep 2004
Posts: 1171
Location: Overflow
Matrix
Hello my friends,
I would like to take the chance of being first to post these valuable informations and source codes here so everybody can learn from:

original L3 & L4 microkernel sources in ASM
The L4 µ-Kernel Family Homepage
OS Dev L4 page

L4 microkernel for MIPS and Alpha


Description: tree hierarchy
Filesize: 31.89 KB
Viewed: 3840 Time(s)

tcb.png


Description: arbitrarily structured subsystem hierarchy
Filesize: 75.74 KB
Viewed: 3840 Time(s)

hierarchy.png




Last edited by Matrix on 31 Aug 2014, 08:10; edited 1 time in total
Post 31 Aug 2014, 04:57
View user's profile Send private message Visit poster's website Reply with quote
Matrix



Joined: 04 Sep 2004
Posts: 1171
Location: Overflow
Matrix
simple L4re system structure illustration


Description: Basic Structure of an L4Re based system
Filesize: 26.63 KB
Viewed: 3835 Time(s)

l4re-basic.png


Post 31 Aug 2014, 05:25
View user's profile Send private message Visit poster's website Reply with quote
l_inc



Joined: 23 Oct 2009
Posts: 881
l_inc
L3 and L4 sources might be of historical interest only. Learning from those should be discouraged. Actually even the historical interest should be completely covered by the Liedtke's papers including "Improving ipc by kernel design", "On µ-Kernel Construction", "Improved Address-Space Switching on Pentium Processors by Transparently Multiplexing User Address Spaces" and others.

_________________
Faith is a superposition of knowledge and fallacy
Post 31 Aug 2014, 14:04
View user's profile Send private message Reply with quote
Matrix



Joined: 04 Sep 2004
Posts: 1171
Location: Overflow
Matrix
l_inc wrote:
L3 and L4 sources might be of historical interest only. Learning from those should be discouraged. Actually even the historical interest should be completely covered by the Liedtke's papers including "Improving ipc by kernel design", "On µ-Kernel Construction", "Improved Address-Space Switching on Pentium Processors by Transparently Multiplexing User Address Spaces" and others.

Well, over 1.5 billion iphones use L4 kernels, and is used in aeroplane, train, and various industrial things.
Post 31 Aug 2014, 16:17
View user's profile Send private message Visit poster's website Reply with quote
l_inc



Joined: 23 Oct 2009
Posts: 881
l_inc
Matrix
First of all, iOS has nothing to do with L4. iOS is not even a microkernel OS.
Secondly, if L4 is used somewhere in industry, then it's an OS from the "L4 family", which is by far not the same as the historical L4 microkernel.

_________________
Faith is a superposition of knowledge and fallacy
Post 31 Aug 2014, 18:26
View user's profile Send private message Reply with quote
Matrix



Joined: 04 Sep 2004
Posts: 1171
Location: Overflow
Matrix
ofc megacorporations (and darpa) don't like competition, and we all know they want backdoors in every single computer.
Current consumer grade kernels, systems are limited and altered in every possible way.

i don't really like the idea of using c++ java or flash even haskell to create a microkernel
Kernel should be the smallest and most optimized code on the system that should not have any backdoors.
It is worth the effort of optimizing the microkernel code in ASM, that will affect te whole system's performance.

L4 Microkernel :: Design Overview
Introduction to Microkernel- Based Operating Systems
Exokernel: An Operating System Architecture for Application-Level Resource Management

note that microkenrels and exokernels are DARPA projects.
Post 31 Aug 2014, 22:15
View user's profile Send private message Visit poster's website Reply with quote
pelaillo
Missing in inaction


Joined: 19 Jun 2003
Posts: 878
Location: Colombia
pelaillo
l_inc wrote:
L3 and L4 sources might be of historical interest only.


Perhaps you mentioned it because the availability of seL4 as open source? https://github.com/seL4

Matrix, thank you very much for sharing. This is very interesting stuff.

BTW, they started implementing in HLL because of portability and ported the assembly code without changing the essence. We can continue where they left with the assembly and backport some of the improvements.

A lot of work, but the prize is high: a safe, unbreakable mathematically proven OS in 100% assembly.

Do you know which is the actual legal status of those asm sources? There is conflicting information on the website.
Post 01 Sep 2014, 19:22
View user's profile Send private message Yahoo Messenger Reply with quote
Matrix



Joined: 04 Sep 2004
Posts: 1171
Location: Overflow
Matrix
pelaillo wrote:

Matrix, thank you very much for sharing. This is very interesting stuff.


You are welcome

pelaillo wrote:

BTW, they started implementing in HLL because of portability and ported the assembly code without changing the essence. We can continue where they left with the assembly and backport some of the improvements.

A lot of work, but the prize is high: a safe, unbreakable mathematically proven OS in 100% assembly.


i do agree with you partially, one can usually get away with C, i do code in C too, and gcc does a good job in most cases, but if you use c++ or even higher level language to create your kernel, then your performance will suffer much, and can introduce unexpected errors.

pelaillo wrote:
Do you know which is the actual legal status of those asm sources? There is conflicting information on the website.

The L4 µ-Kernel was wrote by German computer scientist Jochen Liedtke at GMD, IBM Watson Research Center, and Universität Karlsruhe.

He died in 2001, so you can't ask for any license from him anymore, if you want to support his work maybe you can find his relatives and support them.
Post 01 Sep 2014, 20:01
View user's profile Send private message Visit poster's website Reply with quote
Matrix



Joined: 04 Sep 2004
Posts: 1171
Location: Overflow
Matrix
preventing-denial-of-service in L4 kernel
osdir micro-kernel.l4.devel (thread)

Found this thread here, accidentally:
L4/x86 micro kernel by bitRAKE
it was already posted here, but users didn't find it so interesting for some reason...

So,
Who are the players of the L4 game? Why you should be starting to develop an L4 kernel too?

DARPA (no, you won't get opensourced version of the L4 kernel used on drones)

Open Kernel Labs - private company acquired by General Dynamics C4 Systems - OKL4

Uni Karlsruhe - L4Ka::Hazelnut 1999, L4Ka::Pistachio 2001
UNSW - L4/MIPS
TU Dresden - Fiasco


NICTA - Australian Government
University of New South Wales (UNSW)
Australian Department of Communications
Australian Research Council - ICT Centre of Excellence Program.
New South Wales, Queensland and Victorian Governments
Australian National University
University of New South Wales
University of Melbourne
University of Queensland
University of Sydney
Griffith University
Queensland University of Technology
Monash University and other university partners.


Microsoft Research - High assurance: seL4, Barrelfish
Huawei - High assurance: seL4, Barrelfish
HP Labs - High assurance: seL4, Barrelfish

Sysgo AG - P4 (commercial)

L4/x86 - ASM - Jochen Liedtke (GMD, IBM Watson, Uni KA) - Development has been discontinued ! Newer versions currently not available publicly.

Fiasco, Hazelnut, L4/MIPS, L4/Alpha, L4/x86 Development has been discontinued!

B Labs - Codezero Codezero started a commercial clone of the OKL4 microkernel, done by B Labs and supporting ARMv7 processors. Originally open-source, source is now available to commercial licensees only.

A little history:

L4, like its predecessor L3 was created by German computer scientist Jochen Liedtke as a response to the poor performance of earlier microkernel-based operating systems. Liedtke felt that a system designed from the start for high performance, rather than other goals, could produce a microkernel of practical use. His original implementation in hand-coded Intel i386-specific assembly language code sparked off intense interest in the computer industry. Since its introduction, L4 has been developed(stolen,owned,defaced,bastardized) for platform independence and also in improving security, isolation, and robustness.
He died in 2001, no other details available.

There have been various re-implementations (stolen,owned,defaced,bastardized) of the original binary L4 kernel interface (ABI) and its successors, including L4Ka::Pistachio (Uni Karlsruhe), L4/MIPS (UNSW) and Fiasco (TU Dresden). For this reason, the name L4 has been generalized and no longer only refers to Liedtke's original implementation (after the his death he can't even argue with this anymore). It now applies to the whole microkernel family including the L4 kernel interface and its different versions.

L4 is widely deployed. One variant, OKL4 from Open Kernel Labs, shipped in billions of mobile devices.


NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program. NICTA is also funded and supported by the Australian Capital Territory, the New South Wales, Queensland and Victorian Governments, the Australian National University, the University of New South Wales, the University of Melbourne, the University of Queensland, the University of Sydney, Griffith University, Queensland University of Technology, Monash University and other university partners.

NICTA has created 11 new companies, collaborated on joint projects with a range of ICT industries, developed a substantial technology and intellectual property portfolio and continues to supply new talent to the ICT industry through a NICTA-supported PhD program.

In November 2005, NICTA announced that Qualcomm was deploying NICTA's L4 version on their Mobile Station Modem chipsets. This led to the use of L4 in mobile phone handsets on sale from late 2006. In August 2006, ERTOS leader and UNSW professor Gernot Heiser spun out a company called Open Kernel Labs (OK Labs) to support commercial L4 users and further develop L4 for commercial use under the brand name OKL4, in close collaboration with NICTA. OKL4 Version 2.1, released in April 2008, was the first generally available version of L4 which featured capability-based security. OKL4 3.0, released in October 2008, was the last open-source version of OKL4. More recent versions are closed source and based on a rewrite to support a native hypervisor variant called the OKL4 Microvisor. OK Labs also distributed a para-virtualized Linux called OK:Linux, a descendant of Wombat, as well paravirtualized versions of SymbianOS and Android. OK Labs also acquired the rights to seL4 from NICTA.

OKL4 shipments exceeded 1.5 billion in early 2012, mostly on Qualcomm wireless modem chips. Other deployments include automotive infotainment systems.

High assurance: seL4
(because security is their main concern...)
To ease meeting the sometimes conflicting requirements of performance and verification, the team used a middle-out software process starting from an executable specification written in Haskell. seL4 uses Capability-based access control to enable formal reasoning about object accessibility.
(haskell in kernel, great!)

seL4 takes a novel approach to kernel resource management, exporting the management of kernel resources to user level and subjects them to the same capability-based access control as user resources. This model, which was also adopted by Barrelfish

Barrelfish:
Barrelfish is an experimental computer operating system built by ETH Zurich with the assistance of Microsoft Research in Cambridge >> microsoft project
in close associacion with: Microsoft Research, Huawei, and HP Labs for their support.


Description:
Filesize: 66.36 KB
Viewed: 3745 Time(s)

L4_family_tree_small.png


Post 02 Sep 2014, 21:30
View user's profile Send private message Visit poster's website Reply with quote
Display posts from previous:
Post new topic Reply to topic

Jump to:  


< Last Thread | Next Thread >
Forum Rules:
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You cannot attach files in this forum
You can download files in this forum


Copyright © 1999-2020, Tomasz Grysztar. Also on GitHub, YouTube, Twitter.

Website powered by rwasa.