- l4-hackers - example.com Site

Raspberry Pi 3B and L4Linux
by Dejan Cotra 27 Mar '19

27 Mar '19

Hi all, Im trying to run L4Linux on Raspberry Pi 3B. So far I was able to build Fiasco kernel and L4Re for Raspberry Pi 3B. I used aarch64-linux-gnu-gcc toolchain. Also I was able to create Uboot image for hello config, which I successfully run on both qemu and Raspberry Pi 3B. So now Im trying to build L4Linux. First question would be does L4Linux supparm64 architecture? If yes, any hints for configuration? If it does not support arm64 architecture does this also mean that I have to build Fiasco kernel and L4Re for 32bit arm architecture. Thanks in advance, Dejan

2 1

Invalidating mapped flexpages in pagers
by Paul Boddie 19 Mar '19

19 Mar '19

Hello, I have been trying to implement a pager in L4Re where the pager employs a memory region of limited size to satisfy map requests for a dataspace occupying a larger virtual memory region. Upon receiving a map request, the pager identifies the dimensions of the flexpage to be sent to the task experiencing the page fault, and it populates the flexpage's memory with the appropriate data. What this accomplishes so far is that when page faults occur in a task accessing the dataspace, mappings from virtual memory addresses are established in the task referring to the memory region populated by the pager. The task can read from page to page and keep getting new data. However, as each new map request comes in, I want to be able to invalidate the mappings previously made by the pager. Otherwise, I get many pages in the task's address space referring to the same memory, which is obviously not what I intend. Is it possible to send a flexpage from the pager in such a way that the mappings previously established by Fiasco.OC for the memory region are invalidated? Or have I missed some other mechanism for achieving what I am attempting? The L4Re documentation isn't helping me so much here, and I can't seem to find examples of this kind of thing in the source distribution. Thanks for any help anyone can give! Paul

2 5

Huawei R&D lab in Dresden
by Martin Decky 07 Mar '19

07 Mar '19

