flat assembler
Message board for the users of flat assembler.
Index
> OS Construction > original L3 L4 microkernel sources in ASM |
Author |
|
Matrix 31 Aug 2014, 04:57
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
Last edited by Matrix on 31 Aug 2014, 08:10; edited 1 time in total |
|||||||||||||||||||
31 Aug 2014, 04:57 |
|
Matrix 31 Aug 2014, 05:25
simple L4re system structure illustration
|
||||||||||
31 Aug 2014, 05:25 |
|
Matrix 31 Aug 2014, 16:17
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. |
|||
31 Aug 2014, 16:17 |
|
l_inc 31 Aug 2014, 18:26
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 |
|||
31 Aug 2014, 18:26 |
|
Matrix 31 Aug 2014, 22:15
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. |
|||
31 Aug 2014, 22:15 |
|
pelaillo 01 Sep 2014, 19:22
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. |
|||
01 Sep 2014, 19:22 |
|
Matrix 01 Sep 2014, 20:01
pelaillo wrote:
You are welcome pelaillo wrote:
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. |
|||
01 Sep 2014, 20:01 |
|
Matrix 02 Sep 2014, 21:30
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.
|
||||||||||
02 Sep 2014, 21:30 |
|
< Last Thread | Next Thread > |
Forum Rules:
|
Copyright © 1999-2024, Tomasz Grysztar. Also on GitHub, YouTube.
Website powered by rwasa.