[Apology for this job ad. Please ignore if you are not interested in job offers.] Dear all, Huawei is starting a new R&D lab in Dresden. The lab shall focus on microkernel OS design and development, with a well-balanced mix between innovative research (including, but not limited to, topics such as HW/SW co-design, heterogeneous computing, data-centric computing, etc.) and prototype development (including, but not limited to, design and implementation of key operating system services for Huawei's microkernel OS, safety and security certification, formal verification, etc.). We offer prospective job candidates the possibility to impact billions of Huawei devices, collaborate on real-world scenarios for the microkernel multiserver OS design (in the automotive, IoT, telco, industrial and other domains) and even influence future HW design (HiSilicon, one of the major semiconductor companies, is a fully owned subsidiary of Huawei). We are also supporting mutually beneficial collaboration with academia (e.g. ETH Zurich, TU Dresden) and microkernel-related companies. If you are interested in discussing the details of the senior engineer, software architect and researcher roles we offer, please do not hesitate to contact me. We will be also more than happy to talk to you at the upcoming Fachgruppe Betriebssysteme Frühjahrstreffen 2019 in Erlangen next week [1] and at EuroSys 2019 in Dresden in about three weeks [2]. [1] https://www.betriebssysteme.org/aktivitaeten/treffen/2019-erlangen/ [2] https://www.eurosys2019.org/ Best regards Martin Decky Senior Research Engineer Huawei Technologies German Research Center

1 0

Setting up ssd and hard disk in l4linux
by Xinyue Wu 26 Feb '19

26 Feb '19

Dear Developers, I have been trying to mount ssd and hard disk in l4linux. There are some similiar questions in previous archives, and I have done the following things according to them: - configure 'devs' file and 'io' file, add sata to vbus - enable PCI support - enable vPCI driver - enable AHCI driver But when I ran l4linux in hardware, I still couldn't find sata in pci bus, nor could I found my devices under /dev. Does anyone have some suggestions? Or maybe there are something wrong in my device configuration, please let me know if so. Thanks a lot. x86-legacy.devs ================= local Res = Io.Res local Hw = Io.Hw Io.hw_add_devices(function() SATA = Hw.Device(function() Property.hid = "SATA"; Resource.iop1 = Res.io(0x1f0, 0x1f7); Resource.iop2 = Res.io(0x3f6, 0x3f7); Resource.irq = Res.irq(14); end); end) l4lx-x86.io ==================== local hw = Io.system_bus() Io.add_vbusses { l4linux = Io.Vi.System_bus { -- Add a new virtual PCI root bridge PCI0 = Io.Vi.PCI_bus { pci_sata = wrap(hw:match("SATA")); }; }; } l4lx.cfg ====================== local L4 = require("L4"); loader = L4.default_loader; vbus_l4linux = loader:new_channel(); vbus_input = loader:new_channel(); loader:start( { caps = { sigma0 = L4.cast(L4.Proto.Factory, L4.Env.sigma0):create(L4.Proto.Sigma0); icu = L4.Env.icu; l4linux = vbus_l4linux:svr(); }, log = {"IO", "y"}, l4re_dbg = L4.Dbg.Warn, }, "rom/io rom/x86-legacy.devs rom/l4lx-x86.io"); loader:start( { caps = { vbus = vbus_l4linux; }, log = L4.Env.log:m("rws"), }, "rom/vmlinuz mem=1024M console=ttyLv0 earlyprintk=1 l4x_rd=rom/ramdisk-256m.rd root=1:0 ramdisk_size=268435456");

2 1

some questions about l4bd.c in l4linux
by yadong.li 20 Feb '19

20 Feb '19

Hi Adam， I am studying how to support emmc storage in L4Re. I have read the file l4linux/drivers/block/l4bd.c. I have some questions 1、 In “l4linux/drivers/block/l4bd.c”, I can’t find the function implementation of “l4fdxc_request_write” and some with prefix l4fdxc in l4linx or l4， is there some demos? 2、 If it is implemented by ourselves, where is more reasonable to place “l4fdxc_request_write” , in l4 or l4linux ? 3、 If in l4, Which implementation is more reasonable , lib or server? Thank you very much

2 1

Communication between L4Linux tasks and L4re tasks
by Canberk Demirsoy 17 Feb '19

17 Feb '19

Dear Developers, I have a simple question regarding the communication of L4Linux and L4re. I have already read previous entries but could not solve my problem. I am able to establish a communication between the tasks in L4re, but what I need is communication between a task that is running on L4Linux and a task that is running on L4re. How can I do this in simplest way? Any suggestions? Best Regards *Canberk*

2 1

Poll for Separation Kernel (microkernel) CC Protection Profile
by Holger Blasum 20 Jan '19

20 Jan '19

Hello l4-hackers, microkernel-based systems can be used as separation kernels[*] for security. At the moment there is a poll on input for a Common Criteria for Information Technology Security (CC) separation kernel protection profile draft, organized by a certMILS.eu colleague from Rostock Univ, at https://evasys.uni-rostock.de/evasys/online.php?p=ccuf-sk-wg The idea is to have a base protection profile (PP) that all players can agree with and to specify additional functionality as add-ons to the PP (e.g., in the form of PP modules). The questionnaire is an opportunity to provide early feedback. Note that there are no mandatory questions, i.e. you can freely move around / you can leave any question unanswered - the only condition for your feedback be submitted to the collection system is that you go to the last page and use the submit button there. We invite feedback via that poll by end of this week. If, beyond the questionnaire, you want to join the Common Criteria User's Forum separation kernel working group, or anyone would like to have more time, just let me know by answering to this email. [*] https://en.wikipedia.org/wiki/Multiple_Independent_Levels_of_Security Best, -- Holger Blasum, SYSGO

1 1

QEMU advent calendar
by Matthias Lange 21 Dec '18

21 Dec '18

Hi, today we have another small treat for those interested in L4Re. You should check door 21 [1] of the QEMU advent calendar for a peek on what you can build with our newly released #L4Re projects. Happy holidays! Matthias. [1] https://www.qemu-advent-calendar.org/2018/#day-21 -- Matthias Lange, matthias.lange(a)kernkonzept.com, +49-351-41 888 614 Kernkonzept GmbH. Sitz: Dresden. Amtsgericht Dresden, HRB 31129. Geschäftsführer: Dr.-Ing. Michael Hohmuth

1 0

New L4Re projects released
by Matthias Lange 20 Dec '18

20 Dec '18

Dear L4 folks, as the year is slowly coming to an end we want to take the opportunity to announce the release of new L4Re projects to our github [1]. This release includes the development version of our small virtual machine monitor uvmm [2]. It is capable of running Linux on all three of L4Re's supported architectures. Another noteworthy project is io [3] which is our IO device multiplexing and virtualizing component. To get you started we added a new tutorial [4] on how to setup and run a Linux VM on L4Re. We hope you enjoy the new release and we love to hear what you think. Happy holidays! Matthias. [1] https://github.com/kernkonzept [2] https://github.com/kernkonzept/uvmm [3] https://github.com/kernkonzept/io [4] https://github.com/kernkonzept/manifest/wiki/LinuxVM -- Matthias Lange, matthias.lange(a)kernkonzept.com, +49-351-41 888 614 Kernkonzept GmbH. Sitz: Dresden. Amtsgericht Dresden, HRB 31129. Geschäftsführer: Dr.-Ing. Michael Hohmuth

1 0

UEFI L4 image?
by Peter Wiehe 26 Nov '18

26 Nov '18

Hello, can you give me a link to an UEFI flat PE image of L4Re? If that's not available, then perhaps a link to instructions how to produce one myself? Kind regards Peter

2 4